graph

The graph statement describes a graph in Cyclone.

Syntax

The syntax of a graph in Cyclone is as follows:

 graph name { [<var_declaration>]* [<nodes>]*

 [<edges>]* [<invariant>]* [<goal>]? }

In general, a graph described by Cyclone specification language contains four sections: a set of nodes, a set of edges, a set of invariants, and a goal to be achieved.

Scope

Variables declared in this section are considered as graph-scope (global) variables that are visible to other sections.

 graph {

 int i = 0;//global variable

  normal start node  S0 {

       i++;//refer to global variable i

Semantics

The graph section contains everything Cyclone needs in order to discover a path p that provably meets defined path conditions.

< Back