TemporalLogic (Averest)

TemporalLogic Module

This module implements teaching tools for linear temporal logic

Function or value	Description
`LTL2LO1 phi` Full Usage: `LTL2LO1 phi` Parameters: phi : `SpecExpr` Returns: `BoolExpr`	Convert a given LTL formula to an equivalent LO1 formula. Note that the generated formula is not type-consistent with the Quartz semantics, since we are using boolean arrays as monadic predicates. Note further that the three variables (t0,t1,t2) are sufficient, where the formula is applied at time t0 whereas t1 and t2 are auxiliary variables. phi : `SpecExpr` Returns: `BoolExpr`
`Temp2LO1 (t0, t1, t2) phi` Full Usage: `Temp2LO1 (t0, t1, t2) phi` Parameters: t0 : `NatExpr` t1 : `NatExpr` t2 : `NatExpr` phi : `SpecExpr` Returns: `BoolExpr`	t0 : `NatExpr` t1 : `NatExpr` t2 : `NatExpr` phi : `SpecExpr` Returns: `BoolExpr`
`Temp2LO1Interval (t0, b0, t1, b1) t2 phi` Full Usage: `Temp2LO1Interval (t0, b0, t1, b1) t2 phi` Parameters: t0 : `NatExpr` b0 : `bool` t1 : `NatExpr` b1 : `bool` t2 : `NatExpr` phi : `SpecExpr` Returns: `BoolExpr`	t0 : `NatExpr` b0 : `bool` t1 : `NatExpr` b1 : `bool` t2 : `NatExpr` phi : `SpecExpr` Returns: `BoolExpr`
`TemporalLogicProverTool qscoll` Full Usage: `TemporalLogicProverTool qscoll` Parameters: qscoll : `NameValueCollection`	This function is called by the cgi-interface for the TemporalLogicProver. qscoll : `NameValueCollection`