1(* -*-sml-*- *) 2(*****************************************************************************) 3(* Executing f abort b *) 4(* Not for compiling. *) 5(*****************************************************************************) 6 7loadPath := "../official-semantics" :: "../regexp" :: !loadPath; 8app 9 load 10 ["bossLib","metisLib","intLib","stringLib","pred_setLib", 11 "regexpLib","ExecuteSemanticsTheory","PropertiesTheory"]; 12 13quietdec := true; 14open bossLib metisLib intLib stringLib rich_listTheory 15open regexpLib FinitePSLPathTheory UnclockedSemanticsTheory 16 PropertiesTheory ExecuteSemanticsTheory; 17quietdec := false; 18 19(****************************************************************************** 20* Set the trace level of the regular expression library: 21* 0: silent 22* 1: 1 character (either - or +) for each list element processed 23* 2: matches as they are discovered 24* 3: transitions as they are calculated 25* 4: internal state of the automata 26******************************************************************************) 27set_trace "regexpTools" 1; 28 29(****************************************************************************** 30* Set default parsing to natural numbers rather than integers 31******************************************************************************) 32val _ = intLib.deprecate_int(); 33 34(****************************************************************************** 35* Version of Define that doesn't add to the EVAL compset 36******************************************************************************) 37val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 38 39(****************************************************************************** 40* For simplification during symbolic evaluation of Sugar2 formulas 41******************************************************************************) 42 43val EXISTS_COND = prove 44 (``!p c a b. 45 EXISTS p (if c then a else b) = if c then EXISTS p a else EXISTS p b``, 46 RW_TAC std_ss []); 47 48val COND_SIMP = prove 49 (``!c a b. 50 (COND c a F = c /\ a) /\ (COND c a T = ~c \/ a) /\ 51 (COND c T b = c \/ b) /\ (COND c F b = ~c /\ b)``, 52 RW_TAC std_ss [IMP_DISJ_THM]); 53 54(****************************************************************************** 55* Evaluating Sugar2 formulas 56******************************************************************************) 57val _ = computeLib.add_funs 58 ([pred_setTheory.IN_INSERT, 59 pred_setTheory.NOT_IN_EMPTY, 60 EXISTS_COND, 61 COND_SIMP, 62 PSLPathTheory.SEL_REC_AUX, 63 UF_SEM_F_UNTIL_REC, 64 B_SEM, 65 EVAL_US_SEM, 66 EVAL_UF_SEM_F_SUFFIX_IMP, 67 UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP, 68 S_CLOCK_COMP_ELIM, 69 F_TRUE_CLOCK_COMP_ELIM, 70 DECIDE ``SUC n > 0 = T``]); 71 72 73(****************************************************************************** 74* f1 before f2 = [not f2 W (f1 & not f2)] 75******************************************************************************) 76val F_BEFORE_def = 77 Define 78 `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`; 79 80(****************************************************************************** 81* Make ";;" into an infix for S_CAT 82******************************************************************************) 83val _ = set_fixity ";;" (Infixl 500); 84val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`; 85 86(****************************************************************************** 87* Make "->" into an infix for F_IMPLIES 88******************************************************************************) 89val _ = set_fixity "->" (Infixl 600); 90val F_IMPLIES_IX_def = xDefine "F_IMPLIES_IX" `$-> f1 f2 = F_IMPLIES(f1,f2)`; 91 92(****************************************************************************** 93* Make "until" into an infix for F_W 94******************************************************************************) 95val _ = set_fixity "until" (Infixl 440); 96val until_IX_def = xDefine "until_IX" `$until f1 f2 = F_W(f1,f2)`; 97 98(****************************************************************************** 99* Make "abort" into an infix for F_ABORT 100******************************************************************************) 101val _ = set_fixity "abort" (Infixl 445); 102val abort_IX_def = xDefine "abort_IX" `$abort f b = F_ABORT(f,b)`; 103 104(****************************************************************************** 105* eventually! 106******************************************************************************) 107val eventually_bang_def = Define `eventually_bang = F_F`; 108 109(****************************************************************************** 110* always 111******************************************************************************) 112val always_def = Define `always = F_G`; 113 114 115(****************************************************************************** 116* Fig. 8, page 22, from Sugar 2.0 Accellera Submission 117* 118* time 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 17 119* ------------------------------------------------------------------------- 120* start 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 121* req 0 0 0 1 1 0 0 1 1 0 0 0 1 1 0 0 122* ack 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 123* interrupt 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 124******************************************************************************) 125 126val prop_defs = 127 [Define `start = 0`, 128 Define `req = 1`, 129 Define `ack = 2`, 130 Define `interrupt = 3`]; 131 132val Fig8_def = 133 Define 134 (* 0 1 2 3 4 5 6 7 8 9 *) 135 `Fig8 = [{};{start};{start};{req};{req};{ack};{ack};{req};{req};{}; 136 (* 10 11 12 13 14 15 *) 137 {interrupt};{interrupt};{req};{req};{};{}]`; 138 139 140val UF_SEM_Fig8_abort = 141 time 142 EVAL 143 ``UF_SEM 144 (FINITE Fig8) 145 (always 146 (F_BOOL(B_PROP start) 147 -> 148 ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack))) 149 abort 150 (B_PROP interrupt))))``; 151 152val UF_SEM_Fig8_until = 153 time 154 EVAL 155 ``UF_SEM 156 (FINITE Fig8) 157 (always 158 (F_BOOL(B_PROP start) 159 -> 160 ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack))) 161 until 162 (F_BOOL(B_PROP interrupt)))))``; 163 164val F_SEM_Fig8_abort = 165 time 166 EVAL 167 ``F_SEM 168 (FINITE Fig8) 169 B_TRUE 170 (always 171 (F_BOOL(B_PROP start) 172 -> 173 ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack))) 174 abort 175 (B_PROP interrupt))))``; 176 177val F_SEM_Fig8_until = 178 time 179 EVAL 180 ``F_SEM 181 (FINITE Fig8) 182 B_TRUE 183 (always 184 (F_BOOL(B_PROP start) 185 -> 186 ((F_BOOL(B_PROP req) -> eventually_bang (F_BOOL(B_PROP ack))) 187 until 188 (F_BOOL(B_PROP interrupt)))))``; 189