CTL Model Checking: Parser error for the CTL formula "E(xUy)"
Description
Environment
None
Gliffy Diagrams
Activity
Show:
Details
Details
Assignee
Michael Leuschel
Michael LeuschelReporter
Ivaylo Dobrikov
Ivaylo DobrikovPriority
Created July 30, 2015 at 8:35 AM
Updated July 30, 2015 at 8:35 AM
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