Library NARMisc
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 Program.Equality.
Require Import ComhCoq.Extras.LibTactics.
Require Import ComhCoq.GenTacs.
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.NetworkLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Lemma state_disj_paused_notifAbort i n :
pausedStateNet i n -> notifAbortPathNet i n -> False.
Lemma state_disj_tfsCurr_start : forall (i : nat) (n : Network),
tfsCurrStateNet i n -> tfsStartStateNet i n -> False.
Lemma state_disj_tfsCurr_bc : forall (i : nat) (n : Network),
tfsCurrStateNet i n -> tfsBcStateNet i n -> False.
Lemma state_disj_tfsCurr_switchListen : forall (i : nat) (n : Network),
tfsCurrStateNet i n -> switchListenStateNet i n -> False.
Lemma init_nextMode_net m i n :
initStateNet m i n -> nextModeNet m i n. Lemma ovWait_ovReady_nextMode_net i n (p : reachableNet n) :
(forall m t x y, ovWaitStateNet m t x y i n ->
nextModeNet m i n) /\
(forall m t l, ovReadyStateNet m t l i n -> nextModeNet m i n).
Lemma switchBc_nextMode_net m i n :
switchBcStateNet m i n -> nextModeNet m i n. Lemma switchCurr_nextSince_nextMode_net m t i n p :
nextSince m t i n p ->
switchCurrStateNet i n -> nextModeNet m i n.
Lemma nextSince_switchBc_modeEq m m' t i n p :
nextSince m t i n p -> switchBcStateNet m' i n -> m = m'.
Lemma nextSince_ovWait_modeEq m m' t t' x y i n p :
nextSince m t i n p -> ovWaitStateNet m' t' x y i n -> m = m'.
Lemma nextSince_ovReaddy_modeEq m m' t t' l i n p :
nextSince m t i n p -> ovReadyStateNet m' t' l i n -> m = m'.
Theorem tfs_rel_state (n : Network) (m : Mode) (t : Time) (i : nat)
(p : reachableNet n) : tfs m t i n p -> tfsStateNet i n .
Lemma tfsStart_tfs_zero : forall (n : Network) (t : Time)
(i : nat) (m : Mode) (p : reachableNet n),
tfs m t i n p -> tfsStartStateNet i n -> t = zeroTime.
Lemma tfsNext_tfs_zero : forall (n : Network) (t : Time)
(i : nat) (m : Mode) (p : reachableNet n),
tfs m t i n p -> tfsNextStateNet m i n -> t = zeroTime.
Lemma currModeNet_switch_states n n' a m m' i :
reachableNet n -> n -NA- a -NA> n' -> currModeNet m i n ->
currModeNet m' i n' -> m <> m' ->
(switchCurrStateNet i n /\ switchListenStateNet i n') \/
(tfsCurrStateNet i n /\ tfsBcStateNet i n').
Lemma tfsNext_tfs_mode_eq : forall (n : Network) (t : Time)
(i : nat) (m1 m2 : Mode) (p : reachableNet n),
tfs m1 t i n p -> tfsNextStateNet m2 i n -> m1 = m2.
Theorem nextSince_rel_state (n : Network) (m : Mode) (t : Time) (i : nat)
(p : reachableNet n) : nextSince m t i n p -> nextSinceStateNet i n.
Lemma nextSince_next : forall (m : Mode) (t : Time) (i : nat)
(n : Network) (p : reachableNet n),
nextSince m t i n p -> nextModeNet m i n.
Theorem delivered_received (n : Network) (v : list BaseType) (t : Time) (r x : Distance)
(i j : nat) (p : reachableNet n) (l : Position) :
delivered ([-v, l, r-]) t i n p -> i <> j ->
distNet i j n x -> x + 2*speedMax*t <= r -> received v t j n p.
Theorem currSince_curr (n : Network) (m : Mode) (t : Time) (i : nat)
(p : reachableNet n) : currSince m t i n p -> currModeNet m i n.
Theorem tfs_transGuard (n : Network) (m : Mode) (t : Time) (i : nat)
(p : reachableNet n) :
tfsCurrStateNet i n -> tfs m t i n p ->
exists t', transGuard t' i n /\ t + t' <= trans m.
Theorem tfs_bound (n : Network) (m : Mode) (t : Time) (i : nat)
(p : reachableNet n) : tfs m t i n p -> t <= trans m.
Theorem outgoing_timeout_disc (n n' : Network) (a : ActDiscNet) (i : nat)
(p : reachableNet n) (w : n -NA- a -NA> n') (v : list BaseType) (l : Position) :
outgoing v zeroTime i n ->
outgoing v zeroTime i n' \/
exists r, delivered ([-v, l, r-]) zeroTime i n' (reachNetDisc n n' a p w).
Lemma notifAbortPathNet_urgent (i : nat) (n n' : Network) (d : Delay) :
reachableNet n -> notifAbortPathNet i n -> n -ND- d -ND> n' -> False.
Lemma notifBadPathNet_urgent i n n' d :
notifBadPathNet i n -> n -ND- d -ND> n' -> False.
Lemma msgBadPathNet_urgent (n n' : Network) (d : Delay) (i : nat) :
msgBadPathNet i n -> n -ND- d -ND> n' -> False.
Lemma msgAbort_paused_disj_net (i : nat) (n : Network) :
msgAbortPathNet i n -> pausedStateNet i n -> False.
If we are switching from a tfs state to a non tfs state, then we cannot be currSince.
Lemma tfsState_not_currSince (m : Mode) (t : Time) (i : nat) (n n' : Network)
(p : reachableNet n) (a : ActDiscNet) (w : n -NA- a -NA> n') :
tfsStateNet i n -> ~tfsStateNet i n' -> ~currSince m t i n p.
Lemma msgBad_disc_net (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode)
(p : reachableNet n) (w : n -NA- a -NA> n') :
msgBadPathNet i n -> currModeNet m i n ->
msgBadPathNet i n' \/ tfs m zeroTime i n' (reachNetDisc n n' a p w).
(p : reachableNet n) (a : ActDiscNet) (w : n -NA- a -NA> n') :
tfsStateNet i n -> ~tfsStateNet i n' -> ~currSince m t i n p.
Lemma msgBad_disc_net (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode)
(p : reachableNet n) (w : n -NA- a -NA> n') :
msgBadPathNet i n -> currModeNet m i n ->
msgBadPathNet i n' \/ tfs m zeroTime i n' (reachNetDisc n n' a p w).
With a time parameter of 0, the tfs relation is preserved
Lemma tfs_zero_disc_pres (n n' : Network) (a : ActDiscNet) (i : nat) (m : Mode)
(p : reachableNet n) (w : n -NA- a -NA> n') :
tfs m zeroTime i n p ->
tfs m zeroTime i n' (reachNetDisc n n' a p w).
Lemma ovWait_nextSince_time (n : Network) (m : Mode) (x y t t1: Time) (i : nat)
(p : reachableNet n) :
ovWaitStateNet m t x y i n -> nextSince m t1 i n p -> period m - y <= t1.
Lemma nextSince_ovWait_modes_eq (n : Network) (m1 m2 : Mode) (t t1 x y : Time)
(i : nat) (p : reachableNet n) :
ovWaitStateNet m1 t x y i n -> nextSince m2 t1 i n p -> m1 = m2.
Lemma bcWait_bktrk_net (n n' : Network) (m : Mode) (x : Time)
(i : nat) (a : ActDiscNet) (p : reachableNet n) :
bcWaitStateNet m x i n' -> n -NA- a -NA> n' ->
bcWaitStateNet m x i n \/ (sleepingStateNet i n /\ x = zeroTime) \/
(exists l, bcReadyStateNet m l i n /\ x = period m /\
sent [baseMode m, basePosition l] zeroTime i n p).
Lemma msgAbortPathNet_urgent i n n' d :
reachableNet n -> msgAbortPathNet i n -> n -ND- d -ND> n' -> False.
(p : reachableNet n) (w : n -NA- a -NA> n') :
tfs m zeroTime i n p ->
tfs m zeroTime i n' (reachNetDisc n n' a p w).
Lemma ovWait_nextSince_time (n : Network) (m : Mode) (x y t t1: Time) (i : nat)
(p : reachableNet n) :
ovWaitStateNet m t x y i n -> nextSince m t1 i n p -> period m - y <= t1.
Lemma nextSince_ovWait_modes_eq (n : Network) (m1 m2 : Mode) (t t1 x y : Time)
(i : nat) (p : reachableNet n) :
ovWaitStateNet m1 t x y i n -> nextSince m2 t1 i n p -> m1 = m2.
Lemma bcWait_bktrk_net (n n' : Network) (m : Mode) (x : Time)
(i : nat) (a : ActDiscNet) (p : reachableNet n) :
bcWaitStateNet m x i n' -> n -NA- a -NA> n' ->
bcWaitStateNet m x i n \/ (sleepingStateNet i n /\ x = zeroTime) \/
(exists l, bcReadyStateNet m l i n /\ x = period m /\
sent [baseMode m, basePosition l] zeroTime i n p).
Lemma msgAbortPathNet_urgent i n n' d :
reachableNet n -> msgAbortPathNet i n -> n -ND- d -ND> n' -> False.
The notifBadPathNet relation can be broken down into the following cases.
Lemma notifBadPathNet_cases m i n :
notifBadPathNet i n -> currModeNet m i n ->
rangeBadStateNet m i n \/
badOvlpStateNet i n.
Lemma rangeBad_notifBad_net m i n :
rangeBadStateNet m i n -> notifBadPathNet i n.
Lemma badOvlp_notifBad_net i n :
badOvlpStateNet i n -> notifBadPathNet i n.
Lemma ovReady_nextSince_state m t l i n :
ovReadyStateNet m t l i n -> nextSinceStateNet i n.
notifBadPathNet i n -> currModeNet m i n ->
rangeBadStateNet m i n \/
badOvlpStateNet i n.
Lemma rangeBad_notifBad_net m i n :
rangeBadStateNet m i n -> notifBadPathNet i n.
Lemma badOvlp_notifBad_net i n :
badOvlpStateNet i n -> notifBadPathNet i n.
Lemma ovReady_nextSince_state m t l i n :
ovReadyStateNet m t l i n -> nextSinceStateNet i n.
This page has been generated by coqdoc