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