-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathexamples_bin.v
152 lines (123 loc) · 4.06 KB
/
examples_bin.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
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_bin_bt_with_sem := BT_bin_semantics ex_skills.
Import my_bin_bt_with_sem.
Definition sc1 :=
(Node Fallback "do_with_help"
(Node Sequence "go_and_fetch" (Skill sk1)
(Node Sequence "find_and_fetch" (Skill sk2) (Skill sk3)))
(Skill sk4)).
(* execution examples *)
Compute (tick sc1 (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Fail
| sk4 => Succ
end)).
Compute (tick sc1 (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Fail
| sk4 => Fail
end)).
(* Examples with stream semantics *)
Require Import Streams stream.
Module alt_sem := BT_bin_str_sem ex_skills.
Import alt_sem.
CoFixpoint EverythingFails: Stream skills_input :=
Cons (fun s: my_skills =>
match s with
| sk1 => Fail
| sk2 => Fail
| sk3 => Fail
| sk4 => Fail
end)
EverythingFails.
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 => Fail
| sk4 => Succ
end)
(Cons (fun s: my_skills =>
match s with
| sk1 => Succ
| sk2 => Succ
| sk3 => Fail
| sk4 => Succ
end)
all_ok))))).
Compute reptick (Node Fallback "prova" (Skill sk2) (Skill sk3))
3 s1.
Compute tick2 (Node Sequence "s1" (Skill sk1)
(Node Sequence "s2" (Skill sk2) (Skill sk3)))
s1.
Compute reptick (Node Sequence "s1" (Skill sk1)
(Node Sequence "s2" (Skill sk2) (Skill sk3)))
3 s1.
(* SMV specifications *)
Require Import spec_extr bt2spec.
Module spec := BT_bin_spec ex_skills.
Import spec.
Definition uc1 :=
(Node Fallback "do_with_help"
(Node Sequence "go_and_fetch" (Skill sk1)
(Node Sequence "find_and_fetch" (Skill sk2) (Skill sk3)))
(Skill sk4)).
Compute translate_spec (make_spec uc1).