Quelle  circuits.pvs

circuits[T: TYPE]: THEORY
%
%  A circuit is a pre_circuit with no small loops (i.e. reduced)
%
%     pre_circuit?(G: graph[T], w: prewalk): bool = walk?(G,w) AND 
%                                                   w(0) = w(length(w)-1)
%
%  NOTE: The extra term "w(1) /= w(length(w)-2)" in the definition of
%        cyclically_reduced? handles the special case where
%        w(0) is a small loop
%
%        removed "walk?(G,w)" from circuit? defn because it is in pre_circuit
%
BEGIN

   IMPORTING walks[T]

   G: VAR graph[T]


   reducible?(G: graph[T], w: Seq(G)): bool  = 
          (EXISTS (k: posnat): k < length(w) - 1 AND w(k-1) = w(k+1))

   reduced?(G: graph[T], w: Seq(G)): bool = NOT reducible?(G,w)

%
%   cyclically_reduced?(G: graph[T], w: Long_walk(G)): bool = 
%         reduced?(G,w) AND
%         (FORALL (j: below(length(w)-1)): reduced?(G,w^(j+1, length(w)-1) o w^(1,j))) 


   cyclically_reduced?(G: graph[T], w: Seq(G)): bool = length(w) > 2 AND
         reduced?(G,w) AND w(1) /= w(length(w)-2)

   circuit?(G:  graph[T], w: Seq(G)): bool = %% walk?(G,w) AND
                                             cyclically_reduced?(G,w) AND
                                             pre_circuit?(G,w) 

END circuits