1structure ctlTools = 2struct 3 4local 5 6open Globals HolKernel Parse 7 8open bossLib 9open pairTheory 10open pred_setTheory 11open pred_setLib 12open stringLib 13open listTheory 14open simpLib 15open pairSyntax 16open pairLib 17open PrimitiveBddRules 18open DerivedBddRules 19open Binarymap 20open PairRules 21open pairTools 22open setLemmasTheory 23open boolSyntax 24open Drule 25open Tactical 26open Conv 27open Rewrite 28open Tactic 29open bddTools 30open stringBinTree 31open ctlTheory 32open boolTheory 33open ksTheory 34open ksTools 35open commonTools 36open lzPairRules 37open lazyTools 38 39val dpfx = "cto_" 40 41in 42 43(* attempt to prove R1 is total by confirming that term-bdd for !s . ?s'. R(s,s') is true. *) 44(* this raises an exception if R1 is not total. totalisation is done elsewhere (see totalise and mk_ctlKS below) *) 45(* ASSERT: Rtb's term is just R(s,s') *) 46fun total_CONV R1 state Rtb = 47 let val _ = dbgTools.DEN dpfx "tC" (*DBG*) 48 val state' = mk_primed_state state 49 val (st,st') = (strip_pair##strip_pair) (state,state') 50 val tb = BddForall st (BddExists st' Rtb) 51 val th1 = BddThmOracle tb handle ex => (dbgTools.DEX dpfx "tC"; raise ex) 52 val th2 = CONV_RULE (RHS_CONV (STRIP_QUANT_CONV commonTools.ELIM_TUPLED_QUANT_CONV)) 53 (commonTools.ELIM_TUPLED_QUANT_CONV (mk_pforall(state,mk_pexists(state',R1))))(*mk_comb( rator(getTerm Rtb), 54 mk_pair(state,state'))))))*) 55 val th3 = PURE_ONCE_REWRITE_RULE [SYM th2] th1 56 val th4 = CONV_RULE (RHS_CONV (GEN_PALPHA_CONV state)) (CONV_RULE (RHS_CONV (QUANT_CONV (GEN_PALPHA_CONV state'))) 57 (ISPEC (mk_pabs(mk_pair(state,state'),R1)) TOTAL_def)) 58 val th5 = PURE_ONCE_REWRITE_RULE [PBETA_CONV (snd(dest_pexists(snd(dest_pforall(rhs(concl th4))))))] th4 59 val th6 = PURE_ONCE_REWRITE_RULE [SYM th5] th3 60 val _ = dbgTools.DEX dpfx "tC" (*DBG*) 61 in th6 end 62 63(* Convert map from names to terms to names to term_bdds. 64 NOTE: the use of termToTermBddFun requires that the term argument not contain any uninterpreted constants. 65 T is a (string * term) list where each pair is (action name, corresponding transition relation) 66 vm is term_bdd varmap 67 OUT: a map : name of action -> termbdd of corresponding transition relation also add the dot action 68 FIXME: fix NOTE issue above *) 69fun RmakeTmap T vm Ric = 70 let fun makeR (h::t) mp = makeR t (insert(mp,(fst h), 71 DerivedBddRules.GenTermToTermBdd (!DerivedBddRules.termToTermBddFun) vm (snd h))) 72 | makeR [] mp = mp 73 val mp = mkDict String.compare 74 val U_T = if Ric then list_mk_conj(snd(unzip T)) else list_mk_disj(snd(unzip T)) 75 val Tmap = makeR T mp 76 in insert(Tmap,".",DerivedBddRules.GenTermToTermBdd (!DerivedBddRules.termToTermBddFun) vm (U_T)) end 77 78(* return totalised version of transition relation with proof, as well as appropriately modified term-bdd *) 79fun totalise state state' total_tm Rtb vm R1 = 80 let val _ = dbgTools.DEN dpfx "tot" (*DBG*) 81 val (s,sp) = (strip_pair##strip_pair) (state,state') 82 val self = list_mk_conj(List.map (fn v => mk_eq(mk_bool_var (v^"'"),mk_bool_var v)) (List.map term_to_string s)) 83 val tbt = BddNot(BddExists sp Rtb) (* terminal states*) 84 val _ = profTools.bgt (dpfx^"tot_tbl")(*PRF*) 85 val tbl = BddConv(PURE_ONCE_REWRITE_CONV[REWRITE_CONV[GEN_ALL(SYM PAIR_EQ)]self])(t2tb vm self)(* all states have self loops*) 86 val _ = profTools.ent (dpfx^"tot_tbl")(*PRF*) 87 val tbtl = BddOp(bdd.And,tbt,tbl) (* terminal states with self loops *) 88 val _ = dbgTools.DTB (dpfx^"tot_ tbtl") tbtl (*DBG*) 89 val _ = dbgTools.DTM (dpfx^"tot_ pexists state' Rtb") (mk_pexists(state',getTerm Rtb)) (*DBG*) 90 val _ = profTools.bgt (dpfx^"tot_Rt2")(*PRF*) 91 val Rtb2 = BddConv (PURE_ONCE_REWRITE_CONV [SYM (commonTools.lzELIM_TUPLED_QUANT_CONV (mk_pexists(state',getTerm Rtb)))]) 92 (BddOp(bdd.Or,Rtb,tbtl)) 93 val _ = profTools.ent (dpfx^"tot_Rt2")(*PRF*) 94 val _ = dbgTools.DTB (dpfx^"tot_ Rtb2") Rtb2 (*DBG*) 95 val _ = dbgTools.DTM (dpfx^"tot_ R1") R1 (*DBG*) 96 val R1t = getTerm Rtb2 (* new totalised transition relation*) 97 val _ = profTools.bgt (dpfx^"tot_th")(*PRF*) 98 val jf = (fn _ => lzPBETA_RULE 99 (CONV_RULE (RAND_CONV (lzGEN_PALPHA_CONV (mk_pair(state,state'))))(* proof R1t is total*) 100 (CONV_RULE(RAND_CONV(lzPABS_CONV(RAND_CONV (LAND_CONV (RAND_CONV(lzGEN_PALPHA_CONV state')))))) 101 (ISPEC (mk_pabs(mk_pair(state,state'),R1)) TOTAL_THM)))) 102 val totth = mk_lthm (fn _ => (mk_comb(total_tm,mk_pabs(mk_pair(state,state'),R1t)),jf)) jf 103 val _ = profTools.ent (dpfx^"tot_th")(*PRF*) 104 val _ = dbgTools.DTH (dpfx^"tot_ totth") totth (*DBG*) 105 val _ = dbgTools.DEX dpfx "tot" (*DBG*) 106 in (R1t,totth,Rtb2) end 107 108(* create ks:('prop,'state) kripke_structure, making sure R is total (totalise if necessary); also return tb of R for model checker*) 109fun mk_ctlKS I1 R1 RTm state apl vm ksname = 110 let 111 val _ = dbgTools.DEN dpfx "mc" (*DBG*) 112 val state' = mk_primed_state state 113 val Ric = is_conj R1 114 val _ = profTools.bgt (dpfx^"mc_rm")(*PRF*) 115 val RTm = if Option.isSome RTm then Option.valOf RTm else RmakeTmap [(".",R1)] vm Ric 116 val Rtb = Binarymap.find(RTm,".") 117 val _ = profTools.ent (dpfx^"mc_rm")(*PRF*) 118 val _ = profTools.bgt (dpfx^"mc_totc")(*PRF*) 119 val totth = total_CONV R1 state Rtb handle ex => TRUTH 120 val _ = profTools.ent (dpfx^"mc_totc")(*PRF*) 121 val _ = dbgTools.DTH (dpfx^"mc_ totth1") totth (*DBG*) 122 val _ = dbgTools.DTB (dpfx^"mc_ Rtb3") Rtb (*DBG*) 123 val state_type = type_of state 124 val total_tm = inst [alpha|->state_type,beta|->state_type] (rator(lhs(concl(SPEC_ALL TOTAL_def)))) 125 val _ = profTools.bgt (dpfx^"mc_tot")(*PRF*) 126 val (R1t,totth,Rtb) = if (Term.compare(concl(totth),T)=EQUAL) then totalise state state' total_tm Rtb vm R1 else (R1,totth,Rtb) 127 val _ = profTools.ent (dpfx^"mc_tot")(*PRF*) 128 val _ = dbgTools.DTB (dpfx^"mc_ Rtb4") Rtb (*DBG*) 129 val _ = profTools.bgt (dpfx^"mc_kd")(*PRF*) 130 val _ = profTools.bgt (dpfx^"mc_kd_a")(*PRF*) 131 val apl = if (Option.isSome apl) then Option.valOf apl 132 else List.map (fn ap => mk_pabs(state,ap)) (get_APs (mk_conj (R1,I1))) 133 val _ = profTools.ent (dpfx^"mc_kd_a")(*PRF*) 134 val _ = profTools.bgt (dpfx^"mc_kd_r")(*PRF*) 135 val stset_ty = state_type --> bool 136 val avar= mk_var("a",stringSyntax.string_ty) 137 val ins_tm = inst [alpha|->stset_ty] pred_setSyntax.insert_tm 138 val KS_ap = List.foldl (fn (e,ac) => list_mk_comb(ins_tm,[e,ac])(*``^e INSERT ^ac``*)) 139 (inst [alpha|->stset_ty] pred_setSyntax.empty_tm (*``{}``*)) apl 140 val KS_states = inst [alpha|->state_type] pred_setSyntax.univ_tm (*``UNIV``*) 141 val KS_initstates = mk_pabs(state, I1) 142 val pvar = mk_var("p",stset_ty) 143 val KS_valids = list_mk_pabs([state,pvar],mk_comb(pvar,state)) 144 val KS_trans = mk_pabs(mk_pair(state,state'), R1t) 145 val _ = profTools.ent (dpfx^"mc_kd_r")(*PRF*) 146 val _ = profTools.bgt (dpfx^"mc_kd_d")(*PRF*) 147 val kn = if (Option.isSome ksname) then "ctlKS_"^(Option.valOf ksname) else "ctlKS" 148 val ks_ty = mk_thy_type {Tyop="kripke_structure", Thy="ctl", Args=[stset_ty,state_type]} 149 val ksnm = (new_constant(kn,ks_ty); mk_const(kn,ks_ty)) 150 val ks_def = mk_adf kn (ctlSyntax.mk_cks state_type stset_ty ks_ty KS_states KS_initstates KS_trans KS_ap KS_valids ) 151 (*``<| S := ^KS_states; S0:= ^KS_initstates; R := ^KS_trans; P:= ^KS_ap; L:= ^KS_valids |>``*) 152 val _ = profTools.ent (dpfx^"mc_kd_d")(*PRF*) 153 val _ = profTools.ent (dpfx^"mc_kd")(*PRF*) 154 val _ = profTools.bgt (dpfx^"mc_th")(*PRF*) 155 val (totth,Rtb,Rthm,Ithm) = 156 let val _ = profTools.bgt (dpfx^"mc_th_Rth")(*PRF*) 157 val ksR = inst [alpha |-> stset_ty,beta|->state_type] ctlSyntax.ksR_tm 158 val ksdotR_tm = mk_comb(ksR,rhs(concl ks_def)) 159 val ksnmdotR_tm = mk_comb(ksR,lhs(concl ks_def)) 160 val jf = (fn _ => PBETA_RULE (AP_THM (PURE_REWRITE_RULE [SYM ks_def](*mk totth and Rtb in terms of ks.R*) 161 (PURE_REWRITE_CONV [combinTheory.K_THM,kripke_structure_accfupds] 162 ksdotR_tm)) (mk_pair(state,state')))) 163 val Rthm = mk_lthm (fn _ => (mk_eq(mk_comb(ksnmdotR_tm,mk_pair(state,state')),R1t),jf)) jf 164 val _ = profTools.ent (dpfx^"mc_th_Rth")(*PRF*) 165 val _ = dbgTools.DTB (dpfx^"mc_th Rtb1") Rtb (*DBG*) 166 val _ = profTools.bgt (dpfx^"mc_th_Rtb")(*PRF*) 167 val Rtb = BddConv (PURE_ONCE_REWRITE_CONV [SYM Rthm]) Rtb 168 val _ = profTools.ent (dpfx^"mc_th_Rtb")(*PRF*) 169 val _ = dbgTools.DTB (dpfx^"mc_th Rtb2") Rtb (*DBG*) 170 val _ = dbgTools.DTH (dpfx^"mc_th totth") totth (*DBG*) 171 val _ = dbgTools.DTH (dpfx^"mc_th Rthm") Rthm (*DBG*) 172 val _ = profTools.bgt (dpfx^"mc_th_tot")(*PRF*) 173 val jf = (fn _ => CONV_RULE (RAND_CONV lzPETA_CONV) (PURE_ONCE_REWRITE_RULE [SYM Rthm] totth)) 174 val totth = mk_lthm (fn _ => (mk_comb(total_tm,ksnmdotR_tm),jf)) jf 175 val _ = profTools.ent (dpfx^"mc_th_tot")(*PRF*) 176 val _ = dbgTools.DTH (dpfx^"mc_th totth3") totth (*DBG*) 177 val _ = profTools.bgt (dpfx^"mc_th_Ith")(*PRF*) 178 val ksS0 = inst [alpha |-> stset_ty,beta|->state_type] ctlSyntax.ksS0_tm 179 val ksdotS0_tm = mk_comb(ksS0,rhs(concl ks_def)) 180 val ksnmdotS0_tm = mk_comb(ksS0,lhs(concl ks_def)) 181 val jf = (fn _ => PBETA_RULE (AP_THM (PURE_REWRITE_RULE [SYM ks_def](*used by ctl2muks to abbrev I1 to ks.I*) 182 (PURE_REWRITE_CONV [combinTheory.K_THM,kripke_structure_accfupds] 183 ksdotS0_tm)) state)) 184 val Ithm = mk_lthm (fn _ => (mk_eq(mk_comb(ksnmdotS0_tm,state),I1),jf)) jf 185 val _ = profTools.ent (dpfx^"mc_th_Ith")(*PRF*) 186 val _ = dbgTools.DTH (dpfx^"mc_th Ithm") Ithm (*DBG*) 187 in (totth,Rtb,Rthm,Ithm) end (* Rthm is required when translating to mu KS (in ctlCheck) to abbrev R1 to ks.R *) 188 val _ = profTools.ent (dpfx^"mc_th")(*PRF*) 189 val _ = dbgTools.DEX dpfx "mc" (*DBG*) 190 in (apl,ks_def,totth,Binarymap.insert(RTm,".",Rtb),Rthm,Ithm) end 191 192end 193 194end 195