Library EntAuxResults
This file was written by Colm Bhandal, PhD student, Foundations and Methods group,
School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
*************************** Standard Imports
Require Import ComhCoq.Extras.LibTactics.
Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.EntityLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Lemma reachable_ent_prot p l h k : reachableEnt ([| p, l, h, k |]) ->
reachableProt p. intros. Admitted.
Lemma nextModeEnt_not_stable m1 m2 p l h :
nextModeEnt m1 ([|p, l, h, m2|]) -> False. intros. Admitted.
Lemma mst_tout_mCurr_in m1 m2 :
discActEnabledMState (chanMCurr *?) (<| m1, m2, zeroTime |>). intros.
repeat econstructor. Qed.
Lemma tfsNext_prev_ent m e e' a : tfsNextStateEnt m e' ->
e -EA- a ->> e' -> tfsNextStateEnt m e \/ tfsStartStateEnt e.
Admitted.
Lemma currEq_mode m m'' e :
currEqStateEnt m m'' e -> m = currModeEnt e. Admitted.
Lemma ovAbort_unstable e : reachableEnt e -> ovAbortStateEnt e -> unstable (mstEnt e).
introz U. Admitted.
Lemma tfsCurr_failSafe (e : Entity) (m : Mode) :
tfsCurrStateEnt e -> exists m, nextModeEnt m e /\ failSafe m.
Admitted.
Lemma tfsBc_failSafe (e : Entity) :
tfsBcStateEnt e -> failSafe (currModeEnt e).
introz U. Admitted.
Lemma tfsNext_currMode e m :
reachableEnt e -> tfsNextStateEnt m e -> currModeEnt e = m.
introz U.
Admitted.
Theorem switchCurr_mState (e : Entity) :
reachableEnt e -> switchCurrStateEnt e -> exists m m',
mstEnt e = <| m, m', zeroTime |>. Admitted.
If an entity is in a state ready to output some m l from the broadcast component,
then it is in the position l.
Theorem bcReady_pos (e : Entity) (m : Mode) (l : Position) :
reachableEnt e -> bcReadyStateEnt m l e -> inPosEnt l e. Admitted.
reachableEnt e -> bcReadyStateEnt m l e -> inPosEnt l e. Admitted.
If an entity is in a state ready to output some m l from the overlap component,
then it is in the position l.
Theorem ovReady_pos (e : Entity) (m : Mode) (t : Time) (l : Position) :
reachableEnt e -> ovReadyStateEnt m t l e -> inPosEnt l e. Admitted.
Lemma tfsListen_paused p1 p2 p3 :
tfsListenStateProt (p1 $||$ p2 $||$ p3) -> pausedStateProt (p1 $||$ p2 $||$ p3).
Admitted.
reachableEnt e -> ovReadyStateEnt m t l e -> inPosEnt l e. Admitted.
Lemma tfsListen_paused p1 p2 p3 :
tfsListenStateProt (p1 $||$ p2 $||$ p3) -> pausedStateProt (p1 $||$ p2 $||$ p3).
Admitted.
If an entity inputs a message then that message is incoming.
Lemma input_incomingEnt (v : list BaseType) (e e' : Entity) (l : Position) (r : Distance) :
e -EA- ([-v, l, r-]) #? ->> e' -> incomingEnt v e'.
introz U. inversion U. constructor. inversion H5.
constructor. inversion H8. constructor.
reflexivity. inversion H10. Qed.
Ltac urgency_pre_tac :=
let U := fresh "U" in
(try match goal with [ |- forall e : Entity, _] =>
intros e e' d; introz U end); destrEnts_norm;
match goal with [ RE : reachableEnt _ |- _] =>
apply reachable_ent_prot in RE end; let q := fresh "Q" in reachprot q;
inversion q as [p1 p2 p3 BC OV LI TR]; symmetry in TR.
e -EA- ([-v, l, r-]) #? ->> e' -> incomingEnt v e'.
introz U. inversion U. constructor. inversion H5.
constructor. inversion H8. constructor.
reflexivity. inversion H10. Qed.
Ltac urgency_pre_tac :=
let U := fresh "U" in
(try match goal with [ |- forall e : Entity, _] =>
intros e e' d; introz U end); destrEnts_norm;
match goal with [ RE : reachableEnt _ |- _] =>
apply reachable_ent_prot in RE end; let q := fresh "Q" in reachprot q;
inversion q as [p1 p2 p3 BC OV LI TR]; symmetry in TR.
SE SP and S are the names of the state predicates involved- the entity,
the protocol and the standard ones respectively.
Ltac urgency_pre_tac2 SE SP S :=
urgency_pre_tac;
match goal with
| [ _ : SE ([|?p0, ?l0, ?h0, ?k0|]) |- _] =>
assert (SP p0) as TP;
[inversion U0; assumption | ];
match goal with
| [ TR : p0 = ?p1 $||$ ?p2 $||$ ?p3, TP : SP p0 |- _] =>
rewrite TR in TP end
end;
match goal with [ _ : SP (?p1 $||$ ?p2 $||$ ?p3) |- _]
=> try (assert (S p1) as TS; [inversion TP; assumption | ]);
try (assert (S p2) as TS; [inversion TP; assumption | ]);
try (assert (S p3) as TS; [inversion TP; assumption | ]) end.
urgency_pre_tac;
match goal with
| [ _ : SE ([|?p0, ?l0, ?h0, ?k0|]) |- _] =>
assert (SP p0) as TP;
[inversion U0; assumption | ];
match goal with
| [ TR : p0 = ?p1 $||$ ?p2 $||$ ?p3, TP : SP p0 |- _] =>
rewrite TR in TP end
end;
match goal with [ _ : SP (?p1 $||$ ?p2 $||$ ?p3) |- _]
=> try (assert (S p1) as TS; [inversion TP; assumption | ]);
try (assert (S p2) as TS; [inversion TP; assumption | ]);
try (assert (S p3) as TS; [inversion TP; assumption | ]) end.
Same as urgency_pre_tac2 but the state predicate has 1 parameter.
Ltac urgency_pre_tac2_1 SE SP S :=
urgency_pre_tac;
match goal with
| [ _ : SE ?x1 ([|?p0, ?l0, ?h0, ?k0|]) |- _] =>
assert (SP x1 p0) as TP;
[inversion U0; assumption | ];
match goal with
| [ TR : p0 = ?p1 $||$ ?p2 $||$ ?p3, TP : SP x1 p0 |- _] =>
rewrite TR in TP end
end;
match goal with [ _ : SP ?x1 (?p1 $||$ ?p2 $||$ ?p3) |- _]
=> try (assert (S x1 p1) as TS; [inversion TP; assumption | ]);
try (assert (S x1 p2) as TS; [inversion TP; assumption | ]);
try (assert (S x1 p3) as TS; [inversion TP; assumption | ]) end.
urgency_pre_tac;
match goal with
| [ _ : SE ?x1 ([|?p0, ?l0, ?h0, ?k0|]) |- _] =>
assert (SP x1 p0) as TP;
[inversion U0; assumption | ];
match goal with
| [ TR : p0 = ?p1 $||$ ?p2 $||$ ?p3, TP : SP x1 p0 |- _] =>
rewrite TR in TP end
end;
match goal with [ _ : SP ?x1 (?p1 $||$ ?p2 $||$ ?p3) |- _]
=> try (assert (S x1 p1) as TS; [inversion TP; assumption | ]);
try (assert (S x1 p2) as TS; [inversion TP; assumption | ]);
try (assert (S x1 p3) as TS; [inversion TP; assumption | ]) end.
Same as urgency_pre_tac2 but the state predicate has 2 parameters.
Ltac urgency_pre_tac2_2 SE SP S :=
urgency_pre_tac;
match goal with
| [ _ : SE ?x1 ?x2 ([|?p0, ?l0, ?h0, ?k0|]) |- _] =>
assert (SP x1 x2 p0) as TP;
[inversion U0; assumption | ];
match goal with
| [ TR : p0 = ?p1 $||$ ?p2 $||$ ?p3, TP : SP x1 x2 p0 |- _] =>
rewrite TR in TP end
end;
match goal with [ _ : SP ?x1 ?x2 (?p1 $||$ ?p2 $||$ ?p3) |- _]
=> try (assert (S x1 x2 p1) as TS; [inversion TP; assumption | ]);
try (assert (S x1 x2 p2) as TS; [inversion TP; assumption | ]);
try (assert (S x1 x2 p3) as TS; [inversion TP; assumption | ]) end.
Lemma gotMsgStateEnt_urgent (e e' : Entity) (d : Delay) m l :
reachableEnt e -> gotMsgStateEnt m l e -> e -ED- d ->> e' -> False.
Admitted.
Lemma gotRangeStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> gotRangeStateEnt m r e -> e -ED- d ->> e' -> False.
Admitted.
Lemma currCompStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> currCompStateEnt m r e -> e -ED- d ->> e' -> False.
Admitted.
Lemma abortOvlpStateEnt_urgent (e e' : Entity) (d : Delay) :
reachableEnt e -> abortOvlpStateEnt e -> e -ED- d ->> e' -> False.
Admitted.
Lemma tfsStartStateEnt_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsStartStateEnt e -> e -ED- d ->> e' -> False.
urgency_pre_tac2 tfsStartStateEnt tfsStartStateProt tfsStartState.
lets MC : modeState_curr_enabled k0.
remember (chanMCurr ;? [baseMode (currModeMState k0)]) as a.
assert (discActEnabled p2 a). rewrite Heqa.
apply tfsStart_mCurr_in. assumption.
del_noSyncNow_tac NS. eapply NS.
rewrite TR. apply daeParR. apply daeParL. assumption. rewrite Heqa.
assumption. Qed.
Lemma tfsListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsListenStateEnt e -> e -ED- d ->> e'
-> False.
urgency_pre_tac2 tfsListenStateEnt tfsListenStateProt tfsListenState.
del_triple_sort_tac.
lets PA : tfsListen_paused TP. assert (pausedState p3). inversion PA.
assumption. lets PAP : paused_unpause_in_sort H.
lets TAP : tfsListen_unpause_out_sort TS. apply SORT2_3 in TAP.
apply TAP. apply PAP. Qed.
Lemma tfsNext_urgent : forall (m : Mode) (e e' : Entity) (d : Delay),
reachableEnt e -> tfsNextStateEnt m e -> e -ED- d ->> e' -> False.
intro m. intros e e' d. introz U.
lets TCM : tfsNext_currMode U U0.
urgency_pre_tac2_1 tfsNextStateEnt tfsNextStateProt tfsNextState.
lets FS : failSafeSucc_successor m.
assert (k0 -mtr-> failSafeSucc m) as FS2. simpl in TCM.
rewrite TCM. assumption.
lets MS : mState_stable_next_enabled FS2. noSyncNow_tac.
elim_intro MS MS1 MS2.
lets TF : tfsNext_mStable_out TS.
assert (discActEnabled p0 (chanMStable;! [])) as DA.
rewrite TR. apply parTriple_dae_intro2. assumption.
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA2.
assumption.
lets TF : tfsNext_mNext_out TS.
assert (discActEnabled p0 (chanMNext;! [baseMode (failSafeSucc m)]))
as DA. rewrite TR. apply parTriple_dae_intro2. assumption.
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA2.
apply MS2. Qed.
Lemma bcReady_urgent (m : Mode) (l : Position) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> bcReadyStateEnt m l e -> e -ED- d ->> e'
-> False. urgency_pre_tac2_2 bcReadyStateEnt bcReadyStateProt bcReadyState.
noSyncNow_tac. lets BO : bcReady_outProc_out TS.
assert (discActEnabled p0 (chanOutProc;! [baseMode m, basePosition l])) as DA.
rewrite TR. apply parTriple_dae_intro1. assumption.
lets IO : interface_outProc_in h0 [baseMode m, basePosition l].
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA1. assumption.
Qed.
Lemma ovAbort_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> ovAbortStateEnt e -> e -ED- d ->> e'
-> False. intros e e' d. introz U.
lets OUS : ovAbort_unstable U U0.
urgency_pre_tac2 ovAbortStateEnt ovAbortStateProt ovAbortState.
noSyncNow_tac. lets OAS : ovAbort_stable_out TS.
lets US : unstable_stable_in OUS.
assert (discActEnabled p0 (chanMStable *!)) as DA.
rewrite TR. apply parTriple_dae_intro2. assumption.
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA2.
assumption. Qed.
Lemma tfsBc_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsBcStateEnt e -> e -ED- d ->> e'
-> False. intros e e' d. introz U. lets Q : U.
urgency_pre_tac2 tfsBcStateEnt tfsBcStateProt tfsBcState.
lets TOT : tfsBc_trans_out TS.
inversion BC.
lets BIT : bcWait_trans_in H. del_triple_sort_tac. eapply enabledInSort_in in BIT.
apply SORT1_2 in BIT. apply BIT. apply enabledInSort_out. assumption.
lets SIT : sleep_trans_in H. del_triple_sort_tac. eapply enabledInSort_in in SIT.
apply SORT1_2 in SIT. apply SIT. apply enabledInSort_out. assumption.
assert (bcReadyStateEnt m l1 ([|p0, l0, h0, k0|])) as BCE. constructor.
rewrite TR. constructor. assumption. lets BCU : bcReady_urgent U BCE.
apply BCU. apply U1. Qed.
Lemma switchBc_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchBcStateEnt m e -> e -ED- d ->> e'
-> False. intros e e' d. introz U. lets Q : U.
urgency_pre_tac2_1 switchBcStateEnt switchBcStateProt switchBcState.
lets TOT : switchBc_wake_out TS.
inversion BC.
lets BIT : bcWait_wake_in H. del_triple_sort_tac. eapply enabledInSort_in in BIT.
apply SORT1_2 in BIT. apply BIT. apply enabledInSort_out. apply TOT.
lets SIT : sleeping_wake_in H. del_triple_sort_tac. eapply enabledInSort_in in SIT.
apply SORT1_2 in SIT. apply SIT. apply enabledInSort_out. apply TOT.
assert (bcReadyStateEnt m0 l1 ([|p0, l0, h0, k0|])) as BCE. constructor.
rewrite TR. constructor. assumption. lets BCU : bcReady_urgent U BCE.
apply BCU. apply U1. Qed.
Lemma swithcCurr_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchCurrStateEnt e -> e -ED- d ->> e'
-> False. intros e e' d. introz U. lets Q : U.
urgency_pre_tac2 switchCurrStateEnt switchCurrStateProt switchCurrState.
lets SMS : switchCurr_mState U U0. decompEx2 SMS m1 m2 MS.
lets NIM : mst_tout_mCurr_in m1 m2.
lets SOM : switchCurr_mCurr_out TS.
assert (discActEnabled p0 (chanMCurr *!)) as DA.
rewrite TR. apply parTriple_dae_intro2. assumption.
noSyncNow_tac. apply NS in DA. decompAnd2 DA NDA1 NDA2.
apply NDA2. simpl in MS. rewrite MS. assumption. Qed.
Lemma switchListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchListenStateEnt e -> e -ED- d ->> e'
-> False. urgency_pre_tac2 switchListenStateEnt switchListenStateProt
switchListenState.
assert (switchStateProt p0) as SP. rewrite TR. constructor. apply switLisSt.
assumption. lets PS : paused_switch U. rewrite <- PS in SP. rewrite TR in SP.
del_triple_sort_tac. assert (pausedState p3) as PS3. inversion SP. assumption.
lets PIU : paused_unpause_in_sort PS3. lets SOU : switchListen_unpause_out_sort TS.
apply SORT2_3 in SOU. apply SOU. apply PIU. Qed.
Lemma msgAbortPathEnt_urgent e e' d :
reachableEnt e -> msgAbortPathEnt e ->
e -ED- d ->> e' -> False. intro.
introz U. inversion U; subst.
assert (gotMsgStateEnt m'' l' ([|p, l, h, k|])).
econstructor; eassumption.
eapply gotMsgStateEnt_urgent; eassumption.
assert (gotRangeStateEnt m'' r ([|p, l, h, k|])).
econstructor; eassumption.
eapply gotRangeStateEnt_urgent; eassumption.
assert (currCompStateEnt m'' r ([|p, l, h, k|])).
econstructor; eassumption.
eapply currCompStateEnt_urgent; eassumption.
assert (abortOvlpStateEnt ([|p, l, h, k|])).
econstructor; eassumption.
eapply abortOvlpStateEnt_urgent; eassumption. Qed.
urgency_pre_tac;
match goal with
| [ _ : SE ?x1 ?x2 ([|?p0, ?l0, ?h0, ?k0|]) |- _] =>
assert (SP x1 x2 p0) as TP;
[inversion U0; assumption | ];
match goal with
| [ TR : p0 = ?p1 $||$ ?p2 $||$ ?p3, TP : SP x1 x2 p0 |- _] =>
rewrite TR in TP end
end;
match goal with [ _ : SP ?x1 ?x2 (?p1 $||$ ?p2 $||$ ?p3) |- _]
=> try (assert (S x1 x2 p1) as TS; [inversion TP; assumption | ]);
try (assert (S x1 x2 p2) as TS; [inversion TP; assumption | ]);
try (assert (S x1 x2 p3) as TS; [inversion TP; assumption | ]) end.
Lemma gotMsgStateEnt_urgent (e e' : Entity) (d : Delay) m l :
reachableEnt e -> gotMsgStateEnt m l e -> e -ED- d ->> e' -> False.
Admitted.
Lemma gotRangeStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> gotRangeStateEnt m r e -> e -ED- d ->> e' -> False.
Admitted.
Lemma currCompStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> currCompStateEnt m r e -> e -ED- d ->> e' -> False.
Admitted.
Lemma abortOvlpStateEnt_urgent (e e' : Entity) (d : Delay) :
reachableEnt e -> abortOvlpStateEnt e -> e -ED- d ->> e' -> False.
Admitted.
Lemma tfsStartStateEnt_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsStartStateEnt e -> e -ED- d ->> e' -> False.
urgency_pre_tac2 tfsStartStateEnt tfsStartStateProt tfsStartState.
lets MC : modeState_curr_enabled k0.
remember (chanMCurr ;? [baseMode (currModeMState k0)]) as a.
assert (discActEnabled p2 a). rewrite Heqa.
apply tfsStart_mCurr_in. assumption.
del_noSyncNow_tac NS. eapply NS.
rewrite TR. apply daeParR. apply daeParL. assumption. rewrite Heqa.
assumption. Qed.
Lemma tfsListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsListenStateEnt e -> e -ED- d ->> e'
-> False.
urgency_pre_tac2 tfsListenStateEnt tfsListenStateProt tfsListenState.
del_triple_sort_tac.
lets PA : tfsListen_paused TP. assert (pausedState p3). inversion PA.
assumption. lets PAP : paused_unpause_in_sort H.
lets TAP : tfsListen_unpause_out_sort TS. apply SORT2_3 in TAP.
apply TAP. apply PAP. Qed.
Lemma tfsNext_urgent : forall (m : Mode) (e e' : Entity) (d : Delay),
reachableEnt e -> tfsNextStateEnt m e -> e -ED- d ->> e' -> False.
intro m. intros e e' d. introz U.
lets TCM : tfsNext_currMode U U0.
urgency_pre_tac2_1 tfsNextStateEnt tfsNextStateProt tfsNextState.
lets FS : failSafeSucc_successor m.
assert (k0 -mtr-> failSafeSucc m) as FS2. simpl in TCM.
rewrite TCM. assumption.
lets MS : mState_stable_next_enabled FS2. noSyncNow_tac.
elim_intro MS MS1 MS2.
lets TF : tfsNext_mStable_out TS.
assert (discActEnabled p0 (chanMStable;! [])) as DA.
rewrite TR. apply parTriple_dae_intro2. assumption.
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA2.
assumption.
lets TF : tfsNext_mNext_out TS.
assert (discActEnabled p0 (chanMNext;! [baseMode (failSafeSucc m)]))
as DA. rewrite TR. apply parTriple_dae_intro2. assumption.
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA2.
apply MS2. Qed.
Lemma bcReady_urgent (m : Mode) (l : Position) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> bcReadyStateEnt m l e -> e -ED- d ->> e'
-> False. urgency_pre_tac2_2 bcReadyStateEnt bcReadyStateProt bcReadyState.
noSyncNow_tac. lets BO : bcReady_outProc_out TS.
assert (discActEnabled p0 (chanOutProc;! [baseMode m, basePosition l])) as DA.
rewrite TR. apply parTriple_dae_intro1. assumption.
lets IO : interface_outProc_in h0 [baseMode m, basePosition l].
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA1. assumption.
Qed.
Lemma ovAbort_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> ovAbortStateEnt e -> e -ED- d ->> e'
-> False. intros e e' d. introz U.
lets OUS : ovAbort_unstable U U0.
urgency_pre_tac2 ovAbortStateEnt ovAbortStateProt ovAbortState.
noSyncNow_tac. lets OAS : ovAbort_stable_out TS.
lets US : unstable_stable_in OUS.
assert (discActEnabled p0 (chanMStable *!)) as DA.
rewrite TR. apply parTriple_dae_intro2. assumption.
apply NS in DA. decompAnd2 DA NDA1 NDA2. apply NDA2.
assumption. Qed.
Lemma tfsBc_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsBcStateEnt e -> e -ED- d ->> e'
-> False. intros e e' d. introz U. lets Q : U.
urgency_pre_tac2 tfsBcStateEnt tfsBcStateProt tfsBcState.
lets TOT : tfsBc_trans_out TS.
inversion BC.
lets BIT : bcWait_trans_in H. del_triple_sort_tac. eapply enabledInSort_in in BIT.
apply SORT1_2 in BIT. apply BIT. apply enabledInSort_out. assumption.
lets SIT : sleep_trans_in H. del_triple_sort_tac. eapply enabledInSort_in in SIT.
apply SORT1_2 in SIT. apply SIT. apply enabledInSort_out. assumption.
assert (bcReadyStateEnt m l1 ([|p0, l0, h0, k0|])) as BCE. constructor.
rewrite TR. constructor. assumption. lets BCU : bcReady_urgent U BCE.
apply BCU. apply U1. Qed.
Lemma switchBc_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchBcStateEnt m e -> e -ED- d ->> e'
-> False. intros e e' d. introz U. lets Q : U.
urgency_pre_tac2_1 switchBcStateEnt switchBcStateProt switchBcState.
lets TOT : switchBc_wake_out TS.
inversion BC.
lets BIT : bcWait_wake_in H. del_triple_sort_tac. eapply enabledInSort_in in BIT.
apply SORT1_2 in BIT. apply BIT. apply enabledInSort_out. apply TOT.
lets SIT : sleeping_wake_in H. del_triple_sort_tac. eapply enabledInSort_in in SIT.
apply SORT1_2 in SIT. apply SIT. apply enabledInSort_out. apply TOT.
assert (bcReadyStateEnt m0 l1 ([|p0, l0, h0, k0|])) as BCE. constructor.
rewrite TR. constructor. assumption. lets BCU : bcReady_urgent U BCE.
apply BCU. apply U1. Qed.
Lemma swithcCurr_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchCurrStateEnt e -> e -ED- d ->> e'
-> False. intros e e' d. introz U. lets Q : U.
urgency_pre_tac2 switchCurrStateEnt switchCurrStateProt switchCurrState.
lets SMS : switchCurr_mState U U0. decompEx2 SMS m1 m2 MS.
lets NIM : mst_tout_mCurr_in m1 m2.
lets SOM : switchCurr_mCurr_out TS.
assert (discActEnabled p0 (chanMCurr *!)) as DA.
rewrite TR. apply parTriple_dae_intro2. assumption.
noSyncNow_tac. apply NS in DA. decompAnd2 DA NDA1 NDA2.
apply NDA2. simpl in MS. rewrite MS. assumption. Qed.
Lemma switchListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchListenStateEnt e -> e -ED- d ->> e'
-> False. urgency_pre_tac2 switchListenStateEnt switchListenStateProt
switchListenState.
assert (switchStateProt p0) as SP. rewrite TR. constructor. apply switLisSt.
assumption. lets PS : paused_switch U. rewrite <- PS in SP. rewrite TR in SP.
del_triple_sort_tac. assert (pausedState p3) as PS3. inversion SP. assumption.
lets PIU : paused_unpause_in_sort PS3. lets SOU : switchListen_unpause_out_sort TS.
apply SORT2_3 in SOU. apply SOU. apply PIU. Qed.
Lemma msgAbortPathEnt_urgent e e' d :
reachableEnt e -> msgAbortPathEnt e ->
e -ED- d ->> e' -> False. intro.
introz U. inversion U; subst.
assert (gotMsgStateEnt m'' l' ([|p, l, h, k|])).
econstructor; eassumption.
eapply gotMsgStateEnt_urgent; eassumption.
assert (gotRangeStateEnt m'' r ([|p, l, h, k|])).
econstructor; eassumption.
eapply gotRangeStateEnt_urgent; eassumption.
assert (currCompStateEnt m'' r ([|p, l, h, k|])).
econstructor; eassumption.
eapply currCompStateEnt_urgent; eassumption.
assert (abortOvlpStateEnt ([|p, l, h, k|])).
econstructor; eassumption.
eapply abortOvlpStateEnt_urgent; eassumption. Qed.
The interface component is irrelevant to the msgAbortPath.
Lemma msgAbort_inter_irrel p l h h' k :
msgAbortPathEnt ([|p, l, h, k|]) ->
msgAbortPathEnt ([|p, l, h', k|]). Admitted.
Theorem del_listening_pre (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' ->
abortOvlpStateEnt e \/ badOvlpStateEnt e \/ listeningStateEnt e \/ pausedStateEnt e.
introz U. Admitted.
Theorem del_ovlp (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' ->
dormantStateEnt e \/ tfsCurrStateEnt e \/
exists m, exists t, exists x, exists y, ovWaitStateEnt m t x y e . Admitted.
Theorem del_listening (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' -> listeningStateEnt e. Admitted.
Lemma switchCurr_switch_ent (e : Entity) :
switchCurrStateEnt e -> switchStateEnt e. intros.
inversion H. inversion H0. do 2 constructor.
apply switCurSt. assumption. Qed.
msgAbortPathEnt ([|p, l, h, k|]) ->
msgAbortPathEnt ([|p, l, h', k|]). Admitted.
Theorem del_listening_pre (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' ->
abortOvlpStateEnt e \/ badOvlpStateEnt e \/ listeningStateEnt e \/ pausedStateEnt e.
introz U. Admitted.
Theorem del_ovlp (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' ->
dormantStateEnt e \/ tfsCurrStateEnt e \/
exists m, exists t, exists x, exists y, ovWaitStateEnt m t x y e . Admitted.
Theorem del_listening (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' -> listeningStateEnt e. Admitted.
Lemma switchCurr_switch_ent (e : Entity) :
switchCurrStateEnt e -> switchStateEnt e. intros.
inversion H. inversion H0. do 2 constructor.
apply switCurSt. assumption. Qed.
If the software components of an entity transition are not equal, then
the transition is necessarily a tau action, and either the process performs a tau,
synchs with the interface, synchs with the mode state or reads the current position.
Lemma link_ent_proc_neq_disc p p' h h' l l' k k' a :
p <> p' -> [|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
a = aeTau /\ (
p -PA- tauAct -PA> p' \/
(exists h' c v, p -PA- c ;! v -PA> p' /\ h -i- c {? v -i> h') \/
(exists h' c v, p -PA- c ;? v -PA> p' /\ h -i- c {! v -i> h') \/
(exists k' c m, p -PA- c ;! [baseMode m] -PA> p' /\ k -ms- c .? m -ms> k') \/
(exists k' c m, p -PA- c ;? [baseMode m] -PA> p' /\ k -ms- c .! m -ms> k') \/
(exists k' c, p -PA- c *! -PA> p' /\ k -ms- c @? -ms> k') \/
(exists k' c, p -PA- c *? -PA> p' /\ k -ms- c @! -ms> k') \/
p -PA- chanPos ;? [basePosition l] -PA> p').
intros. inversion H0; (split;[ try reflexivity | ]);
try (subst; contradict H; reflexivity).
left; repeat eexists; eassumption.
right; left; repeat eexists; eassumption.
right. right. left. repeat eexists; eassumption.
right. right. left. repeat eexists; eassumption.
do 6 right. left. repeat eexists; eassumption.
do 5 right. left. repeat eexists; eassumption.
do 4 right. left. repeat eexists; eassumption.
do 3 right. left. repeat eexists; eassumption.
do 4 right. left. repeat eexists; eassumption.
repeat right. repeat eexists; eassumption.
Qed.
Lemma nextEq_mode (m' m'' : Mode) (e : Entity) :
nextEqStateEnt m' m'' e -> nextModeEnt m' e.
introz U. inversion U. Admitted.
Lemma nextMode_ent_mState p l h k m :
nextModeEnt m ([|p, l, h, k|]) -> nextModeMState k = Some m.
introz U. Admitted.
Lemma stepEnt_disc_pres_pos (e e' : Entity) a :
e -EA- a ->> e' -> posEnt e = posEnt e'. intros.
destruct e, e'. inversion H; reflexivity. Qed.
Ltac ent_disc_pres_pos_tac := match goal with
[V : [|_, ?l, _, _|] -EA- ?b ->> [|_, ?l', _, _|] |- _ ] =>
let EDP := fresh "EDP" in
lets EDP : stepEnt_disc_pres_pos V; simpl in EDP end.
Lemma gotMsg_gotRange_track_ent (m m' : Mode) (l l' l1 : Position)
(r : Distance) (p p' : ProcTerm) h h' k k' a :
gotMsgStateEnt m l1 ([|p, l, h, k|]) ->
gotRangeStateEnt m' r ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
l = l' /\ m = m' /\
r = {| distance := dist2d l l1 -nn- speedMax *nn* msgLatency |}.
Admitted.
Lemma gotRange_currPincCheck_track_ent (m2 m1' m2' : Mode) (l l' : Position)
(r r' : Distance) (p p' : ProcTerm) h h' k k' a :
gotRangeStateEnt m2 r ([|p, l, h, k|]) ->
currPincCheckStateEnt m1' m2' r' ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
m2 = m2' /\ r = r' /\ m1' = currModeMState k.
Admitted.
Lemma currComp_listening_track_ent m'' r l l' p p' h h' k k' a :
currCompStateEnt m'' r ([|p, l, h, k|]) ->
listeningStateEnt ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
k -ms- chanMStable @! -ms> k' /\ h = h'. Admitted.
Lemma currComp_nextPincCheck_track_ent (m2 m1' m2' : Mode) (l l' : Position)
(r r' : Distance) (p p' : ProcTerm) h h' k k' a :
currCompStateEnt m2 r ([|p, l, h, k|]) ->
nextPincCheckStateEnt m1' m2' r' ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
m2 = m2' /\ r = r' /\ nextModeMState k = Some m1'.
Admitted.
Lemma ovReady_ovWait_track_ent m m' t t' x' y' l0 a
p p' l l' h h' k k' :
ovReadyStateEnt m t l0 ([|p, l, h, k|]) ->
ovWaitStateEnt m' t' x' y' ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
p -PA- chanOutProc ;! [baseMode m, basePosition l0] -PA> p' /\
h -i- chanOutProc {? [baseMode m, basePosition l0] -i> h' /\
k = k' /\ m = m' /\ l = l0.
Admitted.
Lemma tfsStart_next_ent e e' a :
e -EA- a ->> e' -> tfsStartStateEnt e ->
tfsStartStateEnt e' \/ exists m, tfsNextStateEnt m e'.
Admitted.
Lemma tfsNext_next_ent e e' a m :
e -EA- a ->> e' -> tfsNextStateEnt m e ->
tfsNextStateEnt m e' \/ tfsCurrStateEnt e'.
Admitted.
Lemma tfsCurr_next_ent e e' a :
e -EA- a ->> e' -> tfsCurrStateEnt e ->
tfsCurrStateEnt e' \/ tfsBcStateEnt e'.
Admitted.
Lemma tfsBc_next_ent e e' a :
e -EA- a ->> e' -> tfsBcStateEnt e ->
tfsBcStateEnt e' \/ tfsListenStateEnt e'.
Admitted.
Lemma tfsListen_next_ent e e' a :
e -EA- a ->> e' -> tfsListenStateEnt e ->
tfsListenStateEnt e' \/ dormantStateEnt e'.
Admitted.
Lemma link_ent_outList p p' l l' k k' li li' lo lo' ln ln' b :
[|p, l, {| li := li; lo := lo; ln := ln |}, k|] -EA- b ->>
[|p', l', {| li := li'; lo := lo'; ln := ln' |}, k'|] ->
lo = lo' \/ exists v, outList lo -tl- v ?? -tl> outList lo'
\/ outList lo -tl- v !! -tl> outList lo'. Admitted.
p <> p' -> [|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
a = aeTau /\ (
p -PA- tauAct -PA> p' \/
(exists h' c v, p -PA- c ;! v -PA> p' /\ h -i- c {? v -i> h') \/
(exists h' c v, p -PA- c ;? v -PA> p' /\ h -i- c {! v -i> h') \/
(exists k' c m, p -PA- c ;! [baseMode m] -PA> p' /\ k -ms- c .? m -ms> k') \/
(exists k' c m, p -PA- c ;? [baseMode m] -PA> p' /\ k -ms- c .! m -ms> k') \/
(exists k' c, p -PA- c *! -PA> p' /\ k -ms- c @? -ms> k') \/
(exists k' c, p -PA- c *? -PA> p' /\ k -ms- c @! -ms> k') \/
p -PA- chanPos ;? [basePosition l] -PA> p').
intros. inversion H0; (split;[ try reflexivity | ]);
try (subst; contradict H; reflexivity).
left; repeat eexists; eassumption.
right; left; repeat eexists; eassumption.
right. right. left. repeat eexists; eassumption.
right. right. left. repeat eexists; eassumption.
do 6 right. left. repeat eexists; eassumption.
do 5 right. left. repeat eexists; eassumption.
do 4 right. left. repeat eexists; eassumption.
do 3 right. left. repeat eexists; eassumption.
do 4 right. left. repeat eexists; eassumption.
repeat right. repeat eexists; eassumption.
Qed.
Lemma nextEq_mode (m' m'' : Mode) (e : Entity) :
nextEqStateEnt m' m'' e -> nextModeEnt m' e.
introz U. inversion U. Admitted.
Lemma nextMode_ent_mState p l h k m :
nextModeEnt m ([|p, l, h, k|]) -> nextModeMState k = Some m.
introz U. Admitted.
Lemma stepEnt_disc_pres_pos (e e' : Entity) a :
e -EA- a ->> e' -> posEnt e = posEnt e'. intros.
destruct e, e'. inversion H; reflexivity. Qed.
Ltac ent_disc_pres_pos_tac := match goal with
[V : [|_, ?l, _, _|] -EA- ?b ->> [|_, ?l', _, _|] |- _ ] =>
let EDP := fresh "EDP" in
lets EDP : stepEnt_disc_pres_pos V; simpl in EDP end.
Lemma gotMsg_gotRange_track_ent (m m' : Mode) (l l' l1 : Position)
(r : Distance) (p p' : ProcTerm) h h' k k' a :
gotMsgStateEnt m l1 ([|p, l, h, k|]) ->
gotRangeStateEnt m' r ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
l = l' /\ m = m' /\
r = {| distance := dist2d l l1 -nn- speedMax *nn* msgLatency |}.
Admitted.
Lemma gotRange_currPincCheck_track_ent (m2 m1' m2' : Mode) (l l' : Position)
(r r' : Distance) (p p' : ProcTerm) h h' k k' a :
gotRangeStateEnt m2 r ([|p, l, h, k|]) ->
currPincCheckStateEnt m1' m2' r' ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
m2 = m2' /\ r = r' /\ m1' = currModeMState k.
Admitted.
Lemma currComp_listening_track_ent m'' r l l' p p' h h' k k' a :
currCompStateEnt m'' r ([|p, l, h, k|]) ->
listeningStateEnt ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
k -ms- chanMStable @! -ms> k' /\ h = h'. Admitted.
Lemma currComp_nextPincCheck_track_ent (m2 m1' m2' : Mode) (l l' : Position)
(r r' : Distance) (p p' : ProcTerm) h h' k k' a :
currCompStateEnt m2 r ([|p, l, h, k|]) ->
nextPincCheckStateEnt m1' m2' r' ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
m2 = m2' /\ r = r' /\ nextModeMState k = Some m1'.
Admitted.
Lemma ovReady_ovWait_track_ent m m' t t' x' y' l0 a
p p' l l' h h' k k' :
ovReadyStateEnt m t l0 ([|p, l, h, k|]) ->
ovWaitStateEnt m' t' x' y' ([|p', l', h', k'|]) ->
[|p, l, h, k|] -EA- a ->> [|p', l', h', k'|] ->
p -PA- chanOutProc ;! [baseMode m, basePosition l0] -PA> p' /\
h -i- chanOutProc {? [baseMode m, basePosition l0] -i> h' /\
k = k' /\ m = m' /\ l = l0.
Admitted.
Lemma tfsStart_next_ent e e' a :
e -EA- a ->> e' -> tfsStartStateEnt e ->
tfsStartStateEnt e' \/ exists m, tfsNextStateEnt m e'.
Admitted.
Lemma tfsNext_next_ent e e' a m :
e -EA- a ->> e' -> tfsNextStateEnt m e ->
tfsNextStateEnt m e' \/ tfsCurrStateEnt e'.
Admitted.
Lemma tfsCurr_next_ent e e' a :
e -EA- a ->> e' -> tfsCurrStateEnt e ->
tfsCurrStateEnt e' \/ tfsBcStateEnt e'.
Admitted.
Lemma tfsBc_next_ent e e' a :
e -EA- a ->> e' -> tfsBcStateEnt e ->
tfsBcStateEnt e' \/ tfsListenStateEnt e'.
Admitted.
Lemma tfsListen_next_ent e e' a :
e -EA- a ->> e' -> tfsListenStateEnt e ->
tfsListenStateEnt e' \/ dormantStateEnt e'.
Admitted.
Lemma link_ent_outList p p' l l' k k' li li' lo lo' ln ln' b :
[|p, l, {| li := li; lo := lo; ln := ln |}, k|] -EA- b ->>
[|p', l', {| li := li'; lo := lo'; ln := ln' |}, k'|] ->
lo = lo' \/ exists v, outList lo -tl- v ?? -tl> outList lo'
\/ outList lo -tl- v !! -tl> outList lo'. Admitted.
This page has been generated by coqdoc