Skip to content

Commit 27c0c23

Browse files
committed
write STM_sequential.agree_prop in plain function syntax
1 parent fb16595 commit 27c0c23

File tree

1 file changed

+10
-11
lines changed

1 file changed

+10
-11
lines changed

lib/STM_sequential.ml

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,16 @@ module Make (Spec: Spec) = struct
1515
(fun acc (c,r) -> Printf.sprintf "%s\n %s : %s" acc (Spec.show_cmd c) (show_res r))
1616
"" trace
1717

18-
let agree_prop =
19-
(fun cs ->
20-
assume (cmds_ok Spec.init_state cs);
21-
let sut = Spec.init_sut () in (* reset system's state *)
22-
let res = check_disagree Spec.init_state sut cs in
23-
let () = Spec.cleanup sut in
24-
match res with
25-
| None -> true
26-
| Some trace ->
27-
Test.fail_reportf " Results incompatible with model\n%s"
28-
@@ print_seq_trace trace)
18+
let agree_prop cs =
19+
assume (cmds_ok Spec.init_state cs);
20+
let sut = Spec.init_sut () in (* reset system's state *)
21+
let res = check_disagree Spec.init_state sut cs in
22+
let () = Spec.cleanup sut in
23+
match res with
24+
| None -> true
25+
| Some trace ->
26+
Test.fail_reportf " Results incompatible with model\n%s"
27+
@@ print_seq_trace trace
2928

3029
let agree_test ~count ~name =
3130
Test.make ~name ~count (arb_cmds Spec.init_state) agree_prop

0 commit comments

Comments
 (0)