CTL Model Checking: Parser error for the CTL formula "E(xUy)"

Description

Braces are not allowed for CTL formulae of the type ExUy. For the sake of clarity, it is sometimes helpful for the readability of formulae like ExUy to separate the path formula by using braces.

Often, one wants to wrap the until formula into braces in order to make clear which is the path formula: E(xUy). For the current version of the CTL parser this is currently not possible.

For instance, the formula "E({addr <2} U {addr = 2})" cannot be pared for the B machine below. The parser exits with the following error message:

Syntax error: [1,14] expecting: r par, '=>'
CTL Parser failed: E ({addr <2} U {addr = 2})

MACHINE Example
DEFINITIONS
ASSERT_CTL_1 == "E {addr <2} U {addr = 2}";
ASSERT_CTL_2 == "E({addr <2} U {addr = 2})";

VARIABLES addr
INVARIANT
addr : INTEGER
INITIALISATION
addr := 0
OPERATIONS
A = PRE addr<2 THEN addr := addr+1 END;
B = PRE addr = 2 THEN skip END
END

Environment

None

Gliffy Diagrams

Activity

Show:

Details

Assignee

Reporter

Priority

Created July 30, 2015 at 8:35 AM
Updated July 30, 2015 at 8:35 AM