Module Ltl

module Ltl: sig .. end

Linear temporal logic

exception No_next_state

No next state in path.

type expr =

`\|`	`True`
`\|`	`False`
`\|`	`Var of string`
`\|`	`And of expr * expr`
`\|`	`Or of expr * expr`
`\|`	`Impl of expr * expr`
`\|`	`Iff of expr * expr`
`\|`	`U of expr * expr`	`(*`	until	`*)`
`\|`	`R of expr * expr`	`(*`	release	`*)`
`\|`	`W of expr * expr`	`(*`	weak	`*)`
`\|`	`M of expr * expr`	`(*`	strong release	`*)`
`\|`	`Not of expr`
`\|`	`X of expr`	`(*`	◯f -- true in next state	`*)`
`\|`	`G of expr`	`(*`	□f -- globally true	`*)`
`\|`	`F of expr`	`(*`	◊f -- eventually true	`*)`

val to_nnf : expr -> expr

Convert formula to negation normal form. Result contains only propositional connectives and U, R, X. Negations will only appear in front of atomic symbols.

val fmla_as_string : expr -> string

Formula as string

val to_atomics : expr -> expr

Rewrite formula to use only propositional operators, X, and U.

val eval_fmla : expr -> (string * bool) list list -> bool

Evaluate formula over path.

val modal_depth : expr -> int

Maximum depth of nested modalities in a formula.