module type TransSys = sig type state val initstate : state val trans : state -> state list end module While : TransSys = struct type state = int let initstate = 0 let trans x = if x < 100 then [x+1] else [] end module RSCollSem (TS: TransSys) = struct module SS = Set.Make(struct type t = TS.state let compare = Pervasives.compare end) (* this t implements T from slide 34 *) let t sigma = SS.union (SS.singleton TS.initstate) (SS.fold (fun elm acc -> let ls = TS.trans elm in List.fold_left (fun acc' elm' -> SS.add elm' acc') acc ls) sigma SS.empty) end (* Now we can define the reachable states of the while example *) module WhileRSCS = RSCollSem (While) (* and compute a Kleene sequence *) let k0 = WhileRSCS.SS.empty let k1 = WhileRSCS.t k0 let k2 = WhileRSCS.t k1 let k3 = WhileRSCS.t k2 (* ... *) (* but you'll need pretty printing / to_string functions *) (* to observe the result *)