1.6 Summary

In this Section, we summaries the fundamental features of Cyclone specification language.

Specification Structure

Overall, a Cyclone specification contains three sections (current version): node section, edge section and goal section. The goal section is optional. If there is no goal section defined, Cyclone will not compile the specification. But it is still a valid specification.

There are four modifiers can be used for specifying a node.

• abstract: a node with abstract modifier cannot contain other information such as variables or expressions.
• start: a node with start modifier specifies an entry point for Cyclone to discover a path defined in a goal section. Only one start node can be specified.
• normal: a node can contain information such as variables and expressions.
• final: a node marked final modifier is a node to be reached by a path to be discovered. Multiple final nodes can be defined. The set of final nodes will be unioned with the nodes specified in a reach statement.

It is illegal to use abstract and normal together. It is legal to use start and final together. By default, a node is abstract.

The keyword edge is for creating an edge in a graph. An edge can be labelled with a string via using label keyword. A where clause can be used on an edge to specify a guard on a transition (not available in the current version).

Goal Section

A goal has the following syntax:

(check | enumerate)  for  Integer+ 
    (condition (PathCondition1,PathCondition2,...,PathConditionn))?
    (reach (Node1,Node2,...,Noden))?

Both condition and reach statements are optional for a goal. If there is no reach statement specified, Cyclone will discover a path that reaches one of the nodes with final modifier. If there is a reach statement and some final nodes defined in node section, then Cyclone will discover a path that reaches one of the union of two sets of nodes.

All path conditions specified in a condition statement are logically conjoined. One can use a single compound path condition to form logical disjunction as follows:

Path Operators

Wisely use path operators can help Cyclone to find path(s) you want. However, there are some common pitfalls of using some of the path operators.

Operator ! cannot be applied to a node in a path, but can be applied to an entire path. Thus, the following code is illegal.

If you would like to exclude S1->S2, then use

If you just want to say exclude S1 along in this path, then use

Operator ^{i..j} can be applied to both a node or an entire path, but not a node in a path. For example, the following is illegal

If you wish to say node S2 must appear three times before node S3 in this path, then you can just use

However, if you wish to say node S2 must appear three times and include this path as well, then you use

If you want to find a path that has a length ranging from i to j, you can construct a compound path condition by using logical disjunction. For example, all path(s) with length from 3 to 5 begins and ends with S1, you could construct the following compound path condition: