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