node

The node statement allows you to declare a node.

Syntax

The syntax of a node statement is as follows:

 [<modifier>]* node name { <expression> }

A node can be declared using different modifiers. The <modifier> here can be a combination of: abstract, normal, start and final. With one exception, abstract and normal cannot be used together. If no modifier is used, then by default Cyclone treats a node as an abstract node.

Scope

Once a node is declared, it is visible to both edge and goal section.

 abstract start final node  S0 { }

 abstract final node  S1 { }

  edge t1 {S0->S1}

  edge t2 {S0->S0}

 goal  {

       let cond = !S2; //error: no node S2 is defined.

When a node's name has the same as a path variable's name created by using the let expression, the latter is preferred by the compiler.

Semantics

A valid Cyclone specification can have multiple final nodes but exactly one start node. Cyclone discovers a path that begins from a start node and ends with one of final nodes (including these nodes specified in a reach statement).

Currently, Cyclone does not provide a syntactic way of creating multiple start nodes. But one can create one additional node (mark it as a starting node) and edges that link multiple nodes to be considered as starting nodes for a path.

< Back