Skip to content

Commit 1569f6f

Browse files
wimmerswimmers
committed
Add ML files
1 parent 258703b commit 1569f6f

10 files changed

+5821
-0
lines changed

‎ML/Checker.sml

Lines changed: 342 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,342 @@
1+
open Reachability_Checker;
2+
3+
(*** Utilities for parsing
4+
* Should be removed at some point
5+
***)
6+
datatype ('a, 'b) instr' = JMPZ' of 'a | ADD' | NOT' | AND' | LT' | LE' | EQ' | PUSH' of 'b | POP' |
7+
LID' of 'a | STOREI' of 'a * 'b | COPY' | CALL' | RETURN' | HALT' |
8+
STOREC' of 'a * 'b | SETF' of bool
9+
10+
datatype ('a, 'b, 'c) instrc' = INSTR' of ('a, 'b) instr' | CEXP' of ('a, 'c) acconstraint
11+
12+
datatype ('a, 'b) bexp' =
13+
Not' of ('a, 'b) bexp' |
14+
And' of ('a, 'b) bexp' * ('a, 'b) bexp' |
15+
Or' of ('a, 'b) bexp' * ('a, 'b) bexp' |
16+
Imply' of ('a, 'b) bexp' * ('a, 'b) bexp' |
17+
Loc' of 'a * 'a | Eq' of 'a * 'b | Lea' of 'a * 'b |
18+
Lta' of 'a * 'b | Ge' of 'a * 'b | Gt' of 'a * 'b
19+
20+
infix 9 Lea' Lta' Ge' Gt' Eq'
21+
infix 8 And'
22+
infix 7 Or' Imply'
23+
24+
fun map_acconstraint f g = fn
25+
LTa (a, b) => LTa (f a, g b) |
26+
LEa (a, b) => LEa (f a, g b) |
27+
EQa (a, b) => EQa (f a, g b) |
28+
GE (a, b) => GE (f a, g b) |
29+
GT (a, b) => GT (f a, g b)
30+
31+
fun map_act f = fn
32+
In a => In (f a) |
33+
Out a => Out (f a) |
34+
Sil a => Sil (f a)
35+
36+
fun map_instr f_nat f_int = fn
37+
JMPZ' n => JMPZ (f_nat n) |
38+
PUSH' i => PUSH (f_int i) |
39+
LID' n => LID (f_nat n) |
40+
STOREI' (n, i) => STOREI (f_nat n, f_int i) |
41+
STOREC' (n, i) => STOREC (f_nat n, f_int i) |
42+
ADD' => ADD | NOT' => NOT | AND' => AND | LT' => LT | LE' => LE | EQ' => EQ |
43+
POP' => POP | COPY' => COPY | CALL' => CALL | RETURN' => RETURN | HALT' => HALT |
44+
SETF' b => SETF b
45+
46+
fun map_instrc f_nat f_int f_time = fn
47+
INSTR' instr => INSTR (map_instr f_nat f_int instr) |
48+
CEXP' ac => CEXP (map_acconstraint f_nat f_time ac)
49+
50+
fun map_bexp f_nat f_int = fn
51+
Not' a => Not (map_bexp f_nat f_int a) |
52+
a And' b => And (map_bexp f_nat f_int a, map_bexp f_nat f_int b) |
53+
a Or' b => Or (map_bexp f_nat f_int a, map_bexp f_nat f_int b) |
54+
a Imply' b => Imply (map_bexp f_nat f_int a, map_bexp f_nat f_int b) |
55+
Loc' (p, l) => Loc (f_nat p, f_nat l) |
56+
v Lta' x => Lta (f_nat v, f_int x) |
57+
v Lea' x => Lea (f_nat v, f_int x) |
58+
v Eq' x => Eq (f_nat v, f_int x) |
59+
v Ge' x => Ge (f_nat v, f_int x) |
60+
v Gt' x => Gt (f_nat v, f_int x)
61+
62+
val to_int = Int_of_integer o IntInf.fromInt
63+
val to_nat = nat_of_integer o IntInf.fromInt
64+
val nat_of_int = nat_of_integer o integer_of_int
65+
66+
67+
(*** Parsing ***)
68+
open Scan_More;
69+
70+
fun scan_pairc_int x = scan_pairc [scan_int, scan_int] x
71+
val scan_acconstraint_lt = scan_pairc_int "LTa" (op LTa)
72+
val scan_acconstraint_le = scan_pairc_int "LEa" (op LEa)
73+
val scan_acconstraint_eq = scan_pairc_int "EQa" (op EQa)
74+
val scan_acconstraint_ge = scan_pairc_int "GE" (op GE)
75+
val scan_acconstraint_gt = scan_pairc_int "GT" (op GT)
76+
val scan_acconstraint = Scan.first [
77+
scan_acconstraint_lt,
78+
scan_acconstraint_le,
79+
scan_acconstraint_eq,
80+
scan_acconstraint_ge,
81+
scan_acconstraint_gt
82+
]
83+
84+
fun scan_infix_pairc_int x = scan_infix_pairc scan_int scan_int x;
85+
86+
fun scan_parens lparen rparen inner =
87+
op $$ lparen |-- scan_whitespace |-- inner --| scan_whitespace --| op $$ rparen
88+
89+
val scan_bexp_elem = Scan.first [
90+
scan_pairc_int "Loc'" (op Loc'),
91+
scan_pairc_int "Lea''" (op Lea'),
92+
scan_pairc_int "Eq'" (op Eq'),
93+
scan_pairc_int "Lta'" (op Lta'),
94+
scan_pairc_int "Ge'" (op Ge'),
95+
scan_pairc_int "Gt'" (op Gt')
96+
]
97+
fun scan_bexp xs =
98+
let
99+
val scan_parens = scan_parens "(" ")"
100+
fun scan_7 xs =
101+
xs |>
102+
(
103+
scan_infix_pairc scan_6 scan_7 "Imply'" op Imply' ||
104+
scan_infix_pairc scan_6 scan_7 "Or'" op Or' ||
105+
scan_6
106+
)
107+
and scan_6 xs =
108+
xs |> (scan_infix_pairc scan_0 scan_6 "And'" op And' || scan_0)
109+
and scan_inner_bexp xs = xs |> scan_parens scan_7
110+
and scan_prefix sep constr =
111+
Scan.this_string sep -- scan_whitespace |-- scan_inner_bexp >> constr
112+
and scan_0 xs =
113+
xs |>
114+
(
115+
scan_prefix "Not'" op Not' ||
116+
scan_bexp_elem ||
117+
scan_inner_bexp
118+
)
119+
in
120+
scan_7 xs
121+
end
122+
123+
val scan_singlec_int = scan_singlec scan_int
124+
125+
val scan_act = Scan.first [
126+
scan_singlec_int "In" op In,
127+
scan_singlec_int "Out" op Out,
128+
scan_singlec_int "Sil" op Sil
129+
]
130+
131+
val scan_bool =
132+
Scan.this_string "true" >> K true || Scan.this_string "false" >> K false
133+
134+
val instr_nullaries = [
135+
("ADD'", op ADD'),
136+
("NOT'", op NOT'),
137+
("AND'", op AND'),
138+
("LT'", op LT'),
139+
("LE'", op LE'),
140+
("EQ'", op EQ'),
141+
("COPY'", op COPY'),
142+
("CALL'", op CALL'),
143+
("RETURN'", op RETURN'),
144+
("HALT'", op HALT'),
145+
("POP'", op POP')
146+
]
147+
val scan_nullary_instr = Scan.first (map (uncurry scan_nullary) instr_nullaries)
148+
val scan_instr = scan_nullary_instr ||
149+
Scan.first [
150+
scan_pairc_int "STOREI'" op STOREI',
151+
scan_pairc_int "STOREC'" op STOREC',
152+
scan_singlec scan_int "JMPZ'" op JMPZ',
153+
scan_singlec scan_int "LID'" op LID',
154+
scan_singlec scan_int "PUSH'" op PUSH',
155+
scan_singlec scan_bool "SETF'" op SETF'
156+
]
157+
val scan_instrc =
158+
scan_singlec scan_nullary_instr "INSTR'" op INSTR' ||
159+
scan_singlec (scan_parens "(" ")" scan_instr) "INSTR'" op INSTR' ||
160+
scan_singlec (scan_parens "(" ")" scan_acconstraint) "CEXP'" op CEXP'
161+
162+
fun scan_option p = scan_nullary "NONE" NONE || scan_singlec p "SOME" SOME
163+
164+
fun scan_quadruple' (p1, p2, p3, p4) =
165+
scan_parens "(" ")" (
166+
(p1 --| op $$ "," --| scan_whitespace) --
167+
(p2 --| op $$ "," --| scan_whitespace) --
168+
(p3 --| op $$ "," --| scan_whitespace) --
169+
p4 >> (fn (((a, b), c), d) => (a, b, c, d))
170+
)
171+
val scan_invariant = scan_list (scan_list (scan_list scan_acconstraint))
172+
val scan_trans =
173+
scan_quadruple' (scan_int, scan_act, scan_int, scan_int) |>
174+
scan_list |>
175+
scan_list |>
176+
scan_list
177+
val scan_prog = scan_parens "(" ")" scan_instrc |> scan_option |> scan_list
178+
(* XXX Why do we need this renewed fixity declaration? *)
179+
val scan_all =
180+
scan_int --- (* p *)
181+
scan_int --- (* m *)
182+
scan_list scan_int --- (* k *)
183+
scan_int --- (* max_steps *)
184+
scan_invariant --- (* inv *)
185+
scan_trans --- (* trans *)
186+
scan_prog --- (* prog *)
187+
scan_bexp --- (* query *)
188+
scan_list (scan_pair [scan_int, scan_int]) --- (* bounds *)
189+
(scan_int |> scan_list |> scan_list) --- (* pred *)
190+
scan_list scan_int --- (* s *)
191+
scan_int (* na *)
192+
(* XXX Can we end with EOF or EOS here? *)
193+
194+
195+
(*** Printing utilites ***)
196+
fun println s = print (s ^ "\n")
197+
198+
fun list_to_string f = (fn x => "[" ^ x ^ "]") o String.concatWith ", " o map f;
199+
200+
fun print_result NONE = println("Invalid input\n")
201+
| print_result (SOME REACHABLE) = println("Property is not satisfied\n")
202+
| print_result (SOME UNREACHABLE) = println("Property is not satisfied\n")
203+
| print_result (SOME INIT_INV_ERR) =
204+
println("The invariant of the initial state is not fulfilled initially\n")
205+
206+
207+
(*** Wrapping up the checker ***)
208+
fun check_and_verify2 p m ignore_k max_steps inv trans prog query bounds pred s na () =
209+
let
210+
val _ = debug_level := 1
211+
212+
val map_constraint = map (map_acconstraint to_nat to_int);
213+
val inv = map (map map_constraint) inv;
214+
val trans =
215+
map (map (map (fn (g, a, r, l) => (to_nat g, (map_act to_nat a, (to_nat r, to_nat l)))))) trans;
216+
val prog = map (map_option (map_instrc to_nat to_int to_int)) prog
217+
val query = map_bexp to_nat to_int query
218+
val bounds = map (fn (a, b) => (to_int a, to_int b)) bounds
219+
val pred = map (map to_nat) pred
220+
val s = map to_int s
221+
val p = to_nat p
222+
val m = to_nat m
223+
val max_steps = to_nat max_steps
224+
val na = to_nat na;
225+
val _ = if !debug_level >= 1 then println("Now calculating ceiling") else ();
226+
val k = k p m max_steps inv trans prog;
227+
val k = map (map (map nat_of_int)) k;
228+
val _ = if !debug_level >= 1 then println("Finished calculating ceiling") else ();
229+
val _ =
230+
if !debug_level >= 2 then
231+
println (
232+
"\n"
233+
^ list_to_string (list_to_string (list_to_string (IntInf.toString o integer_of_nat))) k
234+
^ "\n"
235+
)
236+
else ()
237+
238+
val test1 = uPPAAL_Reachability_Problem_precompiled_start_state
239+
p m max_steps inv trans prog bounds pred s
240+
val _ = if !debug_level >= 1 then println ("Test 1: " ^ (if test1 then "Passed" else "Failed")) else ()
241+
val test1a = uPPAAL_Reachability_Problem_precompiled p m inv pred trans prog
242+
val _ = if !debug_level >= 1 then println ("Test 1a: " ^ (if test1a then "Passed" else "Failed")) else ()
243+
val test1aa = check_pre p m inv pred trans prog
244+
val _ = if !debug_level >= 1 then println ("Test 1aa: " ^ (if test1aa then "Passed" else "Failed")) else ()
245+
(*
246+
val b = equal_nata (size_list inv) p andalso equal_nata (size_list pred) p andalso
247+
equal_nata (size_list trans) p
248+
val c = (all_interval_nat
249+
(fn i =>
250+
equal_nata (size_list (nth pred i))
251+
(size_list (nth trans i)) andalso
252+
equal_nata (size_list (nth inv i)) (size_list (nth trans i))) zero_nat p)
253+
val d = list_all
254+
(fn t =>
255+
list_all
256+
(list_all (fn (_, (_, (_, l))) => less_nat l (size_list t))) t)
257+
trans
258+
val e = equal_nata (size_list k) (plus_nat m one_nat) andalso
259+
less_nat zero_nat p andalso less_nat zero_nat m
260+
val f = all_interval_nat (fn i => not (null (nth trans i))) zero_nat p
261+
val g = all_interval_nat
262+
(fn q => not (null (nth (nth trans q) zero_nat)))
263+
zero_nat p
264+
val h = equal_nata (nth k zero_nat) zero_nat
265+
val i = ball (clkp_set inv prog) (fn (_, a) => less_eq_int zero_inta a)
266+
val j = eq_set (card_UNIV_nat, equal_nat) (clk_set inv prog) (Set (upt one_nat (suc m)))
267+
val test1aa1 = check_resets prog andalso b andalso c andalso d andalso e andalso f andalso g
268+
andalso h andalso i andalso j
269+
val _ = println ("Test 1aa1: " ^ (if test1aa1 then "Passed" else "Failed"))
270+
*)
271+
val test1ab = check_ceiling p m max_steps inv trans prog k;
272+
val _ = if !debug_level >= 1 then println ("Test 1ab: " ^ (if test1ab then "Passed" else "Failed")) else ()
273+
val test1b =
274+
uPPAAL_Reachability_Problem_precompiled_start_state_axioms p max_steps trans
275+
prog bounds pred s;
276+
val _ = if !debug_level >= 1 then println ("Test 1b: " ^ (if test1b then "Passed" else "Failed")) else ()
277+
val init_pred_check = init_pred_check p prog max_steps pred s;
278+
val _ = if !debug_level >= 1 then println ("Init pred: " ^ (if init_pred_check then "Passed" else "Failed")) else ()
279+
val bounded_check = bounded_int bounds s
280+
val _ = println ("Boundedness check: " ^ (if bounded_check then "Passed" else "Failed"))
281+
val indep_1 = time_indep_check1 pred prog max_steps
282+
val _ = if !debug_level >= 1 then println ("Time independence check 1: " ^ (if indep_1 then "Passed" else "Failed")) else ()
283+
val indep_2 = time_indep_check2 trans prog max_steps
284+
val _ = if !debug_level >= 1 then println ("Time independence check 2: " ^ (if indep_1 then "Passed" else "Failed")) else ()
285+
val d = conjunction_check2 trans prog max_steps
286+
val _ = if !debug_level >= 1 then println ("Conjunction check: " ^ (if d then "Passed" else "Failed")) else ()
287+
(*
288+
val test2 = uPPAAL_Reachability_Problem_precompiled_axioms trans na
289+
val _ = println ("Test 2: " ^ (if test2 then "Passed" else "Failed"))
290+
*)
291+
val t = Time.now ()
292+
val result = Reachability_Checker.check_and_verify p m k max_steps inv trans prog query bounds pred s na ()
293+
val t = Time.- (Time.now (), t)
294+
val _ = println("Internal time for precondition check + actual checking: " ^ Time.toString t)
295+
val _ = println("")
296+
val _ = println("# additions on DBM entries:" ^ Int.toString (!cnt))
297+
val _ = println("# states added to wait list:" ^ Int.toString (!cnt2))
298+
val _ = println("# states added to passed list:" ^ Int.toString (!cnt3))
299+
val _ = println("")
300+
in
301+
print_result result
302+
end;
303+
304+
fun check_and_verify_parse input =
305+
let
306+
val (result, _) = scan_all input
307+
handle x => (println "Parse error"; raise x)
308+
val (result, na) = result
309+
val (result, s) = result
310+
val (result, pred) = result
311+
val (result, bounds) = result
312+
val (result, query) = result
313+
val (result, prog) = result
314+
val (result, trans) = result
315+
val (result, inv) = result
316+
val (result, max_steps) = result
317+
val (result, ignore_k) = result
318+
val (result, m) = result
319+
val p = result
320+
in
321+
check_and_verify2 p m ignore_k max_steps inv trans prog query bounds pred s na
322+
end;
323+
324+
fun read_lines stream =
325+
let
326+
val input = TextIO.inputLine stream
327+
handle Size => (println "Input line too long!"; raise Size)
328+
in
329+
case input of
330+
NONE => ""
331+
| SOME input => input ^ read_lines stream
332+
end
333+
334+
fun check_and_verify_from_stream stream =
335+
let
336+
val input = read_lines stream
337+
in
338+
if input = ""
339+
then (println "Failed to read line from input!"; fn () => ())
340+
(* We append a space to terminate the input for the parser *)
341+
else input ^ " " |> explode_string |> check_and_verify_parse
342+
end;

‎ML/Mlton_Main.sml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
val main = check_and_verify_from_stream (TextIO.stdIn)
2+
val _ = if MLton.isMLton then main() else ()

‎ML/Scan_More.ML

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
infix 5 ---;
2+
3+
structure Scan_More =
4+
struct
5+
6+
(** Copied from Mlton/sml90 to achieve compatiblity with Isabelle/ML **)
7+
exception Ord
8+
fun ord s =
9+
if String.size s = 0
10+
then raise Ord
11+
else Char.ord(String.sub(s, 0))
12+
13+
(** Additional parsers to read ints, lists, and datatype constructor terms **)
14+
val explode_string = map Char.toString o String.explode;
15+
val scan_neg = op $$ "~" >> K (~1);
16+
val scan_nat = Scan.many1 (fn x => ord "0" <= ord x andalso ord x <= ord "9") >> (the o Int.fromString o String.concat);
17+
val scan_int = Scan.optional scan_neg 1 -- scan_nat >> op *;
18+
val scan_whitespace = Scan.many (fn x => ord x = ord " ");
19+
fun (p1 --- p2) = (p1 --| scan_whitespace -- p2)
20+
fun scan_collection lparen rparen sep (item_parser : (string list -> 'a * string list)) =
21+
op $$ lparen |--
22+
(
23+
(item_parser -- Scan.repeat (op $$ sep --- item_parser >> snd) >> op ::) ||
24+
Scan.succeed []
25+
)
26+
--| op $$ rparen;
27+
fun scan_list item_parser = scan_collection "[" "]" "," item_parser;
28+
fun scan_tuple item_parser = scan_collection "(" ")" "," item_parser;
29+
fun scan_collection' lparen rparen sep item_parsers =
30+
let
31+
fun scan_inner [] = Scan.succeed []
32+
| scan_inner [p] = p >> (fn x => [x])
33+
| scan_inner (p :: ps) =
34+
(p -- op $$ sep -- scan_whitespace >> (fst o fst)) -- scan_inner ps >> op ::
35+
in op $$ lparen -- scan_inner item_parsers -- op $$ rparen >> (snd o fst) end
36+
fun scan_tuple' ps = scan_collection' "(" ")" "," ps;
37+
fun scan_pair ps = scan_tuple' ps >> (fn [a,b] => (a,b))
38+
fun scan_triple ps = scan_tuple' ps >> (fn [a,b,c] => (a,b,c))
39+
fun scan_quadruple ps = scan_tuple' ps >> (fn [a,b,c,d] => (a,b,c,d))
40+
fun scan_pairc ps head constr =
41+
Scan.this_string head -- scan_whitespace |-- scan_pair ps >> constr
42+
fun scan_singlec p head constr =
43+
Scan.this_string head -- scan_whitespace |-- p >> constr
44+
fun scan_nullary head constr =
45+
Scan.this_string head >> K constr
46+
fun scan_infix_pair p1 p2 sep =
47+
p1 --| (scan_whitespace -- Scan.this_string sep -- scan_whitespace) -- p2
48+
fun scan_infix_pairc p1 p2 sep constr =
49+
scan_infix_pair p1 p2 sep >> constr
50+
51+
end;

0 commit comments

Comments
 (0)