Skip to content

Commit aea6f7f

Browse files
sim642sim642
committed
Lisa modelcheck/program
1 parent 2074b7d commit aea6f7f

File tree

4 files changed

+627
-0
lines changed

4 files changed

+627
-0
lines changed

‎src/modelcheck/program/dune

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

‎src/modelcheck/program/modelcheck_program.ml

Lines changed: 272 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,272 @@
1+
(** Programmide mudelkontroll. *)
2+
open Modelcheck
3+
4+
(** Väärtuskeskkond.
5+
Muutujate nimed on sõned ja väärtused täisarvud. *)
6+
module Env = Map.Make (String)
7+
type env = int Env.t [@@deriving ord]
8+
9+
module type ProgramModel =
10+
sig
11+
(** Programmi mudeli olekud koosnevad programmi punktist ja keskkonnast. *)
12+
type point [@@deriving ord, show]
13+
include Model with type t = point * env
14+
end
15+
16+
(** Abifunktsioon juhuarvu step funktsiooni implementeerimiseks. *)
17+
let nondet (point': 'a) (x: string) ((l, u): int * int) env: ('a * env) list =
18+
List.init (u - l + 1) (fun i ->
19+
(point', Env.add x (l + i) env)
20+
)
21+
22+
(** Mudel järgmise programmi jaoks:
23+
24+
1: int x = 1;
25+
2: int y = __VERIFIER_nondet_int(); // -10..10
26+
3: int z = __VERIFIER_nondet_int(); // -10..10
27+
4: if (z > 5)
28+
5: x = y;
29+
6: else
30+
7: x++;
31+
8: assert(x != 0); // kas võib ebaõnnestuda?
32+
33+
*)
34+
module ExampleProgram =
35+
struct
36+
type point = P2 | P3 | P4 | P5 | P7 | P8 [@@deriving ord, show]
37+
type t = point * env [@@deriving ord]
38+
39+
let initial: t = (P2, Env.singleton "x" 1)
40+
41+
let step ((point, env): t): t list =
42+
failwith "TODO"
43+
44+
let is_error ((point, env): t): bool =
45+
failwith "TODO"
46+
end
47+
48+
(** Mudel järgmise programmi jaoks:
49+
50+
1: unsigned int x = __VERIFIER_nondet_uint(); // 0..1500
51+
2: unsigned int y = x;
52+
3: while (x < 1024) {
53+
4: x++;
54+
5: y++;
55+
6: }
56+
7: assert(x == y); // kas võib ebaõnnestuda?
57+
58+
*)
59+
module CountUpProgram =
60+
struct
61+
type point = P1 | P2 | P3 | P4 | P5 | P7 [@@deriving ord, show]
62+
type t = point * env [@@deriving ord]
63+
64+
let initial: t = (P1, Env.empty)
65+
66+
let step ((point, env): t): t list =
67+
failwith "TODO"
68+
69+
let is_error ((point, env): t): bool =
70+
failwith "TODO"
71+
end
72+
73+
(** Mudel järgmise programmi jaoks:
74+
75+
1: unsigned int y = 1;
76+
2: unsigned int x0 = __VERIFIER_nondet_uint(); // 0..5
77+
3: unsigned int n0 = __VERIFIER_nondet_uint(); // 1..5
78+
4: unsigned int x = x0;
79+
5: unsigned int n = n0;
80+
6: while (n > 1) {
81+
7: if (n % 2 == 0)
82+
8: n = n / 2;
83+
9: else {
84+
10: y = x * y;
85+
11: n = (n + 1) / 2;
86+
12: }
87+
13: x = x * x;
88+
14: }
89+
15: y = x * y;
90+
16: assert(y == pow(x0, n0)); // kas võib ebaõnnestuda?
91+
92+
*)
93+
module PowProgram =
94+
struct
95+
type point = P2 | P3 | P4 | P5 | P6 | P7 | P8 | P10 | P11 | P13 | P15 | P16 [@@deriving ord, show]
96+
type t = point * env [@@deriving ord]
97+
98+
let initial: t = (P2, Env.singleton "y" 1)
99+
100+
let step ((point, env): t): t list =
101+
failwith "TODO"
102+
103+
(** Vihje: Kasuta Crashcourse.Basics.pow funktsiooni. *)
104+
let is_error ((point, env): t): bool =
105+
failwith "TODO"
106+
end
107+
108+
(** Mudel parandatud PowProgram jaoks. *)
109+
module FixedPowProgram =
110+
struct
111+
include PowProgram (* Ei pea kõike kopeerima. *)
112+
113+
let step ((point, env): t): t list =
114+
match point with (* Siin saab üle defineerida ühe juhu. *)
115+
116+
| _ -> step (point, env)
117+
end
118+
119+
(** Mudel järgmise programmi jaoks:
120+
121+
1: unsigned int y = 0;
122+
2: unsigned int n = __VERIFIER_nondet_uint(); // 0..15
123+
3: unsigned int x = n;
124+
4: while (x > 0) {
125+
5: x--;
126+
6: y++;
127+
7: }
128+
8: assert(y == n); // kas võib ebaõnnestuda?
129+
130+
*)
131+
module CountUpDownProgram =
132+
struct
133+
type point = P2 | P3 | P4 | P5 | P6 | P8 [@@deriving ord, show]
134+
type t = point * env [@@deriving ord]
135+
136+
let initial: t = (P2, Env.singleton "y" 0)
137+
138+
let step ((point, env): t): t list =
139+
failwith "TODO"
140+
141+
let is_error ((point, env): t): bool =
142+
failwith "TODO"
143+
end
144+
145+
(** Mudel järgmise programmi jaoks:
146+
147+
1: unsigned int sum = 0;
148+
2: unsigned int i = 1;
149+
3: unsigned int n = __VERIFIER_nondet_uint(); // 0..15
150+
4: while (i < n) {
151+
5: sum += i;
152+
6: i++;
153+
7: }
154+
8: assert(sum == n * (n + 1) / 2); // kas võib ebaõnnestuda?
155+
156+
*)
157+
module SumProgram =
158+
struct
159+
type point = P3 | P4 | P5 | P6 | P8 [@@deriving ord, show]
160+
type t = point * env [@@deriving ord]
161+
162+
let initial: t = (P3, Env.add "i" 1 (Env.singleton "sum" 0))
163+
164+
let step ((point, env): t): t list =
165+
failwith "TODO"
166+
167+
let is_error ((point, env): t): bool =
168+
failwith "TODO"
169+
end
170+
171+
(** Mudel parandatud SumProgram jaoks. *)
172+
module FixedSumProgram =
173+
struct
174+
include SumProgram (* Ei pea kõike kopeerima. *)
175+
176+
let step ((point, env): t): t list =
177+
match point with (* Siin saab üle defineerida ühe juhu. *)
178+
179+
| _ -> step (point, env)
180+
end
181+
182+
(** Arvutab ruutjuure täisarvust.
183+
Vt. https://en.wikipedia.org/wiki/Integer_square_root. *)
184+
let isqrt n =
185+
int_of_float (sqrt (float_of_int n))
186+
187+
(** Mudel järgmise programmi jaoks:
188+
189+
1: unsigned int l = 0;
190+
2: unsigned int y = __VERIFIER_nondet_uint(); // 0..50
191+
3: while ((l + 1) * (l + 1) <= y)
192+
4: l++;
193+
5: assert(l == isqrt(y)); // kas võib ebaõnnestuda?
194+
195+
*)
196+
module LinearSqrtProgram =
197+
struct
198+
type point = P2 | P3 | P4 | P5 [@@deriving ord, show]
199+
type t = point * env [@@deriving ord]
200+
201+
let initial: t = (P2, Env.singleton "l" 0)
202+
203+
let step ((point, env): t): t list =
204+
failwith "TODO"
205+
206+
(** Vihje: Kasuta ülaldefineeritud isqrt funktsiooni. *)
207+
let is_error ((point, env): t): bool =
208+
failwith "TODO"
209+
end
210+
211+
(** Mudel järgmise programmi jaoks:
212+
213+
1: unsigned int l = 0;
214+
2: unsigned int y = __VERIFIER_nondet_uint(); // 0..50
215+
3: unsigned int r = y + 1;
216+
4: unsigned int m;
217+
5: while (l != r - 1) {
218+
6: m = (l + r) / 2;
219+
7: if (m * m <= y)
220+
8: l = m;
221+
9: else
222+
10: r = m;
223+
11: }
224+
12: assert(l == isqrt(y)); // kas võib ebaõnnestuda?
225+
226+
*)
227+
module BinarySqrtProgram =
228+
struct
229+
type point = P2 | P3 | P5 | P6 | P7 | P8 | P10 | P12 [@@deriving ord, show]
230+
type t = point * env [@@deriving ord]
231+
232+
let initial: t = (P2, Env.singleton "l" 0)
233+
234+
let step ((point, env): t): t list =
235+
failwith "TODO"
236+
237+
(** Vihje: Kasuta ülaldefineeritud isqrt funktsiooni. *)
238+
let is_error ((point, env): t): bool =
239+
failwith "TODO"
240+
end
241+
242+
(** Mudel järgmise programmi jaoks:
243+
244+
1: unsigned int s = __VERIFIER_nondet_uint(); // 0..50
245+
2: unsigned int x0;
246+
3: if (s <= 1)
247+
4: x0 = s;
248+
5: else {
249+
6: x0 = s / 2;
250+
7: unsigned int x1 = (x0 + s / x0) / 2;
251+
8: while (x1 < x0) {
252+
9: x0 = x1;
253+
10: x1 = (x0 + s / x0) / 2;
254+
11: }
255+
12: }
256+
13: assert(x0 == isqrt(s)); // kas võib ebaõnnestuda?
257+
258+
*)
259+
module NewtonSqrtProgram =
260+
struct
261+
type point = P1 | P3 | P4 | P6 | P7 | P8 | P9 | P10 | P13 [@@deriving ord, show]
262+
type t = point * env [@@deriving ord]
263+
264+
let initial: t = (P1, Env.empty)
265+
266+
let step ((point, env): t): t list =
267+
failwith "TODO"
268+
269+
(** Vihje: Kasuta ülaldefineeritud isqrt funktsiooni. *)
270+
let is_error ((point, env): t): bool =
271+
failwith "TODO"
272+
end

‎test/modelcheck/program/dune

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

0 commit comments

Comments
 (0)