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