Library NetAuxBasics
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 Reals.
Require Import List.
Require Import ComhCoq.Extras.LibTactics.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.EntityLanguage.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.GenTacs.
Inductive initialNet : Network -> Prop :=
| initNtNil : initialNet []
| initNtCons e n : initialEnt e -> initialNet n ->
initialNet (e :: n).
Inductive reachableNet : Network -> Type :=
| reachNetInit (n : Network) : initialNet n -> reachableNet n
| reachNetDisc (n n' : Network) (a : ActDiscNet) : reachableNet n ->
n -NA- a -NA> n' -> reachableNet n'
| reachNetDel (n n' : Network) (d : Delay) : reachableNet n ->
n -ND- d -ND> n' -> reachableNet n'.
Lemma link_net_prot_reach n p l h k i :
reachableNet n -> [|p, l, h, k|] @ i .: n -> reachableProt p.
Ltac link_netprotreach_tac U :=
match goal with
[H : reachableNet ?n, H0 : [|_, _, _, _|] @ _ .: ?n |- _] =>
let U1 := fresh U in lets U1 : link_net_prot_reach H H0
end.
Parameter currModeNet : Mode -> nat -> Network -> Prop.
Inductive transGuard (t : Time) (i : nat) (n : Network) : Prop :=
| tgWitness (p : ProcTerm) (l : Position) (h : Interface) (m m' : Mode) :
[| p , l , h , <| m , m' , t |> |] @ i .: n -> transGuard t i n.
Parameter nextModeNet : Mode -> nat -> Network -> Prop.
Inductive inPosNet (l : Position) (i : nat) (n : Network) : Prop :=
| ipWitness (p : ProcTerm) (h : Interface) (k : ModeState) :
[| p , l , h , k |] @ i .: n -> inPosNet l i n.
Inductive distNet (i i' : nat) (n : Network) : Distance -> Prop :=
| dnWitness (l l' : Position) : inPosNet l i n -> inPosNet l' i' n ->
distNet i i' n (distFun l l').
Inductive outgoing (v : list BaseType) (t : Time) (i : nat) (n : Network) : Prop :=
| ogWitness (p : ProcTerm) (l : Position) (li : InputList) (lo : OutputList) (ln : NotifList) (k : ModeState) :
[| p , l , (mkInterface li lo ln) , k |] @ i .: n -> In (<( v , t )>) (outList lo) -> outgoing v t i n.
Inductive incomingNet (v : list BaseType) (i : nat) (n : Network) : Prop :=
| icWitness (p : ProcTerm) (l : Position) (li : InputList) (lo : OutputList) (ln : NotifList) (k : ModeState) :
[| p , l , (mkInterface li lo ln) , k |] @ i .: n -> In (<( v , zeroTime )>) (inList li) -> incomingNet v i n.
Inductive incomingNetNotif (v : list BaseType) (t : Time) (i : nat) (n : Network) : Prop :=
| icnWitness (p : ProcTerm) (l : Position) (li : InputList) (lo : OutputList) (ln : NotifList) (k : ModeState) :
[| p , l , (mkInterface li lo ln) , k |] @ i .: n -> In (<( v , t )>) (notifList ln) -> incomingNetNotif v t i n.
Inductive mState_in_net (k : ModeState) (i : nat) (n : Network) : Prop :=
minet (p : ProcTerm) (l : Position) (h : Interface) :
[|p, l, h, k|] @ i .: n -> mState_in_net k i n.
Inductive liftEntNet (X : Entity -> Prop) (i : nat) (n : Network) : Prop :=
| lenWitness (e : Entity) : X e -> e @ i .: n -> liftEntNet X i n.
Definition bcWaitStateNet m x := liftEntNet (bcWaitStateEnt m x).
Definition sleepingStateNet := liftEntNet sleepingStateEnt.
Definition bcReadyStateNet m l := liftEntNet (bcReadyStateEnt m l).
Definition dormantStateNet := liftEntNet dormantStateEnt.
Definition tfsStartStateNet := liftEntNet tfsStartStateEnt.
Definition initStateNet m := liftEntNet (initStateEnt m).
Definition ovWaitStateNet m t x y := liftEntNet (ovWaitStateEnt m t x y).
Definition ovReadyStateNet m t l := liftEntNet (ovReadyStateEnt m t l).
Definition switchCurrStateNet := liftEntNet switchCurrStateEnt.
Definition switchListenStateNet := liftEntNet switchListenStateEnt.
Definition switchBcStateNet m := liftEntNet (switchBcStateEnt m).
Definition tfsCurrStateNet := liftEntNet tfsCurrStateEnt.
Definition tfsBcStateNet := liftEntNet tfsBcStateEnt.
Definition tfsListenStateNet := liftEntNet tfsListenStateEnt.
Definition pausedStateNet := liftEntNet pausedStateEnt.
Definition tfsNextStateNet m := liftEntNet (tfsNextStateEnt m).
Definition listeningStateNet := liftEntNet listeningStateEnt.
Definition currCompStateNet m'' r := liftEntNet (currCompStateEnt m'' r).
Definition badOvlpStateNet := liftEntNet badOvlpStateEnt.
Definition rangeBadStateNet m := liftEntNet (rangeBadStateEnt m).
Definition currEqStateNet m m'' := liftEntNet (currEqStateEnt m m'').
Definition broadcastStateNet := liftEntNet broadcastStateEnt.
Definition overlapStateNet := liftEntNet overlapStateEnt.
Definition tfsStateNet := liftEntNet tfsStateEnt.
Definition nextSinceStateNet := liftEntNet (nextSinceStateEnt).
Definition switchStateNet := liftEntNet switchStateEnt.
Definition listenerStateNet := liftEntNet listenerStateEnt.
Definition ovAbortStateNet := liftEntNet ovAbortStateEnt.
Conjecture tfsStateNet_dec : forall (i : nat) (n : Network), decidable (tfsStateNet i n).
Conjecture tfsCurrNet_dec : forall (i : nat) (n : Network),
decidable (tfsCurrStateNet i n).
Lemma tfsCurrStateNet_bktrk_net : forall (n n' : Network) (i : nat) (a : ActDiscNet),
tfsCurrStateNet i n' -> n -NA- a -NA> n' ->
tfsCurrStateNet i n \/
(exists m mF, exists p,
tfsNextStateNet m i n /\ failSafe mF /\
mState_in_net (<| m, mF, modeTransTime m mF p |>) i n').
Conjecture tfsCurrState_del_pres_net : forall (n n' : Network) (d : Delay) (i : nat),
n -ND- d -ND> n' ->
(tfsCurrStateNet i n <-> tfsCurrStateNet i n').
Lemma mState_switch_states : forall (n n' : Network) (i : nat)
(a : ActDiscNet) (k k' : ModeState), reachableNet n -> k <> k' ->
n -NA- a -NA> n' -> mState_in_net k i n -> mState_in_net k' i n' ->
(tfsCurrStateNet i n /\ tfsBcStateNet i n') \/
(switchCurrStateNet i n /\ switchListenStateNet i n').
Conjecture tfsState_del_pres_net : forall (n n' : Network) (i : nat) (d : Delay),
n -ND- d -ND> n' -> (tfsStateNet i n <-> tfsStateNet i n').
Lemma switch_states_mState : forall (n n' : Network) (i : nat) (a : ActDiscNet)
(m : Mode), n -NA- a -NA> n' -> switchCurrStateNet i n ->
switchListenStateNet i n' -> nextModeNet m i n -> currModeNet m i n'.
A network transition which sees a software component of some entity
transform to a different software term is necessarily a tau transition.
Lemma procNeq_tau_net p p' l l' h h' k k' n n' a i :
[|p, l, h, k|] @ i .: n -> [|p', l', h', k'|] @ i .: n' ->
n -NA- a -NA> n' -> p <> p' -> a = anTau.
[|p, l, h, k|] @ i .: n -> [|p', l', h', k'|] @ i .: n' ->
n -NA- a -NA> n' -> p <> p' -> a = anTau.
The action linking a change from switchCurr to switchListen is always a tau.
Lemma switchCurr_listen_trans_tau (n n' : Network) (a : ActDiscNet) (i : nat) :
n -NA- a -NA> n' -> switchCurrStateNet i n -> switchListenStateNet i n' ->
a = anTau.
Lemma tfsStart_tfs_net i n :
tfsStartStateNet i n -> tfsStateNet i n.
Lemma tfsNext_tfs_net m i n :
tfsNextStateNet m i n -> tfsStateNet i n.
Lemma tfsCurr_tfs_net i n :
tfsCurrStateNet i n -> tfsStateNet i n.
Lemma tfsBc_tfs_net i n :
tfsBcStateNet i n -> tfsStateNet i n.
Lemma tfsListen_tfs_net i n :
tfsListenStateNet i n -> tfsStateNet i n.
n -NA- a -NA> n' -> switchCurrStateNet i n -> switchListenStateNet i n' ->
a = anTau.
Lemma tfsStart_tfs_net i n :
tfsStartStateNet i n -> tfsStateNet i n.
Lemma tfsNext_tfs_net m i n :
tfsNextStateNet m i n -> tfsStateNet i n.
Lemma tfsCurr_tfs_net i n :
tfsCurrStateNet i n -> tfsStateNet i n.
Lemma tfsBc_tfs_net i n :
tfsBcStateNet i n -> tfsStateNet i n.
Lemma tfsListen_tfs_net i n :
tfsListenStateNet i n -> tfsStateNet i n.
The following three tactics are mostly simply auxiliaries to the main
result of fwd_track_net_tac.
Ltac first_eexists_5 t := first [t | (do 1 eexists);t | (do 2 eexists);t |
(do 3 eexists);t | (do 4 eexists);t | (do 5 eexists);t].
Ltac econstr_easssump := econstructor; eassumption.
Ltac first_ex_econ_eass := first_eexists_5 econstr_easssump.
(do 3 eexists);t | (do 4 eexists);t | (do 5 eexists);t].
Ltac econstr_easssump := econstructor; eassumption.
Ltac first_ex_econ_eass := first_eexists_5 econstr_easssump.
RE is the entity level result upon which this tactic works. Essentially,
this tactic lifts RE from the entity to the network level. Note that the tactic
assumes a disjunctive goal of two branches and may not work otherwise.
Ltac fwd_track_net_tac RE :=
let U := fresh in let U0 := fresh in
intros U U0; destruct U0;
let e' := fresh "e'" in let b := fresh "b" in
let LNE := fresh "LNE" in
link_netentdiscfwd_tac e' b LNE;
[subst; left | match goal with [LNE1 : _ -EA- b ->> e', e : Entity,
H0 : _ ?e |- _] =>
lets LOW : RE LNE1 H0;
or_flat; ex_flat; [left | right] end];
first_ex_econ_eass.
Lemma tfsStart_next_net n n' a i :
n -NA- a -NA> n' -> tfsStartStateNet i n ->
tfsStartStateNet i n' \/ exists m, tfsNextStateNet m i n'.
Lemma tfsNext_next_net m n n' a i :
n -NA- a -NA> n' -> tfsNextStateNet m i n ->
tfsNextStateNet m i n' \/ tfsCurrStateNet i n'.
Lemma tfsCurr_next_net n n' a i :
n -NA- a -NA> n' -> tfsCurrStateNet i n ->
tfsCurrStateNet i n' \/ tfsBcStateNet i n'.
Lemma tfsBc_next_net n n' a i :
n -NA- a -NA> n' -> tfsBcStateNet i n ->
tfsBcStateNet i n' \/ tfsListenStateNet i n'.
Lemma tfsListen_next_net n n' a i :
n -NA- a -NA> n' -> tfsListenStateNet i n ->
tfsListenStateNet i n' \/ dormantStateNet i n'.
Lemma rangeBad_next_net m m'' i n n' a :
n -NA- a -NA> n' -> rangeBadStateNet m'' i n -> currModeNet m i n ->
rangeBadStateNet m'' i n' \/ currEqStateNet m m'' i n'.
Lemma badOvlp_next_net i n n' a :
n -NA- a -NA> n' -> badOvlpStateNet i n ->
badOvlpStateNet i n' \/ listeningStateNet i n'.
Ltac netState_auto_pre := match goal with [U : [|_, _, _, _|] = _,
U1 : _ $||$ _ $||$ _ = _ |- _] =>
eapply lenWitness;[ | eassumption];
rewrite <- U; eapply lifpe; rewrite <- U1 end; constructor.
let U := fresh in let U0 := fresh in
intros U U0; destruct U0;
let e' := fresh "e'" in let b := fresh "b" in
let LNE := fresh "LNE" in
link_netentdiscfwd_tac e' b LNE;
[subst; left | match goal with [LNE1 : _ -EA- b ->> e', e : Entity,
H0 : _ ?e |- _] =>
lets LOW : RE LNE1 H0;
or_flat; ex_flat; [left | right] end];
first_ex_econ_eass.
Lemma tfsStart_next_net n n' a i :
n -NA- a -NA> n' -> tfsStartStateNet i n ->
tfsStartStateNet i n' \/ exists m, tfsNextStateNet m i n'.
Lemma tfsNext_next_net m n n' a i :
n -NA- a -NA> n' -> tfsNextStateNet m i n ->
tfsNextStateNet m i n' \/ tfsCurrStateNet i n'.
Lemma tfsCurr_next_net n n' a i :
n -NA- a -NA> n' -> tfsCurrStateNet i n ->
tfsCurrStateNet i n' \/ tfsBcStateNet i n'.
Lemma tfsBc_next_net n n' a i :
n -NA- a -NA> n' -> tfsBcStateNet i n ->
tfsBcStateNet i n' \/ tfsListenStateNet i n'.
Lemma tfsListen_next_net n n' a i :
n -NA- a -NA> n' -> tfsListenStateNet i n ->
tfsListenStateNet i n' \/ dormantStateNet i n'.
Lemma rangeBad_next_net m m'' i n n' a :
n -NA- a -NA> n' -> rangeBadStateNet m'' i n -> currModeNet m i n ->
rangeBadStateNet m'' i n' \/ currEqStateNet m m'' i n'.
Lemma badOvlp_next_net i n n' a :
n -NA- a -NA> n' -> badOvlpStateNet i n ->
badOvlpStateNet i n' \/ listeningStateNet i n'.
Ltac netState_auto_pre := match goal with [U : [|_, _, _, _|] = _,
U1 : _ $||$ _ $||$ _ = _ |- _] =>
eapply lenWitness;[ | eassumption];
rewrite <- U; eapply lifpe; rewrite <- U1 end; constructor.
Assume a network state predicate as the goal, and enough information in the
hypothesis to prove it: an entInNet, an equality between that entity and its
various components, and an equality between a process triple and the process of
that entity. Then this tactic should solve the goal.
Ltac netState_auto_tac :=
netState_auto_pre; eassumption.
Lemma tfsState_elim_net i n :
tfsStateNet i n -> tfsStartStateNet i n \/
(exists m, tfsNextStateNet m i n) \/
tfsCurrStateNet i n \/ tfsBcStateNet i n \/
tfsListenStateNet i n.
Lemma tfsListen_failSafe_net m i n :
tfsListenStateNet i n -> currModeNet m i n -> failSafe m.
Lemma tfs_currMode_disc_pres (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode) :
n -NA- a -NA> n' -> currModeNet m i n -> ~ failSafe m ->
tfsStateNet i n -> tfsStateNet i n'.
Lemma paused_switch_net (n : Network) (i : nat) :
reachableNet n -> (pausedStateNet i n <-> switchStateNet i n).
Lemma bcWaitNet_del_bkwd (n n' : Network) (m : Mode) (x : Time)
(i : nat) (d : Delay) : n -ND- d -ND> n' ->
bcWaitStateNet m x i n' -> bcWaitStateNet m (x +dt+ d) i n.
netState_auto_pre; eassumption.
Lemma tfsState_elim_net i n :
tfsStateNet i n -> tfsStartStateNet i n \/
(exists m, tfsNextStateNet m i n) \/
tfsCurrStateNet i n \/ tfsBcStateNet i n \/
tfsListenStateNet i n.
Lemma tfsListen_failSafe_net m i n :
tfsListenStateNet i n -> currModeNet m i n -> failSafe m.
Lemma tfs_currMode_disc_pres (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode) :
n -NA- a -NA> n' -> currModeNet m i n -> ~ failSafe m ->
tfsStateNet i n -> tfsStateNet i n'.
Lemma paused_switch_net (n : Network) (i : nat) :
reachableNet n -> (pausedStateNet i n <-> switchStateNet i n).
Lemma bcWaitNet_del_bkwd (n n' : Network) (m : Mode) (x : Time)
(i : nat) (d : Delay) : n -ND- d -ND> n' ->
bcWaitStateNet m x i n' -> bcWaitStateNet m (x +dt+ d) i n.
An entity in an initial network is itself initial.
Lemma initialNet_ent e i n : initialNet n -> e @ i .: n ->
initialEnt e.
initialEnt e.
Looks for an initial network in the hypotheses and also an entity in
that network and adds the hypothesis that the entity in question is initial.
Ltac initNet_ent_tac := let U0 := fresh in
match goal with [U : initialNet ?n,
U1 : ?e @ ?i .: ?n |- _] => lets U0 : initialNet_ent U U1 end.
Ltac initNet_contra U :=
inversion U as [e U1 U2]; inversion U1;
initNet_ent_tac; match goal with [U3 : [|_, _, _, _|] = ?e,
U4 : initialEnt ?e |- _] => rewrite <- U3 in U4;
inversion U4 end; match goal with [U5 : initialProc _ |- _] =>
inversion U5 end; match goal with [U6 : procProtocol = _ |- _] =>
symmetry in U6; subst_all U6 end; match reverse goal with
[U7 : context[procProtocol] |- _] => inversion U7 end; subst;
match goal with
| [U8 : context[dormant] |- _] => inversion U8
| [U8 : context[sleeping] |- _] => inversion U8
| [U8 : context[listening] |- _] => inversion U8
end.
Lemma initial_not_bcWait_net (n : Network) (m : Mode) (x : Time) (i : nat) :
initialNet n -> bcWaitStateNet m x i n -> False.
match goal with [U : initialNet ?n,
U1 : ?e @ ?i .: ?n |- _] => lets U0 : initialNet_ent U U1 end.
Ltac initNet_contra U :=
inversion U as [e U1 U2]; inversion U1;
initNet_ent_tac; match goal with [U3 : [|_, _, _, _|] = ?e,
U4 : initialEnt ?e |- _] => rewrite <- U3 in U4;
inversion U4 end; match goal with [U5 : initialProc _ |- _] =>
inversion U5 end; match goal with [U6 : procProtocol = _ |- _] =>
symmetry in U6; subst_all U6 end; match reverse goal with
[U7 : context[procProtocol] |- _] => inversion U7 end; subst;
match goal with
| [U8 : context[dormant] |- _] => inversion U8
| [U8 : context[sleeping] |- _] => inversion U8
| [U8 : context[listening] |- _] => inversion U8
end.
Lemma initial_not_bcWait_net (n : Network) (m : Mode) (x : Time) (i : nat) :
initialNet n -> bcWaitStateNet m x i n -> False.
If we're nextSince & we can delay, then we're in the ovWait state.
Lemma nextSince_del_ovWait (n n' : Network) (i : nat) (d : Delay) :
n -ND- d -ND> n' -> nextSinceStateNet i n ->
exists m t x y, ovWaitStateNet m t (delToTime (x +dt+ d)) (delToTime (y +dt+ d)) i n.
Lemma switchCurr_switchListen_net_link (n n' : Network) (i : nat)
(a : ActDiscNet) (e e' : Entity) :
switchCurrStateEnt e -> switchListenStateEnt e' ->
e @ i .: n -> e' @ i .: n' -> n -NA- a -NA> n' ->
a = anTau /\ interEnt e = interEnt e'.
Lemma init_nextMode_net m i n :
reachableNet n -> initStateNet m i n -> nextModeNet m i n.
Lemma ovReady_prev_net_strong m t l n n' i a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
(exists x0 y0, ovWaitStateNet m t x0 y0 i n).
Lemma ovWait_prev_net_strong m t x y n n' i a :
ovWaitStateNet m t x y i n' -> n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists t0 l0, ovReadyStateNet m t0 l0 i n) \/
initStateNet m i n.
Lemma nextMode_pres_fwd_net m i n n' a :
reachableNet n -> nextModeNet m i n ->
~(switchCurrStateNet i n \/ ovAbortStateNet i n \/
tfsCurrStateNet i n) ->
n -NA- a -NA> n' -> nextModeNet m i n'.
Lemma ovWait_del_pres_bkwd_net_strong n n' d m t x y i :
n -ND- d -ND> n' -> ovWaitStateNet m t x y i n' ->
ovWaitStateNet m t (x +dt+ d) (y +dt+ d) i n.
Lemma ovReady_del_pres_bkwd_net n n' d m t l i :
n -ND- d -ND> n' -> ovReadyStateNet m t l i n' ->
ovReadyStateNet m t l i n.
Lemma nextModeNet_del_pres n n' d m i :
n -ND- d -ND> n' -> nextModeNet m i n -> nextModeNet m i n'.
Lemma ovWait_ovReady_nextMode_net m t x y l i n :
reachableNet n -> ovWaitStateNet m t x y i n \/ ovReadyStateNet m t l i n ->
nextModeNet m i n.
Lemma ovWaitState_nextMode_net (n : Network) (m : Mode) (t x y : Time) (i : nat):
reachableNet n -> ovWaitStateNet m t x y i n -> nextModeNet m i n.
Theorem del_listening_net (n n' : Network) (d : Delay) (e : Entity) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> e @ i .: n -> listeningStateNet i n.
Theorem inPos_pres_disc (n n' : Network) (a : ActDiscNet) (l : Position) (i : nat) :
n -NA- a -NA> n' ->
(inPosNet l i n <-> inPosNet l i n').
Theorem currMode_pres_bkwd (n n' : Network) (a : ActDiscNet) (m' : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m' i n' ->
exists m, currModeNet m i n.
Theorem currMode_pres_fwd (n n' : Network) (a : ActDiscNet) (m : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m i n ->
exists m', currModeNet m' i n'.
Theorem outgoing_del (n n' : Network) (d : Delay) (v : list BaseType) (t : Time) (i : nat) :
n -ND- d -ND> n' -> outgoing v t i n ->
{p : d <= t | outgoing v (minusTime t d p) i n'}.
Corollary outgoing_del_contra (n n' : Network) (d : Delay)
(v : list BaseType) (i : nat) : n -ND- d -ND> n' -> outgoing v zeroTime i n -> False.
Theorem outgoing_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> outgoing v t i n -> 0 < t ->
outgoing v t i n'.
Theorem incomingNetNotif_del (n n' : Network) (d : Delay) (v : list BaseType)
(t : Time) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> incomingNetNotif v t i n ->
{p : d <= t | incomingNetNotif v (minusTime t d p) i n'}.
Theorem incomingNetNotif_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> incomingNetNotif v t i n -> 0 < t ->
incomingNetNotif v t i n'.
Lemma inPos_del_bound_bkwd (n n' : Network) (d : Delay) (l' : Position) (i : nat) :
inPosNet l' i n' -> n -ND- d -ND> n' -> exists l,
inPosNet l i n /\ dist2d l l' <= speedMax * d.
Conjecture currMode_intro : forall (m : Mode) (e : Entity) (i : nat) (n : Network),
m = currModeEnt e -> e @ i .: n -> currModeNet m i n.
Conjecture inPos_ex : forall (i : nat) (n : Network) (e : Entity),
e @ i .: n -> exists l, inPosNet l i n.
Conjecture distNet_intro : forall (e1 e2 : Entity) (i j : nat) (n : Network) (x : Distance),
e1 @ i .: n -> e2 @ j .: n -> x = mkDistance (dist2d e1 e2) -> distNet i j n x.
Conjecture inPos_pos : forall (e : Entity) (i : nat) (l : Position) (n : Network),
e @ i .: n -> inPosNet l i n -> posEnt e = l.
Conjecture reachable_net_ent : forall (n : Network) (e : Entity) (i : nat),
reachableNet n -> e @ i .: n -> reachableEnt e.
Conjecture disc_pres_distNet_bkwd : forall (n n' : Network) (a : ActDiscNet)
(i j : nat) (x : Distance),
n -NA- a -NA> n' -> distNet i j n' x -> distNet i j n x.
Conjecture del_link_distNet_bkwd : forall (n n' : Network) (d : Delay)
(i j : nat) (x' : Distance),
n -ND- d -ND> n' -> distNet i j n' x' ->
exists x, distNet i j n x /\ x <= x' + 2*speedMax*d.
Conjecture distNet_elim : forall (i j : nat) (n : Network) (x : Distance),
distNet i j n x -> exists e1 e2,
e1 @ i .: n /\ e2 @ j .: n /\ x = {| distance := dist2d e1 e2 |}.
Lemma del_net_ent (e : Entity) (i : nat) (n n' : Network) (d : Delay) :
e @ i .: n -> n -ND- d -ND> n' -> exists e', e -ED- d ->> e'.
Lemma inRange_acc_input (n n' : Network) (v : list BaseType) (l : Position)
(r : Distance) (i : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /?: -NA> n' -> e @ i .: n -> dist2d l (posEnt e) <= r ->
exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ i .: n'.
Lemma inRange_out_input (n n' : Network) (v : list BaseType) (l : Position)
(r x: Distance) (i j : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /! i -NA> n' -> e @ j .: n -> i <> j -> distNet i j n' x ->
x <= r -> exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ j .: n'.
Conjecture transGuard_disc_pres : forall (n n' : Network)
(a : ActDiscNet) (t : Time) (i : nat),
n -NA- a -NA> n' -> transGuard t i n -> transGuard t i n'.
Conjecture transGuard_elim : forall (t : Time) (i : nat) (n : Network),
transGuard t i n -> exists m m',
mState_in_net (<| m, m', t |>) i n.
Conjecture transGuard_intro : forall (t : Time) (i : nat) (n : Network)
(m m' : Mode), mState_in_net (<| m, m', t |>) i n ->
transGuard t i n.
Conjecture mState_disc_pres : forall (n n' : Network) (i : nat)
(a : ActDiscNet) (k : ModeState), n -NA- a -NA> n' -> mState_in_net k i n ->
exists k', mState_in_net k' i n'.
Conjecture transGuard_del : forall (n n' : Network)
(d : Delay) (t : Time) (i : nat),
n -ND- d -ND> n' -> transGuard t i n ->
exists p, transGuard (minusTime t d p) i n'.
Conjecture currModeNet_del_pres : forall (n n' : Network) (d : Delay)
(m : Mode) (i : nat), n -ND- d -ND> n' ->
(currModeNet m i n <-> currModeNet m i n').
Conjecture currModeNet_dec : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n \/ ~currModeNet m i n.
Lemma initial_failSafe (n : Network) (e : Entity) (i : nat) :
initialNet n -> e @ i .: n -> failSafe e.
Lemma curr_switch_ent_tau (n n' : Network) (a : ActDiscNet)
(e e' : Entity) (i : nat) (m m' : Mode) :
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n' ->
currModeEnt e = m -> currModeEnt e' = m' -> m <> m' ->
e -EA- aeTau ->> e'.
Lemma reachable_net_prot : forall (n : Network) (i : nat)
(p : ProcTerm) (l : Position) (h : Interface) (k : ModeState),
reachableNet n -> [|p, l, h, k|] @ i .: n ->
reachableProt p.
Lemma currMode_del_pres_bkwd (n n' : Network) (d : Delay) (m : Mode) (i : nat) :
n -ND- d -ND> n' -> currModeNet m i n' -> currModeNet m i n.
Conjecture inPos_ent_net : forall (l : Position) (e : Entity) (i : nat) (n : Network),
inPosEnt l e -> e @ i .: n -> inPosNet l i n.
Conjecture inPos_unique : forall (l l' : Position) (i : nat) (n : Network),
inPosNet l i n -> inPosNet l' i n -> l = l'.
Lemma outNet_incomingNetNotif (n n' : Network) (v : list BaseType) (r : Distance)
(l : Position) (i : nat) : n -NA- ([-v, l, r-]) /! i -NA> n' ->
incomingNetNotif ((baseDistance r)::v) adaptNotif i n'.
n -ND- d -ND> n' -> nextSinceStateNet i n ->
exists m t x y, ovWaitStateNet m t (delToTime (x +dt+ d)) (delToTime (y +dt+ d)) i n.
Lemma switchCurr_switchListen_net_link (n n' : Network) (i : nat)
(a : ActDiscNet) (e e' : Entity) :
switchCurrStateEnt e -> switchListenStateEnt e' ->
e @ i .: n -> e' @ i .: n' -> n -NA- a -NA> n' ->
a = anTau /\ interEnt e = interEnt e'.
Lemma init_nextMode_net m i n :
reachableNet n -> initStateNet m i n -> nextModeNet m i n.
Lemma ovReady_prev_net_strong m t l n n' i a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
(exists x0 y0, ovWaitStateNet m t x0 y0 i n).
Lemma ovWait_prev_net_strong m t x y n n' i a :
ovWaitStateNet m t x y i n' -> n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists t0 l0, ovReadyStateNet m t0 l0 i n) \/
initStateNet m i n.
Lemma nextMode_pres_fwd_net m i n n' a :
reachableNet n -> nextModeNet m i n ->
~(switchCurrStateNet i n \/ ovAbortStateNet i n \/
tfsCurrStateNet i n) ->
n -NA- a -NA> n' -> nextModeNet m i n'.
Lemma ovWait_del_pres_bkwd_net_strong n n' d m t x y i :
n -ND- d -ND> n' -> ovWaitStateNet m t x y i n' ->
ovWaitStateNet m t (x +dt+ d) (y +dt+ d) i n.
Lemma ovReady_del_pres_bkwd_net n n' d m t l i :
n -ND- d -ND> n' -> ovReadyStateNet m t l i n' ->
ovReadyStateNet m t l i n.
Lemma nextModeNet_del_pres n n' d m i :
n -ND- d -ND> n' -> nextModeNet m i n -> nextModeNet m i n'.
Lemma ovWait_ovReady_nextMode_net m t x y l i n :
reachableNet n -> ovWaitStateNet m t x y i n \/ ovReadyStateNet m t l i n ->
nextModeNet m i n.
Lemma ovWaitState_nextMode_net (n : Network) (m : Mode) (t x y : Time) (i : nat):
reachableNet n -> ovWaitStateNet m t x y i n -> nextModeNet m i n.
Theorem del_listening_net (n n' : Network) (d : Delay) (e : Entity) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> e @ i .: n -> listeningStateNet i n.
Theorem inPos_pres_disc (n n' : Network) (a : ActDiscNet) (l : Position) (i : nat) :
n -NA- a -NA> n' ->
(inPosNet l i n <-> inPosNet l i n').
Theorem currMode_pres_bkwd (n n' : Network) (a : ActDiscNet) (m' : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m' i n' ->
exists m, currModeNet m i n.
Theorem currMode_pres_fwd (n n' : Network) (a : ActDiscNet) (m : Mode) (i : nat) :
n -NA- a -NA> n' -> currModeNet m i n ->
exists m', currModeNet m' i n'.
Theorem outgoing_del (n n' : Network) (d : Delay) (v : list BaseType) (t : Time) (i : nat) :
n -ND- d -ND> n' -> outgoing v t i n ->
{p : d <= t | outgoing v (minusTime t d p) i n'}.
Corollary outgoing_del_contra (n n' : Network) (d : Delay)
(v : list BaseType) (i : nat) : n -ND- d -ND> n' -> outgoing v zeroTime i n -> False.
Theorem outgoing_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> outgoing v t i n -> 0 < t ->
outgoing v t i n'.
Theorem incomingNetNotif_del (n n' : Network) (d : Delay) (v : list BaseType)
(t : Time) (i : nat) :
reachableNet n -> n -ND- d -ND> n' -> incomingNetNotif v t i n ->
{p : d <= t | incomingNetNotif v (minusTime t d p) i n'}.
Theorem incomingNetNotif_disc_pres (n n' : Network) (a : ActDiscNet) (v : list BaseType) (t : Time) (i : nat) :
n -NA- a -NA> n' -> incomingNetNotif v t i n -> 0 < t ->
incomingNetNotif v t i n'.
Lemma inPos_del_bound_bkwd (n n' : Network) (d : Delay) (l' : Position) (i : nat) :
inPosNet l' i n' -> n -ND- d -ND> n' -> exists l,
inPosNet l i n /\ dist2d l l' <= speedMax * d.
Conjecture currMode_intro : forall (m : Mode) (e : Entity) (i : nat) (n : Network),
m = currModeEnt e -> e @ i .: n -> currModeNet m i n.
Conjecture inPos_ex : forall (i : nat) (n : Network) (e : Entity),
e @ i .: n -> exists l, inPosNet l i n.
Conjecture distNet_intro : forall (e1 e2 : Entity) (i j : nat) (n : Network) (x : Distance),
e1 @ i .: n -> e2 @ j .: n -> x = mkDistance (dist2d e1 e2) -> distNet i j n x.
Conjecture inPos_pos : forall (e : Entity) (i : nat) (l : Position) (n : Network),
e @ i .: n -> inPosNet l i n -> posEnt e = l.
Conjecture reachable_net_ent : forall (n : Network) (e : Entity) (i : nat),
reachableNet n -> e @ i .: n -> reachableEnt e.
Conjecture disc_pres_distNet_bkwd : forall (n n' : Network) (a : ActDiscNet)
(i j : nat) (x : Distance),
n -NA- a -NA> n' -> distNet i j n' x -> distNet i j n x.
Conjecture del_link_distNet_bkwd : forall (n n' : Network) (d : Delay)
(i j : nat) (x' : Distance),
n -ND- d -ND> n' -> distNet i j n' x' ->
exists x, distNet i j n x /\ x <= x' + 2*speedMax*d.
Conjecture distNet_elim : forall (i j : nat) (n : Network) (x : Distance),
distNet i j n x -> exists e1 e2,
e1 @ i .: n /\ e2 @ j .: n /\ x = {| distance := dist2d e1 e2 |}.
Lemma del_net_ent (e : Entity) (i : nat) (n n' : Network) (d : Delay) :
e @ i .: n -> n -ND- d -ND> n' -> exists e', e -ED- d ->> e'.
Lemma inRange_acc_input (n n' : Network) (v : list BaseType) (l : Position)
(r : Distance) (i : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /?: -NA> n' -> e @ i .: n -> dist2d l (posEnt e) <= r ->
exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ i .: n'.
Lemma inRange_out_input (n n' : Network) (v : list BaseType) (l : Position)
(r x: Distance) (i j : nat) (e : Entity) :
n -NA- ([-v, l, r-]) /! i -NA> n' -> e @ j .: n -> i <> j -> distNet i j n' x ->
x <= r -> exists e', e -EA- ([-v, l, r-]) #? ->> e' /\ e' @ j .: n'.
Conjecture transGuard_disc_pres : forall (n n' : Network)
(a : ActDiscNet) (t : Time) (i : nat),
n -NA- a -NA> n' -> transGuard t i n -> transGuard t i n'.
Conjecture transGuard_elim : forall (t : Time) (i : nat) (n : Network),
transGuard t i n -> exists m m',
mState_in_net (<| m, m', t |>) i n.
Conjecture transGuard_intro : forall (t : Time) (i : nat) (n : Network)
(m m' : Mode), mState_in_net (<| m, m', t |>) i n ->
transGuard t i n.
Conjecture mState_disc_pres : forall (n n' : Network) (i : nat)
(a : ActDiscNet) (k : ModeState), n -NA- a -NA> n' -> mState_in_net k i n ->
exists k', mState_in_net k' i n'.
Conjecture transGuard_del : forall (n n' : Network)
(d : Delay) (t : Time) (i : nat),
n -ND- d -ND> n' -> transGuard t i n ->
exists p, transGuard (minusTime t d p) i n'.
Conjecture currModeNet_del_pres : forall (n n' : Network) (d : Delay)
(m : Mode) (i : nat), n -ND- d -ND> n' ->
(currModeNet m i n <-> currModeNet m i n').
Conjecture currModeNet_dec : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n \/ ~currModeNet m i n.
Lemma initial_failSafe (n : Network) (e : Entity) (i : nat) :
initialNet n -> e @ i .: n -> failSafe e.
Lemma curr_switch_ent_tau (n n' : Network) (a : ActDiscNet)
(e e' : Entity) (i : nat) (m m' : Mode) :
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n' ->
currModeEnt e = m -> currModeEnt e' = m' -> m <> m' ->
e -EA- aeTau ->> e'.
Lemma reachable_net_prot : forall (n : Network) (i : nat)
(p : ProcTerm) (l : Position) (h : Interface) (k : ModeState),
reachableNet n -> [|p, l, h, k|] @ i .: n ->
reachableProt p.
Lemma currMode_del_pres_bkwd (n n' : Network) (d : Delay) (m : Mode) (i : nat) :
n -ND- d -ND> n' -> currModeNet m i n' -> currModeNet m i n.
Conjecture inPos_ent_net : forall (l : Position) (e : Entity) (i : nat) (n : Network),
inPosEnt l e -> e @ i .: n -> inPosNet l i n.
Conjecture inPos_unique : forall (l l' : Position) (i : nat) (n : Network),
inPosNet l i n -> inPosNet l' i n -> l = l'.
Lemma outNet_incomingNetNotif (n n' : Network) (v : list BaseType) (r : Distance)
(l : Position) (i : nat) : n -NA- ([-v, l, r-]) /! i -NA> n' ->
incomingNetNotif ((baseDistance r)::v) adaptNotif i n'.
Linking theorem.
Lemma incoming_net_ent (v : list BaseType) (i : nat) (n : Network) :
incomingNet v i n -> exists e, incomingEnt v e /\ e @ i .: n.
incomingNet v i n -> exists e, incomingEnt v e /\ e @ i .: n.
Linking theorem.
Lemma incoming_ent_net (v : list BaseType) (e : Entity) (i : nat) (n : Network) :
incomingEnt v e -> e @ i .: n -> incomingNet v i n.
Ltac inposdp :=
match goal with
[ w : ?n -NA- _ -NA> ?n', H : inPosNet ?l ?i ?n' |- inPosNet ?l ?i ?n] =>
eapply inPos_pres_disc; [apply w | assumption]
end.
Lemma net_del_elim q q0 q1 l h k i n n' d :
[|q $||$ q0 $||$ q1, l, h, k|] @ i .: n ->
n -ND- d -ND> n' ->
exists q' q0' q1' l' h' k',
[|q' $||$ q0' $||$ q1', l', h', k'|] @ i .: n' /\
q -PD- d -PD> q' /\ q0 -PD- d -PD> q0' /\ q1 -PD- d -PD> q1' /\
h -i- d -i> h' /\ k -ms- d -ms> k' /\
dist2d l l' <= speedMax * d.
Conjecture currMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n <-> exists e, e @ i .: n /\ currModeEnt e = m.
Conjecture nextMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
nextModeNet m i n <-> exists e, e @ i .: n /\ nextModeEnt m e.
Ltac currMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : currModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite currMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Ltac nextMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : nextModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite nextMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Lemma mState_in_net_unique k k' i n :
mState_in_net k i n -> mState_in_net k' i n -> k = k'.
incomingEnt v e -> e @ i .: n -> incomingNet v i n.
Ltac inposdp :=
match goal with
[ w : ?n -NA- _ -NA> ?n', H : inPosNet ?l ?i ?n' |- inPosNet ?l ?i ?n] =>
eapply inPos_pres_disc; [apply w | assumption]
end.
Lemma net_del_elim q q0 q1 l h k i n n' d :
[|q $||$ q0 $||$ q1, l, h, k|] @ i .: n ->
n -ND- d -ND> n' ->
exists q' q0' q1' l' h' k',
[|q' $||$ q0' $||$ q1', l', h', k'|] @ i .: n' /\
q -PD- d -PD> q' /\ q0 -PD- d -PD> q0' /\ q1 -PD- d -PD> q1' /\
h -i- d -i> h' /\ k -ms- d -ms> k' /\
dist2d l l' <= speedMax * d.
Conjecture currMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
currModeNet m i n <-> exists e, e @ i .: n /\ currModeEnt e = m.
Conjecture nextMode_ent_ex : forall (m : Mode) (i : nat) (n : Network),
nextModeNet m i n <-> exists e, e @ i .: n /\ nextModeEnt m e.
Ltac currMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : currModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite currMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Ltac nextMode_ent_ex_tac e U :=
let Q := fresh in let U1 := fresh U in let U2 := fresh U in
match goal with
[H : nextModeNet ?m ?i ?n |- _ ] => lets Q : H; rewrite nextMode_ent_ex in Q;
decompExAnd Q e U1 U2
end.
Lemma mState_in_net_unique k k' i n :
mState_in_net k i n -> mState_in_net k' i n -> k = k'.
Given a network state predicate as the goal and the corresponding
entity state predicate in the hypotheses, this solves things using
lenWitness.
Ltac netState_ent_net_tac := eapply lenWitness;
[eassumption | eassumption].
Lemma tfsNext_currModeNet_eq m1 m2 i n : currModeNet m1 i n ->
tfsNextStateNet m2 i n -> m1 = m2.
[eassumption | eassumption].
Lemma tfsNext_currModeNet_eq m1 m2 i n : currModeNet m1 i n ->
tfsNextStateNet m2 i n -> m1 = m2.
The nextSinceState relation can be broken down into the following cases.
Lemma nexSinceStateNet_cases i n :
nextSinceStateNet i n ->
(exists m t x y, ovWaitStateNet m t x y i n) \/
(exists m t l, ovReadyStateNet m t l i n) \/
(exists m, switchBcStateNet m i n) \/
(switchCurrStateNet i n).
Lemma link_net_ent_disc :
forall (n n' : Network) (e e' : Entity) (i : nat) (a : ActDiscNet),
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n'->
(e = e' \/ (exists a', e -EA- a' ->> e')).
Ltac link_netentdisc_tac b :=
match goal with
| [ U1 : ?n -NA- ?a -NA> ?n', U2 : ?e @ ?i .: ?n,
U3 : ?e' @ ?i .: ?n' |- _] =>
let H1 := fresh in lets H1 : link_net_ent_disc U1 U2 U3;
let H2 := fresh in let H3 := fresh in
elim_intro H1 H2 H3; [subst_all H2 |
let H4 := fresh in invertClearAs2 H3 b H4]
end.
nextSinceStateNet i n ->
(exists m t x y, ovWaitStateNet m t x y i n) \/
(exists m t l, ovReadyStateNet m t l i n) \/
(exists m, switchBcStateNet m i n) \/
(switchCurrStateNet i n).
Lemma link_net_ent_disc :
forall (n n' : Network) (e e' : Entity) (i : nat) (a : ActDiscNet),
n -NA- a -NA> n' -> e @ i .: n -> e' @ i .: n'->
(e = e' \/ (exists a', e -EA- a' ->> e')).
Ltac link_netentdisc_tac b :=
match goal with
| [ U1 : ?n -NA- ?a -NA> ?n', U2 : ?e @ ?i .: ?n,
U3 : ?e' @ ?i .: ?n' |- _] =>
let H1 := fresh in lets H1 : link_net_ent_disc U1 U2 U3;
let H2 := fresh in let H3 := fresh in
elim_intro H1 H2 H3; [subst_all H2 |
let H4 := fresh in invertClearAs2 H3 b H4]
end.
Does some pre-processing on the proof of a backracking theorem at the
network level. Works where the backtracking has two predecessor cases.
Probably needs to be slightly altered if there's a need to handle more cases.
Ltac backtrack_net_pre U :=
let U1 := fresh in let e := fresh "e" in let b := fresh "b" in
state_pred_net_destr U; link_netentdiscbkwd_tac0 e b U1;
let EQ := fresh "EQ" in let EX := fresh in
match goal with [U2 : _ \/ _ |- _ ] =>
elim_intro U2 EQ EX; [left; econstructor | ];
[eassumption | | ]; [ subst; assumption | ex_flat] end.
let U1 := fresh in let e := fresh "e" in let b := fresh "b" in
state_pred_net_destr U; link_netentdiscbkwd_tac0 e b U1;
let EQ := fresh "EQ" in let EX := fresh in
match goal with [U2 : _ \/ _ |- _ ] =>
elim_intro U2 EQ EX; [left; econstructor | ];
[eassumption | | ]; [ subst; assumption | ex_flat] end.
Tactic for eliminating two contradictory state predicates H and H1
Ltac state_pred_elim_net H H1 :=
let e := fresh "e" in let e' := fresh "e'" in
let U1 := fresh in let U2 := fresh in let U3 := fresh in
let U1' := fresh in let U2' := fresh in
inversion H as [e U1 U2]; inversion H1 as [e' U1' U2'];
assert (e' = e) as U3;[eapply entInNetUnique; eassumption | ];
subst_all U3; destruct e as [p0 l0 h0 k0]; inversion U1;
inversion U1'; subst;
match goal with [SP1 : context[p0], SP2 : context[p0] |- _] =>
inversion SP1; inversion SP2 end; subst;
match goal with [PT : _ $||$ _ $||$ _ = ?p1 $||$ ?p2 $||$ ?p3 |- _] =>
inversion PT; subst;
repeat match goal with [PT : context[_ $||$ _ $||$ _] |- _] =>
clear PT end;
match goal with
| [SP1 : context[p1], SP2 : context[p1] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p2], SP2 : context[p2] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p3], SP2 : context[p3] |- _] =>
inversion SP1; subst; inversion SP2
end
end.
Lemma tfsStart_prev_net i n n' a : tfsStartStateNet i n' ->
n -NA- a -NA> n' -> tfsStartStateNet i n \/
exists m t x y, ovWaitStateNet m t x y i n.
Lemma ovReady_prev_net m t l i n n' a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
exists x y, ovWaitStateNet m t x y i n.
Lemma ovWait_del_pres_net m t x y i n n' d : n -ND- d -ND> n' ->
(ovWaitStateNet m t x y i n <-> ovWaitStateNet m t x y i n').
Lemma tfsNext_prev_net m i n n' a : tfsNextStateNet m i n' ->
n -NA- a -NA> n' -> tfsNextStateNet m i n \/ tfsStartStateNet i n.
Lemma del_pres_bkwd_tfsNext m i n n' d :
n -ND- d -ND> n' -> tfsNextStateNet m i n' -> tfsNextStateNet m i n.
Lemma del_pres_bkwd_tfsStart i n n' d :
n -ND- d -ND> n' -> tfsStartStateNet i n' -> tfsStartStateNet i n.
Lemma tfsNext_urgent_net m i n n' d :
tfsNextStateNet m i n -> n -ND- d -ND> n' -> False.
Lemma tfsStart_urgent_net i n n' d :
tfsStartStateNet i n -> n -ND- d -ND> n' -> False.
Lemma ovReady_wait_track_net m t l i m' t' x y n n' a :
ovReadyStateNet m t l i n -> ovWaitStateNet m' t' x y i n' ->
n -NA- a -NA> n' -> m = m' /\
(exists p, t' = minusTime t (period m) p) /\ x = t' /\ y = period m.
Lemma ovWait_track_net m m' t t' x x' y y' i n n' a :
ovWaitStateNet m t x y i n -> ovWaitStateNet m' t' x' y' i n' ->
n -NA- a -NA> n' -> m = m' /\ t = t' /\ x = x' /\ y = y'.
Lemma ovWait_prev_net m t x y i n n' a : ovWaitStateNet m t x y i n' ->
n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists l, ovReadyStateNet m (t +t+ period m) l i n) \/
initStateNet m i n.
Ltac reach_net_prot_tac :=
match goal with [RN : reachableNet ?n,
EIN : [|_, _, _, _|] @ _ .: ?n |- _] =>
let RNP := fresh "RNP" in
let RPT := fresh "RPT" in
lets RNP : reachable_net_prot RN EIN;
lets RPT : reachableProt_triple RNP end.
let e := fresh "e" in let e' := fresh "e'" in
let U1 := fresh in let U2 := fresh in let U3 := fresh in
let U1' := fresh in let U2' := fresh in
inversion H as [e U1 U2]; inversion H1 as [e' U1' U2'];
assert (e' = e) as U3;[eapply entInNetUnique; eassumption | ];
subst_all U3; destruct e as [p0 l0 h0 k0]; inversion U1;
inversion U1'; subst;
match goal with [SP1 : context[p0], SP2 : context[p0] |- _] =>
inversion SP1; inversion SP2 end; subst;
match goal with [PT : _ $||$ _ $||$ _ = ?p1 $||$ ?p2 $||$ ?p3 |- _] =>
inversion PT; subst;
repeat match goal with [PT : context[_ $||$ _ $||$ _] |- _] =>
clear PT end;
match goal with
| [SP1 : context[p1], SP2 : context[p1] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p2], SP2 : context[p2] |- _] =>
inversion SP1; subst; inversion SP2
| [SP1 : context[p3], SP2 : context[p3] |- _] =>
inversion SP1; subst; inversion SP2
end
end.
Lemma tfsStart_prev_net i n n' a : tfsStartStateNet i n' ->
n -NA- a -NA> n' -> tfsStartStateNet i n \/
exists m t x y, ovWaitStateNet m t x y i n.
Lemma ovReady_prev_net m t l i n n' a :
ovReadyStateNet m t l i n' -> n -NA- a -NA> n' ->
ovReadyStateNet m t l i n \/
exists x y, ovWaitStateNet m t x y i n.
Lemma ovWait_del_pres_net m t x y i n n' d : n -ND- d -ND> n' ->
(ovWaitStateNet m t x y i n <-> ovWaitStateNet m t x y i n').
Lemma tfsNext_prev_net m i n n' a : tfsNextStateNet m i n' ->
n -NA- a -NA> n' -> tfsNextStateNet m i n \/ tfsStartStateNet i n.
Lemma del_pres_bkwd_tfsNext m i n n' d :
n -ND- d -ND> n' -> tfsNextStateNet m i n' -> tfsNextStateNet m i n.
Lemma del_pres_bkwd_tfsStart i n n' d :
n -ND- d -ND> n' -> tfsStartStateNet i n' -> tfsStartStateNet i n.
Lemma tfsNext_urgent_net m i n n' d :
tfsNextStateNet m i n -> n -ND- d -ND> n' -> False.
Lemma tfsStart_urgent_net i n n' d :
tfsStartStateNet i n -> n -ND- d -ND> n' -> False.
Lemma ovReady_wait_track_net m t l i m' t' x y n n' a :
ovReadyStateNet m t l i n -> ovWaitStateNet m' t' x y i n' ->
n -NA- a -NA> n' -> m = m' /\
(exists p, t' = minusTime t (period m) p) /\ x = t' /\ y = period m.
Lemma ovWait_track_net m m' t t' x x' y y' i n n' a :
ovWaitStateNet m t x y i n -> ovWaitStateNet m' t' x' y' i n' ->
n -NA- a -NA> n' -> m = m' /\ t = t' /\ x = x' /\ y = y'.
Lemma ovWait_prev_net m t x y i n n' a : ovWaitStateNet m t x y i n' ->
n -NA- a -NA> n' ->
ovWaitStateNet m t x y i n \/
(exists l, ovReadyStateNet m (t +t+ period m) l i n) \/
initStateNet m i n.
Ltac reach_net_prot_tac :=
match goal with [RN : reachableNet ?n,
EIN : [|_, _, _, _|] @ _ .: ?n |- _] =>
let RNP := fresh "RNP" in
let RPT := fresh "RPT" in
lets RNP : reachable_net_prot RN EIN;
lets RPT : reachableProt_triple RNP end.
This page has been generated by coqdoc