| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle digraph_conn_defs.pvs Sprache: PVS |
|||||||||
|
%*******************************************************************************
% % Contributions from: % % Andréia Borges Avelar -- Universidade de Brasília - Brasil % Mauricio Ayala-Rincon -- Universidade de Brasília - Brasil % Cesar Muñoz -- NASA Langley Research Center - US % %******************************************************************************* digraph_conn_defs[T: TYPE]: THEORY BEGIN IMPORTING digraph_deg[T], walks[T], max_di_subgraphs[T] G,G1,G2: VAR digraph[T] %%% Defines a strongly connected digraph connected?(G) : bool = FORALL (u, v : (vert(G))) : reachable?(G)(u, v) %%% Defines a strongly connected component (scc) of a digraph connected_component?(G)(G1) : bool = connected?(G1) AND di_subgraph?(G1, G) conn_comp_with_edges?(G)(G1) : bool = connected_component?(G)(G1) AND FORALL(u, v: (vert(G1)) ): edge?(G)(u,v) IMPLIES edge?(G1)(u,v) %%% Defines a maximal strongly connected component of a digraph max_strongly_conn_comp?(G)(G1: di_subgraph(G)) : bool = conn_comp_with_edges?(G)(G1) AND FORALL (G2: di_subgraph(G)): strict_subset?(vert(G1), vert(G2)) IMPLIES NOT connected_component?(G)(G2) %%% Defines a maximal strongly connected component containing a vertex v vertex_conn_comp?(G)(G1: di_subgraph(G), v: (vert(G))) : bool = max_strongly_conn_comp?(G)(G1) AND vert(G1)(v) % max_connected_component?(G)(G1: di_subgraph(G)) : bool = % maximal?(G, G1, connected_component?(G)) END digraph_conn_defs ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28