1(* ------------------------------------------------------------------------- 2 Please set HOL4_SMV_EXECUTABLE env variable before evaluating this 3 file, Tested with NuSMV 2.6.0 by Chun Tian <ctian@fbk.eu> on May 4 25, 2018. 5 6 ------------------------------------------------------------------------- *) 7 8load "temporalLib"; open temporalLib; 9 10(* ------------------------------------------------------------------------- 11 First, we prove that SUNTIL can be expressed by unary temporal 12 operators provided that we use past temporal operators. It is 13 well-known that this is not possible without the past operators, 14 i.e., with NEXT, ALWAYS, and EVENTUAL, we could not define the 15 binary temporal future operators. 16 ------------------------------------------------------------------------- *) 17 18val SUNTIL_BY_UNARY_OPERATORS = save_thm ( 19 "SUNTIL_BY_UNARY_OPERATORS", 20 LTL_CONV ���(a SUNTIL b) 0 21 = (EVENTUAL (\t. b t /\ PNEXT (PALWAYS a) t)) 0���); 22 23val SWHEN_BY_UNARY_OPERATORS = save_thm ( 24 "SWHEN_BY_UNARY_OPERATORS", 25 LTL_CONV ���(a SWHEN b) 0 26 = (EVENTUAL (\t. a t /\ b t /\ PNEXT (PALWAYS (\t. ~b t)) t)) 0���); 27 28val SBEFORE_BY_UNARY_OPERATORS = save_thm ( 29 "SBEFORE_BY_UNARY_OPERATORS", 30 LTL_CONV ���(a SBEFORE b) 0 = 31 (EVENTUAL (\t. a t /\ ~b t /\ PNEXT (PALWAYS (\t. ~b t)) t)) 0���); 32 33(* ------------------------------------------------------------------------- 34 Manna and Pnueli consider several normal forms for temporal logic 35 formulas. One such normal form are the persistence formulas that 36 are of the form: EVENTUAL (ALWAYS phi) 0 where phi must not 37 contain future temporal operators. Not any temporal logic formula 38 can be brought into this normal form, but the the set of 39 persistence formulas is closed under /\ and \/: Try to prove the 40 second of the theorems below by hand. 41 ------------------------------------------------------------------------- *) 42 43val EVENTUAL_ALWAYS_NF1 = save_thm ( 44 "EVENTUAL_ALWAYS_NF1", 45 LTL_CONV ``(\t. (EVENTUAL (ALWAYS a)) t /\ (EVENTUAL (ALWAYS b)) t) 46 = (EVENTUAL (ALWAYS (\t. a t /\ b t )))``); 47 48val EVENTUAL_ALWAYS_NF2 = save_thm ( 49 "EVENTUAL_ALWAYS_NF2", 50 LTL_CONV ���(\t. (EVENTUAL (ALWAYS a)) t \/ (EVENTUAL (ALWAYS b)) t) 51 = (EVENTUAL (ALWAYS (\t. a t \/ 52 PNEXT (b PSUNTIL (\t. b t /\ ~a t)) t)))���); 53 54(* ------------------------------------------------------------------------- *) 55(* An important feature of SMV is that it can produce a countermodel if the *) 56(* proof fails. To demonstrate this, we now look at the following examples. *) 57(* ------------------------------------------------------------------------- *) 58 59LTL_CONV ``(a UNTIL b) 0 60 = (EVENTUAL (\t. b t /\ PNEXT (PALWAYS a) t)) 0``; 61 62(* ------------------------------------------------------------------------- 63 64 This should produce the following output: 65 SMV computes the following countermodel: 66 =============================================== 67 Formula is not true! Consider the countermodel: 68 =============================================== 69 70 ======== A loop starts here============= 71 ================== State0================== 72 a = 1 73 b = 0 74 ell0 = 1 75 ell1 = 1 76 ell2 = 1 77 ell3 = 0 78 =============================================== 79 resources used: 80 user time: 0 s, system time: 0.01 s 81 BDD nodes allocated: 267 82 Bytes allocated: 917504 83 BDD nodes representing transition relation: 27 + 1 84 =============================================== 85 SMV_AUTOMATON_CONV fails now!!! 86 =============================================== 87 88 uncaught exception HOL_ERR 89 raised at: 1/conv.sml:234.23-234.67 90 91 ------------------------------------------------------------------------- 92 The ell_i variables have been generated by the conversion. To see 93 what their semantics is, you have to invoke the following: 94 ------------------------------------------------------------------------- *) 95 96TEMP_DEFS_CONV ``(a UNTIL b) 0 97 = (EVENTUAL (\t. b t /\ PNEXT (PALWAYS a) t)) 0``; 98 99(* ------------------------------------------------------------------------- 100 You should obtain the following theorem: 101 val it = 102 |- ((a UNTIL b) 0 = EVENTUAL (\t. b t /\ PNEXT (PALWAYS a) t) 0) = 103 (?ell0 ell1 ell2 ell3. 104 (ell0 0 = ell3 0) /\ 105 (ell0 = a UNTIL b) /\ 106 (ell1 = PNEXT (PALWAYS a)) /\ 107 (ell2 = PNEXT (\t. a t /\ ell1 t)) /\ 108 (ell3 = EVENTUAL (\t. b t /\ ell2 t))) : thm 109 ------------------------------------------------------------------------- 110 111 This means ell0 abbreviates a UNTIL b, ell1 abbreviates PNEXT (PALWAYS a), 112 and so on. Now, look again at the counterexample. It says that at 113 the first point of time, a holds, but b not, and this situation is 114 repeated forever (this is said by the phrase "a loop starts 115 here"). Hence, ell0 is true all the time, and therefore a UNTIL b 116 is true all the time. The same holds for PNEXT (PALWAYS a) and 117 PNEXT (\t. a t /\ ell1 t), which is easily seen by the semantics 118 of these operators and the values of "a" and "b". However, ell3 119 does never hold, which means that the right hand side of our goal 120 is never true, while the left hand side is always true. Hence, we 121 see that the formula is not true. The problem is that the event 122 "b" does never hold. If this is excluded, the equation would hold. 123 Check this by the following: 124 125 ------------------------------------------------------------------------- *) 126 127LTL_CONV ``(EVENTUAL b) 0 128 ==> ((a UNTIL b) 0 129 = (EVENTUAL (\t. b t /\ PNEXT (PALWAYS a) t)) 0)``; 130 131(* ------------------------------------------------------------------------- 132 This will be easily proved. However, this does not define UNTIL in any 133 cases. To do this, prove the following: 134 ------------------------------------------------------------------------- *) 135 136LTL_CONV ``(a UNTIL b) 0 137 = (EVENTUAL (\t. b t /\ PNEXT (PALWAYS a) t)) 0 \/ ALWAYS a 0``; 138 139(* ------------------------------------------------------------------------- 140 An important fact is also that top-level propositional operators 141 can be shifted inwards, when they are applied to formulas that 142 start with temporal operators. Just consider the following theorem 143 for the SUNTIL operator. You may find such elimination laws for 144 the other operators, too, if you recall that SUNTIL can express 145 all the other operators. Negating the right and the left hand 146 sides give also elimination laws for top-level disjunctions. 147 ------------------------------------------------------------------------- *) 148 149val SUNTIL_CONJUNCTIONS = store_thm ( 150 "SUNTIL_CONJUNCTIONS", `` 151 ( (\t. (EVENTUAL b) t /\ (c SUNTIL d) t ) = 152 (c 153 SUNTIL 154 (\t. b t /\ (c SUNTIL d) t \/ 155 d t /\ (EVENTUAL b) t) 156 ) 157 ) /\ 158 ( (\t. (ALWAYS a) t /\ (c SUNTIL d) t ) = 159 ((\t. a t /\ c t) SUNTIL (\t. d t /\ (ALWAYS a) t) ) 160 ) /\ 161 ( (\t. (a SBEFORE b) t /\ (c SUNTIL d) t ) = 162 ((\t. ~b t /\ c t) 163 SUNTIL 164 (\t. a t /\ ~b t /\ (c SUNTIL d) t \/ 165 d t /\ (a SBEFORE b) t) 166 ) 167 ) /\ 168 ( (\t. (a SWHEN b) t /\ (c SUNTIL d) t ) = 169 ((\t. ~b t/\ c t) 170 SUNTIL 171 (\t. a t /\ b t /\ (c SUNTIL d) t \/ 172 d t /\ (a SWHEN b) t) 173 ) 174 ) /\ 175 ( (\t. (a UNTIL b) t /\ (c SUNTIL d) t ) = 176 ((\t. a t /\ c t) 177 SUNTIL 178 (\t. b t /\ (c SUNTIL d) t \/ 179 d t /\ (a UNTIL b) t) 180 ) 181 ) /\ 182 ( (\t. (a BEFORE b) t /\ (c SUNTIL d) t ) = 183 ((\t. ~b t /\ c t) 184 SUNTIL 185 (\t. a t /\ ~b t /\ (c SUNTIL d) t \/ 186 d t /\ (a BEFORE b) t) 187 ) 188 ) /\ 189 ( (\t. (a WHEN b) t /\ (c SUNTIL d) t ) = 190 ((\t. ~b t/\ c t) 191 SUNTIL 192 (\t. a t /\ b t /\ (c SUNTIL d) t \/ 193 d t /\ (a WHEN b) t) 194 ) 195 ) 196 ``, 197 REPEAT CONJ_TAC THEN CONV_TAC LTL_CONV); 198 199(* ------------------------------------------------------------------------- *) 200(* Some operator nestings can be eliminated. Look at the following theorems: *) 201(* ------------------------------------------------------------------------- *) 202 203val ALWAYS_NESTINGS = store_thm ( 204 "ALWAYS_NESTINGS", ��� 205 ( ALWAYS(ALWAYS a) = ALWAYS a ) /\ 206 ( ALWAYS(a UNTIL b) = ALWAYS (\t. a t \/ b t) ) /\ 207 ( ALWAYS(a WHEN b) = ALWAYS (\t. a t \/ ~b t) ) /\ 208 ( ALWAYS(a BEFORE b) = ALWAYS (\t. ~b t) ) /\ 209 ( ALWAYS(a SUNTIL b) = 210 \t. ALWAYS (EVENTUAL b) t /\ ALWAYS (\t. a t \/ b t) t ) /\ 211 ( ALWAYS(a SWHEN b) = 212 \t. ALWAYS (EVENTUAL b) t /\ ALWAYS (\t. a t \/ ~b t) t ) /\ 213 ( ALWAYS(a SBEFORE b)= 214 \t. ALWAYS (EVENTUAL a) t /\ ALWAYS (\t. ~b t) t ) 215 ���, 216 REPEAT CONJ_TAC THEN CONV_TAC LTL_CONV); 217 218val EVENTUAL_NESTINGS = store_thm ( 219 "EVENTUAL_NESTINGS", `` 220 ( EVENTUAL(EVENTUAL a) = EVENTUAL a ) /\ 221 ( EVENTUAL(a UNTIL b) = 222 \t. ALWAYS (EVENTUAL (\t.~a t)) t ==> EVENTUAL b t ) /\ 223 ( EVENTUAL(a WHEN b) = 224 \t. ALWAYS (EVENTUAL b) t ==> EVENTUAL(\t. a t /\ b t) t ) /\ 225 ( EVENTUAL(a BEFORE b) = 226 \t. ALWAYS (EVENTUAL b) t ==> EVENTUAL(\t. a t /\ ~b t) t ) /\ 227 ( EVENTUAL(a SUNTIL b) = EVENTUAL b ) /\ 228 ( EVENTUAL(a SWHEN b) = EVENTUAL (\t. a t /\ b t) ) /\ 229 ( EVENTUAL(a SBEFORE b) = EVENTUAL (\t. a t /\ ~b t) ) 230 ``, 231 REPEAT CONJ_TAC THEN CONV_TAC LTL_CONV); 232 233val UNTIL_NESTINGS = store_thm ( 234 "UNTIL_NESTINGS", `` 235 (((NEXT a) UNTIL b) = \t. b t \/((a WHEN b) t) /\ (NEXT(a UNTIL b)) t) /\ 236 (((ALWAYS a) UNTIL b) = \t.b t \/ (ALWAYS a) t ) /\ 237 (((a UNTIL b) UNTIL c)= 238 \t. ~(c t) ==> ((\t. a t \/ b t) UNTIL c) t /\ 239 ( ((\t. a t ==> b t) WHEN NEXT c) t \/ 240 ((b WHEN (\t. a t ==> b t)) WHEN c) t) ) /\ 241 ( ((a WHEN b) UNTIL c)= 242 \t.~c t ==> ((\t. b t ==> a t) UNTIL c) t /\ 243 ((b WHEN (NEXT c)) t \/ ((a WHEN b) WHEN c) t) ) 244 ``, 245 REPEAT CONJ_TAC THEN CONV_TAC LTL_CONV); 246 247(* ------------------------------------------------------------------------- *) 248(* Temporal operators are monotonic: *) 249(* ------------------------------------------------------------------------- *) 250 251val MONOTONICITY = store_thm ( 252 "MONOTONICITY", `` 253 ALWAYS (\t. a t ==> b t) 0 ==> 254 (\t. ALWAYS a t ==> ALWAYS b t ) 0 /\ 255 (\t. EVENTUAL a t ==> EVENTUAL b t ) 0 /\ 256 (\t. (a UNTIL c) t ==> (b UNTIL c) t ) 0 /\ 257 (\t. (a WHEN c) t ==> (b WHEN c) t ) 0 /\ 258 (\t. (a BEFORE c) t ==> (b BEFORE c) t ) 0 /\ 259 (\t. (a SUNTIL c) t ==> (b SUNTIL c) t ) 0 /\ 260 (\t. (a SWHEN c) t ==> (b SWHEN c) t ) 0 /\ 261 (\t. (a SBEFORE c) t ==> (b SBEFORE c) t ) 0 /\ 262 (\t. (c UNTIL a) t ==> (c UNTIL b) t ) 0 /\ 263 (\t. (c BEFORE b) t ==> (c BEFORE a) t ) 0 /\ 264 (\t. (c SUNTIL a) t ==> (c SUNTIL b) t ) 0 /\ 265 (\t. (c SBEFORE b) t ==> (c SBEFORE a) t ) 0 266 ``, 267 REPEAT STRIP_TAC THEN UNDISCH_TAC ``ALWAYS (\t. a t ==> b t) 0`` 268 THEN CONV_TAC LTL_CONV); 269 270(* ------------------------------------------------------------------------- 271 The theory "Past_Temporal_Logic" contains separation theorems that 272 show that we can separate in any temporal logic formula the past 273 and future temporal operators. We now prove special variants of 274 these separation theorems by our SMV based conversion. 275 ------------------------------------------------------------------------- *) 276 277val SEPARATE_ALWAYS_THM = store_thm ( 278 "SEPARATE_ALWAYS_THM", `` 279 (ALWAYS (\t. a t \/ PNEXT b t) 280 = \t. (a t \/ PNEXT b t) /\ ALWAYS (\t. NEXT a t \/ b t) t 281 ) /\ 282 (ALWAYS (\t. a t \/ PSNEXT b t) 283 = \t. (a t \/ PSNEXT b t) /\ ALWAYS (\t. NEXT a t \/ b t) t 284 ) /\ 285 (ALWAYS (\t. a t \/ (b PSUNTIL c) t) 286 = \t. 287 ( (b PSUNTIL c) t \/ ((NEXT c) BEFORE (\t. ~a t)) t ) 288 /\ ALWAYS (\t. b t \/ c t \/ ((NEXT c) BEFORE (\t. ~a t)) t) t 289 ) /\ 290 (ALWAYS (\t. a t \/ (b PBEFORE c) t) 291 = \t. 292 ( (b PBEFORE c) t \/ ((NEXT b) BEFORE (\t. ~a t)) t ) 293 /\ ALWAYS (\t. c t ==> ((NEXT b) BEFORE (\t. ~a t)) t) t 294 ) 295 ``, 296 REPEAT STRIP_TAC THEN CONV_TAC LTL_CONV); 297 298val SEPARATE_EVENTUAL_THM = store_thm ( 299 "SEPARATE_EVENTUAL_THM", `` 300 (EVENTUAL (\t. a t /\ PNEXT b t) 301 = \t. (a t /\ PNEXT b t) \/ EVENTUAL (\t. NEXT a t /\ b t) t 302 ) /\ 303 (EVENTUAL (\t. a t /\ PSNEXT b t) 304 = \t. (a t /\ PSNEXT b t) \/ EVENTUAL (\t. NEXT a t /\ b t) t 305 ) /\ 306 (EVENTUAL (\t. a t /\ (b PSUNTIL c) t) 307 = \t. (b PSUNTIL c) t /\ ((NEXT b) SUNTIL a) t 308 \/ EVENTUAL (\t. c t /\ ((NEXT b) SUNTIL a) t) t 309 ) /\ 310 (EVENTUAL (\t. a t /\ (b PBEFORE c) t) 311 = \t. (b PBEFORE c) t /\ ((NEXT(\t. ~c t)) SUNTIL a) t 312 \/ EVENTUAL (\t. b t /\ ~c t /\ ((NEXT(\t. ~c t)) SUNTIL a) t) t 313 ) 314 ``, 315 REPEAT STRIP_TAC THEN CONV_TAC LTL_CONV); 316 317val SEPARATE_EVENTUAL_ALWAYS_THM = store_thm ( 318 "SEPARATE_EVENTUAL_ALWAYS_THM", `` 319 (EVENTUAL(ALWAYS (\t. a t \/ PNEXT b t)) 320 = EVENTUAL(ALWAYS (\t. NEXT a t \/ b t)) 321 ) /\ 322 (EVENTUAL(ALWAYS (\t. a t \/ PSNEXT b t)) 323 = EVENTUAL(ALWAYS (\t. NEXT a t \/ b t)) 324 ) /\ 325 (EVENTUAL(ALWAYS (\t. a t \/ (b PSUNTIL c) t)) 0 326 = 327 if ALWAYS (\t.~c t) 0 328 then EVENTUAL(ALWAYS a) 0 329 else if ALWAYS (EVENTUAL c) 0 330 then EVENTUAL(ALWAYS 331 (\t. b t \/ c t \/ ((NEXT c) BEFORE (\t. ~a t)) t)) 0 332 else if EVENTUAL(ALWAYS a) 0 333 then EVENTUAL(ALWAYS a) 0 334 else EVENTUAL(\t. c t /\ ALWAYS (NEXT b) t) 0 335 336 ) 337 ``, 338 REPEAT STRIP_TAC THEN CONV_TAC LTL_CONV); 339 340(*--------------------------------------------------------------------------*) 341