-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathexamples_gen.v
166 lines (133 loc) · 5 KB
/
examples_gen.v
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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
Require Import bt basic.
Require Import String.
Open Scope string_scope.
(* Some simple examples of BTs *)
Inductive my_skills :=
sk1 | sk2 | sk3 | sk4.
Definition my_names (x: my_skills) :=
match x with
| sk1 => "goto_kitchen"
| sk2 => "find_bottle"
| sk3 => "fetch_bottle"
| sk4 => "ask_help"
end.
Module ex_skills.
Definition skillSet := my_skills.
Definition skillName := my_names.
End ex_skills.
Module my_bt := BT_gen_semantics ex_skills.
Import my_bt.
Definition ex1 := (Skill sk1). (* a skill *)
Definition ex2 := (* a ternary sequence *)
(Node Sequence "seq3" (Add (Skill sk1)
(Add (Skill sk2)
(Child (Skill sk3))))).
Definition ex3 := (* a binary fallback *)
(Node Fallback "bf" (Add (Skill sk1)
(Child (Skill sk2)))).
Definition ex4 := (* a ternary parallel *)
(Node (Parallel 1) "par" (Add (Skill sk1)
(Add (Skill sk2)
(Child (Skill sk3))))).
Definition ex5 := (* ill-formed parallel *)
(Node (Parallel 3) "nopar" (Add (Skill sk1)
(Child (Skill sk2)))).
Definition sc1 := (* a BT similar to the one from scenario 1 *)
(Node Fallback "do_with_help"
(Add (Node Sequence "go_find_fetch" (Add (Skill sk1)
(Add (Skill sk2)
(Child (Skill sk3)))))
(Child (Skill sk4)))).
Compute sklist sc1.
(* mangled version of sc1, to test normalization *)
Definition sc1m :=
(Node Fallback "do_with_help"
(Add (Node Sequence "go_find_fetch"
(Add (Node Fallback "useless" (Child (Skill sk1)))
(Add (Skill sk2)
(Child (Node Sequence "useless2" (Child (Skill sk3)))))))
(Child (Skill sk4)))).
Compute normalize sc1m.
(* execution examples *)
Compute (tick ex4).
(* current implementation will happily run on this ill-formed BT... *)
Compute (tick ex5).
Compute (tick sc1 (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Fail
| sk4 => Succ
end)).
(* Examples with stream semantics *)
Require Import Streams stream.
Module alt_sem := BT_gen_str_sem ex_skills.
Import alt_sem.
CoFixpoint all_ok: Stream skills_input :=
Cons (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Succ
| sk4 => Succ
end)
all_ok.
Definition s1 :=
Cons (fun s: my_skills =>
match s with
| sk1 => Runn
| sk2 => Fail
| sk3 => Fail
| sk4 => Succ
end)
(Cons (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Fail
| sk3 => Fail
| sk4 => Succ
end)
(Cons (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Runn
| sk3 => Fail
| sk4 => Succ
end)
(Cons (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Fail
| sk4 => Succ
end)
(Cons (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Runn
| sk4 => Succ
end)
(Cons (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Succ
| sk4 => Succ
end)
all_ok))))).
Compute reptick (Node Sequence "prova" (Add (Skill sk1)
(Add (Skill sk2)
(Child (Skill sk3)))))
3 s1.
(* SMV specifications *)
Require Import spec_extr bt2spec.
Module spec := BT_gen_spec ex_skills.
Import spec.
Definition uc1 :=
(Node Fallback "do_with_help"
(Add (Node Sequence "go_find_fetch" (Add (Skill sk1)
(Add (Skill sk2)
(Child (Skill sk3)))))
(Child (Skill sk4)))).
Compute translate_spec (make_spec uc1).