Quellcode-Bibliothek circuits.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
%
%********************************************************************************%

% A circuit is a walk where the end points are the same

circuits[T: TYPE]: THEORY

BEGIN


   IMPORTING walks[T],
             structures@seq_extras[T]


           G: VAR digraph[T]
   w, w1, w2: VAR prewalk[T]


% --------------------------------------------------------------------------------
%     Definitions
% --------------------------------------------------------------------------------

 pre_circuit?(G: digraph[T], w: prewalk): bool = 
   walk?(G,w) AND w(0) = w(length(w)-1)

 circuit?(G: digraph[T], w: prewalk): bool = 
   pre_circuit?(G,w) AND length(w) > 1
   
 loop?(G: digraph[T], w: prewalk): bool =
   pre_circuit?(G, w) AND length(w) = 2

 eq_circuit?(G, w, w1): bool =
   circuit?(G, w) AND circuit?(G, w1) AND eq_prewalk?(rest(w), rest(w1))


% --------------------------------------------------------------------------------
%     Properties
% --------------------------------------------------------------------------------

 eq_circuit_length: LEMMA
   eq_circuit?(G, w1, w2) IMPLIES length(w1) = length(w2)

 eq_circuit_reflexive: LEMMA
   circuit?(G, w) IMPLIES eq_circuit?(G, w, w)

 eq_circuit_symmetric: LEMMA
   eq_circuit?(G, w1, w2) IMPLIES eq_circuit?(G, w2, w1)

 loop_is_circuit: LEMMA
   loop?(G, w) IMPLIES circuit?(G, w)

 equal_rest_equal_circuit: LEMMA
   circuit?(G, w1) AND circuit?(G, w2) AND rest(w1) = rest(w2)
   IMPLIES w1 = w2

 equal_eq_circuit: LEMMA
   eq_circuit?(G, w1, w2) AND rest(w1) = rest(w2)
   IMPLIES w1 = w2

 circuit_equal_fisrt: LEMMA
   circuit?(G, w1) AND circuit?(G, w2) AND circuit?(G, w1 o rest(w2))
   IMPLIES w1`seq(0) = w2`seq(0)

 comp_circuit_inter: LEMMA
   circuit?(G, w1 o rest(w2)) AND length(w2) > 1
   IMPLIES nonempty?(intersection(verts_of(w1), verts_of(w2)))

 eq_circuit_position: LEMMA
   eq_circuit?(G, w1, w2) IMPLIES
   EXISTS (i: below[length(w1)]): w2 = w1 ^ (i, length(w1) - 2) o w1 ^ (0, i)

 eq_circuit_edges: LEMMA
   eq_circuit?(G, w1, w2) IMPLIES edges_of(w1) = edges_of(w2)

 commuted_circuit: LEMMA
   FORALL (i : below[w`length]): circuit?(G, w)
   IMPLIES circuit?(G, w ^ (i, w`length-1) o w ^ (1,i))

 commuted_circuit_is_eq: LEMMA
   FORALL (i : below[w`length]): circuit?(G, w)
   IMPLIES eq_circuit?(G, w, w ^ (i, w`length-1) o w ^ (1,i))
 

 END circuits