Skip to content

Commit 773336e

Browse files
sim642sim642
committed
Lisa modelcheck/mutex
1 parent 4b645e9 commit 773336e

4 files changed

Lines changed: 249 additions & 0 deletions

File tree

‎src/modelcheck/mutex/dune‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(library
2+
(name modelcheck_mutex)
3+
(libraries modelcheck)
4+
(preprocess (pps ppx_deriving.std)))

‎src/modelcheck/mutex/modelcheck_mutex.ml‎

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
(** Muteksite mudelkontroll. *)
2+
3+
(** Naiivne muteks:
4+
5+
Algseisund:
6+
flag = false;
7+
8+
Lõim 1: Lõim 2:
9+
1: while (flag) {} 1: while (flag) {}
10+
2: flag = true; 2: flag = true;
11+
3: // kriitiline sektsioon 3: // kriitiline sektsioon
12+
4: flag = false; 4: flag = false;
13+
5: 5:
14+
15+
*)
16+
module NaiveMutex =
17+
struct
18+
type point = P1 | P2 | P3 | P4 | P5 [@@deriving ord, show]
19+
type t = {
20+
p1: point;
21+
p2: point;
22+
flag: bool;
23+
} [@@deriving ord, show]
24+
25+
let initial: t = {
26+
p1 = P1;
27+
p2 = P1;
28+
flag = false;
29+
}
30+
31+
32+
33+
let step (s: t): t list =
34+
failwith "TODO"
35+
36+
let is_error (s: t): bool =
37+
failwith "TODO"
38+
end
39+
40+
(** Petersoni algoritm (https://en.wikipedia.org/wiki/Peterson%27s_algorithm):
41+
42+
Algseisund:
43+
flag1 = flag2 = false;
44+
turn = 1; // pole tegelt oluline
45+
46+
Lõim 1: Lõim 2:
47+
1: flag1 = true; 1: flag2 = true;
48+
2: turn = 2; 2: turn = 1;
49+
3: while (flag2 && turn == 2) {} 3: while (flag1 && turn == 1) {}
50+
4: // kriitiline sektsioon 4: // kriitiline sektsioon
51+
5: flag1 = false; 5: flag2 = false;
52+
6: 6:
53+
54+
*)
55+
module PetersonAlgorithm =
56+
struct
57+
type point = P1 | P2 | P3 | P4 | P5 | P6 [@@deriving ord, show]
58+
type thread = T1 | T2 [@@deriving ord, show]
59+
type t = {
60+
p1: point;
61+
p2: point;
62+
flag1: bool;
63+
flag2: bool;
64+
turn: thread;
65+
} [@@deriving ord, show]
66+
67+
let initial: t = {
68+
p1 = P1;
69+
p2 = P1;
70+
flag1 = false;
71+
flag2 = false;
72+
turn = T1;
73+
}
74+
75+
76+
77+
let step (s: t): t list =
78+
failwith "TODO"
79+
80+
let is_error (s: t): bool =
81+
failwith "TODO"
82+
end
83+
84+
(** Dekkeri algoritm (https://en.wikipedia.org/wiki/Dekker%27s_algorithm):
85+
86+
Algseisund:
87+
flag1 = flag2 = false;
88+
turn = 1; // pole tegelt oluline
89+
90+
Lõim 1: Lõim 2:
91+
1: flag1 = true; 1: flag2 = true;
92+
2: while (flag2) { 2: while (flag1) {
93+
3: if (turn != 1) { 3: if (turn != 2) {
94+
4: flag1 = false; 4: flag2 = false;
95+
5: while (turn != 1) {} 5: while (turn != 2) {}
96+
6: flag1 = true; 6: flag2 = true;
97+
7: } 7: }
98+
8: } 8: }
99+
9: // kriitiline sektsioon 9: // kriitiline sektsioon
100+
10: turn = 2; 10: turn = 1;
101+
11: flag1 = false; 11: flag2 = false;
102+
12: 12:
103+
104+
*)
105+
module DekkerAlgorithm =
106+
struct
107+
type point = P1 | P2 | P3 | P4 | P5 | P6 | P9 | P10 | P11 | P12 [@@deriving ord, show]
108+
type thread = T1 | T2 [@@deriving ord, show]
109+
type t = {
110+
p1: point;
111+
p2: point;
112+
flag1: bool;
113+
flag2: bool;
114+
turn: thread;
115+
} [@@deriving ord, show]
116+
117+
let initial: t = {
118+
p1 = P1;
119+
p2 = P1;
120+
flag1 = false;
121+
flag2 = false;
122+
turn = T1;
123+
}
124+
125+
126+
127+
let step (s: t): t list =
128+
failwith "TODO"
129+
130+
let is_error (s: t): bool =
131+
failwith "TODO"
132+
end

‎test/modelcheck/mutex/dune‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(test
2+
(name mutex_test)
3+
(libraries ounit2 ounittodo modelcheck modelcheck_mutex)
4+
(preprocess (pps ppx_deriving.std)))

‎test/modelcheck/mutex/mutex_test.ml‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
open OUnit2
2+
open Modelcheck_mutex
3+
4+
5+
module NaiveMutexChecker = Modelcheck.Checker.MakeNaive (NaiveMutex)
6+
7+
let test_naive_correct _ =
8+
assert_equal ~printer:string_of_bool false (NaiveMutexChecker.is_correct ())
9+
10+
let test_naive_all_states _ =
11+
let all_states = NaiveMutexChecker.all_states () in
12+
let assert_exists expected f =
13+
assert_equal ~printer:string_of_bool expected (NaiveMutexChecker.StateSet.exists f all_states)
14+
in
15+
assert_exists true (fun s -> s.p1 = P1 && s.p2 = P1);
16+
assert_exists true (fun s -> s.p1 = P5 && s.p2 = P5);
17+
assert_exists true (fun s -> s.p1 = P3 && s.p2 = P3);
18+
assert_exists true (fun s -> s.p1 = P1 && s.p2 = P3);
19+
assert_exists true (fun s -> s.p1 = P3 && s.p2 = P1);
20+
assert_exists true (fun s -> s.p1 = P5 && s.p2 = P3);
21+
assert_exists true (fun s -> s.p1 = P3 && s.p2 = P5);
22+
assert_equal ~printer:string_of_int 29 (NaiveMutexChecker.StateSet.cardinal all_states)
23+
24+
let test_naive_error_states _ =
25+
let error_states = NaiveMutexChecker.error_states () in
26+
let assert_mem expected state =
27+
assert_equal ~printer:string_of_bool ~msg:(NaiveMutex.show state) expected (NaiveMutexChecker.StateSet.mem state error_states)
28+
in
29+
(* Kõik veaolekud. *)
30+
assert_mem true {p1 = P3; p2 = P3; flag = true};
31+
assert_equal ~printer:string_of_int 1 (NaiveMutexChecker.StateSet.cardinal error_states)
32+
33+
34+
module PetersonAlgorithmChecker = Modelcheck.Checker.MakeNaive (PetersonAlgorithm)
35+
36+
let test_peterson_correct _ =
37+
assert_equal ~printer:string_of_bool true (PetersonAlgorithmChecker.is_correct ())
38+
39+
let test_peterson_all_states _ =
40+
let all_states = PetersonAlgorithmChecker.all_states () in
41+
let assert_exists expected f =
42+
assert_equal ~printer:string_of_bool expected (PetersonAlgorithmChecker.StateSet.exists f all_states)
43+
in
44+
assert_exists true (fun s -> s.p1 = P1 && s.p2 = P1);
45+
assert_exists true (fun s -> s.p1 = P6 && s.p2 = P6);
46+
assert_exists false (fun s -> s.p1 = P4 && s.p2 = P4);
47+
assert_exists true (fun s -> s.p1 = P1 && s.p2 = P4);
48+
assert_exists true (fun s -> s.p1 = P4 && s.p2 = P1);
49+
assert_exists true (fun s -> s.p1 = P6 && s.p2 = P4);
50+
assert_exists true (fun s -> s.p1 = P4 && s.p2 = P6);
51+
assert_equal ~printer:string_of_int 34 (PetersonAlgorithmChecker.StateSet.cardinal all_states)
52+
53+
let test_peterson_error_states _ =
54+
let error_states = PetersonAlgorithmChecker.error_states () in
55+
assert_equal ~printer:string_of_int 0 (PetersonAlgorithmChecker.StateSet.cardinal error_states);
56+
(* Kontrollime veaoleku funktsiooni hüpoteetilistel olekutel. *)
57+
assert_equal ~printer:string_of_bool true (PetersonAlgorithm.is_error {p1 = P4; p2 = P4; flag1 = true; flag2 = true; turn = T1});
58+
assert_equal ~printer:string_of_bool true (PetersonAlgorithm.is_error {p1 = P4; p2 = P4; flag1 = true; flag2 = true; turn = T2})
59+
60+
61+
module DekkerAlgorithmChecker = Modelcheck.Checker.MakeNaive (DekkerAlgorithm)
62+
63+
let test_dekker_correct _ =
64+
assert_equal ~printer:string_of_bool true (DekkerAlgorithmChecker.is_correct ())
65+
66+
let test_dekker_all_states _ =
67+
let all_states = DekkerAlgorithmChecker.all_states () in
68+
let assert_exists expected f =
69+
assert_equal ~printer:string_of_bool expected (DekkerAlgorithmChecker.StateSet.exists f all_states)
70+
in
71+
assert_exists true (fun s -> s.p1 = P1 && s.p2 = P1);
72+
assert_exists true (fun s -> s.p1 = P12 && s.p2 = P12);
73+
assert_exists false (fun s -> s.p1 = P9 && s.p2 = P9);
74+
assert_exists true (fun s -> s.p1 = P1 && s.p2 = P9);
75+
assert_exists true (fun s -> s.p1 = P9 && s.p2 = P1);
76+
assert_exists true (fun s -> s.p1 = P12 && s.p2 = P9);
77+
assert_exists true (fun s -> s.p1 = P9 && s.p2 = P12);
78+
assert_equal ~printer:string_of_int 53 (DekkerAlgorithmChecker.StateSet.cardinal all_states)
79+
80+
let test_dekker_error_states _ =
81+
let error_states = DekkerAlgorithmChecker.error_states () in
82+
assert_equal ~printer:string_of_int 0 (DekkerAlgorithmChecker.StateSet.cardinal error_states);
83+
(* Kontrollime veaoleku funktsiooni hüpoteetilistel olekutel. *)
84+
assert_equal ~printer:string_of_bool true (DekkerAlgorithm.is_error {p1 = P9; p2 = P9; flag1 = true; flag2 = true; turn = T1});
85+
assert_equal ~printer:string_of_bool true (DekkerAlgorithm.is_error {p1 = P9; p2 = P9; flag1 = true; flag2 = true; turn = T2})
86+
87+
88+
let tests =
89+
"modelcheck" >::: [
90+
"mutex" >::: [
91+
"naive" >::: [
92+
"correct" >:: test_naive_correct;
93+
"all_states" >:: test_naive_all_states;
94+
"error_states" >:: test_naive_error_states;
95+
];
96+
"peterson" >::: [
97+
"correct" >:: test_peterson_correct;
98+
"all_states" >:: test_peterson_all_states;
99+
"error_states" >:: test_peterson_error_states;
100+
];
101+
"dekker" >::: [
102+
"correct" >:: test_dekker_correct;
103+
"all_states" >:: test_dekker_all_states;
104+
"error_states" >:: test_dekker_error_states;
105+
];
106+
];
107+
]
108+
109+
let () = run_test_tt_main (OUnitTodo.wrap tests)

0 commit comments

Comments
 (0)