module Ltlast:sig
..end
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.
| *) |