let nusmv_of_ltl ltl name_of_signal name_of_clock =
let rec nusmv_of_ltl ltl =
match ltl with
| Variable name -> name_of_signal name
| True -> "1"
| Posedge clock -> name_of_clock clock true
| Negedge clock -> name_of_clock clock false
| Clock a -> nusmv_of_ltl a
| Not a -> "(! " ^ nusmv_of_ltl a ^ ")"
| And (a, b) -> "(" ^ nusmv_of_ltl a ^ " & " ^ nusmv_of_ltl b ^ ")"
| Next a -> "(X " ^ nusmv_of_ltl a ^ ")"
| Until (a, b) -> "(" ^ nusmv_of_ltl a ^ " U " ^ nusmv_of_ltl b ^ ")"
in
"LTLSPEC " ^ nusmv_of_ltl ltl ^ ";"