occurrence (^{i:j})

The occurrence operator ^{i:j} is a path operator that is used to specify a particular path or node to occur a number of times.

Syntax

The syntax of ^{i:j} is as follows:

    node^{i:j} | (path)^{i:j}

The occurrence operator can be applied on both a node or path. When it applies to a path, parentheses must be used. ^{i:j} can only appear at the end of a node or path. Hence, sometimes it is also referred as a suffix path operator in Cyclone.

Scope

Path operator ^{i:j} can only be used in goal section.

Semantics

A path p or node n is specified with ^{i:j} indicates that p or n must occur between i and j times (inclusive). However, when the form of ^{i} is used this indicates that p or n must occur exactly i times.

To remove ambiguity, when ^{i:j} is applied to a path, parentheses must be used. The following path condition is illegal in Cyclone.

    S1->S2->S3^{1:3}

Example

  S5^{3:5} && (S1->S2->S3)^{3}

The node S5 must appear between 3 and 5 times (inclusive), and the path S1->S2->S3 must appear exactly 3 times.

< Back