1(*****************************************************************************)
2(* Examples of evaluating PSL/Sugar constructs on paths                      *)
3(* Run hol and then do "use examples;"                                       *)
4(*****************************************************************************)
5
6quietdec := true;
7loadPath := "../official-semantics"   ::
8            "../executable-semantics" ::
9            "../regexp"               :: 
10            "../parser.mosmlyacc"     :: 
11            !loadPath;
12load "ParserTools";
13open ParserTools;
14quietdec := false;
15
16(******************************************************************************
17* Random examples just to check something is working!
18******************************************************************************)
19EvalSERE "{x}{y}       |= x;y";
20EvalSERE "{p}{q}       |= p;q";
21EvalSERE "{x}{y}{p}    |= x;T;p";
22EvalSERE "{x}{y}{p}{q} |= T[*];p;T[*]";
23
24EvalFL "{x}{y,p}{q}    |= {x;y} |-> {p;q}";
25EvalFL "{x}{y,p}{q}    |= {x;y} |=> {p;q}";
26EvalFL "{x}{y}{p}{q}   |= {x;y} |-> {p;q}";
27EvalFL "{x}{y}{p}{q}   |= {x;y} |=> {p;q}";
28EvalFL "{x}{y}{p}{q}   |= {x;y;p} |-> {p;q}";
29EvalFL "{x}{y}{p}{q}   |= {x;y;T} |-> {p;q}";
30
31(******************************************************************************
32* Example 1 (LRM Version 1.0, page 45)
33*
34* time  0  1  2  3  4  5  6  7  8  9
35* ----------------------------------
36* clk   0  1  0  1  0  1  0  1  0  1
37* a     0  0  0  1  1  1  0  0  0  0
38* b     0  0  0  0  0  1  0  1  1  0
39*
40* {}{clk}{}{clk;a}{a}{clk;a;b}{}{clk;b}{b}{clk}
41*
42******************************************************************************)
43
44
45(******************************************************************************
46* Individually evaluate "a until! b@clk" on sub-paths of
47* "{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk}"
48******************************************************************************)
49EvalFL "{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= a until! b"; (* w^0 *)
50EvalFL "  {clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= a until! b"; (* w^1 *)
51EvalFL "       {}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= a until! b"; (* w^2 *)
52EvalFL "         {clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= a until! b"; (* w^3 *)
53EvalFL "                {a}{clk,a,b}{}{clk,b}{b}{clk} |= a until! b"; (* w^4 *)
54EvalFL "                   {clk,a,b}{}{clk,b}{b}{clk} |= a until! b"; (* w^5 *)
55EvalFL "                            {}{clk,b}{b}{clk} |= a until! b"; (* w^6 *)
56EvalFL "                              {clk,b}{b}{clk} |= a until! b"; (* w^7 *)
57EvalFL "                                     {b}{clk} |= a until! b"; (* w^8 *)
58EvalFL "                                        {clk} |= a until! b"; (* w^9 *)
59
60(******************************************************************************
61* Evaluate all the above with one command
62******************************************************************************)
63EvalAllFL
64 ("{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk}", "a until! b");
65
66(******************************************************************************
67* Individually evaluate "(a until! b)@clk" on sub-paths of
68* "{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk}"
69******************************************************************************)
70EvalFL "{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= (a until! b)@clk"; (* w^0 *)
71EvalFL "  {clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= (a until! b)@clk"; (* w^1 *)
72EvalFL "       {}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= (a until! b)@clk"; (* w^2 *)
73EvalFL "         {clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk} |= (a until! b)@clk"; (* w^3 *)
74EvalFL "                {a}{clk,a,b}{}{clk,b}{b}{clk} |= (a until! b)@clk"; (* w^4 *)
75EvalFL "                   {clk,a,b}{}{clk,b}{b}{clk} |= (a until! b)@clk"; (* w^5 *)
76EvalFL "                            {}{clk,b}{b}{clk} |= (a until! b)@clk"; (* w^6 *)
77EvalFL "                              {clk,b}{b}{clk} |= (a until! b)@clk"; (* w^7 *)
78EvalFL "                                     {b}{clk} |= (a until! b)@clk"; (* w^8 *)
79EvalFL "                                        {clk} |= (a until! b)@clk"; (* w^9 *)
80
81(******************************************************************************
82* Evaluate all the above with one command
83******************************************************************************)
84EvalAllFL
85 ("{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk}", "(a until! b)@clk");
86
87(******************************************************************************
88* Example 2 (LRM Version 1.0, page 45)
89*
90* time  0  1  2  3  4  5  6  7  8  9
91* ----------------------------------
92* clk1  0  1  0  1  0  1  0  1  0  1
93* a     0  0  0  1  1  1  0  0  0  0
94* b     0  0  0  0  0  1  0  1  1  0
95* c     1  0  0  0  0  1  1  0  0  0
96* clk2  1  0  0  1  0  0  1  0  0  1
97*
98*{c,clk2}{clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}
99*
100******************************************************************************)
101
102(******************************************************************************
103* Individually evaluate "c && next! (a until! b)" on sub-paths of
104* "{c,clk2}{clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}"
105******************************************************************************)
106EvalFL "{c,clk2}{clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
107\       |= c && next! (a until! b)";  (* w^0 *)
108EvalFL "        {clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
109\       |= c && next! (a until! b)";  (* w^1 *)
110EvalFL "              {}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
111\       |= c && next! (a until! b)";  (* w^2 *)
112EvalFL "                {clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
113\       |= c && next! (a until! b)";  (* w^3 *)
114EvalFL "                             {a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
115\       |= c && next! (a until! b)";  (* w^4 *)
116EvalFL "                                {clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
117\       |= c && next! (a until! b)";  (* w^5 *)
118EvalFL "                                            {c,clk2}{clk1,b}{b}{clk1,clk2}\
119\       |= c && next! (a until! b)";  (* w^6 *)
120EvalFL "                                                    {clk1,b}{b}{clk1,clk2}\
121\       |= c && next! (a until! b)";  (* w^7 *)
122EvalFL "                                                            {b}{clk1,clk2}\
123\       |= c && next! (a until! b)";  (* w^8 *)
124EvalFL "                                                               {clk1,clk2}\
125\       |= c && next! (a until! b)";  (* w^9 *)
126
127(******************************************************************************
128* Evaluate all the above with one command
129******************************************************************************)
130EvalAllFL
131 ("{c,clk2}{clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}",
132  "c && next! (a until! b)");
133
134(******************************************************************************
135* Individually evaluate "(c && next! (a until! b))@clk1" on sub-paths of
136* "{c,clk2}{clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}"
137******************************************************************************)
138EvalFL "{c,clk2}{clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
139\       |= (c && next! (a until! b))@clk1";  (* w^0 *)
140EvalFL "        {clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
141\       |= (c && next! (a until! b))@clk1";  (* w^1 *)
142EvalFL "              {}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
143\       |= (c && next! (a until! b))@clk1";  (* w^2 *)
144EvalFL "                {clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
145\       |= (c && next! (a until! b))@clk1";  (* w^3 *)
146EvalFL "                             {a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
147\       |= (c && next! (a until! b))@clk1";  (* w^4 *)
148EvalFL "                                {clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}\
149\       |= (c && next! (a until! b))@clk1";  (* w^5 *)
150EvalFL "                                            {c,clk2}{clk1,b}{b}{clk1,clk2}\
151\       |= (c && next! (a until! b))@clk1";  (* w^6 *)
152EvalFL "                                                    {clk1,b}{b}{clk1,clk2}\
153\       |= (c && next! (a until! b))@clk1";  (* w^7 *)
154EvalFL "                                                            {b}{clk1,clk2}\
155\       |= (c && next! (a until! b))@clk1";  (* w^8 *)
156EvalFL "                                                               {clk1,clk2}\
157\       |= (c && next! (a until! b))@clk1";  (* w^9 *)
158
159(******************************************************************************
160* Evaluate all the above with one command
161******************************************************************************)
162EvalAllFL
163 ("{c,clk2}{clk1}{}{clk1,a,clk2}{a}{clk1,a,b,c}{c,clk2}{clk1,b}{b}{clk1,clk2}",
164  "(c && next! (a until! b))@clk1");
165
166(******************************************************************************
167* Example 1 (LRM Version 1.0, page 33)
168*
169* time  0  1  2  3  4
170* -------------------
171* clk   0  1  0  1  0
172* a     0  1  1  0  0
173* b     0  0  0  1  0
174*
175* {}{clk,a}{a}{clk,b}{b}
176******************************************************************************)
177
178(******************************************************************************
179* Evaluate SEREs on all sub-intervals of given interval
180******************************************************************************)
181EvalAllSERE
182 ("{}{clk,a}{a}{clk,b}{b}",
183  "{a;b}");
184
185EvalAllSERE
186 ("{}{clk,a}{a}{clk,b}{b}",
187  "{a;b}@clk");
188
189(******************************************************************************
190* Example 2 (LRM Version 1.0, page 33)
191*
192* time  0  1  2  3  4  5  6  7
193* ----------------------------
194* clk1  0  1  0  1  0  1  0  1
195* a     0  1  1  0  0  0  0  0
196* b     0  0  0  1  0  0  0  0
197* c     0  0  0  0  1  0  1  0
198* clk2  1  0  0  1  0  0  1  0
199*
200* {clk2}{clk1,a}{a}{clk1,b,clk2}{c}{clk1}{c,clk2}{clk1}
201******************************************************************************)
202
203(******************************************************************************
204* Evaluate SEREs on all sub-intervals of given interval
205******************************************************************************)
206EvalAllSERE
207 ("{clk2}{clk1,a}{a}{clk1,b,clk2}{c}{clk1}{c,clk2}{clk1}",
208  "{{a;b};c}");
209
210EvalAllSERE
211 ("{clk2}{clk1,a}{a}{clk1,b,clk2}{c}{clk1}{c,clk2}{clk1}",
212  "{{a;b}@clk1;c}@clk2");
213
214EvalAllSERE
215 ("{clk2}{clk1,a}{a}{clk1,b,clk2}{c}{clk1}{c,clk2}{clk1}",
216  "{{a;b};c}@clk1");
217
218EvalAllSERE
219 ("{clk2}{clk1,a}{a}{clk1,b,clk2}{c}{clk1}{c,clk2}{clk1}",
220  "{{a;b};c}@clk2");
221
222
223