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 ^ ";"