where

The where clause specifies a condition that can be applied to a variable or transition(edge).

Syntax

The syntax of a where clause is as follows:

 where <expression>;

The expression here must be a boolean expression.

Scope

A where clause can only be used with the declaration of a variable or an edge.

Semantics

A where can be used in the following two ways:

Variable declaration: If a where clause is used with a variable declaration, this means that this variable is a conditional variable. This variable must meet the condition (specified by the where clause) before, during and after each computation in a cyclone specification. The condition must be a boolean expression that can only contain this variable itself or constants. No other variables are allowed in the expression. See below:
```
   int a;
```
```
   int c where c>=0 && c<=a; //illegal: a is another variable
```
```
   const int LEN=5;
```
```
   const int PAD=1;
```
```
 /* okay: the following where clause contains only c itself 
```
```
  * and other constants: LEN and PAD */
```
```
   int c where c>=LEN+PAD;
```
Transition (edge) declaration: If a where clause is used with a transition declaration, this means that this transition is a conditional transition (transition guard). This transition can only happen when the guard/condition (specified by a where clause) is satisfied. This also implies that no other conditions can trigger this transition. The guard/condition in a where clause must refer to global variables or constants. See below:
```
      //t1 can only happen when coin is true.
```
```
      trans t1 {Locked -> Unlocked where coin==true;}
```
```
      //t2 can only happen when push is true.
```
```
      trans t2 {Unlocked -> Locked where push==true;}
```
```
      //t3 can only happen when coin is not true.
```
```
      trans t3 {Locked -> Locked} //implicitly push==false
```
```
      //t4 can only happen when push is not true.
```
```
      trans t4 {Unlocked -> Locked} //implicitly push==false
```

Examples

      int a where a>=0;

The variable a must satisfy the condition a>=0 before, during and after each computation in the specification.

IMPORTANT: a where clause checks the initializer of an variable. See the following example:

      const int LOWER_BOUND = 10;

      int a = 0 where a >= LOWER_BOUND;

Cyclone cannot find a path to satisfy the condition specified by the where clause since variable a is initialized with 0 here.

The following example shows a where clause is used with a transition.

      trans t {In -> Out where door_open==true;}

The transition In -> Out can only happen when the condition door_open==true is met.

< Back