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