Lisa modelcheck

Author: sim642

src/modelcheck/checker.ml

@@ -0,0 +1,30 @@
+open Model
+
+(** Mudelkontrollija, mis kasutab püsipunkti.
+    Vt. Fixpoint moodul. *)
+module MakeNaive (Model: Model) =
+struct
+  module StateSet = Set.Make (Model)
+  module StateSetFP = Fixpoint.MakeSet (StateSet)
+
+
+
+  (** Tagastab kõik saavutatavad olekud. *)
+  let all_states (): StateSet.t =
+    failwith "TODO"
+
+  (** Tagastab kõik saavutatavad veaolekud.
+      Vihje: StateSet.filter. *)
+  let error_states (): StateSet.t =
+    failwith "TODO"
+
+  (** Kas mõni veaolek on saavutatav? *)
+  let has_error (): bool =
+    failwith "TODO"
+
+  (** Kas veaolekud on mittesaavutatavad? *)
+  let is_correct (): bool =
+    failwith "TODO"
+end
+
+

src/modelcheck/dune

@@ -0,0 +1,4 @@
+(library
+ (name modelcheck)
+ (libraries fixpoint)
+ (preprocess (pps ppx_deriving.std)))

src/modelcheck/model.ml

@@ -0,0 +1,14 @@
+module type Model =
+sig
+  (** Oleku tüüp. *)
+  type t [@@deriving ord]
+
+  (** Algolek. *)
+  val initial: t
+
+  (** Tagastab olekule järgnevad võimalikud olekud. *)
+  val step: t -> t list
+
+  (** Kontrollib, kas on veaolek. *)
+  val is_error: t -> bool
+end

src/modelcheck/modelcheck.ml

@@ -0,0 +1,3 @@
+include Model
+
+module Checker = Checker

test/modelcheck/dune

@@ -0,0 +1,4 @@
+(test
+ (name modelcheck_test)
+ (libraries ounit2 ounittodo modelcheck)
+ (preprocess (pps ppx_deriving.std)))

test/modelcheck/modelcheck_test.ml

@@ -0,0 +1,97 @@
+open OUnit2
+open Modelcheck
+
+module BadModel =
+struct
+  type t = int [@@deriving ord, show]
+
+  let initial = 42
+
+  let step i =
+    if i >= 0 then
+      [i - 1; i - 2; i - 3]
+    else
+      []
+
+  let is_error i = i < 0
+end
+
+module BadModelChecker = Checker.MakeNaive (BadModel)
+
+let test_bad_correct _ =
+  assert_equal ~printer:string_of_bool true (BadModelChecker.has_error ());
+  assert_equal ~printer:string_of_bool false (BadModelChecker.is_correct ())
+
+let test_bad_all_states _ =
+  let all_states = BadModelChecker.all_states () in
+  let assert_mem expected state =
+    assert_equal ~printer:string_of_bool ~msg:(BadModel.show state) expected (BadModelChecker.StateSet.mem state all_states)
+  in
+  assert_mem true 42;
+  assert_mem false 43;
+  assert_mem true 0;
+  assert_equal ~printer:string_of_int 46 (BadModelChecker.StateSet.cardinal all_states)
+
+let test_bad_error_states _ =
+  let error_states = BadModelChecker.error_states () in
+  let assert_mem expected state =
+    assert_equal ~printer:string_of_bool ~msg:(BadModel.show state) expected (BadModelChecker.StateSet.mem state error_states)
+  in
+  (* Kõik veaolekud. *)
+  assert_mem true (-1);
+  assert_mem true (-2);
+  assert_mem true (-3);
+  assert_equal ~printer:string_of_int 3 (BadModelChecker.StateSet.cardinal error_states)
+
+
+module GoodModel =
+struct
+  type t = int [@@deriving ord, show]
+
+  let initial = 42
+
+  let step i =
+    if i >= 3 then
+      [i - 1; i - 2; i - 3]
+    else
+      []
+
+  let is_error i = i < 0
+end
+
+module GoodModelChecker = Checker.MakeNaive (GoodModel)
+
+let test_good_correct _ =
+  assert_equal ~printer:string_of_bool false (GoodModelChecker.has_error ());
+  assert_equal ~printer:string_of_bool true (GoodModelChecker.is_correct ())
+
+let test_good_all_states _ =
+  let all_states = GoodModelChecker.all_states () in
+  let assert_mem expected state =
+    assert_equal ~printer:string_of_bool ~msg:(GoodModel.show state) expected (GoodModelChecker.StateSet.mem state all_states)
+  in
+  assert_mem true 42;
+  assert_mem false 43;
+  assert_mem true 0;
+  assert_equal ~printer:string_of_int 43 (GoodModelChecker.StateSet.cardinal all_states)
+
+let test_good_error_states _ =
+  let error_states = GoodModelChecker.error_states () in
+  assert_equal ~printer:string_of_int 0 (GoodModelChecker.StateSet.cardinal error_states)
+
+
+let tests =
+  "modelcheck" >::: [
+    "bad" >::: [
+      "correct" >:: test_bad_correct;
+      "all_states" >:: test_bad_all_states;
+      "error_states" >:: test_bad_error_states;
+    ];
+    "good" >::: [
+      "correct" >:: test_good_correct;
+      "all_states" >:: test_good_all_states;
+      "error_states" >:: test_good_error_states;
+    ];
+  ]
+
+let () = run_test_tt_main (OUnitTodo.wrap tests)