1(*--------------------------------------------------------------------------- 2 CTL as a concrete datatype, and valuations. From Daryl Stewart. 3 ---------------------------------------------------------------------------*) 4 5open HolKernel Parse boolLib bossLib 6open pred_setTheory stringTheory 7 8val _ = new_theory "ctl" 9val _ = ParseExtras.temp_loose_equality() 10 11fun mkMySuffix s prec = add_rule 12 {term_name = s, fixity = Suffix prec, 13 pp_elements = [HardSpace 1, TOK s], 14 paren_style = OnlyIfNecessary, 15 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))}; 16 17fun mkMyPrefix s prec = add_rule 18 {term_name = s, fixity = Prefix prec, 19 pp_elements = [TOK s, HardSpace 1], 20 paren_style = OnlyIfNecessary, 21 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))}; 22 23fun mkMyInfixAlias t s prec = add_rule 24 {term_name = t, fixity = Infix (HOLgrammars.RIGHT, prec), 25 pp_elements = [HardSpace 1, TOK s, BreakSpace(1,0)], 26 paren_style = OnlyIfNecessary, 27 block_style = (AroundSamePrec, (PP.INCONSISTENT, 0))}; 28 29fun mkMyInfix s prec = mkMyInfixAlias s s prec; 30 31 32(*---------------------------------------------------------------------------* 33 * Create the theory. * 34 *---------------------------------------------------------------------------*) 35 36(*---------------------------------------------------------------------------* 37 * Comments from notes from [1] Model Checking and Modular Verification * 38 * (Grumberg and Long) ACMTransactions on Programming Languages and Systems * 39 * Vol. 16, No. 3, May 1994 * 40 * and also [2] Model Checking (Clarke, Grumberg & Peled) * 41 *---------------------------------------------------------------------------*) 42 43val _ = bossLib.Hol_datatype 44 `state_formula 45 = TRUE 46 | FALSE 47 | REG of 'a 48 | NOT of state_formula 49 | SDISJ of state_formula => state_formula 50 | SCONJ of state_formula => state_formula 51 | E of path_formula 52 | A of path_formula; 53 54 path_formula 55 = STATE of state_formula 56 | FAILS of path_formula 57 | PDISJ of path_formula => path_formula 58 | PCONJ of path_formula => path_formula 59 | X of path_formula 60 | FU of path_formula 61 | G of path_formula 62 | U of path_formula => path_formula 63 | R of path_formula => path_formula`; 64 65(*--------------------------------------------------------------------------- 66 Set-up special parsing for constructors, and inform the system 67 that ~, /\, and \/ will be overloaded. 68 ---------------------------------------------------------------------------*) 69 70val _ = mkMyPrefix "REG" 950; (* tighter than ~ *) 71val _ = mkMyPrefix "E" 245; 72val _ = mkMyPrefix "A" 245; 73val _ = mkMyPrefix "STATE" 260; 74val _ = mkMySuffix "FAILS" 250; (* tighter than ==> but weaker than \/ *) 75val _ = mkMyPrefix "FU" 255; 76val _ = mkMyPrefix "G" 255; 77val _ = mkMyInfix "U" 270; 78val _ = mkMyInfix "R" 270; 79val _ = mkMyPrefix "X" 255; 80 81(*--------------------------------------------------------------------------- 82 Things can look slightly ambiguous: 83 84 Term `A X STATE TRUE FAILS` 85 = 86 Term`A ((X (STATE TRUE)) FAILS)` 87 ---------------------------------------------------------------------------*) 88 89let val overloading = app o curry overload_on 90in overloading "~" [boolSyntax.negation, Term`NOT`]; 91 overloading "/\\" [boolSyntax.conjunction, Term`PCONJ`, Term`SCONJ`]; 92 overloading "\\/" [boolSyntax.disjunction, Term`PDISJ`, Term`SDISJ`] 93end; 94 95(*---------------------------------------------------------------------------* 96 * The branching time logic CTL (Computation Tree Logic) [2:p30] 97 * CTL* restricted st X, FU, G, U and R are preceded by a path quantifier 98 * ie path formulae are restricted st 99 * if f and g are state formulae then Xf FUf Gf fUg and fRg are path formulae 100 * All CTL formulae are of type 'a state_formula 101 *---------------------------------------------------------------------------*) 102 103val IS_CTL_def = Define 104 `(IS_CTL (E X STATE f) = IS_CTL f) 105 /\ (IS_CTL (E FU STATE f) = IS_CTL f) 106 /\ (IS_CTL (E G STATE f) = IS_CTL f) 107 /\ (IS_CTL (E ((STATE f1) U (STATE f2))) = IS_CTL f1 /\ IS_CTL f2) 108 /\ (IS_CTL (E ((STATE f1) R (STATE f2))) = IS_CTL f1 /\ IS_CTL f2) 109 /\ (IS_CTL (A X STATE f) = IS_CTL f) 110 /\ (IS_CTL (A FU STATE f) = IS_CTL f) 111 /\ (IS_CTL (A G STATE f) = IS_CTL f) 112 /\ (IS_CTL (A ((STATE f1) U (STATE f2))) = IS_CTL f1 /\ IS_CTL f2) 113 /\ (IS_CTL (A ((STATE f1) R (STATE f2))) = IS_CTL f1 /\ IS_CTL f2) 114 /\ (IS_CTL TRUE = T) 115 /\ (IS_CTL FALSE = T) 116 /\ (IS_CTL (REG _) = T) 117 /\ (IS_CTL ~f = IS_CTL f) 118 /\ (IS_CTL (f1 \/ f2) = IS_CTL f1 /\ IS_CTL f2) 119 /\ (IS_CTL (f1 /\ f2) = IS_CTL f1 /\ IS_CTL f2) 120 /\ (IS_CTL (E _) = F) 121 /\ (IS_CTL (A _) = F)`; 122 123(*---------------------------------------------------------------------------* 124 * Restrictions to Universally Quantified formulae (ACTL* and ACTL) 125 * ACTL* is CTL* with restrictions: 126 * A1) positive normal form (only negate atoms) 127 * A2) no E path quantifier (only A) 128 * ACTL* formulae may be of type 'a state_formula or 'a path_formula 129 *---------------------------------------------------------------------------*) 130 131val ACTLSTAR_FORMULA_def = Define 132 `(ACTLSTAR_STATE TRUE = T) 133 /\ (ACTLSTAR_STATE FALSE = T) 134 /\ (ACTLSTAR_STATE ~TRUE = T) 135 /\ (ACTLSTAR_STATE ~FALSE = T) 136 /\ (ACTLSTAR_STATE (REG _) = T) 137 /\ (ACTLSTAR_STATE (~REG _) = T) 138 /\ (ACTLSTAR_STATE ~(_) = F) 139 /\ (ACTLSTAR_STATE (f1 \/ f2) = ACTLSTAR_STATE f1 /\ ACTLSTAR_STATE f2) 140 /\ (ACTLSTAR_STATE (f1 /\ f2) = ACTLSTAR_STATE f1 /\ ACTLSTAR_STATE f2) 141 /\ (ACTLSTAR_STATE (E _) = F) 142 /\ (ACTLSTAR_STATE (A g) = ACTLSTAR_PATH g) 143 /\ (ACTLSTAR_PATH (STATE f) = ACTLSTAR_STATE f) 144 /\ (ACTLSTAR_PATH (_ FAILS) = F) 145 /\ (ACTLSTAR_PATH (g1 \/ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2) 146 /\ (ACTLSTAR_PATH (g1 /\ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2) 147 /\ (ACTLSTAR_PATH (X g) = ACTLSTAR_PATH g) 148 /\ (ACTLSTAR_PATH (FU g) = ACTLSTAR_PATH g) 149 /\ (ACTLSTAR_PATH (G g) = ACTLSTAR_PATH g) 150 /\ (ACTLSTAR_PATH (g1 U g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2) 151 /\ (ACTLSTAR_PATH (g1 R g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)`; 152 153(*---------------------------------------------------------------------------* 154 * ACTL is CTL with restrictions A1 and A2 155 * ACTL formulae ore of type 'a state_formula 156 *---------------------------------------------------------------------------*) 157 158val IS_ACTL_def = Define `IS_ACTL f = ACTLSTAR_STATE f /\ IS_CTL f`; 159 160 161(*---------------------------------------------------------------------------* 162 * Definition 2: of a structure M 163 * 164 * M = <S a finite set of states 165 * S0 the start states, a subset of S 166 * A finite set of atomic propositions 167 * L function from states to sets of 168 * atomic propositions true in that state 169 * R transition relation, a subset of SxS 170 * F Streett acceptance condition, a subset of powerset(SxS) 171 * > 172 *---------------------------------------------------------------------------*) 173 174val _ = Hol_datatype 175 `STRUCTURE = <| states : 'state -> bool; 176 states0 : 'state -> bool; 177 atoms : 'varatom -> bool; 178 valids : 'state -> 'varatom -> bool; 179 transitions : 'state # 'state -> bool; 180 fairSets : ('state -> bool) # ('state -> bool) -> bool 181 |>`; 182 183 184val wfSTRUCTURE_def = Define 185`wfSTRUCTURE (M: ('state,'atom) STRUCTURE) 186 = (M.states0 SUBSET M.states) /\ 187 (!P Q. (P,Q) IN M.fairSets ==> P SUBSET M.states /\ Q SUBSET M.states) /\ 188 (!s. s IN M.states ==> (M.valids s) SUBSET M.atoms)`; 189 190(*---------------------------------------------------------------------------* 191 * Definition 3: of paths PI: 192 * 193 * PI is infinite sequence of states s0,s1,s2... s.t. !i. R(si, si+1) 194 *---------------------------------------------------------------------------*) 195 196val _ = Hol_datatype `Path = PATH of num -> 'state`; 197 198val _ = mkMyInfix "STATE_NO" 140; 199val _ = mkMyInfix "IS_PATH_IN" 140; 200val _ = mkMyInfix "IS_FAIR_PATH_IN" 140; 201val _ = mkMyInfix "FROM" 140; 202 203val STATE_NO_def = Define `PATH(Sn) STATE_NO n = Sn n`; 204 205val IS_PATH_IN_def = Define 206 `(PI:'state Path) IS_PATH_IN (M:('state,'atom)STRUCTURE) 207 = (PI STATE_NO 0) IN M.states /\ 208 !n. ((PI STATE_NO n), (PI STATE_NO (n+1))) IN M.transitions`; 209 210 211(*---------------------------------------------------------------------------* 212 * Definition 4: of inf(PI): 213 * 214 * inf(PI) = {s | s=si for infinitely many i} 215 * 216 * and of fair Paths 217 * 218 * Mfair(PI) iff !(P,Q) in F. inf(PI) * P <> {} -> inf(PI) * Q <> {} 219 * where * is set intersection 220 *---------------------------------------------------------------------------*) 221 222val INF_def = Define `INF PI = {s | !m. ?n. n > m /\ (PI STATE_NO m = s)}`; 223 224val IS_FAIR_PATH_IN_def = Define 225 `(PI:'state Path) IS_FAIR_PATH_IN (M:('state,'atom)STRUCTURE) 226 = (PI IS_PATH_IN M) /\ 227 !P Q. (P,Q) IN M.fairSets 228 ==> ~(((INF PI) INTER P) = {}) 229 ==> ~(((INF PI) INTER Q) = {})`; 230 231(*---------------------------------------------------------------------------* 232 * PISn denotes sn in PI 233 * PIn denotes the Path sn,sn+1,sn+2... 234 *---------------------------------------------------------------------------*) 235 236val FROM_def = Define `PI FROM n = PATH(\x. PI STATE_NO (n+x))`; 237 238 239(*---------------------------------------------------------------------------*) 240(* Definition 5: Satisfaction of formulae. *) 241(*---------------------------------------------------------------------------*) 242 243val SAT_defn = 244 tDefine "SAT" 245 `(STATESAT ((M:('s,'a)STRUCTURE), s:'s) (TRUE:'a state_formula) = T) 246 /\ (STATESAT (M,s) FALSE = F) 247 /\ (STATESAT (M,s) (REG a) = ?PI. (PI STATE_NO 0 = s) /\ 248 (PI IS_FAIR_PATH_IN M) /\ 249 (a IN (valids M s))) 250 /\ (STATESAT (M,s) ~f = ~STATESAT (M,s) f) 251 /\ (STATESAT (M,s) (f1 \/ f2) = STATESAT (M,s) f1 \/ STATESAT (M,s) f2) 252 /\ (STATESAT (M,s) (f1 /\ f2) = STATESAT (M,s) f1 /\ STATESAT (M,s) f2) 253 /\ (STATESAT (M,s) (E g1) = ?PI. (PI IS_FAIR_PATH_IN M) /\ 254 (PI STATE_NO 0 = s) /\ PATHSAT(M,PI) g1) 255 /\ (STATESAT (M,s) (A g1) = !PI. (PI IS_FAIR_PATH_IN M) /\ 256 (PI STATE_NO 0 = s) ==> PATHSAT(M,PI) g1) 257 258 /\ (PATHSAT (M,PI) (STATE f1) = STATESAT (M, PI STATE_NO 0) f1) 259 /\ (PATHSAT (M,PI) (g1 FAILS) = ~PATHSAT (M,PI) g1) 260 /\ (PATHSAT (M,PI) (g1 \/ g2) = PATHSAT (M,PI) g1 \/ PATHSAT (M,PI) g2) 261 /\ (PATHSAT (M,PI) (g1 /\ g2) = PATHSAT (M,PI) g1 /\ PATHSAT (M,PI) g2) 262 /\ (PATHSAT (M,PI) (X g1) = PATHSAT (M, PI FROM 1) g1) 263 /\ (PATHSAT (M,PI) (FU g1) = ?k. k >= 0 /\ PATHSAT (M,(PI FROM k)) g1) 264 /\ (PATHSAT (M,PI) (G g1) = !i. i>=0 ==> PATHSAT (M,PI FROM i) g1) 265 /\ (PATHSAT (M,PI) (g1 U g2) = ?k. k>=0 /\ PATHSAT (M,PI FROM k) g2 /\ 266 !j. 0<=j/\j<k ==> PATHSAT(M,PI FROM j) g1) 267 /\ (PATHSAT (M,PI) (g1 R g2) = !j. j>=0 268 ==> (!i. i<j ==> ~PATHSAT(M,PI FROM i) g1) 269 ==> PATHSAT(M,PI FROM j) g2)` 270(*--------------------------------------------------------------------------- 271 Trivial termination proof ... the built-in termination 272 prover should really get this. 273 ---------------------------------------------------------------------------*) 274 (WF_REL_TAC `measure (\s. case s of 275 INL (x,y) => state_formula_size (\v.0) y 276 | INR (x,y) => path_formula_size (\v.0) y)`); 277 278val _ = export_theory() 279