let

In Cyclone specification language, the condition statement allows you to specify multiple path conditions over a path p to be discovered. Sometime one would like to create a list of path conditions before using them in the condition statement so that they can be reused, extended or factored. The let expression allows you to declare a path variable that points to path condition(s).

Syntax

The syntax of a let expression is as follows:

 let name [ = <PathCondition> ] ;

Here is an example:

 let cond = (S1->S2) || (S1->S5);

(S1->S2) || (S1->S5) is stored in the path variable cond. Thus, one now can use this variable cond in a condition statement.

 check for  7 condition (!cond) reach (S0)

Scope

A let expression can only be used in the goal section. Path variables declared by using let expressions are only visible in the goal section. In the case of a path variable declared by a let expression has the same name as other names such as a node's name, the path variable is preferred by the compiler. For example,

 node  S0 {...}

...

 goal  {

       let S0 = <<(S1->S2->S3);

       check for  7 condition (S0) reach (S0,S3)

Node S0 declared in the node section is no longer visible in the condition statement. Thus, S0 in the condition statement is a path variable that specifies a path condition. That is S1->S2->S3 must appear at the end of a path p (to be discovered by Cyclone). However, S0 in the reach statement still is a node. Thus, it is recommended to use different variable names to distinguish a path variable from others.

Semantics

Path variables declared by the let expressions are evaluated during the parsing. This is different from variables created as graph or state/node scope based, they are evaluated after parsing for semantic and type checking. For example,

 let cond1;

 let cond2;

 cond2=cond1;//Syntax Error:cond2 is not assigned to a path condition.

 let cond3=cond3;

/*Semantic Error: no node cond3 is found */

 check for 5 condition (cond3) reach (S0)

A path variable declared by a let expression essentially is a reference that points to a path condition. Thus, the standard logical operators can be applied to them. However, prefix and postfix operators are prohibited.

 let cond1 = !(S2->S3) && (S1->_->_->S1);//legal expression

 let cond2 = cond1^{2:5};//illegal expression

Cyclone treats cond2 as an illegal expression. The compiler reports an syntax error, though it throws an semantic exception (since let expressions are processed by the parser).

An Example

Here is an example of using let expressions for the following graph:

 goal  {

       let branch1 = S1->S3->S5;//1st branch

       let branch2 = S2->S3->S5;//2nd branch

       let branch3 = S2->S4->S5;//3rd branch

       let branch4 = S5->S1;//4th branch

       let task1 = branch1 && branch3;//cover 1st and 3rd branch

       let task2 = branch2 && branch1;//cover 1st and 2nd branch

       let task3 = branch3 || branch4;//cover 3rd or 4th branch

/*find all possible paths with a length of 8 for each task.*/

       enumerate for 8 condition ( (task1 ^ task2 ^ task3)

              && !(task1 && task2 && task3) ) reach (S0)

< Back