Up  

Module Ltl

module Ltl: sig .. end

Linear temporal logic

exception No_next_frame

No next frame 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

*)
| G of expr (*

□f

*)
| F of expr (*

◊f

*) 
val fmla_as_string : expr -> string

Represent formula as string.

val to_atomics : expr -> expr

Rewrite formula to use only atomic connectives/modal operators.

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

Evaluate formula over path.

val modal_depth : expr -> int

Calculate maximum depth of nested modalities in a formula.