module Ltlast:sig
..end
The abstract tree of LTL formula. Such tree is used by ltl parser/lexer before its translation into Buchi automata by the LTL2BA external tool.
type
formula =
| |
LNext of |
(* | 'Next' temporal operator | *) |
| |
LUntil of |
(* | 'Until' temporal operator | *) |
| |
LFatally of |
(* | 'Fatally' temporal operator | *) |
| |
LGlobally of |
(* | 'Globally' temporal operator | *) |
| |
LRelease of |
(* | 'Release' temporal operator (reminder: f1 R f2 <=> !(!f1 U !f2)) | *) |
| |
LNot of |
(* | 'not' logic operator | *) |
| |
LAnd of |
(* | 'and' logic operator | *) |
| |
LOr of |
(* | 'or' logic operator | *) |
| |
LImplies of |
(* | '=>' logic operator | *) |
| |
LIff of |
(* | '<=>' logic operator | *) |
| |
LTrue |
(* | 'true' logic constant | *) |
| |
LFalse |
(* | 'false' logic constant | *) |
| |
LCall of |
(* | Logic predicate. The String has to be the name of an operation from C program | *) |
| |
LReturn of |
(* | Logic predicate. The String has to be the name of an operation from C program | *) |
| |
LCallOrReturn of |
(* | Logic predicate. The String has to be the name of an operation from C program | *) |
| |
LIdent of |
(* | Logic expression. The String is the name of a fresh variable defined by the expression and used to be in conformance with the input syntax of LTL2BA tool. | *) |
LTL formula parsed abstract syntax trees