+ val atom_ : P.t -> t
+ (** [atom_ dir b q] creates a down_left or down_right atom for state
+ [q]. The atom is positive if [b == true].
+ *)
+
+ val not_ : t -> t
+ val or_ : t -> t -> t
+ val and_ : t -> t -> t
+ (** Boolean connective *)
+
+ val of_bool : bool -> t
+ (** Convert an ocaml Boolean value to a formula *)
+
+ val eval : P.ctx -> t -> bool
+ (** Evaluate a formula given a context for atomic predicates *)
+end