-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathMain-testing.uci
99 lines (91 loc) · 2.23 KB
/
Main-testing.uci
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
(* testing Main *)
(* see more detailed tests of Comp in Comp-testing.uci *)
load Main.
functionality Main.MainReal(Comp.CompReal).
prover [""]. (* we'll do without SMT solvers *)
var pt : port.
assumption envport_pt : envport func pt.
(* first experiment with real world *)
real.
send [email protected]$func.
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 4))@Comp.CompAdv.Pt1.resume$(func ++ [1]).
run.
send ((adv, 5))@Comp.CompAdv.Pt2.resume$(func ++ [1]).
run.
send ((adv, 6))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 1]).
run.
send ((adv, 7))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 2]).
run.
assert msg_out
((func, 1))@Main.Dir.D.ok@pt
ctrl_env.
finish.
(* first experiment with ideal world *)
ideal.
send [email protected]$func.
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 4))@Comp.CompAdv.Pt1.resume$(func ++ [1]).
run.
send ((adv, 5))@Comp.CompAdv.Pt2.resume$(func ++ [1]).
run.
send ((adv, 6))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 1]).
run.
send ((adv, 7))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 2]).
run.
assert msg_out
((func, 1))@Main.Dir.D.ok@pt
ctrl_env.
finish.
(* second experiment with real world *)
real.
send [email protected]$func.
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 4))@Comp.CompAdv.Pt1.resume$(func ++ [1]).
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 6))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 1]).
run.
send ((adv, 5))@Comp.CompAdv.Pt2.resume$(func ++ [1]).
run.
send ((adv, 7))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 2]).
run.
send ((adv, 5))@Comp.CompAdv.Pt2.resume$(func ++ [1]).
run.
assert msg_out
((func, 1))@Main.Dir.D.ok@pt
ctrl_env.
finish.
(* second experiment with ideal world *)
ideal.
send [email protected]$func.
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 4))@Comp.CompAdv.Pt1.resume$(func ++ [1]).
run.
send ((adv, 2))@Main.Adv.A.resume$func.
run.
send ((adv, 6))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 1]).
run.
send ((adv, 5))@Comp.CompAdv.Pt2.resume$(func ++ [1]).
run.
send ((adv, 7))@FwdSched.FwdSchedAdv.ok$(func ++ [1; 2]).
run.
send ((adv, 5))@Comp.CompAdv.Pt2.resume$(func ++ [1]).
run.
assert msg_out
((func, 1))@Main.Dir.D.ok@pt
ctrl_env.
finish.