functor (A : Model.S->
  sig
    val is_safe_fwd_invariant : A.State.t list -> bool
    val is_safe_bwd_invariant : A.State.t list -> bool
    val is_empty_path_feasible : unit -> bool
    val is_non_empty_path_fwd_feasible :
      A.Automaton.Transition.t list -> bool
    val is_non_empty_path_bwd_feasible :
      A.Automaton.Transition.t list -> bool
  end