1structure modelCheckLib :> modelCheckLib = 2struct 3 4(* 5quietdec := true; 6 7val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 8loadPath := (concat home_dir "src/deep_embeddings") :: 9 (concat home_dir "src/translations") :: 10 (concat home_dir "src/tools") :: 11 (concat hol_dir "examples/PSL/path") :: 12 (concat hol_dir "examples/PSL/1.1/official-semantics") :: !loadPath; 13 14map load 15 ["full_ltlTheory", "arithmeticTheory", "automaton_formulaTheory", "xprop_logicTheory", "prop_logicTheory", 16 "infinite_pathTheory", "tuerk_tacticsLib", "symbolic_semi_automatonTheory", "listTheory", "pred_setTheory", "pred_setSyntax", 17 "temporal_deep_mixedTheory", "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "pairTheory", 18 "ltl_to_automaton_formulaTheory", "rltl_to_ltlTheory", 19 "numLib", "listLib", "translationsLibTheory", "rltlTheory", "computeLib", 20 "congLib", "temporal_deep_simplificationsLib", "Trace", 21 "symbolic_kripke_structureTheory", "pred_setLib", "Varmap", "HOLset", "ListConv1", 22 "psl_lemmataTheory", "ProjectionTheory", "psl_to_rltlTheory", 23 "translationsLib", "temporalLib", "bdd", "ctl_starTheory"]; 24*) 25 26open HolKernel boolLib bossLib 27 full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory prop_logicTheory 28 infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory 29 temporal_deep_mixedTheory pred_setTheory rich_listTheory set_lemmataTheory pairTheory pred_setSyntax 30 ltl_to_automaton_formulaTheory numLib listLib listSyntax translationsLibTheory 31 rltl_to_ltlTheory rltlTheory computeLib congLib temporal_deep_simplificationsLib 32 Trace symbolic_kripke_structureTheory Varmap psl_lemmataTheory ProjectionTheory psl_to_rltlTheory 33 translationsLib temporalLib ctl_starTheory; 34 35(* this is Moscow ML only *) 36open bdd; 37 38(* 39show_assums := false; 40show_assums := true; 41show_types := true; 42show_types := false; 43quietdec := false; 44*) 45 46 47val model_check_temp_file = ref "smv_file.smv"; 48 49 50val _ = init 10000000 1000000; 51 52local 53 fun get_const t = 54 if (is_const t) then dest_const t else get_const (rator t) 55 56 57 (*Translates a prop_logic formula that may contain only basic operators 58 to an sml string. Thefore it uses the mapping of propositional variables 59 to numbers given by the map parameter. Additionally this map is 60 extended if new propositional variables are found.*) 61 62 exception translation2smv_exp 63 64 fun get_arg_num (map, maxindex) term = 65 let 66 val num_option = Binarymap.peek (map, term); 67 in 68 if (isSome num_option) then 69 (valOf num_option, (map, maxindex)) 70 else 71 let 72 val map = Binarymap.insert (map, term, maxindex+1); 73 in 74 (maxindex+1, (map, maxindex+1)) 75 end 76 end; 77 78 fun get_arg_var uv term = 79 let 80 val (num, uv) = get_arg_num uv term 81 val s = "x"^(int_to_string num); 82 in 83 (s, uv) 84 end; 85 86 87 fun prop_list_to_var_list uv [] = ([], uv) | 88 prop_list_to_var_list uv (e::l) = 89 let 90 val (num, uv) = get_arg_num uv e; 91 val _ = if (getVarnum () < (2*num+2)) then setVarnum (2*num+2) else (); 92 val (l, uv) = prop_list_to_var_list uv l; 93 in 94 ((2*num)::l, uv) 95 end; 96 97 fun xprop_prop_logic_to_bdd (uv:((term, int) Binarymap.dict * int)) term = 98 let 99 val (f, _) = get_const term; 100 in 101 if ((f = "XP_TRUE") orelse (f = "P_TRUE")) then (TRUE, uv) else 102 if ((f = "XP_FALSE") orelse (f = "P_FALSE")) then (FALSE, uv) else 103 if ((f = "XP_PROP") orelse (f = "P_PROP")) then 104 let 105 val arg = rand term; 106 val (num, uv) = get_arg_num uv arg 107 val _ = if (getVarnum () < (2*num+2)) then setVarnum (2*num+2) else (); 108 val s = ithvar (2*num); 109 in 110 (s, uv) 111 end else 112 if (f = "XP_NEXT_PROP") then 113 let 114 val arg = rand term; 115 val (num, uv) = get_arg_num uv arg 116 val _ = if (getVarnum() < (2*num+1)) then setVarnum (2*num+2) else (); 117 val s = ithvar (2*num+1); 118 in 119 (s, uv) 120 end else 121 if ((f = "XP_NOT") orelse (f = "P_NOT")) then 122 let 123 val arg = rand term; 124 val (s, uv) = xprop_prop_logic_to_bdd uv arg 125 in 126 (NOT s, uv) 127 end else 128 if ((f = "XP_AND") orelse (f = "P_AND")) then 129 let 130 val (arg1,arg2) = dest_pair (rand term); 131 val (s1, uv) = xprop_prop_logic_to_bdd uv arg1 132 val (s2, uv) = xprop_prop_logic_to_bdd uv arg2 133 in 134 (AND (s1, s2), uv) 135 end else 136 if ((f = "XP_OR") orelse (f = "P_OR")) then 137 let 138 val (arg1,arg2) = dest_pair (rand term); 139 val (s1, uv) = xprop_prop_logic_to_bdd uv arg1 140 val (s2, uv) = xprop_prop_logic_to_bdd uv arg2 141 in 142 (OR (s1, s2), uv) 143 end else 144 if ((f = "XP_IMPL") orelse (f = "P_IMPL")) then 145 let 146 val (arg1,arg2) = dest_pair (rand term); 147 val (s1, uv) = xprop_prop_logic_to_bdd uv arg1 148 val (s2, uv) = xprop_prop_logic_to_bdd uv arg2 149 in 150 (IMP (s1, s2), uv) 151 end else 152 if ((f = "XP_EQUIV") orelse (f = "P_EQUIV"))then 153 let 154 val (arg1,arg2) = dest_pair (rand term); 155 val (s1, uv) = xprop_prop_logic_to_bdd uv arg1 156 val (s2, uv) = xprop_prop_logic_to_bdd uv arg2 157 in 158 (BIIMP (s1, s2), uv) 159 end else 160 if ((f = "XP_COND") orelse (f = "P_COND")) then 161 let 162 val arg_list = strip_pair (rand term); 163 val (arg1,arg2, arg3) = (el 1 arg_list, el 2 arg_list, el 3 arg_list); 164 val (s1, uv) = xprop_prop_logic_to_bdd uv arg1 165 val (s2, uv) = xprop_prop_logic_to_bdd uv arg2 166 val (s3, uv) = xprop_prop_logic_to_bdd uv arg3 167 in 168 (ITE s1 s2 s3, uv) 169 end else 170 if ((f = "XP_CURRENT_EXISTS") orelse (f = "P_EXISTS")) then 171 let 172 val p = rand term; 173 val l = fst (dest_list (rand (rator term))); 174 val (s, uv) = xprop_prop_logic_to_bdd uv p 175 val (l', uv) = prop_list_to_var_list uv l 176 in 177 (bdd.exist (bdd.makeset l') s, uv) 178 end else 179 if ((f = "XP_CURRENT_FORALL") orelse (f = "P_FORALL")) then 180 let 181 val p = rand term; 182 val l = fst (dest_list (rand (rator term))); 183 val (s, uv) = xprop_prop_logic_to_bdd uv p 184 val (l', uv) = prop_list_to_var_list uv l 185 in 186 (bdd.forall (bdd.makeset l') s, uv) 187 end else 188 if ((f = "XP_NEXT_EXISTS")) then 189 let 190 val p = rand term; 191 val l = fst (dest_list (rand (rator term))); 192 val (s, uv) = xprop_prop_logic_to_bdd uv p 193 val (l', uv) = prop_list_to_var_list uv l 194 val l' = map (fn x => x + 1) l'; 195 in 196 (bdd.exist (bdd.makeset l') s, uv) 197 end else 198 if ((f = "XP_NEXT_FORALL")) then 199 let 200 val p = rand term; 201 val l = fst (dest_list (rand (rator term))); 202 val (s, uv) = xprop_prop_logic_to_bdd uv p 203 val (l', uv) = prop_list_to_var_list uv l 204 val l' = map (fn x => x + 1) l'; 205 in 206 (bdd.forall (bdd.makeset l') s, uv) 207 end else 208 let 209 val _ = print ("\n\nERROR!!! UNKNOWN LOGIC TERM "^f^"\n"); 210 val _ = print_term term; 211 val _ = print "\n\n"; 212 in 213 raise translation2smv_exp 214 end 215 end; 216 217(* 218val t = ``XP_NEXT_EXISTS [2] (XP_COND (XP_NEXT_PROP 1, XP_NEXT_PROP 2, XP_PROP 3))``; 219val t = ``P_COND (P_PROP 1, P_PROP 2, P_PROP 3)``; 220dest_pair (rator t) 221 222val uv = ((Binarymap.mkDict compare):(term, int) Binarymap.dict, 0); 223val (b, _) = xprop_prop_logic_to_bdd uv t 224 225printset b 226val set = Intset.empty 227help "intset" 228 229hash b 230definitions_of_bdd TextIO.stdOut b Intset.empty 231 232val t = ``P_COND (P_PROP 1, P_PROP 2, P_PROP 3)``; 233dest_pair (rator t) 234 235val uv = ((Binarymap.mkDict compare):(term, int) Binarymap.dict, 0); 236val (b, _) = xprop_prop_logic_to_bdd uv t 237 238val set = Intset.empty 239help "intset" 240 241*) 242 243 fun num_to_var_string n = 244 let 245 val next_var = (n mod 2 = 1); 246 val var_s = "x"^(int_to_string (n div 2)) 247 val var_s = if (next_var) then "next("^var_s^")" else var_s; 248 in 249 var_s 250 end; 251 252 fun bdd_to_definition b = 253 if (bdd.hash b = 1) then "1" else 254 if (bdd.hash b = 0) then "0" else 255 if (((bdd.hash (bdd.high b) = 1) andalso (bdd.hash (bdd.low b) = 0))) then (num_to_var_string (bdd.var b)) else 256 if (((bdd.hash (bdd.high b) = 0) andalso (bdd.hash (bdd.low b) = 1))) then ("!"^(num_to_var_string (bdd.var b))) else 257 "def_"^(int_to_string (hash b)); 258 259 260 261 fun add_def file_st b = 262 let 263 val def = bdd_to_definition b; 264 in 265 if (String.isPrefix "def_" def) then 266 let 267 val var_s = num_to_var_string (bdd.var b); 268 269 val res = if ((bdd.hash (bdd.high b) = 1)) then 270 ("("^(num_to_var_string (bdd.var b))^" | "^bdd_to_definition (low b)^")") else 271 if ((bdd.hash (bdd.low b) = 1)) then 272 ("(!"^(num_to_var_string (bdd.var b))^" | "^bdd_to_definition (high b)^")") else 273 if ((bdd.hash (bdd.high b) = 0)) then 274 ("(!"^(num_to_var_string (bdd.var b))^" & "^bdd_to_definition (low b)^")") else 275 if ((bdd.hash (bdd.low b) = 0)) then 276 ("("^(num_to_var_string (bdd.var b))^" & "^bdd_to_definition (high b)^")") else 277 "("^ var_s ^" & "^(bdd_to_definition (high b))^") | (!"^var_s^" & "^(bdd_to_definition (low b)) ^")"; 278 val res = def ^ " := " ^ res ^";\n"; 279 val _ = TextIO.output(file_st,res); 280 val _ = TextIO.flushOut file_st; 281 in 282 () 283 end 284 else 285 () 286 end; 287 288 289 fun definitions_of_bdd file_st s [] = () | 290 definitions_of_bdd file_st s (b::bl) = 291 292 let 293 val (s, bl) = 294 if (bdd.hash b = 1) then (s, bl) else 295 if (bdd.hash b = 0) then (s, bl) else 296 if (Intset.member (s,(hash b))) then (s, bl) else 297 let 298 val s = Intset.add (s, (hash b)); 299 val _ = add_def file_st b; 300 val bl = (high b)::(low b)::bl; 301 in 302 (s, bl) 303 end; 304 in 305 definitions_of_bdd file_st s bl 306 end; 307 308 309 fun ctl_to_smv uv term = 310 let 311 val (f, _) = get_const term; 312 in 313 if (f = "CTL_TRUE") then ("TRUE", uv, []) else 314 if (f = "CTL_FALSE") then ("FALSE", uv, []) else 315 if (f = "CTL_PROP") then 316 let 317 val p_term = rand term; 318 val (p_bdd, uv) = xprop_prop_logic_to_bdd uv p_term; 319 val p_string = bdd_to_definition p_bdd; 320 in 321 (p_string, uv, [p_bdd]) 322 end else 323 if (f = "CTL_NOT") then 324 let 325 val arg = rand term; 326 val (arg_string, uv, bdds) = ctl_to_smv uv arg; 327 in 328 ("!("^arg_string^")", uv, bdds) 329 end else 330 if (f = "CTL_AND") then 331 let 332 val (arg1,arg2) = dest_pair (rand term); 333 val (arg1_string, uv, bdds1) = ctl_to_smv uv arg1; 334 val (arg2_string, uv, bdds2) = ctl_to_smv uv arg2; 335 in 336 ("("^arg1_string^") & ("^arg2_string^")", uv, bdds1 @ bdds2) 337 end else 338 if (f = "CTL_OR") then 339 let 340 val (arg1,arg2) = dest_pair (rand term); 341 val (arg1_string, uv, bdds1) = ctl_to_smv uv arg1; 342 val (arg2_string, uv, bdds2) = ctl_to_smv uv arg2; 343 in 344 ("("^arg1_string^") | ("^arg2_string^")", uv, bdds1 @ bdds2) 345 end else 346 if (f = "CTL_IMPL") then 347 let 348 val (arg1,arg2) = dest_pair (rand term); 349 val (arg1_string, uv, bdds1) = ctl_to_smv uv arg1; 350 val (arg2_string, uv, bdds2) = ctl_to_smv uv arg2; 351 in 352 ("("^arg1_string^") -> ("^arg2_string^")", uv, bdds1 @ bdds2) 353 end else 354 if (f = "CTL_EQUIV") then 355 let 356 val (arg1,arg2) = dest_pair (rand term); 357 val (arg1_string, uv, bdds1) = ctl_to_smv uv arg1; 358 val (arg2_string, uv, bdds2) = ctl_to_smv uv arg2; 359 in 360 ("("^arg1_string^") <-> ("^arg2_string^")", uv, bdds1 @ bdds2) 361 end else 362 if (f = "CTL_E_NEXT") then 363 let 364 val arg = rand term; 365 val (arg_string, uv, bdds) = ctl_to_smv uv arg; 366 in 367 ("EX ("^arg_string^")", uv, bdds) 368 end else 369 if (f = "CTL_A_NEXT") then 370 let 371 val arg = rand term; 372 val (arg_string, uv, bdds) = ctl_to_smv uv arg; 373 in 374 ("AX ("^arg_string^")", uv, bdds) 375 end else 376 if (f = "CTL_E_ALWAYS") then 377 let 378 val arg = rand term; 379 val (arg_string, uv, bdds) = ctl_to_smv uv arg; 380 in 381 ("EG ("^arg_string^")", uv, bdds) 382 end else 383 if (f = "CTL_A_ALWAYS") then 384 let 385 val arg = rand term; 386 val (arg_string, uv, bdds) = ctl_to_smv uv arg; 387 in 388 ("AG ("^arg_string^")", uv, bdds) 389 end else 390 if (f = "CTL_E_EVENTUAL") then 391 let 392 val arg = rand term; 393 val (arg_string, uv, bdds) = ctl_to_smv uv arg; 394 in 395 ("EF ("^arg_string^")", uv, bdds) 396 end else 397 if (f = "CTL_A_EVENTUAL") then 398 let 399 val arg = rand term; 400 val (arg_string, uv, bdds) = ctl_to_smv uv arg; 401 in 402 ("AF ("^arg_string^")", uv, bdds) 403 end else 404 if (f = "CTL_E_SUNTIL") then 405 let 406 val (arg1,arg2) = dest_pair (rand term); 407 val (arg1_string, uv, bdds1) = ctl_to_smv uv arg1; 408 val (arg2_string, uv, bdds2) = ctl_to_smv uv arg2; 409 in 410 ("E (("^arg1_string^") U ("^arg1_string^"))", uv, bdds1 @ bdds2) 411 end else 412 if (f = "CTL_E_UNTIL") then 413 let 414 val (arg1,arg2) = dest_pair (rand term); 415 val (arg1_string, uv, bdds1) = ctl_to_smv uv arg1; 416 val (arg2_string, uv, bdds2) = ctl_to_smv uv arg2; 417 in 418 ("(E (("^arg1_string^") U ("^arg2_string^"))) | (EG ("^arg1_string^"))", uv, bdds1 @ bdds2) 419 end else 420 let 421 val _ = print ("\n\nERROR!!! UNKNOWN TERM "^f^"\n"); 422 val _ = print_term term; 423 val _ = print "\n\n"; 424 in 425 raise translation2smv_exp 426 end 427 end 428 429 in 430 431 fun ctl_ks_fair2smv_string ks_term file_st = 432 let 433 val p_term = rand (rator (rand (rator ((rator (ks_term)))))) 434 val xp_term = rand (rand (rator (rator (ks_term)))) 435 val (fc, _) = dest_list (rand ks_term) 436 val ctl = rand (rator (ks_term)) 437 438 val uv = ((Binarymap.mkDict compare):(term, int) Binarymap.dict, 0); 439 440 441 val (p_bdd, uv) = xprop_prop_logic_to_bdd uv p_term; 442 val p_string = bdd_to_definition p_bdd; 443 val (xp_bdd, uv) = xprop_prop_logic_to_bdd uv xp_term 444 val xp_string = bdd_to_definition xp_bdd; 445 val (ctl_string, uv, ctl_bdds) = ctl_to_smv uv ctl 446 447 fun fairness_string uv [] = ("", uv, []) | 448 fairness_string uv (e::l) = 449 let 450 val (fc_bdd, uv) = xprop_prop_logic_to_bdd uv e 451 val fc_string = bdd_to_definition fc_bdd; 452 453 val (FC_string, uv, bdds) = fairness_string uv l; 454 in 455 ("FAIRNESS ("^fc_string^")\n"^FC_string, uv, fc_bdd::bdds) 456 end; 457 val (fc_string, uv, fc_bdds) = fairness_string uv fc; 458 459 460 461 fun used_vars_add s b = 462 Vector.foldl (fn (n, s) => Intset.add (s, n div 2)) s (scanset (support b)); 463 464 val vars = Intset.empty; 465 val vars = used_vars_add vars p_bdd; 466 val vars = used_vars_add vars xp_bdd; 467 val vars = foldl (fn (b, s) => used_vars_add s b) vars (fc_bdds@ctl_bdds); 468 469 fun varstring 0 = "" | 470 varstring n = 471 if (Intset.member (vars, n)) then 472 (varstring (n-1))^" x"^(int_to_string n)^": boolean;\n" 473 else 474 (varstring (n-1)); 475 476 477 val ks_string = term_to_string ks_term; 478 val ks_string_list = String.fields (fn x=> (x = #"\n")) ks_string 479 val _ = map (fn x => TextIO.output(file_st, "-- "^x^"\n")) ks_string_list; 480 val _ = TextIO.output(file_st, "\n\n"); 481 val _ = TextIO.output(file_st, "-- used variables\n\n"); 482 val _ = TextIO.flushOut file_st; 483 484 fun varrenaming_foldr ((term, var), s) = 485 let 486 val x = "x"^(int_to_string var); 487 val t = term_to_string term; 488 val line = x^": "^t^"\n"; 489 val _ = TextIO.output(file_st, "-- "^line); 490 val _ = TextIO.flushOut file_st; 491 in 492 (s^line) 493 end; 494 val varrenaming_list = Binarymap.listItems (fst uv); 495 val varrenaming_list = sort (fn (_, x) => fn (_, y) => (x > y)) varrenaming_list; 496 497 val varrenaming_string = foldr varrenaming_foldr "" varrenaming_list; 498 499 val _ = TextIO.output(file_st,"MODULE main\n\n"^ 500 "VAR\n"^(varstring (#2 uv))^"\n"^ 501 "INIT \n"^(p_string)^"\n\n"^ 502 "TRANS \n"^(xp_string)^"\n\n"^ 503 (fc_string)^"\n\n"^ 504 "DEFINE\n"); 505 val _ = TextIO.flushOut file_st; 506 507 508 val s = Intset.empty; 509 val bl = p_bdd::xp_bdd::(fc_bdds@ctl_bdds); 510 val _ = definitions_of_bdd file_st s bl; 511 512 val _ = TextIO.output(file_st,"\n\nCTLSPEC "^ctl_string^"\n\n"); 513 val _ = TextIO.flushOut file_st; 514 515 in 516 varrenaming_string 517 end; 518 end; 519 520 521fun fair_empty_ks2smv_string term file_st = 522 let 523 val ks_term = rhs (concl (REWRITE_CONV [IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___TO___CTL_KS_FAIR_SEM] term)); 524 in 525 ctl_ks_fair2smv_string ks_term file_st 526 end; 527 528 529fun modelCheckFairEmptyness ks_term thm = 530 let 531 val file_st = TextIO.openOut(!model_check_temp_file); 532 val vars = fair_empty_ks2smv_string ks_term file_st; 533 val _ = TextIO.closeOut file_st; 534 val res = SMV_RUN_FILE (!model_check_temp_file); 535 536 in 537 if (res) then true else 538 let 539 val _ = print vars; 540 val _ = print "===============================================\n"; 541 val _ = print_thm thm; 542 val _ = print "\n===============================================\n"; 543 in 544 false 545 end 546 end; 547 548 549fun model_check___ks_fair_emptyness thm = 550 let 551 val ks_term = rhs (rand (body (rand (concl thm)))) 552 val eq_term = lhs (rand (body (rand (concl thm)))) 553 val erg = modelCheckFairEmptyness ks_term thm; 554 val thm = if erg then (SOME (mk_oracle_thm "SMV" ([], eq_term))) else NONE 555 in 556 thm 557 end 558 559 560fun model_check___ltl_contradiction f = 561 let 562 val thm = ltl_contradiction2ks_fair_emptyness true f 563 in 564 model_check___ks_fair_emptyness thm 565 end 566 567fun model_check___ltl_equivalent l1 l2 = 568 let 569 val thm = ltl_equivalent2ks_fair_emptyness true l1 l2 570 in 571 model_check___ks_fair_emptyness thm 572 end 573 574fun model_check___ltl_equivalent_initial l1 l2 = 575 let 576 val thm = ltl_equivalent_initial2ks_fair_emptyness true l1 l2 577 in 578 model_check___ks_fair_emptyness thm 579 end 580 581fun model_check___ltl_ks_sem l M = 582 let 583 val thm = ltl_ks_sem2ks_fair_emptyness true l M 584 in 585 model_check___ks_fair_emptyness thm 586 end 587 588fun model_check___psl_contradiction f = 589 let 590 val thm = psl_contradiction2ks_fair_emptyness true f 591 in 592 model_check___ks_fair_emptyness thm 593 end 594 595fun model_check___psl_equivalent f1 f2 = 596 let 597 val thm = psl_equivalent2ks_fair_emptyness true f1 f2 598 in 599 model_check___ks_fair_emptyness thm 600 end 601 602fun model_check___psl_ks_sem f M = 603 let 604 val thm = psl_ks_sem2ks_fair_emptyness true f M 605 in 606 model_check___ks_fair_emptyness thm 607 end 608 609(* examples: 610 611val ltl1 = ``LTL_SUNTIL (LTL_PROP (P_PROP a), LTL_PROP (P_PROP b))``; 612 613val ltl2 = ``LTL_EVENTUAL (LTL_AND (LTL_PROP (P_PROP b), 614 LTL_PNEXT (LTL_PALWAYS (LTL_PROP (P_PROP a)))))``; 615 616(* SOME thm *) 617model_check___ltl_equivalent_initial ltl1 ltl2; 618 619(* NONE *) 620model_check___ltl_equivalent ltl1 ltl2; 621 622*) 623 624end 625