(*****************************************************************************) (* Create "Sugar2SemanticsTheory" containing abstract syntax and semantics *) (* of the basic language, initially following the Accellera documentation, *) (* but now incorporating changes resulting from proof experiments, *) (* see: http://www.cl.cam.ac.uk/~mjcg/Sugar/ *) (*****************************************************************************) (****************************************************************************** * In the Sugar 2 documentation: * * http://www.haifa.il.ibm.com/projects/verification/sugar/literature.html * * a model is a quintuple (S,S0,R,P,L) where * * - S : 'state is a set of states * - S0 : 'state -> bool is a subset of S, the initial states * - R : 'state # 'state -> bool is a transition relation * - P : 'prop is a set of atomic proposition * - L : 'state -> ('prop -> bool) maps each state to the * set of propositions true in that state * * N.B. terms that follow are not contrained to use type variables * 'state and 'prop, but may use 'a, 'b etc * or whatever typechecking assigns. ******************************************************************************) (*****************************************************************************) (* START BOILERPLATE *) (*****************************************************************************) (****************************************************************************** * Load theory of paths and additional definitions of functions on lists * (commented out for compilation) ******************************************************************************) (* load "PathTheory"; load "rich_listTheory"; load "intLib"; *) (****************************************************************************** * Boilerplate needed for compilation ******************************************************************************) open HolKernel Parse boolLib bossLib; (****************************************************************************** * Open theories of paths and lists ******************************************************************************) open PathTheory listTheory rich_listTheory; (****************************************************************************** * Set default parsing to natural numbers rather than integers ******************************************************************************) val _ = intLib.deprecate_int(); (*****************************************************************************) (* END BOILERPLATE *) (*****************************************************************************) (****************************************************************************** * Start a new theory called Sugar2Semantics ******************************************************************************) val _ = new_theory "Sugar2Semantics"; (****************************************************************************** * Stop S parsing to the S-combinator ******************************************************************************) val _ = hide "S"; (****************************************************************************** * KRIPKE_STRUCTURE M iff M is a well-formed Kripke structure * i.e. every initial state is a state, * and L maps each state to a set of propositions. * For many results the structure M=(S,S0,R,P,L) does not need * to be a well-formed Kripke structure. ******************************************************************************) val KRIPKE_STRUCTURE_def = Define KRIPKE_STRUCTURE (S: 'state -> bool, S0:'state -> bool, R: 'state # 'state -> bool, P: 'prop -> bool, L: 'state -> ('prop -> bool)) = (!s. S0 s ==> S s) /\ (!s p . L s p ==> P p); (****************************************************************************** * A useful special case (possibly the only one we'll need) is to * identify propositions with predicates on states, and then we just need * to specify the set of itial state B and transition relation R *******************************************************************************) val SIMPLE_KRIPKE_STRUCTURE_def = Define SIMPLE_KRIPKE_STRUCTURE (B:'state -> bool) (R:'state#'state->bool) = ((\s:'state. T), B, R, (\f:'state -> bool. T), (\(s:'state) (f:'state -> bool). f s)); (****************************************************************************** * Sanity check that a simple Kripke structure is a Kripke structure ******************************************************************************) val SIMPLE_KRIPKE_STRUCTURE = store_thm ("SIMPLE_KRIPKE_STRUCTURE", KRIPKE_STRUCTURE(SIMPLE_KRIPKE_STRUCTURE B R), RW_TAC std_ss [KRIPKE_STRUCTURE_def,SIMPLE_KRIPKE_STRUCTURE_def]); (****************************************************************************** * Boolean expressions (added B_TRUE for use in definition of F_SEM) ******************************************************************************) val bexp_def = Hol_datatype bexp = B_PROP of 'a (* atomic proposition *) | B_NOT of bexp (* negation *) | B_AND of bexp # bexp; (* conjunction *) (****************************************************************************** * Definition of truth ******************************************************************************) val B_OR_def = Define B_OR(b1,b2) = B_NOT(B_AND(B_NOT b1, B_NOT b2)); (****************************************************************************** * Definition of truth ******************************************************************************) val B_TRUE_def = Define B_TRUE = B_OR(B_PROP ARB, B_NOT(B_PROP ARB)); (****************************************************************************** * Definition of falsity ******************************************************************************) val B_FALSE_def = Define B_FALSE = B_NOT B_TRUE; (****************************************************************************** * Sugar Extended Regular Expressions (SEREs) ******************************************************************************) val sere_def = Hol_datatype sere = S_BOOL of 'a bexp (* boolean expression *) | S_CAT of sere # sere (* r1 ; r2 *) | S_FUSION of sere # sere (* r1 : r2 *) | S_OR of sere # sere (* r1 | r2 *) | S_RIG_AND of sere # sere (* r1 && r2 *) | S_FLEX_AND of sere # sere (* r1 & r2 *) | S_REPEAT of sere (* r[*] *) | S_CLOCK of sere # 'a bexp; (* r@clk *) (****************************************************************************** * Formulas of Sugar Foundation Language (FL) ******************************************************************************) val fl_def = Hol_datatype fl = F_BOOL of 'a bexp (* boolean expression *) | F_NOT of fl (* \neg f *) | F_AND of fl # fl (* f1 \wedge f2 *) | F_NEXT of fl (* X! f *) | F_UNTIL of fl # fl (* [f1 U f2] *) | F_SUFFIX_IMP of 'a sere # fl (* {r}(f) *) | F_STRONG_IMP of 'a sere # 'a sere (* r1 |-> r2! *) | F_WEAK_IMP of 'a sere # 'a sere (* r1 |-> r2 *) | F_ABORT of fl # 'a bexp (* f abort b *) | F_WEAK_CLOCK of fl # 'a bexp (* r@clk *) | F_STRONG_CLOCK of fl # 'a bexp; (* r@clk! *) (****************************************************************************** * Formulas of Sugar Optional Branching Extension (OBE) ******************************************************************************) val obe_def = Hol_datatype obe = O_BOOL of 'a bexp (* boolean expression *) | O_NOT of obe (* \neg f *) | O_AND of obe # obe (* f1 \wedge f2 *) | O_EX of obe (* EX f *) | O_EU of obe # obe (* E[f1 U f2] *) | O_EG of obe; (* EG f *) (****************************************************************************** * Selectors for components of a model M = (S,S0,R,P,L) ******************************************************************************) val getS_def = Define getS (S,S0,R,P,L) = S; val getS0_def = Define getS0 (S,S0,R,P,L) = S0; val getR_def = Define getR (S,S0,R,P,L) = R; val getP_def = Define getP (S,S0,R,P,L) = P; val getL_def = Define getL (S,S0,R,P,L) = L; (****************************************************************************** * L and \hat{L} operators used in the semantics ******************************************************************************) val L_def = Define L M = getL M; val LHAT_def = Define LHAT M = MAP (getL M); (****************************************************************************** * B_SEM M l b means "l |= b" * and also that b only contains atomic propositions in getP M ******************************************************************************) val B_SEM_def = Define (B_SEM M l (B_PROP(p:'p)) = p IN (getP M) /\ p IN l) /\ (B_SEM M l (B_NOT b) = ~(B_SEM M l b)) /\ (B_SEM M l (B_AND(b1,b2)) = B_SEM M l b1 /\ B_SEM M l b2); val B_SEM = store_thm ("B_SEM", (B_SEM M l (B_PROP(p:'p)) = p IN (getP M) /\ p IN l) /\ (B_SEM M l B_TRUE = T) /\ (B_SEM M l B_FALSE = F) /\ (B_SEM M l (B_NOT b) = ~(B_SEM M l b)) /\ (B_SEM M l (B_AND(b1,b2)) = B_SEM M l b1 /\ B_SEM M l b2) /\ (B_SEM M l (B_OR(b1,b2)) = B_SEM M l b1 \/ B_SEM M l b2), RW_TAC std_ss [B_SEM_def,B_OR_def,B_TRUE_def,B_FALSE_def] THEN PROVE_TAC[]); (****************************************************************************** * Unclocked semantics of SEREs * US_SEM M w r means "w is in the language of r" in the unclocked semantics ******************************************************************************) val US_SEM_def = Define (US_SEM M w (S_BOOL b) = ?l. (w = [l]) /\ B_SEM M l b) /\ (US_SEM M w (S_CAT(r1,r2)) = ?w1 w2. (w = w1 <> w2) /\ US_SEM M w1 r1 /\ US_SEM M w2 r2) /\ (US_SEM M w (S_FUSION(r1,r2)) = ?w1 w2 l. (w = w1 <> [l] <> w2) /\ US_SEM M (w1<>[l]) r1 /\ US_SEM M ([l]<>w2) r2) /\ (US_SEM M w (S_OR(r1,r2)) = US_SEM M w r1 \/ US_SEM M w r2) /\ (US_SEM M w (S_RIG_AND(r1,r2)) = US_SEM M w r1 /\ US_SEM M w r2) /\ (US_SEM M w (S_FLEX_AND(r1,r2)) = ?w1 w2. (w = w1 <> w2) /\ ((US_SEM M w r1 /\ US_SEM M w1 r2) \/ (US_SEM M w r2 /\ US_SEM M w1 r1) )) /\ (US_SEM M w (S_REPEAT r) = ?wlist. (w = CONCAT wlist) /\ EVERY (\w. US_SEM M w r) wlist); (****************************************************************************** * Clocked semantics of SEREs * S_SEM M w c r means "w is in the language of r in context c" ******************************************************************************) val S_SEM_def = Define (S_SEM M w c (S_BOOL b) = ?n. n >= 1 /\ (LENGTH w = n) /\ (!i. 1 <= i /\ i < n ==> B_SEM M (EL (i-1) w) (B_NOT c)) /\ B_SEM M (EL (n-1) w) (B_AND(c,b))) /\ (S_SEM M w c (S_CAT(r1,r2)) = ?w1 w2. (w = w1 <> w2) /\ S_SEM M w1 c r1 /\ S_SEM M w2 c r2) /\ (S_SEM M w c (S_FUSION(r1,r2)) = ?w1 w2 l. (w = w1 <> [l] <> w2) /\ S_SEM M (w1<>[l]) c r1 /\ S_SEM M ([l]<>w2) c r2) /\ (S_SEM M w c (S_OR(r1,r2)) = S_SEM M w c r1 \/ S_SEM M w c r2) /\ (S_SEM M w c (S_RIG_AND(r1,r2)) = S_SEM M w c r1 /\ S_SEM M w c r2) /\ (S_SEM M w c (S_FLEX_AND(r1,r2)) = ?w1 w2. (w = w1 <> w2) /\ ((S_SEM M w c r1 /\ S_SEM M w1 c r2) \/ (S_SEM M w c r2 /\ S_SEM M w1 c r1) )) /\ (S_SEM M w c (S_REPEAT r) = ?wlist. (w = CONCAT wlist) /\ EVERY (\w. S_SEM M w c r) wlist) /\ (S_SEM M w c (S_CLOCK(r,c1)) = S_SEM M w c1 r); (****************************************************************************** * Unclocked semantics of Sugar formulas * UF_SEM M p f means "p |= f" in the unclocked semantics * (F_WEAK_IMP case unfolded to make totality proof go through) ******************************************************************************) val UF_SEM_def = Define (UF_SEM M p (F_BOOL b) = B_SEM M (L M (PATH_EL p 0)) b) /\ (UF_SEM M p (F_NOT f) = ~(UF_SEM M p f)) /\ (UF_SEM M p (F_AND(f1,f2)) = UF_SEM M p f1 /\ UF_SEM M p f2) /\ (UF_SEM M p (F_NEXT f) = PL p 1 /\ UF_SEM M (RESTN p 1) f) /\ (UF_SEM M p (F_UNTIL(f1,f2)) = ?k :: PL p. UF_SEM M (RESTN p k) f2 /\ !j :: PL p. j < k ==> UF_SEM M (RESTN p j) f1) /\ (UF_SEM M p (F_SUFFIX_IMP(r,f)) = !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r ==> UF_SEM M (RESTN p j) f) /\ (UF_SEM M p (F_STRONG_IMP(r1,r2)) = !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1 ==> ?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2) /\ (UF_SEM M p (F_WEAK_IMP(r1,r2)) = !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1 ==> (?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2) \/ !k :: PL p. j <= k ==> ?w. US_SEM M (LHAT M (PATH_SEG p (j,k)) <> w) r2) /\ (UF_SEM M p (F_ABORT (f,b)) = UF_SEM M p f \/ ?j :: PL p. 0 < j /\ ?p'. (* IS_INFINITE_PATH p' /\ *) UF_SEM M (RESTN p j) (F_BOOL b) /\ UF_SEM M (PATH_CAT(PATH_SEG p (0,j-1),p')) f); (****************************************************************************** * UF_SEM M p f means "p |= f" in the unclocked semantics * Derivation of folded equation ******************************************************************************) val UF_SEM = store_thm ("UF_SEM", (UF_SEM M p (F_BOOL b) = B_SEM M (L M (PATH_EL p 0)) b) /\ (UF_SEM M p (F_NOT f) = ~(UF_SEM M p f)) /\ (UF_SEM M p (F_AND(f1,f2)) = UF_SEM M p f1 /\ UF_SEM M p f2) /\ (UF_SEM M p (F_NEXT f) = PL p 1 /\ UF_SEM M (RESTN p 1) f) /\ (UF_SEM M p (F_UNTIL(f1,f2)) = ?k :: PL p. UF_SEM M (RESTN p k) f2 /\ !j :: PL p. j < k ==> UF_SEM M (RESTN p j) f1) /\ (UF_SEM M p (F_SUFFIX_IMP(r,f)) = !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r ==> UF_SEM M (RESTN p j) f) /\ (UF_SEM M p (F_STRONG_IMP(r1,r2)) = !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1 ==> ?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2) /\ (UF_SEM M p (F_WEAK_IMP(r1,r2)) = !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1 ==> (?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2) \/ !k :: PL p. j <= k ==> ?w. US_SEM M (LHAT M (PATH_SEG p (j,k)) <> w) r2) /\ (UF_SEM M p (F_ABORT (f,b)) = UF_SEM M p f \/ ?j :: PL p. 0 < j /\ ?p'. (* IS_INFINITE_PATH p' /\ *) UF_SEM M (RESTN p j) (F_BOOL b) /\ UF_SEM M (PATH_CAT(PATH_SEG p (0,j-1),p')) f), SIMP_TAC std_ss [UF_SEM_def]); (****************************************************************************** * FIRST_RISE M p c i = LHAT(p(0,i)) |=T= {(\neg c)[*];c} * (i is the first rising edge of clock c in path p) ******************************************************************************) val FIRST_RISE_def = Define FIRST_RISE M p c i = S_SEM M (MAP (getL M) (PATH_SEG p (0,i))) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)); (****************************************************************************** * NEXT_RISE M p c (i,j) = Lhat(p(i,j)) |=T= {(\neg c)[*];c} * (i is the first rising edge after j of clock c in path p) ******************************************************************************) val NEXT_RISE_def = Define NEXT_RISE M p c (i,j) = S_SEM M (MAP (getL M) (PATH_SEG p (i,j))) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)); (****************************************************************************** * Contexts (strong or weak clock) ******************************************************************************) val context_def = Hol_datatype context = STRONG_CLOCK of 'a bexp (* strong clock: c! *) | WEAK_CLOCK of 'a bexp; (* weak clock: c *) (****************************************************************************** * Clocked semantics of Sugar formulas * Definition due to Konrad Slind that uses * cunning feature of TFL to prove that F_SEM is total ******************************************************************************) val F_SEM_defn = Hol_defn "F_SEM" (F_SEM M p (STRONG_CLOCK c) (F_BOOL b) = ?i :: PL p. FIRST_RISE M p c i /\ B_SEM M (L M (PATH_EL p i)) b) /\ (F_SEM M p (STRONG_CLOCK c) (F_NOT f) = ~(F_SEM M p (WEAK_CLOCK c) f)) /\ (F_SEM M p (STRONG_CLOCK c) (F_AND(f1,f2)) = ?i :: PL p. FIRST_RISE M p c i /\ F_SEM M (RESTN p i) (STRONG_CLOCK c) f1 /\ F_SEM M (RESTN p i) (STRONG_CLOCK c) f2) /\ (F_SEM M p (STRONG_CLOCK c) (F_NEXT f) = ?i :: PL p. FIRST_RISE M p c i /\ ?j :: PL p. i < j /\ NEXT_RISE M p c (i+1,j) /\ F_SEM M (RESTN p j) (STRONG_CLOCK c) f) /\ (F_SEM M p (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = ?i k :: PL p. k >= i /\ FIRST_RISE M p c i /\ F_SEM M (RESTN p k) (WEAK_CLOCK B_TRUE) (F_BOOL c) /\ F_SEM M (RESTN p k) (STRONG_CLOCK c) f2 /\ !j :: PL p. i <= j /\ j < k /\ F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL c) ==> F_SEM M (RESTN p j) (STRONG_CLOCK c) f1) /\ (* (F_SEM M p (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = ?i :: PL p. (?k :: PL p. i <= k /\ NEXT_RISE M p c (i,k) /\ F_SEM M (RESTN p k) (STRONG_CLOCK c) f2) /\ !j :: PL p. j < i ==> ?k :: PL p. j <= k /\ NEXT_RISE M p c (j,k) /\ F_SEM M (RESTN p k) (STRONG_CLOCK c) f1) *) (F_SEM M p (STRONG_CLOCK c) (F_SUFFIX_IMP(r,f)) = ?i :: PL p. FIRST_RISE M p c i /\ !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r ==> F_SEM M (RESTN p j) (STRONG_CLOCK c) f) /\ (F_SEM M p (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2)) = ?i :: PL p. FIRST_RISE M p c i /\ !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r1 ==> ?k :: PL p. j <= k /\ S_SEM M (LHAT M (PATH_SEG p (j,k))) c r2) /\ (F_SEM M p (STRONG_CLOCK c) (F_WEAK_IMP(r1,r2)) = F_SEM M p (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2)) \/ (F_SEM M p (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2)) /\ !j :: PL p. ?k :: PL p. j <= k /\ NEXT_RISE M p c (j,k))) /\ (F_SEM M p (STRONG_CLOCK c) (F_ABORT (f,b)) = ?i :: PL p. FIRST_RISE M p c i /\ (F_SEM M (RESTN p i) (STRONG_CLOCK c) f \/ ?j :: PL p. i < j /\ ?p'. (* IS_INFINITE_PATH p' /\ *) F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL(B_AND(c,b))) /\ F_SEM M (PATH_CAT(PATH_SEG p (i,j-1),p')) (STRONG_CLOCK c) f)) /\ (F_SEM M p (STRONG_CLOCK c) (F_WEAK_CLOCK(f,c1)) = F_SEM M p (WEAK_CLOCK c1) f) /\ (F_SEM M p (STRONG_CLOCK c) (F_STRONG_CLOCK(f,c1)) = F_SEM M p (STRONG_CLOCK c1) f) /\ (****************************************************************************** * Start of weak clock clauses ******************************************************************************) (F_SEM M p (WEAK_CLOCK c) (F_BOOL b) = !i :: PL p. FIRST_RISE M p c i ==> B_SEM M (L M (PATH_EL p i)) b) /\ (F_SEM M p (WEAK_CLOCK c) (F_NOT f) = ~(F_SEM M p (STRONG_CLOCK c) f)) /\ (F_SEM M p (WEAK_CLOCK c) (F_AND(f1,f2)) = !i :: PL p. FIRST_RISE M p c i ==> (F_SEM M (RESTN p i) (WEAK_CLOCK c) f1 /\ F_SEM M (RESTN p i) (WEAK_CLOCK c) f2)) /\ (F_SEM M p (WEAK_CLOCK c) (F_NEXT f) = !i :: PL p. FIRST_RISE M p c i ==> ?j :: PL p. i < j /\ NEXT_RISE M p c (i+1,j) /\ F_SEM M (RESTN p j) (WEAK_CLOCK c) f) /\ (F_SEM M p (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = (?i :: PL p. FIRST_RISE M p c i /\ ?l :: PL p. i <= l /\ ((?k :: PL p. l <= k /\ NEXT_RISE M p c (l,k) /\ F_SEM M (RESTN p k) (WEAK_CLOCK c) f2) \/ !m :: PL p. l <= m ==> F_SEM M (RESTN p m) (WEAK_CLOCK B_TRUE) (F_BOOL (B_NOT c))) /\ !j :: PL p. i <= j /\ j < l ==> (?k :: PL p. j <= k /\ NEXT_RISE M p c (j,k) /\ F_SEM M (RESTN p k) (WEAK_CLOCK c) f1) \/ !m :: PL p. j <= m ==> F_SEM M (RESTN p m) (WEAK_CLOCK B_TRUE) (F_BOOL (B_NOT c))) \/ !i :: PL p. F_SEM M (RESTN p i) (WEAK_CLOCK B_TRUE) (F_BOOL (B_NOT c))) /\ (* (F_SEM M p (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = F_SEM M p (STRONG_CLOCK c) (F_UNTIL(f1,f2)) \/ (?k :: PL p. !l :: PL p. l >= k (* changed from l > k *) ==> F_SEM M (RESTN p l) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c)) /\ !j :: PL p. j <= k ==> F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL c) ==> F_SEM M (RESTN p j) (WEAK_CLOCK c) f1)) /\ (F_SEM M p (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = ?i :: PL p. ((?k :: PL p. i <= k /\ NEXT_RISE M p c (i,k) /\ F_SEM M (RESTN p k) (WEAK_CLOCK c) f2) \/ !k :: PL p. i <= k ==> F_SEM M (RESTN p k) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c))) /\ !j :: PL p. j < i ==> (?k :: PL p. j <= k /\ NEXT_RISE M p c (j,k) /\ F_SEM M (RESTN p k) (WEAK_CLOCK c) f1) \/ !k :: PL p. j <= k ==> F_SEM M (RESTN p k) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c))) *) (F_SEM M p (WEAK_CLOCK c) (F_SUFFIX_IMP(r,f)) = !i :: PL p. FIRST_RISE M p c i ==> !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r ==> F_SEM M (RESTN p j) (WEAK_CLOCK c) f) /\ (F_SEM M p (WEAK_CLOCK c) (F_STRONG_IMP(r1,r2)) = F_SEM M p (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2)) \/ (F_SEM M p (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2)) /\ ?k :: PL p. !l :: PL p. l >= k (* changed from l > k *) ==> F_SEM M (RESTN p l) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c)))) /\ (F_SEM M p (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2)) = !i :: PL p. FIRST_RISE M p c i ==> !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r1 ==> ((?k :: PL p. j <= k /\ S_SEM M (LHAT M (PATH_SEG p (j,k))) c r2) \/ !k :: PL p. j <= k ==> ?w. S_SEM M (LHAT M (PATH_SEG p (j,k)) <> w) c r2)) /\ (F_SEM M p (WEAK_CLOCK c) (F_ABORT (f,b)) = !i :: PL p. FIRST_RISE M p c i ==> (F_SEM M (RESTN p i) (WEAK_CLOCK c) f \/ ?j :: PL p. i < j /\ ?p'. (* IS_INFINITE_PATH p' /\ *) F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL(B_AND(c,b))) /\ F_SEM M (PATH_CAT(PATH_SEG p (i,j-1),p')) (WEAK_CLOCK c) f)) /\ (F_SEM M p (WEAK_CLOCK c) (F_WEAK_CLOCK(f,c1)) = F_SEM M p (WEAK_CLOCK c1) f) /\ (F_SEM M p (WEAK_CLOCK c) (F_STRONG_CLOCK(f,c1)) = F_SEM M p (STRONG_CLOCK c1) f); val new_fl_size_def = Define (new_fl_size (F_BOOL _) = 0) /\ (new_fl_size other = fl_size (\a.0) other); val new_context_size_def = Define (new_context_size (STRONG_CLOCK _) = 0) /\ (new_context_size (WEAK_CLOCK _) = 1); val (F_SEM_def, F_SEM_ind) = Count.apply Defn.tprove (F_SEM_defn, WF_REL_TAC inv_image ($< LEX$<) (\(u,v,w,x). (if (?c d. ((w = WEAK_CLOCK c) /\ (x = F_WEAK_IMP d)) \/ ((w = STRONG_CLOCK c) /\ (x = F_STRONG_IMP d))) then 0 else new_fl_size x, new_context_size w)) THEN EVAL_TAC THEN RW_TAC arith_ss [DECIDE (Term 0 < 1 + x)] THEN ((Cases_on f THEN EVAL_TAC THEN DECIDE_TAC) ORELSE (Cases_on f1 THEN EVAL_TAC THEN DECIDE_TAC) ORELSE (Cases_on f2 THEN EVAL_TAC THEN DECIDE_TAC))); val _ = save_thm("F_SEM_def",F_SEM_def); val _ = save_thm("F_SEM_ind",F_SEM_ind); (****************************************************************************** * PATH M p is true iff p is a path with respect to transition relation getR M ******************************************************************************) val PATH_def = Define PATH M p = !n. (getR M)(PATH_EL p n, PATH_EL p (n+1)); (****************************************************************************** * O_SEM M s f means "M, s |= f" ******************************************************************************) val O_SEM_def = Define (O_SEM M s (O_BOOL b) = B_SEM M (L M s) b) /\ (O_SEM M s (O_NOT f) = ~(O_SEM M s f)) /\ (O_SEM M s (O_AND(f1,f2)) = O_SEM M s f1 /\ O_SEM M s f2) /\ (O_SEM M s (O_EX f) = ?p. PATH M p /\ (IS_FINITE_PATH p ==> 1 < PATH_LENGTH p) /\ (PATH_EL p 0 = s) /\ O_SEM M (PATH_EL p 1) f) /\ (O_SEM M s (O_EU(f1,f2)) = ?p. PATH M p /\ (PATH_EL p 0 = s) /\ ?k :: PL p. O_SEM M (PATH_EL p k) f2 /\ !j. j < k ==> O_SEM M (PATH_EL p j) f1) /\ (O_SEM M s (O_EG f) = ?p. PATH M p /\ (PATH_EL p 0 = s) /\ !j :: PL p. O_SEM M (PATH_EL p j) f); (****************************************************************************** * Rules for compiling clocked SEREs to unclocked SEREs * (from B.1, page 66, of Sugar 2.0 Accellera document) ******************************************************************************) val S_CLOCK_COMP_def = Define (S_CLOCK_COMP c (S_BOOL b) = (S_CAT (S_REPEAT (S_BOOL (B_NOT c)),S_BOOL(B_AND(c, b))))) /\ (S_CLOCK_COMP c (S_CAT(r1,r2)) = S_CAT(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2)) /\ (S_CLOCK_COMP c (S_FUSION(r1,r2)) = S_FUSION(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2)) /\ (S_CLOCK_COMP c (S_OR(r1,r2)) = S_OR(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2)) /\ (S_CLOCK_COMP c (S_RIG_AND(r1,r2)) = S_RIG_AND(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2)) /\ (S_CLOCK_COMP c (S_FLEX_AND(r1,r2)) = S_FLEX_AND(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2)) /\ (S_CLOCK_COMP c (S_REPEAT r) = S_REPEAT(S_CLOCK_COMP c r)) /\ (S_CLOCK_COMP c (S_CLOCK(r, c1)) = S_CLOCK_COMP c1 r); (****************************************************************************** * Some abbreviations needed for definition of F_CLOCK_COMP ******************************************************************************) val F_U_CLOCK_def = Define F_U_CLOCK c f = F_UNTIL(F_BOOL(B_NOT c),F_AND(F_BOOL c, f)); val F_OR_def = Define F_OR(f1,f2) = F_NOT(F_AND(F_NOT f1, F_NOT f2)); val F_F_def = Define F_F f = F_UNTIL(F_BOOL B_TRUE, f); val F_G_def = Define F_G f = F_NOT(F_F(F_NOT f)); val F_WEAK_NEXT_def = Define F_WEAK_NEXT f = F_NOT(F_NEXT(F_NOT f)); val F_W_def = Define F_W(f1,f2) = F_OR(F_UNTIL(f1,f2), F_G f1); val F_W_CLOCK_def = Define F_W_CLOCK c f = F_W(F_BOOL(B_NOT c),F_AND(F_BOOL c, f)); (****************************************************************************** * Rules for compiling clocked FL formulas to unclocked formulas * (from B.1, page 66 and 67, of Sugar 2.0 Accellera document) * * Update from IBM: the correct rewrite rules for X! should be: * * (X! f)@clk! = [!clk U clk & X! (!clk U clk & (f@clk!))] * (X! f)@clk = [!clk W clk & X! (!clk U clk & (f@clk!))] * * Change by MJCG on 12.09.02: * (X! f)@clk = [!clk W clk & X! (!clk U clk & (f@clk))] ******************************************************************************) val F_CLOCK_COMP_def = Define (F_CLOCK_COMP (STRONG_CLOCK c) (F_BOOL b) = F_U_CLOCK c (F_BOOL b)) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_NOT f) = F_NOT(F_CLOCK_COMP (WEAK_CLOCK c) f)) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_AND(f1,f2)) = F_U_CLOCK c (F_AND(F_CLOCK_COMP (STRONG_CLOCK c) f1, F_CLOCK_COMP (STRONG_CLOCK c) f2))) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_NEXT f) = F_U_CLOCK c (F_NEXT(F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f)))) /\ (* (F_CLOCK_COMP (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = F_UNTIL(F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f1), F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f2))) *) (F_CLOCK_COMP (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = F_U_CLOCK c (F_UNTIL(F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f1), F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f2)))) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_SUFFIX_IMP(r,f)) = F_U_CLOCK c (F_SUFFIX_IMP(S_CLOCK_COMP c r, F_CLOCK_COMP (STRONG_CLOCK c) f))) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2)) = F_U_CLOCK c (F_STRONG_IMP (S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_WEAK_IMP(r1,r2)) = F_U_CLOCK c (F_OR (F_STRONG_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2), F_AND (F_G(F_F(F_BOOL c)), F_WEAK_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))))) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_ABORT (f,b)) = F_U_CLOCK c (F_ABORT(F_CLOCK_COMP (STRONG_CLOCK c) f, B_AND(c,b)))) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_WEAK_CLOCK(f,c1)) = F_CLOCK_COMP (WEAK_CLOCK c1) f) /\ (F_CLOCK_COMP (STRONG_CLOCK c) (F_STRONG_CLOCK(f,c1)) = F_CLOCK_COMP (STRONG_CLOCK c1) f) /\ (****************************************************************************** * Start of weak clock clauses ******************************************************************************) (F_CLOCK_COMP (WEAK_CLOCK c) (F_BOOL b) = F_W_CLOCK c (F_BOOL b)) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_NOT f) = F_NOT(F_CLOCK_COMP (STRONG_CLOCK c) f)) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_AND(f1,f2)) = F_W_CLOCK c (F_AND(F_CLOCK_COMP (WEAK_CLOCK c) f1, F_CLOCK_COMP (WEAK_CLOCK c) f2))) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_NEXT f) = F_W_CLOCK c (F_NEXT(F_U_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f)))) /\ (* (F_CLOCK_COMP (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = F_UNTIL(F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f1), F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f2))) *) (F_CLOCK_COMP (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = F_W_CLOCK c (F_UNTIL(F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f1), F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f2)))) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_SUFFIX_IMP(r,f)) = F_W_CLOCK c (F_SUFFIX_IMP(S_CLOCK_COMP c r, F_CLOCK_COMP (WEAK_CLOCK c) f))) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_STRONG_IMP(r1,r2)) = F_W_CLOCK c (F_OR (F_STRONG_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2), F_AND (F_F(F_G(F_BOOL(B_NOT c))), F_WEAK_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))))) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2)) = F_W_CLOCK c (F_WEAK_IMP (S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_ABORT (f,b)) = F_W_CLOCK c (F_ABORT(F_CLOCK_COMP (WEAK_CLOCK c) f, B_AND(c,b)))) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_WEAK_CLOCK(f,c1)) = F_CLOCK_COMP (WEAK_CLOCK c1) f) /\ (F_CLOCK_COMP (WEAK_CLOCK c) (F_STRONG_CLOCK(f,c1)) = F_CLOCK_COMP (STRONG_CLOCK c1) f); val _ = export_theory();