1(*List.app load ["bossLib","stringTheory","stringLib","HolBddLib","pairTheory","pred_setLib","listLib","CTL","pairSyntax","pairRules","pairTools","muTheory","boolSyntax","Drule","Tactical","Conv","Rewrite","Tactic","boolTheory"]*) 2 3structure muCheck = 4struct 5 6local 7 8open Globals HolKernel Parse 9 10open bossLib pairTheory pred_setTheory pred_setLib stringLib 11 listTheory simpLib pairSyntax pairLib PrimitiveBddRules 12 DerivedBddRules Binarymap PairRules pairTools boolSyntax Drule 13 Tactical Conv Rewrite Tactic boolTheory listSyntax stringTheory 14 boolSimps pureSimps listSimps numLib HolSatLib 15 16open setLemmasTheory muSyntax muSyntaxTheory muTheory stringBinTree 17 muTools commonTools ksTheory cearTheory bddTools envTheory envTools 18 cacheTools cacheTheory ksTools lazyTools lzPairRules lzConv 19 20val dpfx = "mc_" 21 22in 23 24fun mk_gen_ap_thm ksname state msa mf = 25 let 26 val _ = dbgTools.DEN dpfx "mga" (*DBG*) 27 val _ = dbgTools.DTM (dpfx^"mga_mf") mf (*DBG*) 28 val _ = dbgTools.DTH (dpfx^ "mga_msa") msa (*DBG*) 29 val ap = rand mf 30 val _ = dbgTools.DTM (dpfx^"mga_ap") ap (*DBG*) 31 val apth = GSYM(lzPBETA_RULE (SPEC ap ((CONV_RULE lzSWAP_VARS_CONV) msa))) 32 val _ = dbgTools.DTH (dpfx^"mga_apth") apth (*DBG*) 33 val _ = dbgTools.DEX dpfx "mga" (*DBG*) 34 in apth end 35 36fun mk_gen_modal_thm Tth modth mf = 37 let 38 val _ = dbgTools.DEN dpfx "mgm" (*DBG*) 39 (*val _ = dbgTools.DTH (dpfx^ Tth) (*DBG*) 40 val _ = dbgTools.DTH (dpfx^ modth) (*DBG*) 41 val _ = dbgTools.DTM (dpfx^ mf) *) 42 val nm = hd(snd(strip_comb mf)) 43 (*val ks1 = AP_THM Tth nm 44 val ks2 = PURE_REWRITE_RULE [find_CONV (mk_comb(snd(dest_eq(concl Tth)), nm))] ks1*) 45 val res = lzPBETA_RULE (PURE_REWRITE_RULE [Tth] (SPEC nm modth)) 46 (*val _ = dbgTools.DTH (dpfx^ res) (*DBG*)*) 47 val _ = dbgTools.DEX dpfx "mgm" (*DBG*) 48 in res end 49 50(* returns mappings for each rv v->(x->"v"="x") where x are all the rv's in the formula (binding occurances included) *) 51(* except for the cases v=x because that gives a trivial thm that causes the rewriter to loop *) 52fun mk_seths mf = 53 let 54 val _ = dbgTools.DEN dpfx "mse" (*DBG*) 55 val rvtm = ``(RV x):^(ty_antiq(type_of mf))`` 56 val mutm = ``(mu Q .. f):^(ty_antiq(type_of mf))`` 57 val nutm = ``(nu Q .. f):^(ty_antiq(type_of mf))`` 58 val rvs = Binaryset.addList(Binaryset.empty Term.compare, 59 ((List.map (fn tm => rand tm) (find_terms (can (match_term rvtm)) mf)) @ 60 (List.map (fn tm => List.hd(snd(strip_comb tm))) 61 (find_terms (can (match_term mutm)) mf)) @ 62 (List.map (fn tm => List.hd(snd(strip_comb tm))) 63 (find_terms (can (match_term nutm)) mf)))) 64 val seglpairs = List.map (fn l => (hd l,last l)) (cartprod [Binaryset.listItems rvs,Binaryset.listItems rvs]) 65 val segl2 = List.map (fn v => (v,list2map(List.map (fn (x,y) => (fromHOLstring y,mk_eq(x,y))) 66 (List.filter (fn (x,y) => Term.compare(x,v)=EQUAL) 67 seglpairs)))) (Binaryset.listItems rvs) 68 val seths = list2map(List.map (fn (v,gll) => 69 (fromHOLstring v, 70 Binarymap.map (fn (y,gl) => (* FIXME: this lz has not been verified *) 71 let val jf = (fn _ => 72 (PURE_REWRITE_RULE 73 [GEN_ALL(List.last(CONJUNCTS (SPEC_ALL EQ_CLAUSES)))] 74 (stringLib.string_EQ_CONV gl))) 75 in mk_lthm (fn _ => (if Term.compare(lhs gl,rhs gl)=EQUAL 76 then mk_eq(gl,T) else mk_neg(gl),jf)) jf end) 77 gll)) segl2) 78 val sel = (List.map snd (List.concat (List.map snd (Binarymap.listItems 79 (Binarymap.map (Binarymap.listItems o snd) seths))))) 80 val _ = dbgTools.DEX dpfx "mse" (*DBG*) 81 in (seths,sel) end 82 83(* for when we have not got sel precomputed *) 84fun prove_imf f = 85 let val p_ty = muSyntax.get_prop_type f 86 val sel = snd (mk_seths f) 87 val imfth = mk_imf_thm (inst [alpha |-> p_ty] muSyntax.mu_imf_tm) f (mk_tysimps sel p_ty) p_ty 88 in imfth end 89 90fun mk_gen_rv_thms mf ksname state rvl ie wfKS_ks = 91 let 92 val _ = dbgTools.DEN dpfx "mgr" (*DBG*) 93 val _ = dbgTools.DTH (dpfx^"mgr_wfKS_ks") wfKS_ks (*DBG*) 94 val _ = dbgTools.DTH (dpfx^"mgr_spec_MU_SAT_RV") (ISPECL [state,ksname] MU_SAT_RV) (*DBG*) 95 val _ = dbgTools.DTH (dpfx^"mgr_msr_ante") (CONV_RULE lzFORALL_IMP_CONV(ISPECL [state,ksname] MU_SAT_RV))(*DBG*) 96 val msr = MP (CONV_RULE lzFORALL_IMP_CONV (ISPECL [state,ksname] MU_SAT_RV)) wfKS_ks 97 val msreq = ISPEC state (MP (ISPEC ksname MU_SAT_RV_ENV_EQ) wfKS_ks) 98 val _ = dbgTools.DEX dpfx "mgr" (*DBG*) 99 in (msr,mk_seths mf,msreq) end 100 101fun mk_gen_thms T (apl,ks_def,wfKS_ks) state state' st vm = 102 let 103 val _ = dbgTools.DEN dpfx "mgt" (*DBG*) 104 (* Note: this assumes varmap assignments are contiguous stating from zero TODO: get rid of this assumption *) 105 val i2ap = Vector.fromList (List.map (fn ap => BddVar true vm ap) st) 106 val apnm2ix =fst(Vector.foldl (fn(nm,(bm,ix)) => (Binarymap.insert(bm,term_to_string2(getTerm(nm)),ix),ix+1)) 107 (Binarymap.mkDict String.compare,0) i2ap) 108 (*val _ = dbgTools.DST (dpfx^ ("vector i2ap\n")) 109 val _ = Vector.app (fn nm => dbgTools.DST (dpfx^ ("("^(term_to_string(getTerm nm))^")")) ) i2ap(*DBG*) 110 val _ = dbgTools.DST (dpfx^ ("mapnm2ix\n")) 111 val _ =Binarymap.app (fn(nm,ix)=> dbgTools.DST (dpfx^ ("("^nm^","^(int_to_string ix)^")"))) apnm2ix(*DBG*)*) 112 val ksname = lhs(concl ks_def) 113 val (prop_type,state_type) = get_types ksname 114 val env_ty = stringLib.string_ty --> state_type --> bool 115 val stpset_ty = (mk_prod(state_type,state_type)) --> bool 116 val KSap = List.foldl (fn (e,ac) => list_mk_comb (inst [alpha|->prop_type] pred_setSyntax.insert_tm,[e,ac])) 117 (inst [alpha|->prop_type] pred_setSyntax.empty_tm) apl 118 val msthl = List.map (fn th => MATCH_MP (CONV_RULE lzFORALL_IMP_CONV (ISPECL [state,ksname] th)) wfKS_ks) 119 (MU_SAT_AP::MU_SAT_DMD::MU_SAT_BOX::[MU_SAT_T,MU_SAT_F,MU_SAT_NEG,MU_SAT_CONJ,MU_SAT_DISJ]) 120 val Lth = mk_Lth ks_def 121 val _ = dbgTools.DTH (dpfx^"mgt_ Lth") Lth (*DBG*) 122 (*val _ = List.app (fn th => dbgTools.DTH (dpfx^ th) ) msthl val _ = dbgTools.DST (dpfx^ "msthl\n") *) 123 (*val msa = PBETA_RULE (PURE_REWRITE_RULE [Lth] (List.nth(msthl,0)))*) 124 val pvar = mk_var("p",prop_type) 125 val jf = (fn _ => (PURE_REWRITE_RULE [Lth] (List.nth(msthl,0)))) 126 val msa = lzPBETA_RULE 127 (mk_lthm (fn _ => (``!e p. MU_SAT (AP p) ^ksname e ^state = 128 ^(list_mk_comb(rhs(concl Lth),[state,pvar]))``,jf)) jf) 129 (*val _ = dbgTools.DTH (dpfx^ msa) val _ = dbgTools.DST (dpfx^ "msa\n") *) 130 val msp = List.map GSYM (List.drop(msthl,3)) 131 val (Tth,dmdth) = mk_Tth ks_def ksname (List.nth(msthl,1)) (List.nth(msthl,2)) state' state_type prop_type 132 val githms = mk_gen_inv_thms ksname state wfKS_ks 133 val _ = dbgTools.DEX dpfx "mgt" (*DBG*) 134 in (msp,msa,Tth,dmdth,githms) end 135 136(* note this assumes that an AP is a boolean term *) 137(* if AP's are over non-booleans, then we do suitable preprocessing on the model to turn stuff into booleans 138 otherwise you can't make BDD's out of them *) 139fun mk_ap_tb vm absf mf sth = 140 let 141 val _ = dbgTools.DEN dpfx "mat" (*DBG*) 142 (*val _ = dbgTools.DTM (dpfx^ mf) val _ = dbgTools.DST (dpfx^ "(mf)\n") (*DBG*) 143 val _ = dbgTools.DTH (dpfx^ sth) val _ = dbgTools.DST (dpfx^ "(sth)\n") (*DBG*)*) 144 val ap = pbody (snd (dest_comb mf)) 145 val tb = if (Option.isSome absf) then (* FIXME: can we remove the reference to absf? *) 146 let val htb = Option.valOf absf 147 val ht = getTerm htb 148 val cstate = fst(dest_pair(List.hd (snd (strip_comb ht)))) 149 in BddExists (strip_pair cstate) (BddOp(bdd.And,htb, t2tb vm ap)) end 150 else t2tb vm ap 151 (*val _ = dbgTools.DTM (dpfx^ (getTerm tb)) val _ = dbgTools.DST (dpfx^ "(tb)\n") (*DBG*)*) 152 val res = BddEqMp sth tb 153 val _ = dbgTools.DEX dpfx "mat" (*DBG*) 154 in res end 155 156fun mk_con_tb_tm vm tm = if (Term.compare(tm,T)=EQUAL) then BddCon true vm else BddCon false vm 157 158fun mk_con_tb b vm mf sth = 159 let 160 val _ = dbgTools.DEN dpfx "mct" (*DBG*) 161 (*val _ = dbgTools.DTH (dpfx^ sth) (*DBG*) 162 val _ = dbgTools.DST (dpfx^ " sth\n") (*DBG*)*) 163 val res = BddEqMp sth (BddCon b vm) 164 val _ = dbgTools.DEX dpfx "mct" (*DBG*) 165 in res end 166 167fun mk_rv_tb ee (_,_,_,_,ix,_,_,_,_,_) mf sth = 168 let 169 val _ = dbgTools.DEN dpfx "mrt" (*DBG*) 170 (*val _ = dbgTools.DTH (dpfx^ sth) (*DBG*) 171 val _ = dbgTools.DST (dpfx^ "rv tb sth\n") (*DBG*) 172 val _ = dbgTools.DST (dpfx^ (int_to_string ix)) (*DBG*) 173 val _ = dbgTools.DST (dpfx^ " ix\n") (*DBG*) 174 val _ = dbgTools.DST (dpfx^ (int_to_string (Array.length ee))) (*DBG*) 175 val _ = dbgTools.DST (dpfx^ " ee length\n") (*DBG*) 176 val _ = dbgTools.DTM (dpfx^ (getTerm (snd(Array.sub(ee,ix))))) (*DBG*) 177 val _ = dbgTools.DST (dpfx^ "rv tb\n") (*DBG*)*) 178 val res = BddEqMp sth (snd(Array.sub(ee,ix))) 179 (*val _ = dbgTools.DTM (dpfx^ (getTerm res)) (*DBG*)*) 180 val _ = dbgTools.DEX dpfx "mrt" (*DBG*) 181 in res end 182 183fun mk_rv_spec_thm msr seth sel msreq ie ee state (tb,gth,sth,env,ix,rsc,ithm,abthm,_,_) dp mf = 184 let 185 val _ = dbgTools.DEN dpfx "mrst" (*DBG*) 186 (*val _ = dbgTools.DTM (dpfx^ ie) val _ = dbgTools.DST (dpfx^ " ie \n") (*DBG*)*) 187 val bv = rand mf 188 (*val _ = dbgTools.DTM (dpfx^ bv) val _ = dbgTools.DST (dpfx^ " bv \n") (*DBG*)*) 189 val v = fromHOLstring(bv) 190 (*val _ = dbgTools.DTH (dpfx^ msr) val _ = dbgTools.DST (dpfx^ "msr\n") (*DBG*) 191 val _ = if (Option.isSome sth) then dbgTools.DTH (dpfx^ (Option.valOf sth)) else dbgTools.DST (dpfx^ " NONE") 192 val _ = dbgTools.DST (dpfx^ "\nsth\n") (*DBG*) 193 val _ = dbgTools.DTM (dpfx^ ie) val _ = dbgTools.DST (dpfx^ " ie\n") (*DBG*) 194 val _ = List.app (fn th => let val _ = dbgTools.DTH (dpfx^ th) 195 val _ = dbgTools.DST (dpfx^ "seth\n") in () end)(*DBG*) 196 ((List.map snd (Binarymap.listItems(Binarymap.find(seth,v))))@[ENV_UPDATE_def,BETA_THM])(*DBG*)*) 197 val th = if (Int.compare(ix,dp)=EQUAL 198 andalso (Vector.sub(rsc,ix)>0)) (*i.e.current bnd var top level fv filt by >0 test*) 199 then (* this has already been proved in FixExp *) 200 Option.valOf sth 201 else (* otherwise not innermost bound var so must account for change in environment *) 202 let 203 (*val _ = dbgTools.DST (dpfx^ "else\n") 204 val _ = dbgTools.DTH (dpfx^ (ISPECL [ie,fromMLstring v] msr)) 205 val _ = dbgTools.DST (dpfx^ " msr1\n") (*DBG*) 206 val _ = List.app (fn th => let val _ = dbgTools.DTH (dpfx^ th) 207 val _ = dbgTools.DST (dpfx^ " seths\n") in () end)(*DBG*) 208 (List.map snd (Binarymap.listItems(Binarymap.find(seth,v))))(*DBG*) 209 val _ = dbgTools.DTH (dpfx^ (eval_env ie ie bv seth [])) (*DBG*) 210 val _ = dbgTools.DST (dpfx^ " env_eval thm\n") (*DBG*)*) 211 in SYM (CONV_RULE(RHS_CONV(PURE_ONCE_REWRITE_CONV [eval_env ie ie bv state seth sel []])) 212 (ISPECL [ie,bv] msr)) end 213 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ "rv spec thm\n") (*DBG*)*) 214 val _ = dbgTools.DEX dpfx "mrst" (*DBG*) 215 in th end 216 217(* in case an mf is an RV, getting the spec thm is more than just SPEC'ing the gth with the ie *) 218fun get_spec_thm ie spec_func gth mf = 219 let 220 val _ = dbgTools.DEN dpfx "gst" (*DBG*) 221 (*val _ = dbgTools.DTH (dpfx^ gth) val _ = dbgTools.DST (dpfx^ " gth\n") (*DBG*)*) 222 val res = if is_RV mf (* RV case *) 223 then spec_func mf (* this calls mk_rv_spec_thm *) 224 else let 225 (*val _ = dbgTools.DST (dpfx^ "not RV \n") val _ = dbgTools.DST (dpfx^ _type (type_of ie)) 226 val _ = dbgTools.DST (dpfx^ " ie type\n") (*DBG*) 227 val _ = dbgTools.DTH (dpfx^ gth) val _ = dbgTools.DST (dpfx^ " gth with type\n") (*DBG*)*) 228 in SPEC ie gth end 229 val _ = dbgTools.DEX dpfx "gst" (*DBG*) 230 in res end 231 232(* dummy theorem, not used by FixExp *) 233(* we don't just put TRUTH here because a gen thm needs to be SPEC'able *) 234fun mk_fp_gen_thm state mf = INST_TYPE [``:'a`` |-> type_of state] ENV_UPDATE_INV 235 236fun get_cache_entry mf (muAP cch) = !cch 237| get_cache_entry mf (muRV cch) = !cch 238| get_cache_entry mf (muAnd(cch,_)) = !cch 239| get_cache_entry mf (muOr(cch,_)) = !cch 240| get_cache_entry mf (muNot(cch,_)) = !cch 241| get_cache_entry mf (muTR cch) = !cch 242| get_cache_entry mf (muFL cch) = !cch 243| get_cache_entry mf (muDIAMOND(cch,_)) = !cch 244| get_cache_entry mf (muBOX(cch,_)) = !cch 245| get_cache_entry mf (fpmu(_,cch,_)) = !cch 246| get_cache_entry mf (fpnu(_,cch,_)) = !cch 247 248fun mk_spec_inv_thm githm nodes ie0 ie1 mf seth = 249 let 250 val _ = dbgTools.DEN dpfx "msit" (*DBG*) 251 val (opr,args) = strip_comb mf 252 (*val _ = dbgTools.DTM (dpfx^ mf) val _ = dbgTools.DST (dpfx^ " mf\n") (*DBG*) 253 val _ = dbgTools.DTM (dpfx^ ie0) val _ = dbgTools.DST (dpfx^ " ie0\n") (*DBG*) 254 val _ = dbgTools.DTM (dpfx^ ie1) val _ = dbgTools.DST (dpfx^ " ie1\n") (*DBG*) 255 val _ = dbgTools.DTH (dpfx^ githm) val _ = dbgTools.DST (dpfx^ " githm\n") (*DBG*) *) 256 val res = 257 case (fst (dest_const opr)) of 258 "AP" => ISPECL [ie0,ie1] githm 259 | "RV" => let val Hv = List.hd args 260 val v = fromHOLstring Hv 261 (*val _ = dbgTools.DTM (dpfx^" spec_inv goal\n" ``^ie0 ^Hv = ^ie1 ^Hv``) (*DBG*)*) 262 val sel = (List.map snd (Binarymap.listItems(Binarymap.find(seth,v)))) 263 val goal = mk_eq(mk_comb(ie0,Hv),mk_comb(ie1,Hv)) (*``^ie0 ^Hv = ^ie1 ^Hv`` *) 264 val jf = (fn _ => (prove(goal,SIMP_TAC std_ss ([ENV_UPDATE_def]@sel))) ) 265 val ethm = mk_lthm (fn _ => (goal,jf)) jf 266 (*val _ = dbgTools.DTH (dpfx^ ethm) val _ = dbgTools.DST (dpfx^ " ethm\n") (*DBG*)*) 267 in (*MATCH_*)MP (ISPECL [ie0,ie1] githm) ethm end 268 | "And" => ISPECL [ie0,ie1] githm 269 | "Or" => ISPECL [ie0,ie1] githm 270 | "Not" => ISPECL [ie0,ie1] githm 271 | "TR" => ISPECL [ie0,ie1] githm 272 | "FL" => ISPECL [ie0,ie1] githm 273 | "DIAMOND" => ISPECL [ie0,ie1] githm 274 | "BOX" => ISPECL [ie0,ie1] githm 275 | "mu" => ISPECL [ie0,ie1] githm 276 | "nu" => ISPECL [ie0,ie1] githm 277 | _ => Raise Match 278 (*val _ = dbgTools.DTH (dpfx^ res) val _ = dbgTools.DST (dpfx^ " mk_spec_inv_thm res\n") (*DBG*)*) 279 val _ = dbgTools.DEX dpfx "msit" (*DBG*) 280 in res end 281 282(* goal is a conjunction of equalities of the form ie0 Q = ie1 Q TODO:speed this up*) 283fun mk_se_thm goal sel = 284 let 285 val _ = dbgTools.DEN dpfx "mst" (*DBG*) 286 (*val _ = dbgTools.DTM (dpfx^ goal) val _ = dbgTools.DST (dpfx^ " goal\n") (*DBG*)*) 287 (*val _ =List.app (fn th => dbgTools.DTH (dpfx^" cache seth\n" th)) sel(*DBG*)*) 288 val jf = (fn _ => (prove(goal,SIMP_TAC std_ss (ENV_UPDATE_def::sel)))) 289 val res = mk_lthm (fn _ => (goal,jf)) jf 290 val _ = dbgTools.DEX dpfx "mst" (*DBG*) 291 in res end 292 293(* retrieve term_bdd from cache. if missing use callbacks to create it and update cache *) 294fun cache_get cch ie tb_func gth_func dp nodes mf seth sel state = 295 let val (tb,gth,sth,env,ix,rsc,ithm,abthm,ado_subthm,ado_eqthm) = !cch 296 val _ = dbgTools.DEN dpfx "cg" (*DBG*) 297 (*val _ = dbgTools.DTM (dpfx^ mf) val _ = dbgTools.DST (dpfx^ " mf\n") (*DBG*) 298 val _ = dbgTools.DST (dpfx^ (Int.toString dp)) val _ = dbgTools.DST (dpfx^ " dp\n") (*DBG*) 299 val _ = dbgTools.DST (dpfx^ (Int.toString ix)) val _ = dbgTools.DST (dpfx^ " ix\n") (*DBG*) 300 val _ = if then let val _ = print_rsc rsc "" in () end else () (*DBG*) 301 val _ = dbgTools.DST (dpfx^ (Int.toString(Vector.length rsc))) (*DBG*) 302 val _ = dbgTools.DST (dpfx^ " rsc length\n") (*DBG*)*) 303 fun check_rv rsc dp = if (dp=(~1)) then true else if (Vector.sub(rsc,dp)=0) then check_rv rsc (dp-1) else false 304 (*val _ = with_flag (show_types,true) dbgTools.DTM (dpfx^ ie) val _ = dbgTools.DST (dpfx^ " ie\n") (*DBG*) 305 val _ = with_flag (show_types,true) dbgTools.DTM (dpfx^ env) val _ = dbgTools.DST (dpfx^ " env\n") (*DBG*)*) 306 val res = if (Term.compare(env,ie)=EQUAL) 307 then 308 if (Option.isSome tb) 309 then Option.valOf tb 310 else 311 if (Option.isSome sth) 312 then let val tb = tb_func mf (Option.valOf sth) 313 val _ = upd_cch_tb cch tb 314 in tb end 315 else 316 if (Option.isSome gth) 317 then let 318 val _ = dbgTools.DST (dpfx^"cg_ gth SOME\n") (*DBG*) 319 (*val _ = with_flag(show_types,true) dbgTools.DTH (dpfx^ (Option.valOf gth)) (*DBG*) 320 val _ = dbgTools.DST (dpfx^ " gth\n") (*DBG*)*) 321 val sth = get_spec_thm ie gth_func (Option.valOf gth) mf (* could be an RV *) 322 val tb = tb_func mf sth 323 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth 324 in tb end 325 else let 326 val _ = dbgTools.DST (dpfx^"cg_ gth NONE\n") (*DBG*) 327 (*val _ = dbgTools.DTM (dpfx^ mf) (*DBG*)*) 328 val gth = gth_func mf (* can't be an RV because we stuffed its gth with TRUTH *) 329 (*val _ = dbgTools.DTH (dpfx^ gth) val _ = dbgTools.DST (dpfx^ " gth\n") *)(*DBG*) 330 val sth = ISPEC ie gth 331 (*val _ = dbgTools.DTH (dpfx^ sth) val _ = dbgTools.DST (dpfx^ " sth22\n") (*DBG*)*) 332 val tb = tb_func mf sth 333 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth val _ = upd_cch_gth cch gth 334 in tb end 335 else 336 if (Option.isSome tb andalso (check_rv rsc dp)) 337 then (* above check prevents dirty read i.e. only if no subformula contains a currently bound RV *) 338 if (Option.isSome gth) 339 then let 340 val _ = dbgTools.DST (dpfx^"cg_ cached\n") (*DBG*) 341 (*val _ = dbgTools.DTM (dpfx^ (getTerm (Option.valOf tb))) (*DBG*) 342 val _ = dbgTools.DST (dpfx^ " cached tb\n") (*DBG*) 343 val _ = if then let val _ = print _rsc rsc "cached tb" in () end else () (*DBG*)*) 344 val sth1 = get_spec_thm ie gth_func (Option.valOf gth) mf (* could be an RV *) 345 val sth0 = Option.valOf sth 346 (*val _ = dbgTools.DTH (dpfx^ sth0) val _ = dbgTools.DST (dpfx^ " sth0\n") (*DBG*)*) 347 val sithm = mk_spec_inv_thm ithm nodes env ie mf seth 348 (*val _ = dbgTools.DTH (dpfx^ (sithm)) val _ = dbgTools.DST (dpfx^ "sithm0\n") (*DBG*)*) 349 val sithm = if (is_imp(concl sithm)) 350 then (*MATCH_*)MP sithm (mk_se_thm (fst(dest_imp(concl sithm))) sel) 351 else sithm 352 (*val _ = dbgTools.DTH (dpfx^ (sithm)) val _ = dbgTools.DST (dpfx^ "sithm1\n") (*DBG*)*) 353 val sithm = AP_THM sithm state 354 (*val _ = dbgTools.DTH (dpfx^ (sithm)) val _ = dbgTools.DST (dpfx^ "sithm2\n") (*DBG*)*) 355 val tb = BddEqMp sithm (Option.valOf tb) 356 val _ = dbgTools.DST (dpfx^"cg_ tb cache read done\n") 357 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth1 val _ = upd_cch_env cch ie 358 in tb end 359 else failwith("Internal error: cache_get: Cache has term_bdd but no gen thm") 360 else (* otherwise we have to recompute this tb (however note that no clean subformula will be recomputed) *) 361 if (Option.isSome gth) 362 then let val _ = dbgTools.DST (dpfx^"cg_ recompute SOME gth\n") (*DBG*) 363 val sth = get_spec_thm ie gth_func (Option.valOf gth) mf (* could be an RV *) 364 val tb = tb_func mf sth 365 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth val _ = upd_cch_env cch ie 366 in tb end 367 else let val _ = dbgTools.DST (dpfx^"cg_ recompute NONE gth\n") (*DBG*) 368 val gth = gth_func mf 369 val sth = if (is_RV mf) then gth else ISPEC ie gth 370 (*val _ = with_flag(show_types,true) dbgTools.DTH (dpfx^ gth) 371 val _ = dbgTools.DST (dpfx^ " gth\n") (*DBG*) *) 372 val tb = tb_func mf sth 373 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth 374 val _ = upd_cch_gth cch gth val _ = upd_cch_env cch ie 375 in tb end 376 val _ = dbgTools.DEX dpfx "cg" (*DBG*) 377 in res end 378 379fun get_abthms mf f1 f2 cch = 380 let (*FIXME: don't do the extra work if f1 and f2 are the same *) 381 val abthm = #8(!cch) 382 val abthm = Option.valOf abthm 383 val abthnm = lhs(concl abthm) 384 val mf1 = List.hd(snd(strip_comb mf)) 385 val mf2 = List.last(snd(strip_comb mf)) 386 val cab1 = #8(get_cache_entry mf1 f1) 387 val cab2 = #8(get_cache_entry mf2 f2) 388 val cab1 = Option.valOf cab1 389 val cab1nm = lhs(concl cab1) 390 val cab2 = Option.valOf cab2 391 val cab2nm = lhs(concl cab2) 392 in (abthm,abthnm,mf1,mf2,cab1,cab1nm,cab2,cab2nm) end 393 394fun muCheck_aux ((_,(msa,absf,ksname),_,_,_),(seth,sel,state,ie)) mf vm dp (muAP cch) = 395 let val _ = profTools.bgt (dpfx^"mc_ap")(*PRF*) 396 val tb = cache_get cch ie (mk_ap_tb vm absf) (mk_gen_ap_thm ksname state msa) dp [] mf seth sel state 397 val _ = profTools.ent (dpfx^"mc_ap")(*PRF*) 398 in tb end 399 | muCheck_aux ((_,_,(msr,_,msreq,ee),_,_),(seth,sel,state,ie)) mf vm dp (muRV cch) = 400 let val _ = profTools.bgt (dpfx^"mc_rv")(*PRF*) 401 val tb = cache_get cch ie (mk_rv_tb ee (!cch)) (mk_rv_spec_thm msr seth sel msreq ie ee state (!cch) dp) dp [] 402 mf seth sel state 403 val _ = profTools.ent (dpfx^"mc_rv")(*PRF*) 404 in tb end 405 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muAnd(cch,(f1,f2))) = 406 let 407 val (abthm,abthnm,mf1,mf2,cab1,cab1nm,cab2,cab2nm) = get_abthms mf f1 f2 cch 408 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.And (snd(strip_comb(mf))) vm (f1,f2) dp abthm) 409 (fn mf => GEN ``e:^(ty_antiq(type_of ie))`` 410 (ISPECL [``e:^(ty_antiq(type_of ie))``,cab1nm,cab2nm] 411 (List.nth(msp,3)))) dp [f1,f2] mf seth sel state 412 in tb end 413 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muOr(cch,(f1,f2))) = 414 let 415 val (abthm,abthnm,mf1,mf2,cab1,cab1nm,cab2,cab2nm) = get_abthms mf f1 f2 cch 416 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.Or (snd(strip_comb(mf))) vm (f1,f2) dp abthm) 417 (fn mf => GEN ``e:^(ty_antiq(type_of ie))`` 418 (ISPECL [``e:^(ty_antiq(type_of ie))``,cab1nm,cab2nm] 419 (List.nth(msp,4)))) dp [f1,f2] mf seth sel state 420 in tb end 421 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muNot(cch,f1)) = 422 let 423 val (abthm,abthnm,mf1,_,cabthm,cabthmnm,_,_) = get_abthms mf f1 f1 cch 424 val tb = cache_get cch ie (NotExp (args,(seth,sel,state,ie)) mf1 vm dp f1 abthm) 425 (fn mf => (ISPEC cabthmnm ((CONV_RULE SWAP_VARS_CONV) (List.nth(msp,2))))) dp [f1] mf seth sel state 426 in tb end 427 | muCheck_aux ((msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muTR cch) = 428 cache_get cch ie (mk_con_tb true vm) (fn mf => (List.nth(msp,0))) dp [] mf seth sel state 429 | muCheck_aux ((msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muFL cch) = 430 cache_get cch ie (mk_con_tb false vm) (fn mf => (List.nth(msp,1))) dp [] mf seth sel state 431 | muCheck_aux (args as (_,_,_,(_,Tth,(dmdth,_),_,_),_),(seth,sel,state,ie)) mf vm dp (muDIAMOND(cch,(act,f1))) = 432 let 433 val (abthm,abthnm,_,_,cabthm,cabthmnm,_,_) = get_abthms mf f1 f1 cch 434 val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act false (List.last(snd(strip_comb mf))) 435 vm f1 dp abthm) 436 (mk_gen_modal_thm Tth dmdth) dp [f1] mf seth sel state 437 in tb end 438 | muCheck_aux (args as (_,_,_,(_,Tth,(_,boxth),_,_),_),(seth,sel,state,ie)) mf vm dp (muBOX(cch,(act,f1))) = 439 let 440 val (abthm,abthnm,_,_,cabthm,cabthmnm,_,_) = get_abthms mf f1 f1 cch 441 val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act true (List.last(snd(strip_comb mf))) 442 vm f1 dp abthm) 443 (mk_gen_modal_thm Tth boxth) dp [f1] mf seth sel state 444 in tb end 445 | muCheck_aux (args,(seth,sel,state,ie)) mf vm dp (fpmu(bvch,cch,f1)) = 446 let 447 val rvnm = List.hd(snd(strip_comb mf)) 448 val (abthm,abthnm,mf1,_,cabthm,cabthmnm,_,_) = get_abthms mf f1 f1 cch 449 val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon false vm) vm 450 (bvch,cch,f1) (dp+1) abthm cabthm) (mk_fp_gen_thm state) dp [f1] 451 mf seth sel state 452 in tb end 453 | muCheck_aux (args,(seth,sel,state,ie)) mf vm dp (fpnu(bvch,cch,f1)) = 454 let 455 val rvnm = List.hd(snd(strip_comb mf)) 456 val (abthm,abthnm,mf1,_,cabthm,cabthmnm,_,_) = get_abthms mf f1 f1 cch 457 val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon true vm) vm 458 (bvch,cch,f1) (dp+1) abthm cabthm) (mk_fp_gen_thm state) dp [f1] 459 mf seth sel state 460 in tb end 461 462and NotExp (args,(seth,sel,state,ie)) mf1 vm dp f1 abthm mf sth = 463 let 464 val _ = dbgTools.DEN dpfx "ne" (*DBG*) 465 val tb = BddNot (muCheck_aux (args,(seth,sel,state,ie)) mf1 vm dp f1) 466 val _ = profTools.bgt (dpfx^"mc_neg")(*PRF*) 467 (*val _ = dbgTools.DTM (dpfx^ (getTerm tb)) val _ = dbgTools.DST (dpfx^ " NotExp tb\n") 468 val _ = dbgTools.DTH (dpfx^ sth) val _ = dbgTools.DST (dpfx^ " NotExp sth\n") (*DBG*)*) 469 val sth = PURE_REWRITE_RULE [SYM abthm] sth 470 (*val _ = dbgTools.DTH (dpfx^ sth) val _ = dbgTools.DST (dpfx^ " NotExp sth abbrev\n") (*DBG*)*) 471 val tb2 = BddEqMp sth tb 472 val _ = profTools.ent (dpfx^"mc_neg")(*PRF*) 473 val _ = dbgTools.DEX dpfx "ne" (*DBG*) 474 in tb2 end 475 476and BinExp (args,(seth,sel,state,ie)) opr [t1,t2] vm (f1,f2) dp abthm mf opthm = 477 let 478 val _ = dbgTools.DEN dpfx "be" (*DBG*) 479 (*val _ = dbgTools.DTM (dpfx^ t1) val _ = dbgTools.DST (dpfx^ ("b1\n")) (*DBG*)*) 480 val b1 = muCheck_aux (args,(seth,sel,state,ie)) t1 vm dp f1 481 (*val _ = dbgTools.DTM (dpfx^ t2) val _ = dbgTools.DST (dpfx^ ("b2\n")) (*DBG*)*) 482 val b2 = muCheck_aux (args,(seth,sel,state,ie)) t2 vm dp f2 483 (*val _ = dbgTools.DST (dpfx^ ("bop\n")) (*DBG*)*) 484 val _ = profTools.bgt (dpfx^"mc_bin")(*PRF*) 485 val bb = BddOp(opr,b1,b2) 486 (*val _ = dbgTools.DTM (dpfx^ (getTerm bb)) val _ = dbgTools.DST (dpfx^ " BinExp bb\n") 487 val _ = dbgTools.DTH (dpfx^ opthm) val _ = dbgTools.DST (dpfx^ " BinExp opthm\n") (*DBG*)*) 488 val opthm = PURE_REWRITE_RULE [SYM abthm] opthm 489 (*val _ = dbgTools.DTH (dpfx^ opthm ) val _ = dbgTools.DST (dpfx^ " BinExp opthm abbrev\n") (*DBG*) *) 490 val tb =BddEqMp opthm bb 491 val _ = profTools.ent (dpfx^"mc_bin")(*PRF*) 492 val _ = dbgTools.DEX dpfx "be" (*DBG*) 493 in tb end 494 | BinExp _ _ _ _ _ _ _ _ _ = Raise Match (* impossible, just here to avoid warning *) 495 496and ModalExp (args as (_,_,_,(RTm,_,_,sp,s2sp),_),(seth,sel,state,ie)) actnm isbox t2 vm f1 dp abthm mf sth = 497 let 498 val _ = dbgTools.DEN dpfx "me" (*DBG*) 499 val tb1 = muCheck_aux (args,(seth,sel,state,ie)) t2 vm dp f1 500 val _ = profTools.bgt (dpfx^"mc_mod")(*PRF*) 501 val tb2 = if isbox then BddAppall sp (bdd.Imp, find(RTm,actnm),(BddReplace s2sp tb1)) 502 else BddAppex sp (bdd.And, find(RTm,actnm),(BddReplace s2sp tb1)) 503 val sth = SPEC (hd(snd(strip_comb(getTerm(tb1))))) sth (* TODO: move this to muCheck_aux as with ~,/\,\/ etc*) 504 (*val _ = dbgTools.DTH (dpfx^ sth) val _ = dbgTools.DST (dpfx^ " ModalExp sth\n") (*DBG*)*) 505 val sth = PURE_REWRITE_RULE [SYM abthm] sth 506 (*val _ = dbgTools.DTH (dpfx^ sth) val _ = dbgTools.DST (dpfx^ " ModalExp sth abbrev\n") 507 val _ = dbgTools.DTM (dpfx^ (getTerm tb2)) val _ = dbgTools.DST (dpfx^ " tb2\n") (*DBG*)*) 508 val ttb = BddEqMp (SYM sth) tb2 509 val _ = profTools.ent (dpfx^"mc_mod")(*PRF*) 510 val _ = dbgTools.DEX dpfx "me" (*DBG*) 511 in ttb end 512 513and FixExp ((p_,ap_,rv_,d_, 514 (wfKS_ks,finS,frv_thms,imf_thms,pextth,rvtt,mssth,fps,eus,Ss,ess,statel,ksname,prop_type,ee,qd,sqd,ce,qt,eeq)), 515 (seth,sel,state,ie)) [t1,t2] initbdd vm (bvch,_,f1) dp abthm cabthm mf _ = 516 let (*FIXME: clean up this monster *) 517 val _ = dbgTools.DEN dpfx "fe" (*DBG*) 518 val _ = profTools.bgt (dpfx^"fe")(*PRF*) 519 (*val _ = dbgTools.DTM (dpfx^ t2) val _ = dbgTools.DST (dpfx^ " t2\n") (*DBG*)*) 520 (* note that the binding occurance uses same cache node as the occurances of the bv in the formula *) 521 val (bvtb,bvgth,bvsth,bvenv,bvix,bvrsc,bvithm,bvabthm,ado_subthm,ado_eqthm) = !bvch 522 val bv = (fromHOLstring(t1)) 523 val p_ty = get_prop_type t2 524 val (ttm,initset,imf_t2g,init_thm,abbrev_thm,fp2thm,adogeneqthm,bigthm,chainth,initsubth) = 525 if (bdd.equal (getBdd(initbdd)) (bdd.TRUE)) 526 then (true,Ss,list_mk_comb(get_mu_ty_nu_tm p_ty,[t1,List.last (snd(strip_comb mf))]), 527 GFP_INIT,NU_FP_STATES,STATES_FP_BIGINTER_2,STATES_DEF_SYM_NU,NU_BIGINTER,GEN_GFP_CHAIN, 528 let val jf = (fn _ => (REWRITE_RULE [SYM (List.last (CONJUNCTS (REWRITE_RULE [wfKS_def] wfKS_ks)))] 529 (INST_TYPE [alpha|->type_of state] SUBSET_UNIV))) 530 in mk_lthm (fn _ => (``!s. s SUBSET ^Ss``,jf)) jf end) 531 else (false,ess,list_mk_comb(get_mu_ty_mu_tm p_ty,[t1,List.last (snd(strip_comb mf))]),LFP_INIT,MU_FP_STATES, 532 STATES_FP_BIGUNION_2,STATES_DEF_SYM_MU,MU_BIGUNION,GEN_LFP_CHAIN,EMPTY_SUBSET) 533 (*val _ = dbgTools.DST (dpfx^ (if ttm then "true" else "false")) val _ = dbgTools.DST (dpfx^ " ttm\n") (*DBG*) 534 val _ = dbgTools.DTM (dpfx^ ie) val _ = dbgTools.DST (dpfx^ " ie\n") (*DBG*)*) 535 (* ado: max same_quant nesting depth is 2 and immediate outer bv (if any) has the same fp operator as this one, 536 and the outer bv has not been just reset *) 537 val ado = (sqd andalso (not (List.null qt)) andalso (ttm=List.hd qt)) 538 andalso (not (Term.compare(numSyntax.zero_tm,List.last(snd(strip_comb(snd(dest_comb ie)))))=EQUAL)) 539 val _ = if ado then dbgTools.DST (dpfx^ "ADO active\n") else dbgTools.DST (dpfx^ "no ADO\n") (*DBG*) 540 (* if ado then start from where we left off. ASSERT:ado==>Option.isSome bvtb *) 541 val ((initset,initbdd),init_thm,abbrev_thm) = 542 if (ado) 543 then let val bvt = getTerm(Option.valOf bvtb) 544 (*val _ = dbgTools.DTM (dpfx^ bvt) val _ = dbgTools.DST (dpfx^ " bvt\n") (*DBG*)*) 545 val e = List.nth(snd(strip_comb bvt),2) (* bvt is a MU_SAT term, so e is prev outer env *) 546 (*val _ = dbgTools.DTM (dpfx^ e) val _ = dbgTools.DST (dpfx^ " e\n") (*DBG*)*) 547 val X = get_env_val state t1 e 548 (*val _ = dbgTools.DTM (dpfx^ X) val _ = dbgTools.DST (dpfx^ " X\n") (*DBG*)*) 549 val th = MP (ISPECL [ksname,fst(dest_env e),t1,state,X] GEN_MS_FP_INIT) wfKS_ks 550 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ " initset MS_FP\n") (*DBG*)*) 551 in ((X,BddEqMp th (Option.valOf bvtb)),GEN_FP_INIT, 552 if (ttm) then GEN_NU_FP_STATES else GEN_MU_FP_STATES) end 553 else ((initset,initbdd),init_thm,abbrev_thm) 554 (*val _ = dbgTools.DTM (dpfx^ initset) val _ = dbgTools.DST (dpfx^ " initset\n") (*DBG*) 555 val _ = dbgTools.DTM (dpfx^ (getTerm(initbdd))) val _ = dbgTools.DST (dpfx^ " initbdd\n") (*DBG*) 556 val _ = dbgTools.DTM (dpfx^ imf_t2g) val _ = dbgTools.DST (dpfx^ " imf_t2g\n") (*DBG*)*) 557 (* if ado then we need the old outer env for proving the env legal assumption to the endth *) 558 val imf_t2 = Binarymap.find(imf_thms,imf_t2g) 559 (*val _ = dbgTools.DTH (dpfx^ imf_t2) val _ = dbgTools.DST (dpfx^ " imf_t2\n") (*DBG*) 560 val _ = if not ado then dbgTools.DTH (dpfx^" abbrev_thm\n" abbrev_thm) (*DBG*) 561 else dbgTools.DTH (dpfx^" ADO abbrev_thm\n" abbrev_thm) (*DBG*)*) 562 (* make a term representing the modified environment *) 563 val ie1 = list_mk_comb(eus,[ie,t1,initset]) 564 fun mk_fp n = mk_comb(list_mk_comb(fps,[t2,t1,ksname,ie1]),n) 565 val ie2 = list_mk_comb(eus,[ie,t1,mk_fp numSyntax.zero_tm]) 566 (* create a new RV theorem for this bound var and add it to the spec thms, and add the bv's initbdd to the env *) 567 val new_rv_thm = SYM (MP (ISPECL [t2,ksname,ie,t1,state,initset,numSyntax.zero_tm] MS_FP_INIT) wfKS_ks) 568 (*val _ = dbgTools.DTH (dpfx^ new_rv_thm) val _ = dbgTools.DST (dpfx^ " new_rv_thm\n") (*DBG*)*) 569 val _ = upd_cch_sth bvch new_rv_thm 570 val ix = (Array.length ee) - qd (* index of current bv in ee and rv_thms arrays *) 571 val _ = 572 if (ado) 573 then Array.update(ee,ix,(bv,BddEqMp (SYM(MP (ISPECL [t2,ksname,ie,t1,initset,state] init_thm) wfKS_ks)) 574 initbdd)) 575 else Array.update(ee,ix,(bv,BddEqMp (SYM(MP (ISPECL [t2,ksname,ie,t1,state] init_thm) wfKS_ks)) initbdd)) 576 val ado_subthm' = if sqd then SOME (lift_ado_sub_thm ado ado_subthm t2 ksname ie1 eeq imf_thms abthm 577 wfKS_ks ie t1 initset seth imf_t2 ess Ss eus adogeneqthm initsubth numSyntax.zero_tm) else NONE 578 val _ = profTools.ent (dpfx^"fe")(*PRF*) 579 fun iter ie2 n = (* ee also changes with each iter, but statefully, so no need to pass it in *) 580 let val _ = dbgTools.DST (dpfx^ ("(iter)\n")) (*DBG*) 581 (*val _ = dbgTools.DTM (dpfx^ t1) val _ = dbgTools.DST (dpfx^ "::") 582 val _ = dbgTools.DTM (dpfx^ n) (*DBG*) 583 val _ = dbgTools.DTM (dpfx^ ie2) val _ = dbgTools.DST (dpfx^ " ie2\n") (*DBG*)*) 584 val _ = profTools.bgt (dpfx^"fe")(*PRF*) 585 val eeqthm = if sqd then mk_ado_pre_sub_thm ado ado_subthm t2 ksname ie1 eeq imf_thms abthm wfKS_ks ie t1 586 initset seth imf_t2 ess eus chainth adogeneqthm initsubth 587 (if (Term.compare(n,numSyntax.zero_tm)=EQUAL) then n else rand n) else TRUTH 588 val _ = profTools.ent (dpfx^"fe")(*PRF*) 589 (*val _ = dbgTools.DTH (dpfx^ eeqthm) val _ = dbgTools.DST (dpfx^ " eeqthm\n") (*DBG*)*) 590 val itr = (muCheck_aux ((p_,ap_,rv_,d_,(wfKS_ks,finS,frv_thms,imf_thms,pextth,rvtt,mssth,fps, 591 eus,Ss,ess,statel,ksname,prop_type,ee,qd-1,sqd,ce, 592 ttm::qt,(eeqthm,abthm)::eeq)), 593 (seth,sel,state,ie2)) (List.last (snd(strip_comb mf))) vm dp f1) 594 val _ = profTools.bgt (dpfx^"fe")(*PRF*) 595 val itrtm = getTerm itr 596 val _ = dbgTools.DTM (dpfx^"fe_itrtm") itrtm (*DBG*) 597 val _ = dbgTools.DTM (dpfx^"fe_n") n (*DBG*) 598 val itrthm = (ISPECL [t2,ksname,ie,t1,state,initset,n] MS_FP) 599 val _ = dbgTools.DTH (dpfx^"fe_itrthm") itrthm (*DBG*) 600 val itr = BddEqMp itrthm itr 601 (* if counterexamples/witnesses are turned on, and we are in the outermost fixed point iteration *) 602 val _ = if (Option.isSome (!ce)) andalso ix=0 then ce := SOME (itr::(Option.valOf (!ce))) else () 603 (*val _ = if (Option.isSome (!ce)) andalso ix=0 then (*DBG*) 604 let val _=dbgTools.DST (dpfx^ "CE len") 605 val _=DMSG(ST((int_to_string(List.length(Option.valOf (!ce))))^"\n"))(*DBG*) 606 val _ = DMSG (BD (getBdd itr)) 607 in () end else ()(*DBG*)*) 608 (*val _ = dbgTools.DTM (dpfx^ (getTerm itr)) val _ = dbgTools.DST (dpfx^ " (itr 2)\n") (*DBG*)*) 609 val prevbdd = snd(Array.sub(ee,ix)) 610 (*val _ = DMSG (BD (getBdd prevbdd)) (*DBG*) 611 val _ = dbgTools.DTM (dpfx^ (getTerm prevbdd)) val _ = dbgTools.DST (dpfx^ " prevbdd\n") (*DBG*)*) 612 val _ = profTools.ent (dpfx^"fe")(*PRF*) 613 val res = let 614 val eqq = (bdd.equal (getBdd prevbdd) (getBdd itr)) 615 val tttb = 616 if eqq 617 then let 618 val _ = dbgTools.DST (dpfx^"fe_ iter fin calcs") (*DBG*) 619 val _ = profTools.bgt (dpfx^"fe")(*PRF*) 620 val orac_th = REWRITE_RULE [pextth] (GENL statel (BddThmOracle (BddOp(bdd.Biimp,prevbdd,itr)))) 621 (*val _ = dbgTools.DTH (dpfx^ orac_th) val _ = dbgTools.DST (dpfx^ "oracle thm\n") (*DBG*)*) 622 val endth = 623 if ado 624 then let (*FIXME: ADO stuff not lazified yet *) 625 (*val _ = dbgTools.DTH (dpfx^ cabthm) 626 val _ = dbgTools.DST (dpfx^ " ADO cabthm\n") (*DBG*) 627 val _ = dbgTools.DTH (dpfx^ abthm) 628 val _ = dbgTools.DST (dpfx^ " ADO abthm\n") (*DBG*)*) 629 val imf_t2 = PURE_ONCE_REWRITE_RULE [abthm] imf_t2 630 (*val _ = dbgTools.DTH (dpfx^ imf_t2) 631 val _ = dbgTools.DST (dpfx^ " ADO imf_t2\n") (*DBG*) 632 val _ =DMSG(TH (valOf ado_subthm')) 633 val _ =dbgTools.DST (dpfx^" ADO subthm'") (*DBG*) 634 val _=DMSG(TH(valOf ado_eqthm)) val _=DMSG(ST "ADO eqthm\n")(*DBG*)*) 635 val ado_imfth = Binarymap.find(imf_thms,t2) 636 (*val _ = dbgTools.DTH (dpfx^" ADO ado_imfth\n") ado_imfth) (*DBG*) 637 val _ = dbgTools.DTM (dpfx^ ie) val _ = dbgTools.DST (dpfx^" ADO ie\n")(*DBG*) 638 val _ = dbgTools.DTH (dpfx^" ADO fst hd eeq\n" (fst(hd eeq))) (*DBG*)*) 639 val adoeqthm2 = MATCH_MP SUBSET_TRANS 640 (LIST_CONJ[MATCH_MP EQ_IMP_SUBSET (Option.valOf ado_eqthm), 641 (SPEC (fst (dest_env ie)) 642 (MATCH_MP fp2thm 643 (LIST_CONJ [imf_t2,ado_imfth, 644 wfKS_ks, 645 PURE_ONCE_REWRITE_RULE[adogeneqthm](fst(hd eeq))] 646 )))]) 647 (*val _ = dbgTools.DTH (dpfx^" ADO adoeqthm2\n" adoeqthm2) (*DBG*)*) 648 val sabbrev_thm = ISPECL [t2,ksname,ie,n,t1,initset] abbrev_thm 649 (*val _ =dbgTools.DTH (dpfx^" ADO sabbrev_thm\n" sabbrev_thm) (*DBG*)*) 650 in PURE_ONCE_REWRITE_RULE [SYM abthm] 651 (MP (MP sabbrev_thm (LIST_CONJ [wfKS_ks,imf_t2,finS, 652 Option.valOf ado_subthm'])) adoeqthm2) 653 end 654 else MP (PURE_REWRITE_RULE [SYM abthm] (ISPECL [t2,ksname,ie,n,t1] abbrev_thm)) 655 (LIST_CONJ [wfKS_ks,imf_t2]) 656 (*val _ = dbgTools.DTH (dpfx^ endth) val _ = dbgTools.DST (dpfx^ " endth\n") (*DBG*) 657 val _ = dbgTools.DTH (dpfx^ mssth) val _ = dbgTools.DST (dpfx^ " mssth\n") (*DBG*)*) 658 val t2b = (SYM (PURE_ONCE_REWRITE_RULE [mssth] (AP_THM (MP endth orac_th) state))) 659 (*val _ = dbgTools.DTH (dpfx^ t2b) val _ = dbgTools.DST (dpfx^ " t2b\n") (*DBG*)*) 660 (* make ado eqthm and sub_thm for next round *) 661 val _ = if sqd then 662 let val t2b' = (CONV_RULE (RHS_CONV (RATOR_CONV (PURE_ONCE_REWRITE_CONV [abthm]))) 663 (PEXT (PairRules.PGEN state (BETA_RULE (REWRITE_RULE [IN_DEF,MU_SAT_def] t2b))))) 664 (*val _ = dbgTools.DTH (dpfx^t2b') val _ = dbgTools.DST (dpfx^ " t2b'\n") (*DBG*)*) 665 val ado_eqthm' = CONV_RULE(RHS_CONV(REWRITE_CONV[MP(ISPECL[t2,ksname,ie,t1] bigthm) 666 wfKS_ks])) t2b' 667 (*val _ = dbgTools.DTH (dpfx^ado_eqthm') 668 val _ = dbgTools.DST (dpfx^" ado_eqthm'\n") (*DBG*)*) 669 val _ = upd_cch_eqth bvch ado_eqthm' 670 (* make ado subthm *) 671 val ado_subthm = mk_ado_sub_thm ado (Option.valOf ado_subthm') t2 ksname ie1 eeq 672 imf_thms abthm wfKS_ks ie t1 initset (rator (getTerm prevbdd)) seth 673 imf_t2 ess eus chainth n 674 val _ = upd_cch_subth bvch ado_subthm 675 in () end else () 676 (*val _ = dbgTools.DST (dpfx^ bv) (*DBG*)*) 677 val _ = profTools.ent (dpfx^"fe")(*PRF*) 678 val _ = dbgTools.DST (dpfx^"fe_ iter fin done") (*DBG*) 679 in BddEqMp t2b prevbdd end 680 else let val _ = profTools.bgt (dpfx^"fe")(*PRF*) 681 val ie3 = list_mk_comb(eus,[ie,t1,mk_fp(mk_comb(``SUC``,n))]) 682 val _ = dbgTools.DTM (dpfx^"fe_ie3") ie3 (*DBG*) 683 val _ = Array.update(ee,ix,(bv,itr)) 684 val _ = dbgTools.CBTML (dpfx^"fe_rv_thm_tml") [t2,ie,initset,t1,n] 685 val _ = dbgTools.CBTH (dpfx^"fe_rvtt") rvtt 686 val rv_thm = SYM (SPECL [t2,ie,initset,t1,n] rvtt) 687 val _ = dbgTools.DTH (dpfx^"fe_rv_thm") rv_thm (*DBG*) 688 val _ = upd_cch_sth bvch rv_thm 689 val _ = profTools.ent (dpfx^"fe")(*PRF*) 690 val _ = dbgTools.DST (dpfx^"fe_ iter end") (*DBG*) 691 in iter ie3 ``SUC ^n`` end 692 in tttb end 693 in res end 694 val fpres = iter ie2 numSyntax.zero_tm 695 val _ = dbgTools.DEX dpfx "fe" (*DBG*) 696 in fpres end 697 | FixExp _ _ _ _ _ _ _ _ _ _= Raise Match (* impossible, just here to avoid warning *) 698 699(* init the model *) 700fun init_model I1 T1 state vm Ric = 701 let val (apl,ks_def,wfKS_ks,RTm,ITdf) = mk_wfKS I1 T1 NONE state vm Ric NONE NONE NONE 702 in (apl,ks_def,wfKS_ks,RTm,ITdf) end 703 704(* init model dependent data structures and theorems *) 705fun init_thms (apl,ks_def,wfKS_ks) T1 state vm Ric absf = (*FIXME: this becomes very slow for alu 2x2*) 706 let 707 val _ = dbgTools.DEN dpfx "it" (*DBG*) 708 val ksname = lhs(concl ks_def) 709 val (prop_ty,st_ty) = get_types ksname 710 val st_set_ty = st_ty --> bool 711 val state' = mk_primed_state state 712 val (st,st') = (strip_pair##strip_pair) (state,state') 713 val s2s' = List.map (fn(v,v') => (BddVar true vm v,BddVar true vm v')) (ListPair.zip(st,st')) 714 val f_ty = ``:^(prop_ty) mu`` 715 val env_ty = string_ty --> st_ty --> bool 716 val ks_ty = type_of ksname 717 val eus = ``ENV_UPDATE:^(ty_antiq(env_ty --> string_ty --> st_set_ty --> env_ty))`` 718 val fps = ``FP:^(ty_antiq(f_ty --> string_ty --> ks_ty --> env_ty --> ``:num`` --> st_ty --> bool))`` 719 val Ss = mk_comb(``KS_S:^(ty_antiq(ks_ty --> st_ty --> bool))``,ksname) 720 val ess = ``{}:^(ty_antiq(st_set_ty))`` 721 val (msp,msa,Tth,(dmdth,boxth),githms) = mk_gen_thms T1 (apl,ks_def,wfKS_ks) state state' st vm 722 val mssth = GSYM (SIMP_RULE std_ss [IN_DEF] MU_SAT_def) 723 val jf = (fn _ => (GENL [``f:^(ty_antiq(f_ty))``,``e:^(ty_antiq(env_ty))``, 724 ``X:^(ty_antiq(st_set_ty))``,``Q:string``,``n:num``] 725 (ISPEC state (GENL [``s:^(ty_antiq(st_ty))``] 726 (SPEC_ALL (MATCH_MP (SIMP_RULE std_ss [MS_FP] (GEN_ALL (SIMP_RULE std_ss [ENV_UPDATE] 727 (ISPECL [``f:(^(ty_antiq(f_ty)))``,``Q:string``,``ks:^(ty_antiq(type_of ksname))``, 728 ``e[[[Q<--X]]]:(^(ty_antiq(env_ty)))``] SAT_RV_ENV_SUBST)))) wfKS_ks)))))) 729 val rvtt = mk_lthm (fn _ => 730 (list_mk_forall([``f:^(ty_antiq(f_ty))``,``e:^(ty_antiq(env_ty))``,``X:^(ty_antiq(st_set_ty))``, 731 ``Q:string``,``n:num``], 732 mk_eq(``MU_SAT (RV Q) ^ksname e[[[Q<--FP f Q ^ksname e[[[Q<--X]]] (SUC n)]]] ^state``, 733 ``FP f Q ^ksname e[[[Q<--X]]] (SUC n) ^state``)),jf)) jf 734 val _ = dbgTools.DTH (dpfx^"it_rvtt") rvtt (*DBG*) 735 val pextth = GSYM (CONV_RULE (STRIP_QUANT_CONV (RHS_CONV commonTools.lzELIM_TUPLED_QUANT_CONV)) 736 (ONCE_REWRITE_RULE [(lzGEN_PALPHA_CONV state (rhs(concl(SPEC_ALL(INST_TYPE 737 [alpha|->st_ty,beta |->bool] FUN_EQ_THM)))))] 738 (INST_TYPE [alpha |-> st_ty, beta |-> bool] FUN_EQ_THM))) 739 val _ = dbgTools.DTH (dpfx^"it_pextth") pextth (*DBG*) 740 val fS = mk_comb (inst [alpha |-> type_of state] pred_setSyntax.finite_tm,mk_ks_dot_S ksname) 741 val jf = fn _ => (prove(fS(*``FINITE (^ksname).S``*),PROVE_TAC [wfKS_def,wfKS_ks, 742 BOOLVEC_UNIV_FINITE_CONV (List.length st)])) 743 val finS = mk_lthm (fn _ => (fS(*``FINITE (^ksname).S``*),jf)) jf 744 val _ = dbgTools.DEX dpfx "it" (*DBG*) 745 in ((msp,(msa,absf,ksname), (Tth,(dmdth,boxth),st',s2s'),(finS,pextth,rvtt,mssth,fps,eus,Ss,ess,st,prop_ty)), 746 state,githms) 747 end 748 749(* init data structures and theorems that depend on the property and environment *) 750fun init_prop (nf,mf) ee ksname state wfKS_ks vm githms msp prop_ty = 751 let val _ = dbgTools.DEN dpfx "ip" (*DBG*) 752 val mf = inst [alpha |-> prop_ty] mf (* it is possible that mf 's type var has not been instantiated *) 753 val sqd = ((sameq_depth mf)=2) (* whether or not ado will be enabled at all *) 754 val rvl = Array.foldr (fn((rv,tb),l)=> (rv,getTerm tb)::l) [] ee 755 val st_ty = type_of state 756 val f_ty = ``:^(prop_ty) mu`` 757 val env_ty = list_mk_fun([string_ty,st_ty],bool) 758 val ie = if (List.null rvl) then (``EMPTY_ENV:^(ty_antiq(env_ty))``) else mk_env rvl state 759 val _ = profTools.bgt (dpfx^"init_prop_rv")(*PRF*) 760 val (msr,(seth,sel),msreq) = mk_gen_rv_thms mf ksname state rvl ie wfKS_ks 761 val _ = profTools.ent (dpfx^"init_prop_rv")(*PRF*) 762 val _ = profTools.bgt (dpfx^"init_prop_imf")(*PRF*) 763 (*val _ = prove (``IMF ^mf``, REWRITE_TAC ([IMF_def,MU_SUB_def,NNF_def,RVNEG_def]@(tsimps "mu") @ sel)) *) 764 val _ = if is_valid mf then () else failwith ("Bound variable occurs negatively:"^(term_to_string mf)) 765 val _ = profTools.ent (dpfx^"init_prop_imf")(*PRF*) 766 val qd = qdepth mf 767 val ee2 = Array.array((Array.length ee)+qd,("dummy",BddCon true vm)) 768 val _ = Array.copy {src=ee,dst=ee2,di=0} 769 (*val tmr2 = Timer.startRealTimer()(*PRF*)*) 770 val (mfml,imf_thms,frv_thms) = mk_cache ee ie (nf,mf) mf qd githms state (seth,sel) msp 771 (*val _ = Binarymap.app (fn (k,v) => let val _ = dbgTools.DTM (dpfx^ k) (*DBG*) 772 val _ = dbgTools.DST (dpfx^ " key\n") (*DBG*) 773 val _ = dbgTools.DTH (dpfx^ v) (*DBG*) 774 val _ = dbgTools.DST (dpfx^ " v\n") (*DBG*) 775 in () end) frv_thms val _ = dbgTools.DST (dpfx^ " frv_thms\n") (*DBG*)*) 776 val _ = profTools.bgt (dpfx^"init_prop_adoimf")(*PRF*) 777 val imf_thms = mk_ado_imf_thms mf seth (tsimps ``:'a mu``) frv_thms imf_thms 778 val _ = profTools.ent (dpfx^"init_prop_adoimf")(*PRF*) 779 (*val _ = Binarymap.app (fn (k,v) => let val _ = dbgTools.DTM (dpfx^k) (*DBG*) 780 val _ = dbgTools.DST (dpfx^ " key\n") (*DBG*) 781 val _ = dbgTools.DTH (dpfx^ v) (*DBG*) 782 val _ = dbgTools.DST (dpfx^ " v\n") (*DBG*) 783 in () end) imf_thms val _ = dbgTools.DST (dpfx^ " imf_thms\n") (*DBG*)*) 784 (*val _ = dbgTools.DST (dpfx^ (Time.toString(Timer.checkRealTimer tmr2))) (*PRF*) *) 785 val _ = dbgTools.DEX dpfx "ip" (*DBG*) 786 in (ie,(msr,seth,sel,msreq,ee2),mfml,imf_thms,frv_thms,qd,sqd,mf) end 787 788(* init data structures and theorems used by model checker *) 789fun init I1 T1 state vm Ric ce (nf,mf) ee absf {ks=model_data,th=init_data} = 790 let val _ = dbgTools.DEN dpfx "init" (*DBG*) 791 val _ = profTools.bgt (dpfx^"init")(*PRF*) 792 val _ = profTools.bgt (dpfx^"init_mod")(*PRF*) 793 val (apl,ks_def,wfKS_ks,RTm,ITdf) = if Option.isSome model_data then Option.valOf model_data 794 else init_model I1 T1 state vm Ric 795 val _ = profTools.ent (dpfx^"init_mod")(*PRF*) 796 val _ = if Option.isSome init_data then dbgTools.DST (dpfx^"init_ isSome") (*DBG*) 797 else dbgTools.DST (dpfx^"init_ no init data")(*DBG*) 798 val _ = profTools.bgt (dpfx^"init_thm")(*PRF*) 799 val ((msp,(msa,absf,ksname),(Tth,(dmdth,boxth),st',s2s'), 800 (finS,pextth,rvtt,mssth,fps,eus,Ss,ess,st,prop_ty)),state,githms) = 801 if Option.isSome init_data then Option.valOf init_data else init_thms (apl,ks_def,wfKS_ks) T1 state vm Ric absf 802 val _ = profTools.ent (dpfx^"init_thm")(*PRF*) 803 val _ = profTools.bgt (dpfx^"init_prop")(*PRF*) 804 val (ie,(msr,seth,sel,msreq,ee2),mfml,imf_thms,frv_thms,qd,sqd,mf) = 805 init_prop (nf,mf) ee ksname state wfKS_ks vm githms msp prop_ty 806 val _ = profTools.ent (dpfx^"init_prop")(*PRF*) 807 val ce = if not (Option.isSome (!ce)) andalso is_existential mf 808 then ref (SOME []) else ce (*turn on witness trace if existential mf*) 809 val _ = profTools.ent (dpfx^"init")(*PRF*) 810 val _ = dbgTools.DEX dpfx "init" (*DBG*) 811 in ({ks=SOME (apl,ks_def,wfKS_ks,RTm,ITdf),th=SOME((msp,(msa,absf,ksname),(Tth,(dmdth,boxth),st',s2s'), 812 (finS,pextth,rvtt,mssth,fps,eus,Ss,ess,st,prop_ty)),state,githms)}, 813 (msp, 814 (msa,absf,ksname), 815 (msr,seth,msreq,ee2), 816 (RTm,Tth,(dmdth,boxth),st',s2s'), 817 (wfKS_ks,finS,frv_thms,imf_thms,pextth,rvtt,mssth,fps,eus,Ss,ess,st,ksname,prop_ty,ee2,qd,sqd,ce,[],[])), 818 (ks_def,mf,seth,sel,ie,mfml,frv_thms,ce)) 819 end 820 821(* make final adjustments to result of model checking run 822 such as unwinding any contractions and other syntactic rearrangements of the formula *) 823fun finish tb frv_thms = 824 let 825 val _ = dbgTools.DEN dpfx "fin" (*DBG*) 826 val unfrv = BddApConv (ONCE_REWRITE_CONV [frv_find frv_thms (List.hd(snd(strip_comb(getTerm tb))))]) tb 827 val _ = dbgTools.DEX dpfx "fin" (*DBG*) 828 in unfrv end 829 830(* given the list of top-level approximations, find a path through them and return it as a trace *) 831(* see 31 July 2005 notes on how this works *) 832(* FIXME: a more readable trace would only print out those AP's that are talked about in the corresponding property *) 833(* FIXME: need to extend this to work with properties other than EF f (i.e. EG f) 834 problem with EG is that right now it will giv the shortest path it can find, whereas I feel that 835 for EG the longest path is what is needed *) 836(* FIXME: in amba_ahb, the ctl_grant2 property will fail if the outer EF is replaced by AG 837 that is fine. however, the ce computation fails because the last outermost approximation does not contain 838 any initial state. This is not possible in theory, so points to some problem with the ce machinery*) 839fun makeTrace mf state vm mu_init_data ce Itb = 840 let val _ = dbgTools.DEN dpfx "mt" (*DBG*) 841 val _ = dbgTools.DTM (dpfx^"mt_state") state (*DBG*) 842 val vmc = List.foldl (fn (v,bm) => Binarymap.insert(bm,v,Binarymap.find(vm,v))) (Binarymap.mkDict String.compare) 843 (List.map term_to_string2 (strip_pair state)) 844 val _ = List.app (fn (k,v) => dbgTools.DST (dpfx^"mt_vmc:"^(k^","^(int_to_string v)))) (Binarymap.listItems vmc) 845 val cel = Option.valOf (!ce) 846 val Ib = getBdd Itb 847 val _ = dbgTools.DBD (dpfx^"mt_Ib") Ib(*DBG*) 848 val _ = List.app (dbgTools.DBD (dpfx^"mt_cel") o getBdd) cel(*DBG*) 849 val _ = dbgTools.DNM (dpfx^"mt_cel_sz") (List.length cel)(*DBG*) 850 val gfp = is_nu (NNF mf) 851 val res = 852 if (List.length cel <= 1) 853 then (*no outermost fp (|cel|=0) or the outermost fp comp terminated immediately (|cel|=1), 854 so tr is empty: any initial state is the ce *) 855 [pt_bdd2state state vmc (bddTools.mk_pt Ib vmc)] 856 else let 857 val trbl = List.map getBdd (List.tl cel) (* list of outermost fp computation's approximations *) 858 val _ = dbgTools.DNM (dpfx^"mt_trbl_sz") (List.length trbl)(*DBG*) 859 val _ = List.app (dbgTools.DBD (dpfx^"mt_trbl")) trbl(*DBG*) 860 val Rb = getBdd(Binarymap.find(#4(Option.valOf (#ks(mu_init_data))),".")) (*#4 is RTm*) 861 fun has_to b1 b2 = (* those states in b1 that have a transition to b2 *) 862 let val im = bddTools.mk_next state Rb vm b1 (* image of b1 under R. *) 863 (*preimg of img cut to b2 is all source states *) 864 val pi = bddTools.mk_prev state Rb vm (bdd.AND(im,b2)) (* FIXME: is im superfluous here? *) 865 in bdd.AND(pi,b1) end (* cut down source states to the ones in b1 *) 866 fun mk_tr (apx::trl) prev = (* trace out a path of transitions over trbl *) 867 if not (isSome prev) 868 then let val prev = if gfp 869 then SOME (bddTools.mk_pt Ib vmc) 870 else if not (bdd.equal bdd.FALSE (bdd.AND(apx,Ib))) 871 then SOME (bddTools.mk_pt (bdd.AND(apx,Ib)) vmc) 872 else NONE 873 in if isSome prev 874 then (valOf prev)::mk_tr (apx::trl) prev 875 else mk_tr trl prev 876 end 877 else if (List.length trl)=1 878 then if gfp then [] 879 else (bddTools.mk_pt (hd trl) vmc)::[] 880 else let val napx = 881 if gfp then bdd.DIFF(hd trl,apx) 882 else bdd.DIFF(hd trl,List.nth(trl,1)) 883 in (*next state on the trace*) 884 let val s1 = mk_pt (bdd.AND(napx,bddTools.mk_next state Rb vm (valOf prev))) vmc 885 in s1::(mk_tr trl (SOME s1)) end 886 end 887 | mk_tr [] prev = Raise Match (* this should not happen. Put here to avoid compiler warning *) 888 val tr = if (List.length trbl)=1 889 then let val s1 = bddTools.mk_pt Ib vmc in [s1](*::(mk_tr trbl s1)*) end 890 (*bddTools.mk_pt (List.hd trbl) vmc] *) 891 else mk_tr trbl NONE 892 (*let val s1 = bddTools.mk_pt (bdd.AND(List.hd trbl,Ib)) vmc 893 in s1::(mk_tr (List.tl trbl) s1) end *) 894 val _ = List.app (dbgTools.DBD (dpfx^"mt_tr")) tr(*DBG*) 895 val trace = List.map (pt_bdd2state state vmc) tr 896 val _ = List.app (dbgTools.DTM (dpfx^"mt_trace")) trace(*DBG*) 897 in trace end 898 val _ = dbgTools.DEX dpfx "mt" (*DBG*) 899 in res end 900 901 902 (* (* no outgoing trans from current ce so return this *) 903 if bdd.equal bdd.FALSE (has_to prev napx) 904 then [] 905 else*) 906 907(* try and prove that M |= f i.e. initial states are contained in the term-bdd returned by muCheck *) 908fun checkResult tb mf ks_def (I1,Itb,ITdf) state ie vm = 909 let 910 val _ = dbgTools.DEN dpfx "cr" (*DBG*) 911 val ksname = lhs(concl ks_def) 912 val _ = dbgTools.DTB (dpfx^"cr_tb") tb (*DBG*) 913 val _ = dbgTools.DBD (dpfx^"cr_tb_bdd") (getBdd tb) (*DBG*) 914 (*val _ = dbgTools.DTM (dpfx^ (getTerm tb)) val _ = dbgTools.DST (dpfx^ " tb\n") (*DBG*) 915 val _ = List.app (fn t => let val _ = dbgTools.DTM (dpfx^ t) val _ = dbgTools.DST (dpfx^" tb assum\n") in () end) 916 (HOLset.listItems (getAssums tb))(*DBG*)*) 917 val Itb = if Option.isSome Itb then Option.valOf Itb else BddEqMp (SYM (fst (valOf ITdf))) (t2tb vm I1) 918 val _ = dbgTools.DTB (dpfx^"cr_Itb") Itb (*DBG*) 919 val _ = dbgTools.DBD (dpfx^"cr_Itb_bdd") (getBdd Itb) 920 val sIth = CONV_RULE (RHS_CONV (ONCE_REWRITE_CONV [GSYM SPECIFICATION])) 921 (lzPBETA_RULE (AP_THM (SYM (lzPBETA_RULE 922 (let val jf = (fn _ => (SIMP_CONV std_ss [KS_accfupds,combinTheory.K_DEF,ks_def] 923 (mk_ks_dot_S0 ksname))) 924 in mk_lthm (fn _ => (mk_eq((mk_ks_dot_S0 ksname), 925 getS0 (rhs(concl ks_def))),jf)) jf 926 end))) 927 state)) 928 val _ = dbgTools.DTH (dpfx^"cr_sIth") sIth (*DBG*) 929 val Itb2 = BddEqMp sIth Itb 930 val _ = dbgTools.DTB (dpfx^"cr_Itb2") Itb2 (*DBG*) 931 val Itb3 = (BddOp(bdd.Imp,Itb2,tb)) 932 val _ = dbgTools.DTB (dpfx^"cr_Itb3") Itb3 (*DBG*) 933 val _ = dbgTools.DBD (dpfx^"cr_Itb3_bdd") (getBdd Itb3) 934 (*val _ = dbgTools.DTM (dpfx^ (getTerm Itb3)) val _ = dbgTools.DST (dpfx^ " Itb3\n") (*DBG*) 935 val _ = List.app (fn t=> let val _= dbgTools.DTM (dpfx^t) val _ = dbgTools.DST (dpfx^" Itb3 assum\n") in () end) 936 (HOLset.listItems (getAssums Itb3))(*DBG*)*) 937 val tb1 = BddForall (strip_pair state) Itb3 938 (*val _ = dbgTools.DTM (dpfx^ (getTerm tb1)) val _ = dbgTools.DST (dpfx^ " tb1\n") (*DBG*)*) 939 val mms = CONV_RULE (RHS_CONV lzELIM_TUPLED_QUANT_CONV) (CONV_RULE (RHS_CONV (lzGEN_PALPHA_CONV state)) 940 (ISPECL [mf,ksname,ie] MU_MODEL_SAT_def)) 941 val _ = dbgTools.DTH (dpfx^"cr_mms") mms (*DBG*) 942 val tb2 = BddEqMp (SYM mms) tb1 943 val _ = dbgTools.DTB (dpfx^"cr_tb2") tb2 (*DBG*) 944 val _ = dbgTools.DBD (dpfx^"cr_tb2_bdd") (getBdd tb2) 945 val tbth = SOME (BddThmOracle tb2) handle ex => NONE (* exception means failure *) 946 val _ = dbgTools.DEX dpfx "cr" (*DBG*) 947 in (tbth,SOME Itb) end 948 949(* T1 is map from name of action -> corresponding term (of the action considered as a transition relation) 950 ee is 'environment' i.e. vector of (RV, corresponding termbdd) pairs (termbdd is of set of states assigned to this RV) 951 I is thm def of init state needed to compute the varsets for BddRules.BddExistsAnd, and termbdd replacement op 952 mf is the mu formula to be checked 953 absf is an optional abstraction function 954 OUT: termbdd of set of states satisfying mf, success theorem, ce/witness trace, cache of reusable stuff *) 955fun muCheck ee I1 T1 state vm Ric ce (absf,Itb) ic (nf,mf) = 956 let val _ = dbgTools.DEN dpfx "mc" (*DBG*) 957 val _ = profTools.bgt (dpfx^"mc")(*PRF*) 958 val (ic,init_stuff,(ks_def,mf,seth,sel,ie,mfml,frv_thms,ce')) = init I1 T1 state vm Ric ce (nf,mf) ee absf ic 959 val tb = muCheck_aux (init_stuff,(seth,sel,state,ie)) mf vm ((Array.length ee)-1) mfml 960 val res_tb = finish tb frv_thms 961 val (res_thm,Itb) = if Option.isSome (!ce) 962 then (NONE,Itb) (* in ce gen mode, so result is unimportant *) 963 else checkResult res_tb mf ks_def (I1,Itb,#5(valOf(#ks(ic)))) state ie vm 964 val _ = profTools.ent (dpfx^"mc")(*PRF*) 965 val trace = get_trace ce ce' res_thm ic ee I1 T1 state vm Ric (absf,Itb) ic (nf,mf) 966 val _ = dbgTools.DEX dpfx "mc" (*DBG*) 967 in ((res_tb,res_thm,trace),ic) end (* ic can then be passed in as ic next time *) 968 969(* find counterexample/create witness... *) 970(* FIXME: only tested for AG/EF properties so far, probably needs fixing to work for other properties *) 971(* FIXME thmfy the returned list ... right now a buggy HolCheck can announce false counterexamples *) 972(* FIXME will this work if ce is a loop i.e. if some initial state is reachable from a non-initial one? *) 973and get_trace ce ce' res_thm ic Ree I1 T1 state vm Ric (absf,Itb) mu_init_data (nf,mf) = 974 let 975 val _ = dbgTools.DEN dpfx "gc" (*DBG*) 976 val trace = if Option.isSome (!ce) 977 then NONE (* already in ce mode, called from previous get_trace, which will now use the ref ce *) 978 else 979 if is_universal mf 980 then 981 if Option.isSome res_thm then NONE 982 else if is_traceable (NNF mf) 983 then let val ce = ref (SOME []) (* compute counterexample *) 984 (* model check the neg of f and save all top-level approximations in the ref ce*) 985 val _ = muCheck Ree I1 T1 state vm Ric ce (absf,Itb) mu_init_data 986 (nf^"trace",(NNF(mu_neg mf))) 987 val trace = makeTrace mf state vm mu_init_data ce (valOf Itb) 988 in SOME trace end 989 else NONE (* universal but ce not computable*) 990 else 991 if Option.isSome res_thm andalso is_traceable (NNF mf) 992 then SOME(makeTrace mf state vm ic ce' (valOf Itb))(*return witness*) 993 else NONE (* existential but false or untraceable, so no witness *) 994 val _ = dbgTools.DEX dpfx "gc" (*DBG*) 995 in trace end 996 997 998(* FIXME: uncomment once trace gen is fixed. 999(* get trace and convert to trace of action names*) 1000fun findTraceNames RTm Ree I1 T1 state vm Ric mf (absf,Itb) mu_init_data = 1001 let val tr = get_ce Ree I1 T1 state vm Ric (absf,Itb) mu_init_data mf 1002 val RTm = #4(Option.valOf (#ks(mu_init_data))) 1003 val (actns,dotactn) = List.partition (fn (nm,_) => not (String.compare(nm,".")=EQUAL)) (Binarymap.listItems RTm) 1004 val (acts,acttbl) = ListPair.unzip (actns@dotactn) (* thus giving "." action last priority when pattern matching*) 1005 val (s,sp) = (strip_pair ## strip_pair) (state,mk_primed_state state) 1006 val (stb,sptb) = ListPair.unzip(ListPair.map (fn (s,sp) => (BddVar true vm s,BddVar true vm sp)) (s,sp)) 1007 fun findact (v,vp) = 1008 let val (vl,vpl) = (strip_pair ## strip_pair) (v,vp) 1009 val (vtb,vptb) = ListPair.unzip(ListPair.map (mk_con_tb_tm vm ## mk_con_tb_tm vm) (vl,vpl)) 1010 val assl = ListPair.zip(stb@sptb,vtb@vptb) 1011 val (acts,restbs) = ListPair.unzip(ListPair.map (I ## (BddRestrict assl)) (acts,acttbl)) 1012 val actl = List.filter (fn (nm,tb) => bdd.equal bdd.TRUE (getBdd tb)) (ListPair.zip(acts,restbs)) 1013 val (nm,_) = ListPair.unzip actl 1014 in List.hd nm end 1015 val tr2 = List.map findact (threadlist tr) 1016 in tr2 end 1017*) 1018 1019end 1020end 1021