1(* Interactive use 2 3 app load ["Omega_AutomataTheory", "numLib"]; 4 open Rsyntax 5 6*) 7structure temporalLib :> temporalLib = 8struct 9 10(*--------------------------------------------------------------------------- 11 Note (kxs): the pathname and file handling in this file should be 12 made portable. 13 ---------------------------------------------------------------------------*) 14 15val smv_tmp_dir = ref "/tmp/"; 16 17open HolKernel Parse boolLib Rsyntax; 18 19infixr 3 -->; 20infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL; 21 22local open Omega_AutomataTheory in end; 23 24val ERR = Feedback.mk_HOL_ERR "temporalLib" 25 26local (* Fix the grammar used by this file *) 27 val ambient_grammars = Parse.current_grammars(); 28 val _ = Parse.temp_set_grammars Omega_AutomataTheory.Omega_Automata_grammars 29in 30 31type smv_output = 32 {Proved:bool, 33 Init_Sequence:(string list * string list) list, 34 Loop_Sequence:(string list * string list) list, 35 Resources:string list} 36 37 38datatype temp_formula = 39 truesig | 40 falsesig | 41 var of string | 42 neg of temp_formula | 43 conj of (temp_formula * temp_formula) | 44 disj of (temp_formula * temp_formula) | 45 imp of (temp_formula * temp_formula) | 46 equ of (temp_formula * temp_formula) | 47 ifte of (temp_formula * temp_formula * temp_formula) | 48 next of temp_formula | 49 always of temp_formula | 50 eventual of temp_formula | 51 when of (temp_formula * temp_formula) | 52 swhen of (temp_formula * temp_formula) | 53 until of (temp_formula * temp_formula) | 54 suntil of (temp_formula * temp_formula) | 55 befor of (temp_formula * temp_formula) | 56 sbefor of (temp_formula * temp_formula) | 57 pnext of temp_formula | 58 psnext of temp_formula | 59 palways of temp_formula | 60 peventual of temp_formula | 61 pwhen of (temp_formula * temp_formula) | 62 pswhen of (temp_formula * temp_formula) | 63 puntil of (temp_formula * temp_formula) | 64 psuntil of (temp_formula * temp_formula) | 65 pbefor of (temp_formula * temp_formula) | 66 psbefor of (temp_formula * temp_formula); 67 68 69 70 71 72(* **************************************************************************** *) 73(* Converting functions: hol2temporal & temporal2hol *) 74(* **************************************************************************** *) 75 76val thetrue = T 77val thefalse = F 78val NEXT = Term`NEXT` 79val ALWAYS = Term`ALWAYS` 80val EVENTUAL = Term`EVENTUAL` 81val PNEXT = Term`PNEXT` 82val PSNEXT = Term`PSNEXT` 83val PALWAYS = Term`PALWAYS` 84val PEVENTUAL = Term`PEVENTUAL` 85val WHEN = Term`$WHEN` 86val UNTIL = Term`$UNTIL` 87val BEFORE = Term`$BEFORE` 88val SWHEN = Term`$SWHEN` 89val SUNTIL = Term`$SUNTIL` 90val SBEFORE = Term`$SBEFORE` 91val PWHEN = Term`$PWHEN` 92val PUNTIL = Term`$PUNTIL` 93val PBEFORE = Term`$PBEFORE` 94val PSWHEN = Term`$PSWHEN` 95val PSUNTIL = Term`$PSUNTIL` 96val PSBEFORE = Term`$PSBEFORE` 97 98fun hol2temporal t = 99 if t=thetrue then truesig else if t=thefalse then falsesig 100 else 101 (let val {Name=n,Ty=typ} = dest_var t 102 in var(n) 103 end) 104 handle _=> (* --------------------- signal abstraction ------------------------------ *) 105 (let val {Bvar=v,Body=b} = dest_abs t 106 val {Name=n,Ty=_} = dest_var v 107 in (hol2temporal b) 108 end) 109 handle _=> (* ------ propositional or temporal operator or signal evalutation ------- *) 110 (let val t1 = dest_neg t 111 in neg(hol2temporal t1) 112 end) 113 handle _=> 114 (let val {conj1=t1,conj2=t2} = dest_conj t 115 in conj((hol2temporal t1),(hol2temporal t2)) 116 end) 117 handle _=> 118 (let val {disj1=t1,disj2=t2} = dest_disj t 119 in disj((hol2temporal t1),(hol2temporal t2)) 120 end) 121 handle _=> 122 (let val {ant=t1,conseq=t2} = dest_imp t 123 in imp((hol2temporal t1),(hol2temporal t2)) 124 end) 125 handle _=> 126 (let val {lhs=t1,rhs=t2} = dest_eq t 127 in equ((hol2temporal t1),(hol2temporal t2)) 128 end) 129 handle _=> 130 (let val {cond=t1,larm=t2,rarm=t3} = dest_cond t 131 in ifte((hol2temporal t1),(hol2temporal t2),(hol2temporal t3)) 132 end) 133 handle _=> (* ------ temporal operator or signal evalutation ------- *) 134 (let val {Rator=f,Rand=x} = dest_comb t 135 in if f=NEXT then next(hol2temporal x) 136 else if f=ALWAYS then always(hol2temporal x) 137 else if f=EVENTUAL then eventual(hol2temporal x) 138 else if f=PNEXT then pnext(hol2temporal x) 139 else if f=PSNEXT then psnext(hol2temporal x) 140 else if f=PALWAYS then palways(hol2temporal x) 141 else if f=PEVENTUAL then peventual(hol2temporal x) 142 else (* -------- binary temporal operator or signal evalutation --------- *) 143 let val {Rator=temp_op,Rand=b} = dest_comb f 144 in if temp_op = WHEN then 145 when((hol2temporal b),(hol2temporal x)) 146 else if temp_op = UNTIL then 147 until((hol2temporal b),(hol2temporal x)) 148 else if temp_op = BEFORE then 149 befor((hol2temporal b),(hol2temporal x)) 150 else if temp_op = SWHEN then 151 swhen((hol2temporal b),(hol2temporal x)) 152 else if temp_op = SUNTIL then 153 suntil((hol2temporal b),(hol2temporal x)) 154 else if temp_op = SBEFORE then 155 sbefor((hol2temporal b),(hol2temporal x)) 156 else if temp_op = PWHEN then 157 pwhen((hol2temporal b),(hol2temporal x)) 158 else if temp_op = PUNTIL then 159 puntil((hol2temporal b),(hol2temporal x)) 160 else if temp_op = PBEFORE then 161 pbefor((hol2temporal b),(hol2temporal x)) 162 else if temp_op = PSWHEN then 163 pswhen((hol2temporal b),(hol2temporal x)) 164 else if temp_op = PSUNTIL then 165 psuntil((hol2temporal b),(hol2temporal x)) 166 else if temp_op = PSBEFORE then 167 psbefor((hol2temporal b),(hol2temporal x)) 168 else (hol2temporal f) 169 end 170 handle _=> (hol2temporal f) 171 end) 172 173 174 175 176fun temporal2hol truesig = ���\t:num.T��� 177 | temporal2hol falsesig = ���\t:num.F��� 178 | temporal2hol (var(x)) = mk_var{Name=x,Ty=(==`:num->bool`==)} 179 | temporal2hol (neg f) = 180 let val t = temporal2hol f in ���\t:num. ~^t t��� end 181 | temporal2hol (conj(f1,f2)) = 182 let 183 val t1 = temporal2hol f1 184 val t2 = temporal2hol f2 185 in ���\t:num. ^t1 t /\ ^t2 t��� 186 end 187 | temporal2hol (disj(f1,f2)) = 188 let 189 val t1 = temporal2hol f1 190 val t2 = temporal2hol f2 191 in ���\t:num. ^t1 t \/ ^t2 t��� 192 end 193 | temporal2hol (imp(f1,f2)) = 194 let 195 val t1 = temporal2hol f1 196 val t2 = temporal2hol f2 197 in ���\t:num. ^t1 t ==> ^t2 t��� 198 end 199 | temporal2hol (equ(f1,f2)) = 200 let 201 val t1 = temporal2hol f1 202 val t2 = temporal2hol f2 203 in ���\t:num. ^t1 t = ^t2 t��� 204 end 205 | temporal2hol (ifte(f1,f2,f3)) = 206 let 207 val t1 = temporal2hol f1 208 val t2 = temporal2hol f2 209 val t3 = temporal2hol f3 210 in ���\t:num. if ^t1 t then ^t2 t else ^t3 t��� 211 end 212 | temporal2hol (next f) = 213 mk_comb{Rator=NEXT,Rand=(temporal2hol f)} 214 | temporal2hol (always f) = 215 mk_comb{Rator=ALWAYS,Rand=(temporal2hol f)} 216 | temporal2hol (eventual f) = 217 mk_comb{Rator=EVENTUAL,Rand=(temporal2hol f)} 218 | temporal2hol (pnext f) = 219 mk_comb{Rator=PNEXT,Rand=(temporal2hol f)} 220 | temporal2hol (psnext f) = 221 mk_comb{Rator=PSNEXT,Rand=(temporal2hol f)} 222 | temporal2hol (palways f) = 223 mk_comb{Rator=PALWAYS,Rand=(temporal2hol f)} 224 | temporal2hol (peventual f) = 225 mk_comb{Rator=PEVENTUAL,Rand=(temporal2hol f)} 226 | temporal2hol (when(x,b)) = 227 mk_comb{Rator=mk_comb{Rator=WHEN,Rand=(temporal2hol x)}, 228 Rand=(temporal2hol b)} 229 | temporal2hol (until(x,b)) = 230 mk_comb{Rator=mk_comb{Rator=UNTIL,Rand=(temporal2hol x)}, 231 Rand=(temporal2hol b)} 232 | temporal2hol (befor(x,b)) = 233 mk_comb{Rator=mk_comb{Rator=BEFORE,Rand=(temporal2hol x)}, 234 Rand=(temporal2hol b)} 235 | temporal2hol (swhen(x,b)) = 236 mk_comb{Rator=mk_comb{Rator=SWHEN,Rand=(temporal2hol x)}, 237 Rand=(temporal2hol b)} 238 | temporal2hol (suntil(x,b)) = 239 mk_comb{Rator=mk_comb{Rator=SUNTIL,Rand=(temporal2hol x)}, 240 Rand=(temporal2hol b)} 241 | temporal2hol (sbefor(x,b)) = 242 mk_comb{Rator=mk_comb{Rator=SBEFORE,Rand=(temporal2hol x)}, 243 Rand=(temporal2hol b)} 244 | temporal2hol (pwhen(x,b)) = 245 mk_comb{Rator=mk_comb{Rator=PWHEN,Rand=(temporal2hol x)}, 246 Rand=(temporal2hol b)} 247 | temporal2hol (puntil(x,b)) = 248 mk_comb{Rator=mk_comb{Rator=PUNTIL,Rand=(temporal2hol x)}, 249 Rand=(temporal2hol b)} 250 | temporal2hol (pbefor(x,b)) = 251 mk_comb{Rator=mk_comb{Rator=PBEFORE,Rand=(temporal2hol x)}, 252 Rand=(temporal2hol b)} 253 | temporal2hol (pswhen(x,b)) = 254 mk_comb{Rator=mk_comb{Rator=PSWHEN,Rand=(temporal2hol x)}, 255 Rand=(temporal2hol b)} 256 | temporal2hol (psuntil(x,b)) = 257 mk_comb{Rator=mk_comb{Rator=PSUNTIL,Rand=(temporal2hol x)}, 258 Rand=(temporal2hol b)} 259 | temporal2hol (psbefor(x,b)) = 260 mk_comb{Rator=mk_comb{Rator=PSBEFORE,Rand=(temporal2hol x)}, 261 Rand=(temporal2hol b)} 262 263 264 265 266 267 268(* **************************************************************************** *) 269(* Computing the names of the variables *) 270(* **************************************************************************** *) 271 272fun var_names truesig = [] 273 | var_names falsesig = [] 274 | var_names (var(x)) = [x] 275 | var_names (neg f) = var_names f 276 | var_names (conj(f1,f2)) = (var_names f1)@(var_names f2) 277 | var_names (disj(f1,f2)) = (var_names f1)@(var_names f2) 278 | var_names (imp(f1,f2)) = (var_names f1)@(var_names f2) 279 | var_names (equ(f1,f2)) = (var_names f1)@(var_names f2) 280 | var_names (ifte(f1,f2,f3)) = (var_names f1)@(var_names f2)@(var_names f3) 281 | var_names (next f) = var_names f 282 | var_names (always f) = var_names f 283 | var_names (eventual f) = var_names f 284 | var_names (when(x,b)) = (var_names x)@(var_names b) 285 | var_names (until(x,b)) = (var_names x)@(var_names b) 286 | var_names (befor(x,b)) = (var_names x)@(var_names b) 287 | var_names (swhen(x,b)) = (var_names x)@(var_names b) 288 | var_names (suntil(x,b)) = (var_names x)@(var_names b) 289 | var_names (sbefor(x,b)) = (var_names x)@(var_names b) 290 | var_names (pnext f) = var_names f 291 | var_names (psnext f) = var_names f 292 | var_names (palways f) = var_names f 293 | var_names (peventual f) = var_names f 294 | var_names (pwhen(x,b)) = (var_names x)@(var_names b) 295 | var_names (puntil(x,b)) = (var_names x)@(var_names b) 296 | var_names (pbefor(x,b)) = (var_names x)@(var_names b) 297 | var_names (pswhen(x,b)) = (var_names x)@(var_names b) 298 | var_names (psuntil(x,b)) = (var_names x)@(var_names b) 299 | var_names (psbefor(x,b)) = (var_names x)@(var_names b) 300 301 302 303 304(* **************************************************************************** *) 305(* Generating new variable names *) 306(* **************************************************************************** *) 307 308fun new_sig_var name fb index = 309 let val n = name^(int_to_string index) 310 in if mem n fb then new_sig_var name fb (index+1) 311 else n 312 end 313 314 315 316(* *********************** tsubst & temp_subst ******************************** *) 317(* tsubst v x t replaces each occurence of v by x in the formula t (v need *) 318(* not be a variable). The function temp_subst is a multiple replacement, where *) 319(* the replacement is not done simulaneously. The function def_subst is a *) 320(* special variant that is needed in the tableau construction below. *) 321(* **************************************************************************** *) 322 323fun tsubst v x t = 324 if v=t then x else 325 case t of 326 falsesig => falsesig 327 | truesig => truesig 328 | var(n) => var(n) 329 | neg f => neg(tsubst v x f) 330 | conj(f1,f2) => conj(tsubst v x f1,tsubst v x f2) 331 | disj(f1,f2) => disj(tsubst v x f1,tsubst v x f2) 332 | imp(f1,f2) => imp(tsubst v x f1,tsubst v x f2) 333 | equ(f1,f2) => equ(tsubst v x f1,tsubst v x f2) 334 | ifte(f1,f2,f3) => ifte(tsubst v x f1,tsubst v x f2,tsubst v x f3) 335 | next f => next(tsubst v x f) 336 | always f => always(tsubst v x f) 337 | eventual f => eventual(tsubst v x f) 338 | when(f1,f2) => when(tsubst v x f1,tsubst v x f2) 339 | until(f1,f2) => until(tsubst v x f1,tsubst v x f2) 340 | befor(f1,f2) => befor(tsubst v x f1,tsubst v x f2) 341 | swhen(f1,f2) => swhen(tsubst v x f1,tsubst v x f2) 342 | suntil(f1,f2) => suntil(tsubst v x f1,tsubst v x f2) 343 | sbefor(f1,f2) => sbefor(tsubst v x f1,tsubst v x f2) 344 | pnext f => pnext(tsubst v x f) 345 | psnext f => psnext(tsubst v x f) 346 | palways f => palways(tsubst v x f) 347 | peventual f => peventual(tsubst v x f) 348 | pwhen(f1,f2) => pwhen(tsubst v x f1,tsubst v x f2) 349 | puntil(f1,f2) => puntil(tsubst v x f1,tsubst v x f2) 350 | pbefor(f1,f2) => pbefor(tsubst v x f1,tsubst v x f2) 351 | pswhen(f1,f2) => pswhen(tsubst v x f1,tsubst v x f2) 352 | psuntil(f1,f2) => psuntil(tsubst v x f1,tsubst v x f2) 353 | psbefor(f1,f2) => psbefor(tsubst v x f1,tsubst v x f2) 354 355fun temp_subst [] t = t | 356 temp_subst ((v,x)::sigma) t = temp_subst sigma (tsubst v x t) 357 358 359fun def_subst [] t = t 360 | def_subst (equ(ell,phi)::s) t = def_subst s (tsubst phi ell t) 361 | def_subst _ _ = raise ERR "def_subst" "bind" 362 363 364 365(* **************************************************************************** *) 366(* The function tableau is described in my paper of TPHOL99. It essentially *) 367(* abbreviates any subformula that starts with a temporal operator with a new *) 368(* variable that is then hidden by an existential quantification. *) 369(* Special care has to be taken for the NEXT operator and the past temporal *) 370(* operators. For abbreviating past temporal operators, we must first apply one *) 371(* recursion step according to the recursion theorem for the corresponding past *) 372(* operator and abbreviate then the past next operator applied on the past *) 373(* operator. For the next operator, we use two state variable to compute really *) 374(* an automaton. See the theorem "TEMP_OPS_DEFS_TO_OMEGA" of the theory *) 375(* "Omega_Automata" for more details on the form of the abbreviations. *) 376(* **************************************************************************** *) 377 378 379val fb = ref([]:string list); (* contains the names of forbidden variables *) 380 381fun tableau Phi = 382 case Phi of 383 var(_) => ([],Phi) 384 | neg phi => 385 let val (defs,phi') = tableau phi 386 in (defs,neg(phi')) 387 end 388 | conj(phi,psi) => 389 let val (defs1,phi') = tableau phi 390 val (defs2,psi') = tableau (def_subst defs1 psi) 391 in (defs1 @ defs2,conj(phi',psi')) 392 end 393 | disj(phi,psi) => 394 let val (defs1,phi') = tableau phi 395 val (defs2,psi') = tableau (def_subst defs1 psi) 396 in (defs1 @ defs2,disj(phi',psi')) 397 end 398 | imp(phi,psi) => 399 let val (defs1,phi') = tableau phi 400 val (defs2,psi') = tableau (def_subst defs1 psi) 401 in (defs1 @ defs2,imp(phi',psi')) 402 end 403 | equ(phi,psi) => 404 let val (defs1,phi') = tableau phi 405 val (defs2,psi') = tableau (def_subst defs1 psi) 406 in (defs1 @ defs2, equ(phi',psi')) 407 end 408 | ifte(phi,alpha,beta) => 409 let val (defs1,phi') = tableau phi 410 val (defs2,alpha') = tableau (def_subst defs1 alpha) 411 val (defs3,beta') = tableau (def_subst (defs1 @ defs2) beta) 412 in (defs1 @ defs2 @ defs3,ifte(phi',alpha',beta')) 413 end 414 | next phi => 415 let 416 val (defs,phi') = tableau phi 417 val ell0_name = new_sig_var "ell" (!fb) 0 418 val u = (fb := ell0_name::(!fb) ) 419 val ell1_name = new_sig_var "ell" (!fb) 0 420 val u = (fb := ell1_name::(!fb) ) 421 val ell0 = var(ell0_name) 422 val ell1 = var(ell1_name) 423 val def0 = equ(ell0,phi') 424 val def1 = equ(ell1,next(ell0)) 425 in ( defs @ [def0,def1], ell1) 426 end 427 | always phi => 428 let 429 val (defs,phi') = tableau phi 430 val ell_name = new_sig_var "ell" (!fb) 0 431 val u = (fb := ell_name::(!fb) ) 432 val ell = var(ell_name) 433 val def = equ(ell,always(phi')) 434 in (defs @ [def], ell) 435 end 436 | eventual phi => 437 let 438 val (defs,phi') = tableau phi 439 val ell_name = new_sig_var "ell" (!fb) 0 440 val u = (fb := ell_name::(!fb) ) 441 val ell = var(ell_name) 442 val def = equ(ell,eventual(phi')) 443 in (defs @ [def], ell) 444 end 445 | when(phi,psi) => 446 let 447 val (defs1,phi') = tableau phi 448 val (defs2,psi') = tableau (def_subst defs1 psi) 449 val ell_name = new_sig_var "ell" (!fb) 0 450 val u = (fb := ell_name::(!fb) ) 451 val ell = var(ell_name) 452 val def = equ(ell,when(phi',psi')) 453 in (defs1 @ defs2 @ [def], ell) 454 end 455 | until(phi,psi) => 456 let 457 val (defs1,phi') = tableau phi 458 val (defs2,psi') = tableau (def_subst defs1 psi) 459 val ell_name = new_sig_var "ell" (!fb) 0 460 val u = (fb := ell_name::(!fb) ) 461 val ell = var(ell_name) 462 val def = equ(ell,until(phi',psi')) 463 in (defs1 @ defs2 @ [def], ell) 464 end 465 | befor(phi,psi) => 466 let 467 val (defs1,phi') = tableau phi 468 val (defs2,psi') = tableau (def_subst defs1 psi) 469 val ell_name = new_sig_var "ell" (!fb) 0 470 val u = (fb := ell_name::(!fb) ) 471 val ell = var(ell_name) 472 val def = equ(ell,befor(phi',psi')) 473 in (defs1 @ defs2 @ [def], ell) 474 end 475 | swhen(phi,psi) => 476 let 477 val (defs1,phi') = tableau phi 478 val (defs2,psi') = tableau (def_subst defs1 psi) 479 val ell_name = new_sig_var "ell" (!fb) 0 480 val u = (fb := ell_name::(!fb) ) 481 val ell = var(ell_name) 482 val def = equ(ell,swhen(phi',psi')) 483 in (defs1 @ defs2 @ [def], ell) 484 end 485 | suntil(phi,psi) => 486 let 487 val (defs1,phi') = tableau phi 488 val (defs2,psi') = tableau (def_subst defs1 psi) 489 val ell_name = new_sig_var "ell" (!fb) 0 490 val u = (fb := ell_name::(!fb) ) 491 val ell = var(ell_name) 492 val def = equ(ell,suntil(phi',psi')) 493 in (defs1 @ defs2 @ [def], ell) 494 end 495 | sbefor(phi,psi) => 496 let 497 val (defs1,phi') = tableau phi 498 val (defs2,psi') = tableau (def_subst defs1 psi) 499 val ell_name = new_sig_var "ell" (!fb) 0 500 val u = (fb := ell_name::(!fb) ) 501 val ell = var(ell_name) 502 val def = equ(ell,sbefor(phi',psi')) 503 in (defs1 @ defs2 @ [def], ell) 504 end 505 | pnext phi => 506 let 507 val (defs,phi') = tableau phi 508 val ell_name = new_sig_var "ell" (!fb) 0 509 val u = (fb := ell_name::(!fb) ) 510 val ell = var(ell_name) 511 val def = equ(ell,pnext(phi')) 512 in (defs @ [def], ell) 513 end 514 | psnext phi => 515 let 516 val (defs,phi') = tableau phi 517 val ell_name = new_sig_var "ell" (!fb) 0 518 val u = (fb := ell_name::(!fb) ) 519 val ell = var(ell_name) 520 val def = equ(ell,psnext(phi')) 521 in (defs @ [def], ell) 522 end 523 | palways phi => 524 let 525 val (defs,phi') = tableau phi 526 val ell_name = new_sig_var "ell" (!fb) 0 527 val u = (fb := ell_name::(!fb) ) 528 val ell = var(ell_name) 529 val def = equ(ell,pnext(palways(phi'))) 530 in (defs @ [def], conj(phi',ell)) 531 end 532 | peventual phi => 533 let 534 val (defs,phi') = tableau phi 535 val ell_name = new_sig_var "ell" (!fb) 0 536 val u = (fb := ell_name::(!fb) ) 537 val ell = var(ell_name) 538 val def = equ(ell,psnext(peventual(phi'))) 539 in (defs @ [def], disj(phi',ell)) 540 end 541 | pwhen(phi,psi) => 542 let 543 val (defs1,phi') = tableau phi 544 val (defs2,psi') = tableau (def_subst defs1 psi) 545 val ell_name = new_sig_var "ell" (!fb) 0 546 val u = (fb := ell_name::(!fb) ) 547 val ell = var(ell_name) 548 val def = equ(ell,pnext(pwhen(phi',psi'))) 549 in ( 550 defs1 @ defs2 @ [def], 551 disj(conj(phi,psi),conj(neg(psi),ell)) 552 ) 553 end 554 | puntil(phi,psi) => 555 let 556 val (defs1,phi') = tableau phi 557 val (defs2,psi') = tableau (def_subst defs1 psi) 558 val ell_name = new_sig_var "ell" (!fb) 0 559 val u = (fb := ell_name::(!fb) ) 560 val ell = var(ell_name) 561 val def = equ(ell,pnext(puntil(phi',psi'))) 562 in ( 563 defs1 @ defs2 @ [def], 564 disj(psi',conj(phi',ell)) 565 ) 566 end 567 | pbefor(phi,psi) => 568 let 569 val (defs1,phi') = tableau phi 570 val (defs2,psi') = tableau (def_subst defs1 psi) 571 val ell_name = new_sig_var "ell" (!fb) 0 572 val u = (fb := ell_name::(!fb) ) 573 val ell = var(ell_name) 574 val def = equ(ell,pnext(pbefor(phi',psi'))) 575 in ( 576 defs1 @ defs2 @ [def], 577 conj(neg(psi'),disj(phi',ell)) 578 ) 579 end 580 | pswhen(phi,psi) => 581 let 582 val (defs1,phi') = tableau phi 583 val (defs2,psi') = tableau (def_subst defs1 psi) 584 val ell_name = new_sig_var "ell" (!fb) 0 585 val u = (fb := ell_name::(!fb) ) 586 val ell = var(ell_name) 587 val def = equ(ell,psnext(pswhen(phi',psi'))) 588 in ( 589 defs1 @ defs2 @ [def], 590 disj(conj(phi,psi),conj(neg(psi),ell)) 591 ) 592 end 593 | psuntil(phi,psi) => 594 let 595 val (defs1,phi') = tableau phi 596 val (defs2,psi') = tableau (def_subst defs1 psi) 597 val ell_name = new_sig_var "ell" (!fb) 0 598 val u = (fb := ell_name::(!fb) ) 599 val ell = var(ell_name) 600 val def = equ(ell,psnext(psuntil(phi',psi'))) 601 in ( 602 defs1 @ defs2 @ [def], 603 disj(psi',conj(phi',ell)) 604 ) 605 end 606 | psbefor(phi,psi) => 607 let 608 val (defs1,phi') = tableau phi 609 val (defs2,psi') = tableau (def_subst defs1 psi) 610 val ell_name = new_sig_var "ell" (!fb) 0 611 val u = (fb := ell_name::(!fb) ) 612 val ell = var(ell_name) 613 val def = equ(ell,psnext(psbefor(phi',psi'))) 614 in ( 615 defs1 @ defs2 @ [def], 616 conj(neg(psi'),disj(phi',ell)) 617 ) 618 end 619 | truesig => ([],truesig) 620 | falsesig => ([],falsesig) 621 622 623 624 625 626 627 628(* ************************************************************************************ *) 629(* Based on the above function, the conversion TEMP_DEFS_CONV proves now the equivalence*) 630(* between the term with the local abbreviations and the given LTL formula. Note that *) 631(* the given LTL formula must be of the form ALWAYS phi 0, i.e., we only deal with *) 632(* initial equivalence, which is necessary for the past operators. *) 633(* ------------------------------------------------------------------------------------ *) 634(* new_theory "ltltest"; *) 635(* new_parent "Omega_Automata"; *) 636(* TEMP_DEFS_CONV ���ALWAYS (\t. (EVENTUAL a) t = a t \/ NEXT (EVENTUAL a) t) 0���; *) 637(* val it = *) 638(* |- ALWAYS (\t. EVENTUAL a t = a t \/ NEXT (EVENTUAL a) t) 0 = *) 639(* (?ell0 ell1 ell2 ell3 ell4. *) 640(* ell4 0 /\ *) 641(* (ell0 = EVENTUAL a) /\ *) 642(* (ell1 = EVENTUAL a) /\ *) 643(* (ell2 = ell1) /\ *) 644(* (ell3 = NEXT ell2) /\ *) 645(* (ell4 = ALWAYS (\t. ell0 t = a t \/ ell3 t))) : thm *) 646(* *) 647(* TEMP_DEFS_CONV ���ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0���; *) 648(* val it = *) 649(* |- ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0 = *) 650(* (?ell0 ell1 ell2. *) 651(* ell2 0 /\ *) 652(* (ell0 = PNEXT (PALWAYS b)) /\ *) 653(* (ell1 = EVENTUAL (\t. a t /\ b t /\ ell0 t)) /\ *) 654(* (ell2 = ALWAYS ell1)) : thm *) 655(* *) 656(* ************************************************************************************ *) 657 658(* ---------------------------------------------------------------------------- *) 659(* In the following, we have to deal with goals of the following form *) 660(* asm |- (?l1'...ln'. /\_{i=1^k} phi_i ) ==> Phi. *) 661(* Clearly, we should apply STRIP_TAC to reduce this to the following subgoal: *) 662(* [phi_1,...,phi_k] @ asm |- Phi *) 663(* However, STRIP_TAC is painfully slow, as the number of quantified variables *) 664(* may be larger than 50. Hence, we use a more specialized and more efficient *) 665(* tactic here to do the reduction. Do not replace it with STRIP_TAC. *) 666(* ---------------------------------------------------------------------------- *) 667 668fun MY_STRIP_TAC (asm,g) = 669 let val {ant=a,conseq=Phi} = dest_imp g 670 in 671 (REPEAT ((CONV_TAC LEFT_IMP_EXISTS_CONV) THEN GEN_TAC) 672 THEN DISCH_TAC 673 THEN POP_ASSUM (fn x=> MAP_EVERY ASSUME_TAC (CONJUNCTS x)) 674 ) 675 (asm,g) 676 end 677 678 679 680val boolean_sig_ops = TAC_PROOF( 681 ([],��� 682 ? s_not s_and s_or s_imp s_equiv s_ifte. 683 (!a b c. 684 ( (s_not a) = \t:num. ~a t) /\ 685 ( s_and a b = \t:num. (a t /\ b t) ) /\ 686 ( s_or a b = \t:num. (a t \/ b t) ) /\ 687 ( s_imp a b = \t:num. (a t ==> b t) ) /\ 688 ( s_equiv a b = \t:num. (a t = b t) ) /\ 689 ( s_ifte a b c = \t:num. (if a t then b t else c t)) 690 ) 691 /\ 692 (!a b c. 693 (!t:num. ~a t = (s_not a) t) /\ 694 (!t:num. (a t /\ b t) = s_and a b t) /\ 695 (!t:num. (a t \/ b t) = s_or a b t) /\ 696 (!t:num. (a t ==> b t) = s_imp a b t) /\ 697 (!t:num. (a t = b t) = s_equiv a b t) /\ 698 (!t:num. (if a t then b t else c t) = s_ifte a b c t) 699 ) 700 ���), 701 EXISTS_TAC ���\a.\t:num.~a t��� 702 THEN EXISTS_TAC ���\a b.\t:num. a t /\ b t��� 703 THEN EXISTS_TAC ���\a b.\t:num. a t \/ b t��� 704 THEN EXISTS_TAC ���\a b.\t:num. a t ==> b t��� 705 THEN EXISTS_TAC ���\a b.\t:num. (a t):bool = b t��� 706 THEN EXISTS_TAC ���\a b c.\t:num. if a t then (b t):bool else c t��� 707 THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC 708 THEN REPEAT GEN_TAC THEN REWRITE_TAC[]) 709 710 711 712fun PAST_RECURSION_TAC (asm,g) = 713 let fun tll 0 l = l | tll n (e::l) = tll (n-1) l | tll _ _ = raise ERR "PAST_RECURSION_TAC" "bind" 714 val rec_thm = Past_Temporal_LogicTheory.RECURSION 715 val past_rec_thms = (map (GEN_ALL o SYM) (tll 8 (CONJUNCTS rec_thm))) 716 in 717 ( 718 MAP_EVERY ASSUME_TAC past_rec_thms 719 THEN MAP_EVERY (UNDISCH_TAC o concl) past_rec_thms 720 THEN ASSUME_TAC boolean_sig_ops 721 THEN UNDISCH_TAC (concl boolean_sig_ops) THEN STRIP_TAC 722 THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 723 THEN CONV_TAC(DEPTH_CONV ETA_CONV) 724 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 725 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 726 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 727 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 728 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 729 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 730 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 731 THEN DISCH_TAC THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 732 THEN POP_ASSUM (fn x => REWRITE_TAC[x]) 733 ) (asm,g) 734 end 735 736 737fun TEMP_DEFS_CONV t = 738 let 739 (* ---------------------------------------------------------------------------- *) 740 (* First we construct the goal that is to be proved. For this reason, we invoke *) 741 (* the function tableau above and generate the corresponding hol term. *) 742 (* ---------------------------------------------------------------------------- *) 743 val tt = hol2temporal t 744 val u = (fb := var_names tt) 745 val (defs,pt) = tableau tt 746 fun eta_conv t = (* ----- transforms "\t. ell t" to "ell" ----- *) 747 let val {Bvar=x,Body=b} = dest_abs t 748 val {Rator=ell,Rand=y} = dest_comb b 749 in if(x=y) then ell else t 750 end 751 fun fun_eta_conv t = (* ----- transforms "\t. ell t = phi" to "ell = \t. phi" ----- *) 752 let val {Bvar=x,Body=b} = dest_abs t 753 val {lhs=l,rhs=r} = dest_eq b 754 val ell = rator l 755 val new_r = mk_abs{Bvar=x,Body=r} 756 in mk_eq{lhs=ell,rhs=(eta_conv new_r)} 757 end 758 fun beta_conv t = rhs(concl ((QCONV (REPEATC (DEPTH_CONV BETA_CONV))) t)) 759 val hdefs = map (fun_eta_conv o temporal2hol) defs 760 val hpt = mk_comb{Rator=(temporal2hol pt),Rand=���0���} 761 val hpt = beta_conv hpt 762 val hdefs = map beta_conv hdefs 763 val varnames = map lhs hdefs 764 val defterm = (list_mk_conj hdefs) 765 val tt = list_mk_exists(varnames,mk_conj{conj1 = hpt, conj2 = defterm}) 766 val goal = ([],���^t = ^tt���) : goal 767 (* ---------------------------------------------------------------------------- *) 768 (* Having constructed the goal, we define now the tactic that solves this goal. *) 769 (* ---------------------------------------------------------------------------- *) 770 fun flatten_defs [] = [] | 771 flatten_defs (d::dl) = 772 let val (ell,phi) = case d of equ(ell,phi) => (ell,phi) | _ => raise ERR "TEMP_DEFS_CONV" "" 773 in d::(map (tsubst ell phi) (flatten_defs dl)) 774 end 775 val flat_hdefs = map (fun_eta_conv o temporal2hol) (flatten_defs defs) 776 val inst_list = map rhs flat_hdefs 777 val tac = 778 EQ_TAC 779 THENL[ 780 DISCH_TAC 781 THEN MAP_EVERY EXISTS_TAC inst_list THEN BETA_TAC 782 THEN UNDISCH_TAC t 783 THEN PAST_RECURSION_TAC, 784 MY_STRIP_TAC 785 THEN UNDISCH_TAC hpt THEN ASM_REWRITE_TAC[] THEN BETA_TAC 786 THEN PAST_RECURSION_TAC 787 ] 788 in TAC_PROOF(goal, tac) 789 end; 790 791 792 793 794 795fun UNSAFE_TEMP_DEFS_CONV t = 796 let 797 (* ---------------------------------------------------------------------------- *) 798 (* First we construct the goal that is to be proved. For this reason, we invoke *) 799 (* the function tableau above and generate the corresponding hol term. *) 800 (* ---------------------------------------------------------------------------- *) 801 val tt = hol2temporal t 802 val u = (fb := var_names tt) 803 val (defs,pt) = tableau tt 804 fun eta_conv t = (* ----- transforms "\t. ell t" to "ell" ----- *) 805 let val {Bvar=x,Body=b} = dest_abs t 806 val {Rator=ell,Rand=y} = dest_comb b 807 in if(x=y) then ell else t 808 end 809 fun fun_eta_conv t = (* ----- transforms "\t. ell t = phi" to "ell = \t. phi" ----- *) 810 let val {Bvar=x,Body=b} = dest_abs t 811 val {lhs=l,rhs=r} = dest_eq b 812 val ell = rator l 813 val new_r = mk_abs{Bvar=x,Body=r} 814 in mk_eq{lhs=ell,rhs=(eta_conv new_r)} 815 end 816 fun beta_conv t = rhs(concl ((QCONV (REPEATC (DEPTH_CONV BETA_CONV))) t)) 817 val hdefs = map (fun_eta_conv o temporal2hol) defs 818 val hpt = mk_comb{Rator=(temporal2hol pt),Rand=���0���} 819 val hpt = beta_conv hpt 820 val hdefs = map beta_conv hdefs 821 val varnames = map lhs hdefs 822 val defterm = (list_mk_conj hdefs) 823 val tt = list_mk_exists(varnames,mk_conj{conj1 = hpt, conj2 = defterm}) 824 val goal = ([],���^t = ^tt���) : goal 825 in mk_thm goal 826 end 827 828 829 830 831(* **************************************************************************** 832 833 The conversion LTL2OMEGA_CONV finally does what its name indicates. 834 Given an LTL formula in the form as mentioned in the comment on the 835 conversion TEMP_DEFS_CONV, LTL2OMEGA_CONV computes an equivalent 836 generalized B��chi automaton and proves the equivalence with the (* UOK *) 837 given LTL formula. 838 839 ---------------------------------------------------------------------------- 840 LTL2OMEGA_CONV 841 ``ALWAYS (\t. (EVENTUAL a) t = a t \/ NEXT (EVENTUAL a) t) 0``; 842 val it = 843 |- ALWAYS (\t. EVENTUAL a t = a t \/ NEXT (EVENTUAL a) t) 0 = 844 (?ell0 ell1 ell2 ell3 ell4. 845 ell4 0 /\ 846 (!t. 847 (ell0 t = a t \/ ell0 (SUC t)) /\ 848 (ell1 t = a t \/ ell1 (SUC t)) /\ 849 (ell2 t = ell1 t) /\ 850 (ell3 t = ell2 (SUC t)) /\ 851 (ell4 t = (ell0 t = a t \/ ell3 t) /\ ell4 (SUC t))) /\ 852 (!t1. ?t2. ell0 (t1 + t2) ==> a (t1 + t2)) /\ 853 (!t1. ?t2. ell1 (t1 + t2) ==> a (t1 + t2)) /\ 854 (!t1. 855 ?t2. 856 (ell0 (t1 + t2) = a (t1 + t2) \/ ell3 (t1 + t2)) ==> 857 ell4 (t1 + t2))) : thm 858 859 LTL2OMEGA_CONV ``ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0``; 860 val it = 861 |- ALWAYS (EVENTUAL (\t. a t /\ PALWAYS b t)) 0 = 862 (?ell0 ell1 ell2. 863 (ell2 0 /\ ell0 0) /\ 864 (!t. 865 (ell0 (SUC t) = b t /\ ell0 t) /\ 866 (ell1 t = a t /\ b t /\ ell0 t \/ ell1 (SUC t)) /\ 867 (ell2 t = ell1 t /\ ell2 (SUC t))) /\ 868 (!t1. 869 ?t2. 870 ell1 (t1 + t2) ==> a (t1 + t2) /\ b (t1 + t2) /\ ell0 (t1 + t2)) /\ 871 (!t1. ?t2. ell1 (t1 + t2) ==> ell2 (t1 + t2))) : thm 872 873 ************************************************************************* *) 874 875 876 877fun LTL2OMEGA_CONV t = 878 let 879 val future_temp_ops = constants "Temporal_Logic" 880 val past_temp_ops = constants "Past_Temporal_Logic" 881 val temp_ops = future_temp_ops @ past_temp_ops 882 fun elem 0 l = hd l 883 | elem i l = elem (i-1) (tl l) 884 fun delete 0 (e::l) = l 885 | delete i (e::l) = (e::(delete (i-1) l)) 886 | delete _ _ = raise ERR "LTL2OMEGA_CONV" "" 887 fun get_constants t = 888 if (is_var t) then [] 889 else if (is_const t) then [t] 890 else if (is_abs t) then get_constants(body t) 891 else (* its a function application *) 892 let val {Rator=f,Rand=x} = dest_comb t 893 in (get_constants f) @ (get_constants x) 894 end 895 fun is_prop t = null((intersect (get_constants t) temp_ops)) 896 val def2omega_thms = CONJUNCTS Omega_AutomataTheory.TEMP_OPS_DEFS_TO_OMEGA 897 val past_nx_thms = [elem 9 def2omega_thms,elem 10 def2omega_thms] 898 val def2omega_thms = delete 9 (delete 10 def2omega_thms) 899 fun def2omega def = 900 if (is_prop def) then 901 let val {lhs=ell,rhs=phi} = dest_eq def 902 in (���T���,���!t:num. ^ell t = ^phi t���,���T���) 903 end 904 else 905 let val thm = ((PURE_REWRITE_CONV def2omega_thms) THENC 906 (PURE_REWRITE_CONV past_nx_thms)) def 907 val r = rhs(concl thm) 908 val {conj1=init_condition,conj2=rest} = dest_conj r 909 val {conj1=trans_rel,conj2=accept} = dest_conj rest 910 in (init_condition,trans_rel,accept) 911 end 912 val simplify_conv = rhs o concl o ((DEPTH_CONV BETA_CONV) THENC (REWRITE_CONV[])) 913 val thm0 = TEMP_DEFS_CONV t 914 val defterm = rhs(concl thm0) 915 val (dvars,rest) = strip_exists defterm 916 val restlist = strip_conj rest 917 val init_cond = hd restlist 918 val defs = tl restlist 919 val omega_list = map def2omega defs 920 val init_condition = list_mk_conj (map (fn (x,y,z) => x) omega_list) 921 val trans_rel = list_mk_conj (map (fn (x,y,z) => #Body(dest_forall y)) omega_list) 922 val acceptance = list_mk_conj (map (fn (x,y,z) => z) omega_list) 923 val init_condition = mk_conj{conj1=init_cond, conj2=init_condition} 924 val trans_rel = mk_forall{Bvar=���t:num���,Body=trans_rel} 925 val init_condition = simplify_conv init_condition 926 val trans_rel = simplify_conv trans_rel 927 val acceptance = simplify_conv acceptance 928 val automaton_kernel = list_mk_conj[init_condition,trans_rel,acceptance] 929 val automaton = list_mk_exists(dvars,automaton_kernel) 930 val goal = ([],mk_eq{lhs=defterm,rhs=automaton}):goal 931 fun EX_TAC (asm,g) = 932 let val {Bvar=x,Body=t} = dest_exists g 933 in EXISTS_TAC x (asm,g) 934 end 935 val tac = PURE_REWRITE_TAC[(QCONV (REPEATC(DEPTH_CONV FORALL_AND_CONV))) trans_rel] 936 THEN REWRITE_TAC def2omega_thms 937 THEN REWRITE_TAC past_nx_thms 938 THEN (CONV_TAC(DEPTH_CONV FUN_EQ_CONV)) THEN BETA_TAC 939 THEN REWRITE_TAC[] 940 THEN EQ_TAC THEN MY_STRIP_TAC THEN REPEAT EX_TAC 941 THEN RULE_ASSUM_TAC EQT_INTRO 942 THEN ASM_REWRITE_TAC[] 943 val thm1 = TAC_PROOF(goal,tac) 944 in TRANS thm0 thm1 945 end 946 947 948 949fun UNSAFE_LTL2OMEGA_CONV t = 950 let 951 val future_temp_ops = constants "Temporal_Logic" 952 val past_temp_ops = constants "Past_Temporal_Logic" 953 val temp_ops = future_temp_ops @ past_temp_ops 954 fun elem 0 l = hd l 955 | elem i l = elem (i-1) (tl l) 956 fun delete 0 (e::l) = l 957 | delete i (e::l) = (e::(delete (i-1) l)) 958 | delete _ _ = raise ERR "UNSAFE_LTL2OMEGA_CONV" "" 959 fun get_constants t = 960 if (is_var t) then [] 961 else if (is_const t) then [t] 962 else if (is_abs t) then get_constants(body t) 963 else (* its a function application *) 964 let val {Rator=f,Rand=x} = dest_comb t 965 in (get_constants f) @ (get_constants x) 966 end 967 fun is_prop t = null((intersect (get_constants t) temp_ops)) 968 val def2omega_thms = CONJUNCTS Omega_AutomataTheory.TEMP_OPS_DEFS_TO_OMEGA 969 val past_nx_thms = [elem 9 def2omega_thms,elem 10 def2omega_thms] 970 val def2omega_thms = delete 9 (delete 10 def2omega_thms) 971 fun def2omega def = 972 if (is_prop def) then 973 let val {lhs=ell,rhs=phi} = dest_eq def 974 in (���T���,���!t:num. ^ell t = ^phi t���,���T���) 975 end 976 else 977 let val thm = ((PURE_REWRITE_CONV def2omega_thms) THENC 978 (PURE_REWRITE_CONV past_nx_thms)) def 979 val r = rhs(concl thm) 980 val {conj1=init_condition,conj2=rest} = dest_conj r 981 val {conj1=trans_rel,conj2=accept} = dest_conj rest 982 in (init_condition,trans_rel,accept) 983 end 984 val simplify_conv = rhs o concl o ((DEPTH_CONV BETA_CONV) THENC (REWRITE_CONV[])) 985 val thm0 = UNSAFE_TEMP_DEFS_CONV t 986 val defterm = rhs(concl thm0) 987 val (dvars,rest) = strip_exists defterm 988 val restlist = strip_conj rest 989 val init_cond = hd restlist 990 val defs = tl restlist 991 val omega_list = map def2omega defs 992 val init_condition = list_mk_conj (map (fn (x,y,z) => x) omega_list) 993 val trans_rel = list_mk_conj (map (fn (x,y,z) => #Body(dest_forall y)) omega_list) 994 val acceptance = list_mk_conj (map (fn (x,y,z) => z) omega_list) 995 val init_condition = mk_conj{conj1=init_cond, conj2=init_condition} 996 val trans_rel = mk_forall{Bvar=���t:num���,Body=trans_rel} 997 val init_condition = simplify_conv init_condition 998 val trans_rel = simplify_conv trans_rel 999 val acceptance = simplify_conv acceptance 1000 val automaton_kernel = list_mk_conj[init_condition,trans_rel,acceptance] 1001 val automaton = list_mk_exists(dvars,automaton_kernel) 1002 val goal = ([],mk_eq{lhs=defterm,rhs=automaton}):goal 1003 val thm1 = mk_thm goal 1004 in TRANS thm0 thm1 1005 end 1006 1007 1008 1009 1010 1011 1012 1013(* ************************************************************************************ *) 1014(* The conversions TEMP_DEFS_CONV and LTL2OMEGA_CONV require that their input is a *) 1015(* formula that is a boolean combination of formulas that start with a temporal operator*) 1016(* that is applied to the initial point of time, i.e., to 0. *) 1017(* Normally, users do not want to deal with such initial equivalences, but use formulas *) 1018(* with free numeric variables and also with equations between signals. These formulas *) 1019(* are brought into the normal form required by TEMP_DEFS_CONV and LTL2OMEGA_CONV with *) 1020(* the following conversion. It is however not really a conversion, since it requires *) 1021(* to quantify over the numeric free variables. If the user does not do this, a *) 1022(* universal quantification is assumed. *) 1023(* ------------------------------------------------------------------------------------ *) 1024(* Example: *) 1025(* val t = ��� (ALWAYS a t ==> EVENTUAL a t) /\ *) 1026(* (ALWAYS (EVENTUAL a) x ==> EVENTUAL (ALWAYS a) x) /\ *) 1027(* ( (\t. ~NEXT a t) = NEXT (\t. ~ a t) ) *) 1028(* ���; *) 1029(* val it = *) 1030(* |- (!t x. *) 1031(* (ALWAYS a t ==> EVENTUAL a t) /\ *) 1032(* (ALWAYS (EVENTUAL a) x ==> EVENTUAL (ALWAYS a) x) /\ *) 1033(* ((\t. ~(NEXT a t)) = NEXT (\t. ~(a t)))) = *) 1034(* ALWAYS (\t. ALWAYS a t ==> EVENTUAL a t) 0 /\ *) 1035(* ALWAYS (\x. ALWAYS (EVENTUAL a) x ==> EVENTUAL (ALWAYS a) x) 0 /\ *) 1036(* ALWAYS (\n. ~(NEXT a n) = NEXT (\t. ~(a t)) n) 0 : thm *) 1037(* *) 1038(* ************************************************************************************ *) 1039 1040 1041(* ---------------------------------------------------------------------------- *) 1042(* Given a term t and a variable x that occurs free in t, the function closure *) 1043(* finds the smallest subterm of t that contains x and quantify it depending on *) 1044(* the flag exquan. This function is used to get rid of free numeric variables. *) 1045(* ---------------------------------------------------------------------------- *) 1046 1047exception NOT_GOOD_FORMULA; 1048 1049fun closure exquan x t = 1050 (let val {Name=_,Ty=_} = dest_var t 1051 in if x=t then 1052 if exquan then mk_exists{Bvar=x,Body=t} 1053 else mk_forall{Bvar=x,Body=t} 1054 else t 1055 end) 1056 handle _=> 1057 (let val {Name=_,Ty=_} = dest_const t 1058 in t 1059 end) 1060 handle _=> 1061 (let val {Bvar=y,Body=b} = dest_abs t 1062 in if x=y then t 1063 else mk_abs{Bvar=y,Body=(closure exquan x b)} 1064 end) 1065 handle _=> 1066 if (is_neg t) then mk_neg (closure (not exquan) x (dest_neg t)) 1067 else if (is_conj t) then 1068 let val {conj1=t1,conj2=t2} = dest_conj t 1069 val occ1 = mem x (free_vars t1) 1070 val occ2 = mem x (free_vars t2) 1071 in 1072 if (occ1 andalso occ2) then 1073 if exquan then mk_exists{Bvar=x,Body=t} 1074 else mk_forall{Bvar=x,Body=t} 1075 else if occ1 then 1076 mk_conj{conj1=(closure exquan x t1),conj2=t2} 1077 else if occ2 then 1078 mk_conj{conj1=t1,conj2=(closure exquan x t2)} 1079 else t 1080 end 1081 else if (is_disj t) then 1082 let val {disj1=t1,disj2=t2} = dest_disj t 1083 val occ1 = mem x (free_vars t1) 1084 val occ2 = mem x (free_vars t2) 1085 in 1086 if (occ1 andalso occ2) then 1087 if exquan then mk_exists{Bvar=x,Body=t} 1088 else mk_forall{Bvar=x,Body=t} 1089 else if occ1 then 1090 mk_disj{disj1=(closure exquan x t1),disj2=t2} 1091 else if occ2 then 1092 mk_disj{disj1=t1,disj2=(closure exquan x t2)} 1093 else t 1094 end 1095 else if (is_imp t) then 1096 let val {ant=t1,conseq=t2} = dest_imp t 1097 val occ1 = mem x (free_vars t1) 1098 val occ2 = mem x (free_vars t2) 1099 in 1100 if (occ1 andalso occ2) then 1101 if exquan then mk_exists{Bvar=x,Body=t} 1102 else mk_forall{Bvar=x,Body=t} 1103 else if occ1 then 1104 mk_imp{ant=(closure (not exquan) x t1),conseq=t2} 1105 else if occ2 then 1106 mk_imp{ant=t1,conseq=(closure (not exquan) x t2)} 1107 else t 1108 end 1109 else if (is_eq t) then 1110 let val {lhs=t1,rhs=t2} = dest_eq t 1111 val occ1 = mem x (free_vars t1) 1112 val occ2 = mem x (free_vars t2) 1113 in 1114 if (occ1 andalso occ2) then 1115 if exquan then mk_exists{Bvar=x,Body=t} 1116 else mk_forall{Bvar=x,Body=t} 1117 else raise NOT_GOOD_FORMULA 1118 end 1119 else if (is_cond t) then 1120 let val {cond=t1,larm=t2,rarm=t3} = dest_cond t 1121 val occ1 = mem x (free_vars t1) 1122 val occ2 = mem x (free_vars t2) 1123 val occ3 = mem x (free_vars t3) 1124 in 1125 if (occ1 andalso occ2 andalso occ3) then 1126 if exquan then mk_exists{Bvar=x,Body=t} 1127 else mk_forall{Bvar=x,Body=t} 1128 else raise NOT_GOOD_FORMULA 1129 end 1130 else raise NOT_GOOD_FORMULA; 1131 1132 1133 1134 1135fun TEMP_NORMALIZE_CONV t = 1136 let 1137 (* ---------------------------------------------------------------------------- *) 1138 (* First we check whether there is a free numeric variable. If so, we choose *) 1139 (* one of them and universally quantify them and compute a prenex normal form. *) 1140 (* the function tableau above and generate the corresponding hol term. *) 1141 (* ---------------------------------------------------------------------------- *) 1142 val num_vars = filter (fn x => (type_of x) = (==`:num`==)) (free_vars t) 1143 fun close_all [] t = t 1144 | close_all (x::vl) t = close_all vl (closure false x t) 1145 val t = close_all num_vars t 1146 val forall_always_thm = TAC_PROOF( 1147 ([],���!P. (!n. P n) = ALWAYS P 0���), 1148 REWRITE_TAC[Temporal_LogicTheory.ALWAYS] 1149 THEN BETA_TAC 1150 THEN REWRITE_TAC[arithmeticTheory.ADD_CLAUSES]); 1151 val exists_eventual_thm = TAC_PROOF( 1152 ([],���!P. (?n. P n) = EVENTUAL P 0���), 1153 REWRITE_TAC[Temporal_LogicTheory.EVENTUAL] 1154 THEN BETA_TAC 1155 THEN REWRITE_TAC[arithmeticTheory.ADD_CLAUSES]); 1156 fun QUAN_TEMP_CONV t = 1157 if is_forall t then 1158 let val b = rand t 1159 in BETA_RULE(SPEC b forall_always_thm) 1160 end 1161 else if is_exists t then 1162 let val b = rand t 1163 in BETA_RULE(SPEC b exists_eventual_thm) 1164 end 1165 else REFL t 1166 val thm1 = (QCONV 1167 ((DEPTH_CONV FUN_EQ_CONV) THENC 1168 (DEPTH_CONV BETA_CONV) THENC 1169 (DEPTH_CONV (CHANGED_CONV QUAN_TEMP_CONV)) 1170 )) t 1171 val thm2 = Arith.PRENEX_CONV t 1172 in 1173 TRANS (SYM thm2) thm1 1174 end; 1175 1176 1177 1178 1179 1180(* ************************************************************************************ *) 1181(* The next functions deal with interfacing with the SMV system. *) 1182(* The global variable print_states indicates that the state variables shall be printed.*) 1183(* This is not always desired, since one often wants to have the input sequence of the *) 1184(* model. *) 1185(* ************************************************************************************ *) 1186 1187val print_states = ref false; 1188 1189 1190(* ********************************* term2smv_string ********************************** *) 1191(* term2smv_string translates propositional terms in the atoms (p 0), (p t) and p(SUC t)*) 1192(* into SMV syntax, where (p 0) and (p t) are both written as p and p(SUC t) is written *) 1193(* as next(p) (this will only occur in the transition relation. *) 1194(* ************************************************************************************ *) 1195 1196 1197fun term2smv_string t = 1198 (let val {Name=n,Ty=typ} = dest_const t 1199 in if n="T" then "1" else if n="F" then "0" else n 1200 end) 1201 handle _=> (* ------ propositional or temporal operator or signal evalutation ------- *) 1202 (let val t1 = dest_neg t 1203 in "!"^(term2smv_string t1) 1204 end) 1205 handle _=> 1206 (let val {conj1=t1,conj2=t2} = dest_conj t 1207 in "("^(term2smv_string t1)^" & "^(term2smv_string t2)^")" 1208 end) 1209 handle _=> 1210 (let val {disj1=t1,disj2=t2} = dest_disj t 1211 in "("^(term2smv_string t1)^" | "^(term2smv_string t2)^")" 1212 end) 1213 handle _=> 1214 (let val {ant=t1,conseq=t2} = dest_imp t 1215 in "("^(term2smv_string t1)^" -> "^(term2smv_string t2)^")" 1216 end) 1217 handle _=> 1218 (let val {lhs=t1,rhs=t2} = dest_eq t 1219 in "("^(term2smv_string t1)^" <-> "^(term2smv_string t2)^")" 1220 end) 1221 handle _=> 1222 (let val {cond=t1,larm=t2,rarm=t3} = dest_cond t 1223 val p1 = term2smv_string t1 1224 in "(("^p1^" & "^(term2smv_string t2)^") | (!"^p1^" & "^(term2smv_string t3)^"))" 1225 end) 1226 handle _=> (* ------ signal evalutation ------------ *) 1227 (let val {Rator=f,Rand=x} = dest_comb t 1228 in if (is_var x) then #Name(dest_var f) 1229 else if (x=���0���) then #Name(dest_var f) 1230 else if ((rator x)=���SUC���) then 1231 "next("^(#Name(dest_var f))^")" 1232 else #Name(dest_var f) 1233 end) 1234 1235 1236fun genbuechi2smv_string b = 1237 let 1238 val (state_vars,kernel) = strip_exists b 1239 val {conj1=init_condition,conj2=rest} = dest_conj kernel 1240 val {conj1=transrel,conj2=accept} = dest_conj rest 1241 val inout_vars = free_vars b 1242 val vars = inout_vars @ state_vars 1243 fun var_list2smv [] = "" | 1244 var_list2smv (v::vl) = 1245 let val {Name=n,Ty=_} = dest_var v 1246 in " "^n^" : boolean;\n"^(var_list2smv vl) 1247 end 1248 fun acceptance [] = "" | 1249 acceptance (a::al) = 1250 let val {Bvar=_,Body=a1} = dest_forall a 1251 val {Bvar=_,Body=a2} = dest_exists a1 1252 in "\nFAIRNESS "^(term2smv_string a2)^(acceptance al) 1253 end 1254 in 1255 "MODULE main\n\n"^ 1256 "VAR\n"^(var_list2smv vars)^"\n"^ 1257 "TRANS \n"^(term2smv_string(#Body(dest_forall transrel)))^"\n\n"^ 1258 (acceptance (strip_conj accept))^"\n\n"^ 1259 "SPEC (EG TRUE) -> !"^(term2smv_string init_condition)^"\n\n" 1260 end; 1261 1262 1263fun hol2smv t = 1264 let val thm0 = TEMP_NORMALIZE_CONV (mk_neg t) 1265 val t0 = rhs(concl thm0) 1266 val thm1 = LTL2OMEGA_CONV t0 1267 val b = rhs(concl thm1) 1268 in 1269 genbuechi2smv_string b 1270 end 1271 1272 1273 1274 1275(* *************************** interpret_smv_output *********************************** *) 1276(* This function interpretes the output of smv, i.e. the string list is split up into *) 1277(* a sequence of state descriptions and the proved flag and the resource information. *) 1278(* ************************************************************************************ *) 1279 1280fun interpret_smv_output stl = 1281 let fun beginl [] l = true | 1282 beginl (e::s) [] = false | 1283 beginl (e1::s1) (e2::s2) = (e1=e2) andalso (beginl s1 s2) 1284 fun begins s1 s2 = beginl (explode s1) (explode s2) 1285 fun skip_lines [] = [] | 1286 skip_lines (e::l) = if (e = "\n") then skip_lines l 1287 else if (begins "*** " e) then skip_lines l 1288 else if (begins "WARNING *** " e) then skip_lines l 1289 else (e::l) 1290 val stll = ref stl 1291 val proved = 1292 let val (l, ll) = Option.valOf (List.getItem (skip_lines (!stll))) 1293 in (stll := ll; 1294 beginl [#"\n",#"e",#"u",#"r",#"t"] (rev (explode l))) (* ... is true *) 1295 end 1296 fun read_state_lines() = (* reading lines until empty line is read *) 1297 let val (l, ll) = Option.valOf (List.getItem (!stll)) 1298 val _ = (stll := ll) 1299 in if l="\n" then [] 1300 else l::(read_state_lines()) 1301 end 1302 fun loop_starts() = beginl (explode "-- loop") (explode(hd(!stll))) 1303 fun resource_starts() = beginl (explode "resou") (explode(hd(!stll))) 1304 fun another_state() = beginl (explode "state") (explode(hd(!stll))) 1305 val init_sequence = ref ([]:string list list) 1306 val loop_sequence = ref ([]:string list list) 1307 in (if proved then () 1308 else 1309 (stll := skip_lines(tl(!stll)); 1310 while another_state() do 1311 (stll := tl(!stll); 1312 init_sequence := (read_state_lines())::(!init_sequence); 1313 stll := skip_lines(!stll)); 1314 if loop_starts() then 1315 (stll := tl(!stll); 1316 while another_state() do 1317 (stll := tl(!stll); 1318 loop_sequence := (read_state_lines())::(!loop_sequence); 1319 stll := skip_lines(!stll))) 1320 else ()); 1321 {Proved = proved, 1322 Init_Sequence = rev(!init_sequence), 1323 Loop_Sequence = if !loop_sequence=[] then [] else rev(tl(!loop_sequence)), 1324 Resources = skip_lines(!stll)}) 1325 end 1326 1327(* ************************************************************************************ *) 1328(* Printing the countermodel on the terminal *) 1329(* ************************************************************************************ *) 1330 1331fun print_smv_info smv_info = 1332 let val {Proved = proved, 1333 Init_Sequence = init_sequence, 1334 Loop_Sequence = loop_sequence, 1335 Resources = resources} = smv_info 1336 val state_count = ref 0; 1337 fun s_print (s:string) = print s 1338 fun print_state sa = s_print(String.concat sa) 1339 fun s_print_sequence [] = () | 1340 s_print_sequence (sa::sl) = 1341 ( 1342 s_print ("================== State"^(int_to_string(!state_count))); 1343 s_print ("==================\n"); 1344 state_count := (!state_count) + 1; 1345 print_state sa; 1346 s_print_sequence sl 1347 ) 1348 in if proved then 1349 ( 1350 s_print "SMV has done the proof!\n"; 1351 s_print (String.concat resources); 1352 () 1353 ) 1354 else 1355 ( 1356 s_print "===============================================\n"; 1357 s_print "Formula is not true! Consider the countermodel:\n"; 1358 s_print "===============================================\n"; 1359 s_print_sequence init_sequence; 1360 if loop_sequence=[] then () 1361 else 1362 ( 1363 s_print "\n======== A loop starts here=============\n"; 1364 s_print_sequence loop_sequence 1365 ); 1366 s_print "===============================================\n"; 1367 s_print (String.concat resources); 1368 s_print "===============================================\n"; 1369 () 1370 ) 1371 end 1372 1373 1374 1375(* *************************************************************************** 1376 1377 Given a generalized co-B��chi automaton, the conversion (* UOK *) 1378 SMV_AUTOMATON_CONV checks for nonemptiness of the automaton. If the 1379 language accepted by the automaton is empty, the conversion 1380 generates the following theorem: |- (?a_1...a_n. automaton) = F, 1381 where a_1,...,a_n are the free variables of the given automaton 1382 formula. In case the language is not empty, the conversion will 1383 print out the countermodel that has been generated by SMV which 1384 shows a word that belongs to the language of the automaton. 1385 1386 ************************************************************************* *) 1387 1388fun SMV_RUN_FILE smv_file = 1389 let 1390 val _ = case OS.Process.getEnv "HOL4_SMV_EXECUTABLE" of 1391 SOME file => 1392 Process.system (file ^ " " ^ smv_file ^ " > " ^ 1393 (!smv_tmp_dir) ^ "smv_out") 1394 | NONE => 1395 raise Feedback.mk_HOL_ERR "SMV" smv_file 1396 ("SMV not configured: set the HOL4_SMV_EXECUTABLE environment" ^ 1397 "variable to point to the SMV executable file.") 1398 val file_in = TextIO.openIn ((!smv_tmp_dir) ^ "smv_out") 1399 val s = ref (TextIO.inputLine file_in) 1400 val sl = ref ([]:string list) 1401 val _ = while ((!s)<>NONE) do (sl:=(valOf (!s))::(!sl); s:=TextIO.inputLine file_in) 1402 val _ = TextIO.closeIn file_in 1403 val p = interpret_smv_output(rev(!sl)) 1404 val _ = Process.system ("rm " ^ (!smv_tmp_dir) ^ "smv_out") 1405 in 1406 if #Proved(p) then true 1407 else 1408 (print "SMV computes the following countermodel:\n"; 1409 print_smv_info p; 1410 false 1411 ) 1412 end 1413 1414fun SMV_RUN smv_program = 1415 let 1416 val file_st = TextIO.openOut((!smv_tmp_dir)^"smv_file.smv") 1417 val _ = ( 1418 TextIO.output(file_st,smv_program); 1419 TextIO.flushOut file_st; 1420 TextIO.closeOut file_st) 1421 val p = SMV_RUN_FILE ((!smv_tmp_dir) ^ "smv_file.smv") 1422 in 1423 (Process.system ("rm " ^ (!smv_tmp_dir)^"smv_file.smv"); p) 1424 end 1425 1426fun SMV_AUTOMATON_CONV automaton = 1427 let 1428 val smv_program = genbuechi2smv_string automaton 1429 val proved = SMV_RUN smv_program 1430 in 1431 if (proved) then mk_thm([],mk_eq{lhs=automaton,rhs=���F���}) 1432 else 1433 (NO_CONV ���F���) 1434 end; 1435 1436 1437(* ************************************************************************************ *) 1438(* Finally, we can combine all the stuff together. *) 1439(* ************************************************************************************ *) 1440 1441fun LTL_CONV t = 1442 let val t0 = mk_neg t 1443 val thm0 = TEMP_NORMALIZE_CONV t0 1444 val t1 = rhs(concl thm0) 1445 val thm1 = LTL2OMEGA_CONV t1 1446 val automaton = rhs(concl thm1) 1447 val thm2 = SMV_AUTOMATON_CONV automaton 1448 in 1449 EQT_INTRO(REWRITE_RULE[](TRANS (TRANS thm0 thm1) thm2)) 1450 end 1451 1452 1453 1454fun UNSAFE_LTL_CONV t = 1455 let val t0 = mk_neg t 1456 val thm0 = TEMP_NORMALIZE_CONV t0 1457 val t1 = rhs(concl thm0) 1458 val thm1 = UNSAFE_LTL2OMEGA_CONV t1 1459 val automaton = rhs(concl thm1) 1460 val thm2 = SMV_AUTOMATON_CONV automaton 1461 in 1462 EQT_INTRO(REWRITE_RULE[](TRANS (TRANS thm0 thm1) thm2)) 1463 end 1464 1465val _ = Parse.temp_set_grammars ambient_grammars 1466end 1467 1468end 1469