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.
Lemma nextModeEnt_not_stable m1 m2 p l h :
nextModeEnt m1 ([|p, l, h, m2|]) -> False.
Lemma mst_tout_mCurr_in m1 m2 :
discActEnabledMState (chanMCurr *?) (<| m1, m2, zeroTime |>).
Lemma tfsNext_prev_ent m e e' a : tfsNextStateEnt m e' ->
e -EA- a ->> e' -> tfsNextStateEnt m e \/ tfsStartStateEnt e.
Lemma currEq_mode m m'' e :
currEqStateEnt m m'' e -> m = currModeEnt e.
Lemma ovAbort_unstable e : reachableEnt e -> ovAbortStateEnt e -> unstable (mstEnt e).
Lemma tfsCurr_failSafe (e : Entity) (m : Mode) :
tfsCurrStateEnt e -> exists m, nextModeEnt m e /\ failSafe m.
Lemma tfsBc_failSafe (e : Entity) :
tfsBcStateEnt e -> failSafe (currModeEnt e).
Lemma tfsNext_currMode e m :
reachableEnt e -> tfsNextStateEnt m e -> currModeEnt e = m.
Theorem switchCurr_mState (e : Entity) :
reachableEnt e -> switchCurrStateEnt e -> exists m m',
mstEnt e = <| m, m', zeroTime |>.
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.
reachableEnt e -> bcReadyStateEnt m l e -> inPosEnt l e.
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.
Lemma tfsListen_paused p1 p2 p3 :
tfsListenStateProt (p1 $||$ p2 $||$ p3) -> pausedStateProt (p1 $||$ p2 $||$ p3).
reachableEnt e -> ovReadyStateEnt m t l e -> inPosEnt l e.
Lemma tfsListen_paused p1 p2 p3 :
tfsListenStateProt (p1 $||$ p2 $||$ p3) -> pausedStateProt (p1 $||$ p2 $||$ p3).
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'.
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'.
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.
Lemma gotRangeStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> gotRangeStateEnt m r e -> e -ED- d ->> e' -> False.
Lemma currCompStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> currCompStateEnt m r e -> e -ED- d ->> e' -> False.
Lemma abortOvlpStateEnt_urgent (e e' : Entity) (d : Delay) :
reachableEnt e -> abortOvlpStateEnt e -> e -ED- d ->> e' -> False.
Lemma tfsStartStateEnt_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsStartStateEnt e -> e -ED- d ->> e' -> False.
Lemma tfsListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsListenStateEnt e -> e -ED- d ->> e'
-> False.
Lemma tfsNext_urgent : forall (m : Mode) (e e' : Entity) (d : Delay),
reachableEnt e -> tfsNextStateEnt m e -> e -ED- d ->> e' -> False.
Lemma bcReady_urgent (m : Mode) (l : Position) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> bcReadyStateEnt m l e -> e -ED- d ->> e'
-> False.
Lemma ovAbort_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> ovAbortStateEnt e -> e -ED- d ->> e'
-> False.
Lemma tfsBc_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsBcStateEnt e -> e -ED- d ->> e'
-> False.
Lemma switchBc_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchBcStateEnt m e -> e -ED- d ->> e'
-> False.
Lemma swithcCurr_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchCurrStateEnt e -> e -ED- d ->> e'
-> False.
Lemma switchListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchListenStateEnt e -> e -ED- d ->> e'
-> False.
Lemma msgAbortPathEnt_urgent e e' d :
reachableEnt e -> msgAbortPathEnt e ->
e -ED- d ->> e' -> False.
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.
Lemma gotRangeStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> gotRangeStateEnt m r e -> e -ED- d ->> e' -> False.
Lemma currCompStateEnt_urgent (e e' : Entity) (d : Delay) m r :
reachableEnt e -> currCompStateEnt m r e -> e -ED- d ->> e' -> False.
Lemma abortOvlpStateEnt_urgent (e e' : Entity) (d : Delay) :
reachableEnt e -> abortOvlpStateEnt e -> e -ED- d ->> e' -> False.
Lemma tfsStartStateEnt_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsStartStateEnt e -> e -ED- d ->> e' -> False.
Lemma tfsListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsListenStateEnt e -> e -ED- d ->> e'
-> False.
Lemma tfsNext_urgent : forall (m : Mode) (e e' : Entity) (d : Delay),
reachableEnt e -> tfsNextStateEnt m e -> e -ED- d ->> e' -> False.
Lemma bcReady_urgent (m : Mode) (l : Position) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> bcReadyStateEnt m l e -> e -ED- d ->> e'
-> False.
Lemma ovAbort_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> ovAbortStateEnt e -> e -ED- d ->> e'
-> False.
Lemma tfsBc_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> tfsBcStateEnt e -> e -ED- d ->> e'
-> False.
Lemma switchBc_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchBcStateEnt m e -> e -ED- d ->> e'
-> False.
Lemma swithcCurr_urgent (m : Mode) : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchCurrStateEnt e -> e -ED- d ->> e'
-> False.
Lemma switchListen_urgent : forall (e e' : Entity) (d : Delay),
reachableEnt e -> switchListenStateEnt e -> e -ED- d ->> e'
-> False.
Lemma msgAbortPathEnt_urgent e e' d :
reachableEnt e -> msgAbortPathEnt e ->
e -ED- d ->> e' -> False.
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|]).
Theorem del_listening_pre (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' ->
abortOvlpStateEnt e \/ badOvlpStateEnt e \/ listeningStateEnt e \/ pausedStateEnt e.
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 .
Theorem del_listening (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' -> listeningStateEnt e.
Lemma switchCurr_switch_ent (e : Entity) :
switchCurrStateEnt e -> switchStateEnt e.
msgAbortPathEnt ([|p, l, h, k|]) ->
msgAbortPathEnt ([|p, l, h', k|]).
Theorem del_listening_pre (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' ->
abortOvlpStateEnt e \/ badOvlpStateEnt e \/ listeningStateEnt e \/ pausedStateEnt e.
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 .
Theorem del_listening (e e' : Entity) (d : Delay) :
reachableEnt e -> e -ED- d ->> e' -> listeningStateEnt e.
Lemma switchCurr_switch_ent (e : Entity) :
switchCurrStateEnt e -> switchStateEnt e.
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').
Lemma nextEq_mode (m' m'' : Mode) (e : Entity) :
nextEqStateEnt m' m'' e -> nextModeEnt m' e.
Lemma nextMode_ent_mState p l h k m :
nextModeEnt m ([|p, l, h, k|]) -> nextModeMState k = Some m.
Lemma stepEnt_disc_pres_pos (e e' : Entity) a :
e -EA- a ->> e' -> posEnt e = posEnt e'.
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 |}.
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.
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'.
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'.
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.
Lemma tfsStart_next_ent e e' a :
e -EA- a ->> e' -> tfsStartStateEnt e ->
tfsStartStateEnt e' \/ exists m, tfsNextStateEnt m e'.
Lemma tfsNext_next_ent e e' a m :
e -EA- a ->> e' -> tfsNextStateEnt m e ->
tfsNextStateEnt m e' \/ tfsCurrStateEnt e'.
Lemma tfsCurr_next_ent e e' a :
e -EA- a ->> e' -> tfsCurrStateEnt e ->
tfsCurrStateEnt e' \/ tfsBcStateEnt e'.
Lemma tfsBc_next_ent e e' a :
e -EA- a ->> e' -> tfsBcStateEnt e ->
tfsBcStateEnt e' \/ tfsListenStateEnt e'.
Lemma tfsListen_next_ent e e' a :
e -EA- a ->> e' -> tfsListenStateEnt e ->
tfsListenStateEnt e' \/ dormantStateEnt e'.
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'.
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').
Lemma nextEq_mode (m' m'' : Mode) (e : Entity) :
nextEqStateEnt m' m'' e -> nextModeEnt m' e.
Lemma nextMode_ent_mState p l h k m :
nextModeEnt m ([|p, l, h, k|]) -> nextModeMState k = Some m.
Lemma stepEnt_disc_pres_pos (e e' : Entity) a :
e -EA- a ->> e' -> posEnt e = posEnt e'.
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 |}.
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.
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'.
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'.
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.
Lemma tfsStart_next_ent e e' a :
e -EA- a ->> e' -> tfsStartStateEnt e ->
tfsStartStateEnt e' \/ exists m, tfsNextStateEnt m e'.
Lemma tfsNext_next_ent e e' a m :
e -EA- a ->> e' -> tfsNextStateEnt m e ->
tfsNextStateEnt m e' \/ tfsCurrStateEnt e'.
Lemma tfsCurr_next_ent e e' a :
e -EA- a ->> e' -> tfsCurrStateEnt e ->
tfsCurrStateEnt e' \/ tfsBcStateEnt e'.
Lemma tfsBc_next_ent e e' a :
e -EA- a ->> e' -> tfsBcStateEnt e ->
tfsBcStateEnt e' \/ tfsListenStateEnt e'.
Lemma tfsListen_next_ent e e' a :
e -EA- a ->> e' -> tfsListenStateEnt e ->
tfsListenStateEnt e' \/ dormantStateEnt e'.
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'.
This page has been generated by coqdoc