Module Ltlast

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 formula (*
'Next' temporal operator
*)
| LUntil of formula * formula (*
'Until' temporal operator
*)
| LFatally of formula (*
'Fatally' temporal operator
*)
| LGlobally of formula (*
'Globally' temporal operator
*)
| LRelease of formula * formula (*
'Release' temporal operator (reminder: f1 R f2 <=> !(!f1 U !f2))
*)
| LNot of formula (*
'not' logic operator
*)
| LAnd of formula * formula (*
'and' logic operator
*)
| LOr of formula * formula (*
'or' logic operator
*)
| LImplies of formula * formula (*
'=>' logic operator
*)
| LIff of formula * formula (*
'<=>' logic operator
*)
| LTrue (*
'true' logic constant
*)
| LFalse (*
'false' logic constant
*)
| LCall of string (*
Logic predicate. The String has to be the name of an operation from C program
*)
| LReturn of string (*
Logic predicate. The String has to be the name of an operation from C program
*)
| LCallOrReturn of string (*
Logic predicate. The String has to be the name of an operation from C program
*)
| LIdent of string (*
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