Module Ltl
module Ltl: sig .. end
LTL Properties
type
| |
Variable of string |
| |
True |
| |
Clock of ltl |
| |
Posedge of string |
| |
Negedge of string |
| |
Not of ltl |
| |
And of ltl * ltl |
| |
Next of ltl |
| |
Until of ltl * ltl |
val variable : string -> ltl
val not_ : ltl -> ltl
val and_ : ltl -> ltl -> ltl
val or_ : ltl -> ltl -> ltl
val imply : ltl -> ltl -> ltl
val equivalent : ltl -> ltl -> ltl
val next : bool -> ltl -> ltl
val until : bool -> ltl -> ltl -> ltl
val eventually : ltl -> ltl
val always : ltl -> ltl
val never : ltl -> ltl
val until_overlap : bool -> ltl -> ltl -> ltl
val before : bool -> ltl -> ltl -> ltl
val before_overlap : bool -> ltl -> ltl -> ltl
val next_repeat : bool -> int -> ltl -> ltl
val next_ae : bool -> bool -> int -> int -> ltl -> ltl
val next_event : bool -> ltl -> ltl -> ltl
val next_event_repeat : bool -> int -> ltl -> ltl -> ltl
val next_event_ae : bool -> bool -> int -> int -> ltl -> ltl -> ltl
val clock : ltl -> ltl -> ltl
val posedge : string -> ltl -> ltl
val negedge : string -> ltl -> ltl
val nusmv_of_ltl : ltl -> (string -> string) -> (string -> bool -> string) -> string