Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / 11.BaseState
Base State
PRIORITY
#!python module PRIORITY { imports { pr(ENTITY) ex(OBSERVER2NUMBER) } signature { op priority : Entity -> Observer2Number } }
PRIOR
#!python module PRIOR { imports { pr(INEQUALITY) pr(PRIORITY) ex(OBSERVER2RELATION/ENTITY) } signature { op prior : -> Observer2Relation/Entity } axioms { vars S : System vars X Y : Entity -- (X prior(S) Y) = (priority(X)(S) > priority(Y)(S)) . eq deducible((X prior(S) Y) |- (priority(X)(S) > priority(Y)(S))) = true . eq deducible((priority(X)(S) > priority(Y)(S)) |- (X prior(S) Y)) = true . } }
CLAIM1/PRIOR
#!python module CLAIM1/PRIOR { imports { pr(LK) pr(PRIOR) } signature { op s : -> System ops x y z : -> Entity ops claim1 claim2 claim3 : -> Prop } axioms { eq claim1 = deducible((x prior(s) x) |- nil) . eq claim2 = deducible((x prior(s) y),(y prior(s) x) |- nil) . eq claim3 = deducible((x prior(s) y),(y prior(s) z) |- (x prior(s) z)) . } }
SCORE/CLAIM1/PRIOR
#!python -- confirm irreflexivity open CLAIM1/PRIOR . ops i : -> Inference . ops q1 q2 : -> Sequent . eq q1 = ((priority(x)(s) > priority(x)(s)) |- nil) . eq q2 = ((x prior(s) x) |- (priority(x)(s) > priority(x)(s))) . eq antecedent(i) = (q1,q2) . eq ((x prior(s) x) |- nil) = consequent(i) . red claim1 . close -- confirm asymmetricity open CLAIM1/PRIOR . ops i : -> Inference . ops q1 q2 q3 : -> Sequent . eq q1 = ((priority(x)(s) > priority(y)(s)),(priority(y)(s) > priority(x)(s)) |- nil) . eq q2 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) . eq q3 = ((y prior(s) x) |- (priority(y)(s) > priority(x)(s))) . eq antecedent(i) = (q1,q2,q3) . eq ((x prior(s) y),(y prior(s) x) |- nil) = consequent(i) . red claim2 . close -- confirm transitivity open CLAIM1/PRIOR . ops i1 i2 : -> Inference . ops q1 q2 q3 q4 : -> Sequent . eq q1 = ((priority(x)(s) > priority(y)(s)),(priority(y)(s) > priority(z)(s)) |- (priority(x)(s) > priority(z)(s))) . eq q2 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) . eq q3 = ((y prior(s) z) |- (priority(y)(s) > priority(z)(s))) . eq q4 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) . eq antecedent(i1) = (q1,q2,q3) . trans ((x prior(s) y),(y prior(s) z) |- (priority(x)(s) > priority(z)(s))) => consequent(i1) . trans consequent(i1) => ((x prior(s) y),(y prior(s) z) |- (priority(x)(s) > priority(z)(s))) . eq antecedent(i2) = (consequent(i1),q4) . eq ((x prior(s) y),(y prior(s) z) |- (x prior(s) z)) = consequent(i2) . red claim3 . close
#!python
LEMMA5/COMPLEMENT/NUMBER
#!python make LEMMA5/COMPLEMENT/NUMBER ( LEMMA5/COMPLEMENT( NUMBER { sort Elt -> Number }, RELATION/NUMBER { sort Relation -> Relation/Number }, IRREFLEXIVE/NUMBER { sort Irreflexive -> Irreflexive/Number }, ASYMMETRIC/NUMBER { sort Asymmetric -> Asymmetric/Number }, TRANSITIVE/NUMBER { sort Transitive -> Transitive/Number }, PARTIALORDER/NUMBER { sort PartialOrder -> PartialOrder/Number }, TOTALORDER/NUMBER { sort TotalOrder -> TotalOrder/Number }, COMPLEMENT/NUMBER ) )
CLAIM2/PRIOR
#!python module CLAIM2/PRIOR { imports { pr(PRIOR) pr(LEMMA5/COMPLEMENT/NUMBER) pr(COMPLEMENT/ENTITY) } signature { op s : -> System ops x y z : -> Entity ops claim1 claim2 claim3 : -> Prop } axioms { eq claim1 = deducible((x [prior(s)] y),(y prior(s) z) |- (x prior(s) z)) . eq claim2 = deducible((x prior(s) y),(y [prior(s)] z) |- (x prior(s) z)) . eq claim3 = deducible((x [prior(s)] y),(y [prior(s)] z) |- (x [prior(s)] z)) . } }
SCORE/CLAIM2/PRIOR
#!python -- proof that the partialorder prior satisfies axioms of PartialOrder' -- proof of claim1 open CLAIM2/PRIOR . ops i1 : -> Inference . ops q1 q2 q3 : -> Sequent . eq q1 = (nil |- (priority(x)(s) [>] priority(y)(s)),(priority(y)(s) > priority(x)(s))) . eq q2 = ((priority(y)(s) > priority(x)(s)) |- (y prior(s) x)) . eq q3 = ((x [prior(s)] y),(y prior(s) x) |- nil) . eq antecedent(i1) = (q1,q2,q3) . trans ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) => consequent(i1) . trans consequent(i1) => ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) . ops i2 : -> Inference . ops q4 q5 q6 : -> Sequent . eq q4 = ((priority(x)(s) [>] priority(y)(s)), (priority(y)(s) > priority(z)(s)) |- (priority(x)(s) > priority(z)(s))) . eq q5 = ((y prior(s) z) |- (priority(y)(s) > priority(z)(s))) . eq q6 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) . eq antecedent(i2) = (q4,q5,q6) . trans ((priority(x)(s) [>] priority(y)(s)),(y prior(s) z) |- (x prior(s) z)) => consequent(i2) . trans consequent(i2) => ((priority(x)(s) [>] priority(y)(s)),(y prior(s) z) |- (x prior(s) z)) . ops i3 : -> Inference . eq antecedent(i3) = (consequent(i1),consequent(i2)) . eq ((x [prior(s)] y),(y prior(s) z) |- (x prior(s) z)) = consequent(i3) . red claim1 . close -- proof of claim2 open CLAIM2/PRIOR . ops i1 : -> Inference . ops q1 q2 q3 : -> Sequent . eq q1 = (nil |- (priority(y)(s) [>] priority(z)(s)),(priority(z)(s) > priority(y)(s))) . eq q2 = ((priority(z)(s) > priority(y)(s)) |- (z prior(s) y)) . eq q3 = ((y [prior(s)] z),(z prior(s) y) |- nil) . eq antecedent(i1) = (q1,q2,q3) . trans ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) => consequent(i1) . trans consequent(i1) => ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) . ops i2 : -> Inference . ops q4 q5 q6 : -> Sequent . eq q4 = ((priority(x)(s) > priority(y)(s)), (priority(y)(s) [>] priority(z)(s)) |- (priority(x)(s) > priority(z)(s))) . eq q5 = ((x prior(s) y) |- (priority(x)(s) > priority(y)(s))) . eq q6 = ((priority(x)(s) > priority(z)(s)) |- (x prior(s) z)) . eq antecedent(i2) = (q4,q5,q6) . trans ((x prior(s) y),(priority(y)(s) [>] priority(z)(s)) |- (x prior(s) z)) => consequent(i2) . trans consequent(i2) => ((x prior(s) y),(priority(y)(s) [>] priority(z)(s)) |- (x prior(s) z)) . ops i3 : -> Inference . eq antecedent(i3) = (consequent(i1),consequent(i2)) . eq ((x prior(s) y),(y [prior(s)] z) |- (x prior(s) z)) = consequent(i3) . red claim2 . close -- proof of claim3 open CLAIM2/PRIOR . ops i1 : -> Inference . ops q1 q2 q3 : -> Sequent . eq q1 = (nil |- (priority(x)(s) [>] priority(y)(s)),(priority(y)(s) > priority(x)(s))) . eq q2 = ((priority(y)(s) > priority(x)(s)) |- (y prior(s) x)) . eq q3 = ((x [prior(s)] y),(y prior(s) x) |- nil) . eq antecedent(i1) = (q1,q2,q3) . trans ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) => consequent(i1) . trans consequent(i1) => ((x [prior(s)] y) |- (priority(x)(s) [>] priority(y)(s))) . ops i2 : -> Inference . ops q4 q5 q6 : -> Sequent . eq q4 = (nil |- (priority(y)(s) [>] priority(z)(s)),(priority(z)(s) > priority(y)(s))) . eq q5 = ((priority(z)(s) > priority(y)(s)) |- (z prior(s) y)) . eq q6 = ((y [prior(s)] z),(z prior(s) y) |- nil) . eq antecedent(i2) = (q4,q5,q6) . trans ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) => consequent(i2) . trans consequent(i2) => ((y [prior(s)] z) |- (priority(y)(s) [>] priority(z)(s))) . ops i3 : -> Inference . ops q7 q8 q9 : -> Sequent . eq q7 = ((priority(x)(s) [>] priority(z)(s)),(priority(z)(s) > priority(x)(s)) |- nil) . eq q8 = ((z prior(s) x) |- (priority(z)(s) > priority(x)(s))) . eq q9 = (nil |- (x [prior(s)] z),(z prior(s) x)) . eq antecedent(i3) = (q7,q8,q9) . trans ((priority(x)(s) [>] priority(z)(s)) |- (x [prior(s)] z)) => consequent(i3) . trans consequent(i3) => ((priority(x)(s) [>] priority(z)(s)) |- (x [prior(s)] z)) . ops i4 : -> Inference . ops q10 : -> Sequent . eq q10 = ((priority(x)(s) [>] priority(y)(s)),(priority(y)(s) [>] priority(z)(s)) |- (priority(x)(s) [>] priority(z)(s))) . eq antecedent(i4) = (q10,consequent(i1),consequent(i2)) . trans ((x [prior(s)] y),(y [prior(s)] z) |- (priority(x)(s) [>] priority(z)(s))) => consequent(i4) . trans consequent(i4) => ((x [prior(s)] y),(y [prior(s)] z) |- (priority(x)(s) [>] priority(z)(s))) . ops i5 : -> Inference . eq antecedent(i5) = (consequent(i3),consequent(i4)) . eq ((x [prior(s)] y),(y [prior(s)] z) |- (x [prior(s)] z)) = consequent(i5) . red claim3 . close
#!python
PRIOR/REV1
#!python module PRIOR { imports { pr(INEQUALITY) pr(PRIORITY) ex(OBSERVER2PARTIALORDER'/ENTITY) } signature { op prior : -> Observer2PartialOrder'/Entity } axioms { vars S : System vars X Y : Entity -- (X prior(S) Y) = (priority(X)(S) > priority(Y)(S)) . eq deducible((X prior(S) Y) |- (priority(X)(S) > priority(Y)(S))) = true . eq deducible((priority(X)(S) > priority(Y)(S)) |- (X prior(S) Y)) = true . } }
ENTRY
#!python module ENTRY { imports { pr(OBSERVER2LIST/ENTITY) } signature { op entry : -> Observer2List/Entity } }
AHEAD
#!python module AHEAD { imports { pr(FORMER/ENTITY) pr(ENTRY) ex(OBSERVER2RELATION/ENTITY) } signature { op ahead : -> Observer2Relation/Entity } axioms { vars S : System vars X Y : Entity eq (X ahead(S) Y) = (X former(entry(S)) Y) . } }
SCORE/CLAIM1/AHEAD
#!python open AHEAD . ops s : -> System . ops x y z : -> Entity . red deducible((x ahead(s) x) |- nil) . red deducible((x ahead(s) y),(y ahead(s) x) |- nil) . red deducible((x ahead(s) y),(y ahead(s) z) |- (x ahead(s) z)) . close
AHEAD/REV1
#!python module AHEAD { imports { pr(FORMER/ENTITY) pr(ENTRY) ex(OBSERVER2PARTIALORDER/ENTITY) } signature { op ahead : -> Observer2PartialOrder/Entity } axioms { vars S : System vars X Y : Entity -- (X ahead(S) Y) = (X former(entry(S)) Y) . eq deducible((X former(entry(S)) Y) |- (X ahead(S) Y)) = true . eq deducible((X ahead(S) Y) |- (X former(entry(S)) Y)) = true . eq deducible((X @ entry(S)),(Y @ entry(S)) |- (X ahead(S) Y),(X = Y),(Y ahead(S) X)) = true . eq deducible((X ahead(S) Y) |- (X @ entry(S))) = true . eq deducible((X ahead(S) Y) |- (Y @ entry(S))) = true . } }
PRECEDE
#!python module PRECEDE { imports { pr(PRIOR) pr(AHEAD) pr(OVERRIDE/ENTITY) } signature { op precede : -> Observer2PartialOrder/Entity } axioms { vars S : System vars X Y : Entity eq precede(S) = [prior(S);ahead(S)] . } }
NEXT
#!python module NEXT { imports { pr(ROOT/ENTITY) pr(PRECEDE) ex(RUNNABLE) } signature { op next : -> Observer2Set/Entity } axioms { vars S : System vars X : Entity eq next(S) = root(runnable(S),precede(S)) . } }
CURRENT
#!python module CURRENT { imports { ex(OBSERVER2SET/ENTITY) } signature { op current : -> Observer2Set/Entity } }
BLOCK
#!python module BLOCK { imports { ex(OBSERVER2RELATION/ENTITY) } signature { op block : -> Observer2Relation/Entity } }
BASESTATE
#!python module BASESTATE { imports { pr(ASSIGN) pr(CURRENT) pr(PRECEDE) pr(BLOCK) } }
CLAIM1/BASESTATE
#!python module CLAIM1/BASESTATE { imports { pr(BASESTATE) pr(LK) } signature { op s : -> System ops x y : -> Entity op claim : -> Prop } axioms { vars X Y : Entity eq deducible((X block(s) X) |- nil) = true . eq deducible((X block(s) Y),(X ahead(s) Y) |- (priority(Y)(s) = assign(Y))) = true . eq deducible((X block(s) Y),(Y ahead(s) X) |- (X [prior(s);ahead(s)] Y)) = true . eq deducible((X block(s) Y),(assign(Y) > priority(X)(s)) |- nil) = true . eq claim = deducible((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x precede(s) y)) . } }
SCORE/CLAIM1/BASESTATE
#!python open CLAIM1/BASESTATE . ops i1 : -> Inference . ops q11 q12 q13 : -> Sequent . eq q11 = ((x block(s) y),(assign(y) > priority(x)(s)) |- nil) . eq q12 = ((priority(y)(s) = assign(y)),(priority(y)(s) > priority(x)(s)) |- (assign(y) > priority(x)(s))) . eq q13 = ((y prior(s) x) |- (priority(y)(s) > priority(x)(s))) . eq antecedent(i1) = (q11,q12,q13) . trans ((x block(s) y),(priority(y)(s) = assign(y)),(y prior(s) x) |- nil) => consequent(i1) . trans consequent(i1) => ((x block(s) y),(priority(y)(s) = assign(y)),(y prior(s) x) |- nil) . ops i2 : -> Inference . ops q21 : -> Sequent . eq q21 = ((x block(s) y),(x ahead(s) y) |- (priority(y)(s) = assign(y))) . eq antecedent(i2) = (consequent(i1),q21) . trans ((x block(s) y),(x ahead(s) y),(y prior(s) x) |- nil) => consequent(i2) . trans consequent(i2) => ((x block(s) y),(x ahead(s) y),(y prior(s) x) |- nil) . ops i3 : -> Inference . ops q31 q32 : -> Sequent . eq q31 = ((x ahead(s) y),(x [prior(s)] y) |- (x precede(s) y)) . eq q32 = (nil |- (x [prior(s)] y),(y prior(s) x)) . eq antecedent(i3) = (consequent(i2),q31,q32) . trans ((x block(s) y),(x ahead(s) y) |- (x [prior(s);ahead(s)] y)) => consequent(i3) . trans consequent(i3) => ((x block(s) y),(x ahead(s) y) |- (x [prior(s);ahead(s)] y)) . ops i4 : -> Inference . ops q41 q42 : -> Sequent . eq q41 = ((x block(s) x) |- nil) . eq q42 = ((x = y),(x block(s) y) |- (x block(s) x)) . eq antecedent(i4) = (q41,q42) . trans ((x = y),(x block(s) y) |- nil) => consequent(i4) . trans consequent(i4) => ((x = y),(x block(s) y) |- nil) . ops i5 : -> Inference . ops q51 : -> Sequent . eq q51 = ((x @ entry(s)),(y @ entry(s)) |- (x ahead(s) y),(x = y),(y ahead(s) x)) . eq antecedent(i5) = (consequent(i4),q51) . trans ((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x ahead(s) y),(y ahead(s) x)) => consequent(i5) . trans consequent(i5) => ((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x ahead(s) y),(y ahead(s) x)) . ops i6 : -> Inference . ops q61 : -> Sequent . eq q61 = ((x block(s) y),(y ahead(s) x) |- (x [prior(s);ahead(s)] y)) . eq antecedent(i6) = (consequent(i3),consequent(i5),q61) . eq ((x @ entry(s)),(y @ entry(s)),(x block(s) y) |- (x [prior(s);ahead(s)] y)) = consequent(i6) . red claim . close
THEOREM1/BASESTATE
#!python module THEOREM1/BASESTATE { imports { pr(BASESTATE) pr(LK) } axioms { vars S : System vars X Y : Entity cq deducible((X @ entry(S)),(Y @ entry(S)),(X block(S) Y) |- (X [prior(S);ahead(S)] Y)) = true if (deducible((X block(S) X) |- nil) = true) and (deducible((X block(S) Y),(X ahead(S) Y) |- (priority(Y)(S) = assign(Y))) = true) and (deducible((X block(S) Y),(Y ahead(S) X) |- (X [prior(S);ahead(S)] Y)) = true) and (deducible((X block(S) Y),(assign(Y) > priority(X)(S)) |- nil) = true) . } }
Updated