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