Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: labgraphs.vdmsl Sprache: VDM

Original von: VDM^©

types

LabGraph = map NodeId to (map ArcId to NodeId)
inv g ==
  UniqueArcIds(g) and
  forall m in set rng g & rng m subset dom g;

AcyclicLabGraph = LabGraph
inv acg ==
  not exists id in set dom acg &
     id in set AllLabDesc(acg,id);

NodeId = nat;

ArcId = nat

functions

AllLabDesc: LabGraph * NodeId -> set of NodeId
AllLabDesc(g,id) ==
  dunion {LabDescendents(g,c,{})| c in set rng g(id)}
pre id in set dom g;

measureLabGraphReached : LabGraph * Id * set of Id -> nat
measureLabGraphReached(g,-,reached) ==
  card dom g - card reached;

LabDescendents: LabGraph * NodeId * set of NodeId -> set of NodeId
LabDescendents(g,id,reached) ==
  if id in set reached
  then {}
  else {id} union
       dunion {LabDescendents(g,c,reached union {id})
              | c in set rng g(id)}
pre id in set dom g
measure measureLabGraphReached;

UniqueArcIds: map NodeId to (map ArcId to NodeId) -> bool
UniqueArcIds(g) ==
  let m = {nid |-> dom g(nid) | nid in set dom g}
  in
    forall nid1, nid2 in set dom m &
       nid1 <> nid2 => m(nid1) inter m(nid2) = {}

values

  lgraph : LabGraph = {1 |-> {1 |-> 2,2 |-> 3},
                       2 |-> {3 |-> 4},
                       3 |-> {4 |-> 5},
                       4 |-> {5 |-> 6},
                       5 |-> {6 |-> 6},
                       6 |-> {|->}}

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.