Library NARTop
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 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.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NARInsuff.
Require Import ComhCoq.NARMisc.
Require Import ComhCoq.NARMsgPosition.
Require Import ComhCoq.NAROvlpTime.
Theorem currSince_lower_bound (n : Network) (t : Time) (m : Mode)
(i : nat) (p : reachableNet n) : currSince m t i n p ->
msgLatency + Rmax adaptNotif transMax < t.
Lemma maxAnTrans_positive : 0 <= Rmax adaptNotif transMax.
Theorem nextSince_fst_deliv_suff (n : Network) (t : Time) (m : Mode)
(i : nat) (l : Position) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n ->
forall q : msgLatency + Rmax adaptNotif transMax < t,
let s := (Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax)
t q maxAnTrans_positive) in
let s' := Rlt_le msgLatency t s in
exists l0 l1 r,
delivered ([-[baseMode m, basePosition l0], l1, r-]) (minusTime t msgLatency s') i n p /\
sufficient m r /\ dist2d l l0 <= speedMax*t.
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 init_ovWait_track_net m m' t' i x y n n' a :
initStateNet m i n -> ovWaitStateNet m' t' x y i n' ->
n -NA- a -NA> n' -> m = m' /\ x = t' /\ y = zeroTime.
Theorem ovWait_sent (n : Network) (m : Mode) (t x y : Time) (i : nat) (p : reachableNet n) :
ovWaitStateNet m t x y i n -> 0 < y ->
exists l q,
sent [baseMode m, basePosition l] (minusTime (period m) y q) i n p.
Theorem nextSince_periodic_sent (n : Network) (m : Mode) (t t' : Time)
(i : nat) (p : reachableNet n) :
nextSince m t i n p -> t' < t ->
exists t'' l,
t' < (time t'') <= t' + period m /\ t'' <= t /\
sent [baseMode m, basePosition l] t'' i n p.
Theorem tfsBc_not_currSince (n : Network) (m : Mode) (t : Time)
(i : nat) (p : reachableNet n) :
tfsBcStateNet i n -> currSince m t i n p -> False.
Theorem currSince_bc_state (n : Network) (m : Mode) (t : Time)
(i : nat) (p : reachableNet n) : currSince m t i n p ->
(exists x, bcWaitStateNet m x i n) \/
(exists l, bcReadyStateNet m l i n).
If we're currSince & we can delay, then we're in the bcWait state.
Corollary currSince_del_bcWait (n n' : Network) (m : Mode) (t : Time)
(i : nat) (d : Delay) (p : reachableNet n) :
n -ND- d -ND> n' -> currSince m t i n p ->
exists x, bcWaitStateNet m (delToTime (x +dt+ d)) i n.
Theorem bcWait_currSince_time (n : Network) (m : Mode) (x t: Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> currSince m t i n p -> period m - x <= t.
Theorem bcWait_sent (n : Network) (m : Mode) (x : Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> zeroTime < x ->
exists l q,
sent [baseMode m, basePosition l] (minusTime (period m) x q) i n p.
Theorem currSince_periodic_sent (n : Network) (m : Mode) (t t' : Time)
(i : nat) (p : reachableNet n) :
currSince m t i n p -> t' < t ->
exists t'' l, t' < (time t'') /\ t'' <= t' + period m /\ t'' <= t /\
sent [baseMode m, basePosition l] t'' i n p.
Theorem currSince_fst_deliv_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
exists q,
let s := (Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax) t q
maxAnTrans_positive) in
let s' := Rlt_le msgLatency t s in
exists r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) (minusTime t msgLatency s') i n p /\
sufficient m r /\ dist2d l l0 <= speedMax*t.
Theorem pre_del_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> ~failSafe m ->
exists t' r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) t' i n p /\
sufficient m r /\ t' [:] (preDeliveredInterval m) /\ t' < t /\
dist2d l l0 <= speedMax*(msgLatency+ t').
(i : nat) (d : Delay) (p : reachableNet n) :
n -ND- d -ND> n' -> currSince m t i n p ->
exists x, bcWaitStateNet m (delToTime (x +dt+ d)) i n.
Theorem bcWait_currSince_time (n : Network) (m : Mode) (x t: Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> currSince m t i n p -> period m - x <= t.
Theorem bcWait_sent (n : Network) (m : Mode) (x : Time)
(i : nat) (p : reachableNet n) :
bcWaitStateNet m x i n -> zeroTime < x ->
exists l q,
sent [baseMode m, basePosition l] (minusTime (period m) x q) i n p.
Theorem currSince_periodic_sent (n : Network) (m : Mode) (t t' : Time)
(i : nat) (p : reachableNet n) :
currSince m t i n p -> t' < t ->
exists t'' l, t' < (time t'') /\ t'' <= t' + period m /\ t'' <= t /\
sent [baseMode m, basePosition l] t'' i n p.
Theorem currSince_fst_deliv_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
exists q,
let s := (Rplus_lt_weaken_lr msgLatency (Rmax adaptNotif transMax) t q
maxAnTrans_positive) in
let s' := Rlt_le msgLatency t s in
exists r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) (minusTime t msgLatency s') i n p /\
sufficient m r /\ dist2d l l0 <= speedMax*t.
Theorem pre_del_suff (n : Network) (m : Mode) (t : Time)
(i : nat) (l : Position) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> ~failSafe m ->
exists t' r l0 l1,
delivered ([-[baseMode m, basePosition l0], l1, r-]) t' i n p /\
sufficient m r /\ t' [:] (preDeliveredInterval m) /\ t' < t /\
dist2d l l0 <= speedMax*(msgLatency+ t').
This page has been generated by coqdoc