Quellcode-Bibliothek circuits.pvs Sprache: 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

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.