Lahenda modelcheck praktikumis

Author: sim642

src/modelcheck/checker.ml

@@ -7,24 +7,27 @@ struct
   module StateSet = Set.Make (Model)
   module StateSetFP = Fixpoint.MakeSet (StateSet)
 
-
+  let f states =
+    StateSet.elements states
+    |> List.concat_map Model.step
+    |> StateSet.of_list
 
   (** Tagastab kõik saavutatavad olekud. *)
   let all_states (): StateSet.t =
-    failwith "TODO"
+    StateSetFP.closure_strict_distr f (StateSet.singleton Model.initial)
 
   (** Tagastab kõik saavutatavad veaolekud.
       Vihje: StateSet.filter. *)
   let error_states (): StateSet.t =
-    failwith "TODO"
+    StateSet.filter Model.is_error (all_states ())
 
   (** Kas mõni veaolek on saavutatav? *)
   let has_error (): bool =
-    failwith "TODO"
+    not (StateSet.is_empty (error_states ()))
 
   (** Kas veaolekud on mittesaavutatavad? *)
   let is_correct (): bool =
-    failwith "TODO"
+    not (has_error ())
 end