reach

The reach statement specifies one or more nodes (states) for a path (p to be discovered) to reach.

Syntax

The syntax of a reach statement is as follows:

 reach (node₁,node₂,...,node_n)

Each node here must be a valid node that is defined in the node section.

Here is an example:

 reach (S0,S1,S2)

Scope

The reach statement cannot be used alone. Typically, the reach statement is used as a part of a check or enumeration statement.

The reach statement must appear after the condition statement.

   check for 6 condition (

       (>>2(S1->S2) && (S3->_->S4)) ||

       (!(S5->S6) && !(S2->S4)) )

   reach (S0)

The reach statement can also be optional for check or enumeration statement.

Semantics

The reach statement specifies the path to be discovered by Cyclone must reach one of the nodes included in the statement (if no other final nodes are defined). Hence, the list of nodes included within the reach statement are formed as a logic disjunction.

If there are some final nodes defined in the node section, and the reach statement also specifies some nodes, then two sets of nodes are unioned.

 start final node  S0 { ... }

 abstract node  S11 { ... }

 final node  S12 { ... }

 goal  {

      check for 8 reach (S0,S10,S3)

/* find a path that has a length of 8

* and reaches one of these nodes: S0,S3,S10,S12.

If the reach statement is not included in the check or enumeration statement, the compiler then will look for nodes that are defined with final and attempt to find a path that reach one of these final nodes.

 start final node  S0 { ... }

 abstract node  S11 { ... }

 final node  S12 { ... }

 goal  {

check for 8

/* find a path that has a length of 8

* and reaches one of these nodes: S0,S12.

If the reach statement is not used in the check or enumeration statement, and no final nodes are defined, the compiler will then report a semantic error.

< Back