-
-module type Oracle_fixpoint =
-sig
- type t = StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
- val equal : t -> t -> bool
- val hash : t -> int
-end
-
-type dStateS = StateSet.t*StateSet.t
-module type Run_fixpoint =
-sig
- type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
- val equal : t -> t -> bool
- val hash : t -> int
-end
-
-module Oracle_fixpoint : Oracle_fixpoint = struct
- type t =
- StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
- let equal (s,l,r,list,t) (s',l',r',list',t') = StateSet.equal s s' &&
- StateSet.equal l l' && StateSet.equal r r' && QName.equal t t'
- let hash (s,l,r,list,t) =
- HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, QName.hash t)
-end
-
-let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
-let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
-module Run_fixpoint : Run_fixpoint = struct
- type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
- let equal (s,l,r,list,t) (s',l',r',list',t') = dequal s s' &&
- dequal l l' && dequal r r' && QName.equal t t'
- let hash (s,l,r,list,t) =
- HASHINT4(dhash s, dhash l, dhash r, QName.hash t)
-end
-