1(*
2quietdec := true;
3
4val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/");
5loadPath := (concat home_dir "src/deep_embeddings") ::
6            (concat home_dir "src/translations") ::
7            (concat home_dir "src/model_check") ::
8            (concat home_dir "src/tools") ::
9            (concat hol_dir "examples/PSL/path") ::
10            (concat hol_dir "examples/PSL/1.1/official-semantics") :: !loadPath;
11
12map load
13 ["full_ltlTheory", "arithmeticTheory", "automaton_formulaTheory", "xprop_logicTheory", "prop_logicTheory",
14  "infinite_pathTheory", "tuerk_tacticsLib", "symbolic_semi_automatonTheory", "listTheory", "pred_setTheory",
15  "temporal_deep_mixedTheory", "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "pairTheory",
16  "ltl_to_automaton_formulaTheory",
17  "numLib", "listLib", "translationsLib", "rltlTheory",
18  "rltl_to_ltlTheory", "psl_to_rltlTheory", "UnclockedSemanticsTheory",
19  "SyntacticSugarTheory", "congLib", "temporal_deep_simplificationsLib",
20  "modelCheckLib", "ibmLib"];
21*)
22
23open HolKernel boolLib bossLib  full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory prop_logicTheory
24     infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory
25     temporal_deep_mixedTheory pred_setTheory rich_listTheory set_lemmataTheory pairTheory rltlTheory
26     ltl_to_automaton_formulaTheory numLib listLib translationsLib rltl_to_ltlTheory psl_to_rltlTheory UnclockedSemanticsTheory
27     SyntacticSugarTheory congLib temporal_deep_simplificationsLib
28     modelCheckLib ibmLib;
29
30
31(*
32show_assums := false;
33show_assums := true;
34show_types := true;
35show_types := false;
36quietdec := false;
37*)
38
39(*
40Inputs:
41
420 aa
431 bb
442 cc
453 dd
46
47
48assert G (aa -> next_event(bb)(cc before dd));
49*)
50
51val psl = ``
52F_ALWAYS (F_IMPLIES(F_STRONG_BOOL (B_PROP (0:num)),
53                    F_STRONG_NEXT_EVENT (B_PROP 1,
54                                         F_STRONG_BEFORE (
55                                            F_STRONG_BOOL (B_PROP 2),
56                                            F_STRONG_BOOL (B_PROP 3)
57                                         ))
58                   )
59         )``;
60
61
62
63(*
64MODULE main
65# 2 envs1
66  VAR aa: boolean;
67# 2 envs1
68  VAR bb: boolean;
69# 2 envs1
70  VAR cc: boolean;
71# 2 envs1
72  VAR dd: boolean;
73  VAR sat_x1: 0..11;
74  ASSIGN init(sat_x1) := ((11 union 8) union 2) union 1;
75  ASSIGN next(sat_x1) := case
76    sat_x1 = 1: ((1 union 11) union 8) union 2;
77    (sat_x1 = 2) & (!spec_define_13): (3 union 7) union 4;
78    (sat_x1 = 3) & spec_define_10: (3 union 7) union 4;
79    (sat_x1 = 4) & (bb & ((!((!dd) & cc)) & (!dd))): 5 union 6;
80    (sat_x1 = 5) & ((!((!dd) & cc)) & (!dd)): 5 union 6;
81    (sat_x1 = 6) & ((!((!dd) & cc)) & dd): 0;
82    (sat_x1 = 7) & (bb & ((!((!dd) & cc)) & dd)): 0;
83    (sat_x1 = 8) & (aa & (bb & ((!((!dd) & cc)) & (!dd)))): 9 union 10;
84    (sat_x1 = 9) & ((!((!dd) & cc)) & (!dd)): 9 union 10;
85    1: 0;
86    esac;
87  DEFINE spec_define_13:= (!spec_define_11) | bb;
88  DEFINE spec_define_10:= (!bb);
89  DEFINE spec_define_11:= aa;
90  DEFINE spec_define_0:= (!(((sat_x1 = 6) & ((!((!dd) & cc)) & dd)) | (((sat_x1 = 7) & (bb & ((!((!dd) & cc)) & dd))) | (((sat_x1 = 10) & ((!((!dd) & cc)) & dd)) | ((sat_x1 = 11) & (aa & (bb & ((!((!dd) & cc)) & dd))))))));
91  DEFINE spec_define_1:= (!(((sat_x1 = 6) & ((!dd) & cc)) | (((sat_x1 = 7) & (bb & ((!dd) & cc))) | (((sat_x1 = 10) & ((!dd) & cc)) | ((sat_x1 = 11) & (aa & (bb & ((!dd) & cc))))))));
92  DEFINE spec_define_2:= spec_define_14;
93  DEFINE spec_define_14:= (!((!dd) & cc));
94  DEFINE spec_define_3:= spec_define_15;
95  DEFINE spec_define_15:= dd & (!((!dd) & cc));
96  DEFINE spec_define_4:= (!spec_define_10);
97  DEFINE spec_define_5:= spec_define_10;
98  DEFINE spec_define_6:= spec_define_11;
99  DEFINE spec_define_7:= spec_define_14;
100  DEFINE spec_define_8:= (!spec_define_14);
101  DEFINE spec_define_9:= (!spec_define_10);
102  DEFINE spec_define_12:= (!spec_define_11);
103  DEFINE spec_define_16:= (!spec_define_10);
104  DEFINE spec_define_17:= spec_define_10;
105  DEFINE spec_define_18:= spec_define_11;
106...
107*)
108
109val pre_A = ``symbolic_semi_automaton (INTERVAL_SET 4 7)
110
111          (P_BIGOR [X11; X8; X2; X1])
112
113          (XP_BIGCOND [
114            (XP_CURRENT X1,
115             XP_NEXT (P_BIGOR [X1; X11; X8; X2]));
116
117            (XP_CURRENT (P_AND(X2, P_NOT (P_OR (P_NOT (P_PROP 0), P_PROP 1)))),
118             XP_NEXT (P_BIGOR [X3; X7; X4]));
119
120            (XP_CURRENT (P_AND(X3, (P_NOT (P_PROP 1)))),
121             XP_NEXT (P_BIGOR [X3; X7; X4]));
122
123            (XP_CURRENT (P_AND(X4, (P_AND (P_PROP 1, P_AND(P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)),  P_NOT (P_PROP 3)))))),
124             XP_NEXT (P_BIGOR [X5; X6]));
125
126            (XP_CURRENT (P_AND(X5, (P_AND(P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)),  P_NOT (P_PROP 3))))),
127             XP_NEXT (P_BIGOR [X5; X6]));
128
129            (XP_CURRENT (P_AND(X6, (P_AND(P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)), (P_PROP 3))))),
130             XP_NEXT X0);
131
132            (XP_CURRENT (P_AND(X7, (P_AND (P_PROP 1, P_AND(P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)),  P_PROP 3))))),
133             XP_NEXT X0);
134
135            (XP_CURRENT (P_AND(X8, (P_AND (P_PROP 0, P_AND (P_PROP 1, P_AND(P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)),  P_NOT (P_PROP 3))))))),
136             XP_NEXT (P_BIGOR [X9; X10]));
137
138            (XP_CURRENT (P_AND(X9, (P_AND(P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)),  P_NOT (P_PROP 3))))),
139             XP_NEXT (P_BIGOR [X9; X10]));
140
141            (XP_TRUE,
142             XP_NEXT X0)
143          ])``
144
145(*
146SPECNEV       AG( ! (
147
148((((( sat_x1)  = (
149    6)))  & ((( !(( ! dd)  & (
150    cc)))  & ( dd)))))  |
151
152((
153
154  ((((( sat_x1)  = ( 7
155   )))  & ((( bb)  & ((( !
156   (( ! dd)  & ( cc)))  & ( dd
157   )))))))
158
159  |
160   ((
161      (((
162   (( sat_x1)  = ( 10)))  & ((( !
163   (( ! dd)  & ( cc)))  & ( dd
164   )))))  |
165
166      ((((( sat_x1)  = (
167    11)))  & ((( aa)  & (((
168    bb)  & ((( !(( ! dd)  & (
169    cc)))  & ( dd))))))
170   )))
171
172  ))
173
174
175)))
176)
177
178*)
179
180val pre_p = ``P_NOT (P_BIGOR [
181          P_AND (X6, P_AND (P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)), P_PROP (3:num)));
182
183          P_AND (X7, P_AND(P_PROP 1, P_AND (P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)), P_PROP 3)));
184
185          P_AND (X10, P_AND (P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)), P_PROP 3));
186
187          P_AND (X11, P_AND (P_PROP 0, P_AND (P_PROP 1, P_AND (P_NOT(P_AND(P_NOT (P_PROP 3), P_PROP 2)), P_PROP 3))))
188        ])``
189
190(*
191State variables
192
1934-7, binary encoding of the states, i.e.
194
195sat_x1 = 0 =  NOT 7 /\ NOT 6 /\ NOT 5 /\ NOT 4
196sat_x1 = 1 :  NOT 7 /\ NOT 6 /\ NOT 5 /\     4
197sat_x1 = 2 :  NOT 7 /\ NOT 6 /\     5 /\ NOT 4
198sat_x1 = 3 :  NOT 7 /\ NOT 6 /\     5 /\     4
199sat_x1 = 4 :  NOT 7 /\     6 /\ NOT 5 /\ NOT 4
200*)
201
202fun inst_enc s t b1 b2 b3 b4 =
203  let
204    val x1 = if (b1 = 1) then ``P_PROP (7:num)`` else ``P_NOT (P_PROP (7:num))``
205    val x2 = if (b2 = 1) then ``P_PROP (6:num)`` else ``P_NOT (P_PROP (6:num))``
206    val x3 = if (b3 = 1) then ``P_PROP (5:num)`` else ``P_NOT (P_PROP (5:num))``
207    val x4 = if (b4 = 1) then ``P_PROP (4:num)`` else ``P_NOT (P_PROP (4:num))``
208
209    val l = mk_list ([x1,x2,x3,x4], type_of x1)
210    val replace = mk_comb (``P_BIGAND:num prop_logic list -> num prop_logic``, l)
211
212    val var = mk_var (s, type_of replace);
213  in
214    subst [var |-> replace] t
215  end
216
217fun inst_all t =
218  let
219    val r = t;
220    val r = inst_enc "X0"  r 0 0 0 0;
221    val r = inst_enc "X1"  r 0 0 0 1;
222    val r = inst_enc "X2"  r 0 0 1 0;
223    val r = inst_enc "X3"  r 0 0 1 1;
224    val r = inst_enc "X4"  r 0 1 0 0;
225    val r = inst_enc "X5"  r 0 1 0 1;
226    val r = inst_enc "X6"  r 0 1 1 0;
227    val r = inst_enc "X7"  r 0 1 1 1;
228    val r = inst_enc "X8"  r 1 0 0 0;
229    val r = inst_enc "X9"  r 1 0 0 1;
230    val r = inst_enc "X10" r 1 0 1 0;
231    val r = inst_enc "X11" r 1 0 1 1;
232    val r = inst_enc "X12" r 1 1 0 0;
233    val r = inst_enc "X13" r 1 1 0 1;
234    val r = inst_enc "X14" r 1 1 1 0;
235    val r = inst_enc "X15" r 1 1 1 1;
236
237    val r_equiv_thm = SIMP_CONV list_ss [XP_BIGCOND_def, P_BIGAND_def, P_BIGOR_def,
238      XP_NEXT_THM, XP_CURRENT_THM, XP_BIGAND_def, XP_BIGOR_def] r
239    val r = rhs (concl r_equiv_thm)
240  in
241    r
242  end;
243
244
245val A = inst_all pre_A;
246val p = inst_all pre_p;
247
248
249
250val psl = ``
251F_ALWAYS (F_IMPLIES(F_WEAK_BOOL (B_PROP (0:num)),
252                    F_WEAK_NEXT_EVENT (B_PROP 1,
253                                         F_WEAK_BEFORE (
254                                            F_WEAK_BOOL (B_PROP 2),
255                                            F_WEAK_BOOL (B_PROP 3)
256                                         ))
257                   )
258         )``;
259
260
261
262
263(*
264
265
266val thm = time (model_check_ibm true A p) psl (*ca. 12 s*)
267val thm = time (model_check_ibm false A p) psl (*ca. 30 min*)
268
269val thm = time (ibm_to_ks A p) psl
270val ks = lhs (concl thm)
271val problem = rhs (concl thm)
272
273
274val file_st = TextIO.openOut("/home/tt291/Desktop/test4.smv");
275
276
277val problem_string = term_to_string problem;
278val string_list = String.fields (fn x=> (x = #"\n")) problem_string
279val _ = map (fn x => TextIO.output(file_st, "-- "^x^"\n")) string_list;
280val _ = TextIO.output(file_st, "\n\n");
281val _ = TextIO.flushOut file_st;
282
283
284val vars = fair_empty_ks2smv_string ks file_st;
285val _ = TextIO.closeOut file_st;
286
287val thm_impl = time (model_check_ibm A p) psl
288
289*)
290
291