condition

The condition statement specifies one or more path conditions over a path p to be discovered by Cyclone.

Syntax

The syntax of a condition statement is as follows:

 condition (PathCondition₁,PathCondition₂,...,PathCondition_n)

Each PathCondition here can either be a compound path condition or a simple path condition.

Here is an example:

 condition ( (S1->S2) && !(S2->S3), S4^{2})

Scope

The condition statement can only appear in either a check or enumeration statement which can only appear in the goal section. The condition statement cannot be used alone. Typically, the condition statement is used as a part of a check or enumeration statement.

   check for 6 condition (

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

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

   reach (S0)

However, the condition statement can also be optional for check or enumeration statement.

Semantics

The condition statement specifies the kinds of path(s) to be discovered by Cyclone. The list of path conditions specified within the condition statement are logically conjoined.

 condition ( (S3->S4->S5), S2, (S5->S6)^{3})

is the same as

 condition ( ((S3->S4->S5) && S2 && (S5->S6)^{3}) )

< Back