Library NARInsuff
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.EntityLanguage.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARMisc.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.ProtAuxResults.
Lemma tfs_state_rel i n (p : reachableNet n) :
tfsStateNet i n -> exists m t, tfs m t i n p.
Lemma tfs_currModeNet m1 m2 t i n p : tfs m1 t i n p ->
currModeNet m2 i n -> ~failSafe m2 -> m1 = m2.
Lemma currModeNet_notifBad_pres_bkwd m i n n' a
(rn : reachableNet n) (w : n -NA- a -NA> n') :
currModeNet m i n' -> notifBadPathNet i n ->
~failSafe m ->
currModeNet m i n \/
exists t, tfs m t i n' (reachNetDisc n n' a rn w).
Lemma currEq_eq_badOvlp_net m m'' i n :
m = m'' -> currEqStateNet m m'' i n -> badOvlpStateNet i n.
Theorem delivered_incomingNetNotif (n : Network) (v : list BaseType) (r : Distance)
(l : Position) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-v, l, r-]) t i n p -> forall q : t < adaptNotif,
incomingNetNotif ((baseDistance r)::v) (minusTime adaptNotif t (Rlt_le t adaptNotif q)) i n.
Theorem insuff_incomingNotif_abort (n n' : Network) (a : ActDiscNet) (m : Mode)
(r : Distance) (l : Position) (i : nat) :
nextModeNet m i n -> n -NA- a -NA> n' -> ~sufficient m r ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n' \/
notifAbortPathNet i n'.
Theorem nextSince_next (n : Network) (m : Mode) (t : Time) (i : nat) (p : reachableNet n) :
nextSince m t i n p -> nextModeNet m i n.
Theorem notifAbort_not_nextSince (n n' : Network)
(a : ActDiscNet) (i : nat) (rn : reachableNet n) :
notifAbortPathNet i n -> n -NA- a -NA> n' ->
notifAbortPathNet i n' \/ ~nextSinceStateNet i n'.
Theorem instant_insuff_abort (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-[baseMode m, basePosition l], l0, r-]) adaptNotif i n p -> ~sufficient m r ->
nextSince m t i n p -> adaptNotif < t ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n \/
notifAbortPathNet i n.
Theorem insuff_incomingNotif_bad (n n' : Network) (a : ActDiscNet) (m : Mode)
(r : Distance) (l : Position) (i : nat) :
currModeNet m i n -> n -NA- a -NA> n' -> ~sufficient m r ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n' \/
notifBadPathNet i n'.
If the badOvlp state holds at a particular reachable state,
and in the next state listening holds, then the next state is tfs for some
time t, with the mode parameter equal to the current mode.
Theorem badOvlp_listening_tfs n n' a i m
(rn : reachableNet n) (w : n -NA- a -NA> n') :
badOvlpStateNet i n -> listeningStateNet i n' ->
currModeNet m i n ->
exists t, tfs m t i n' (reachNetDisc n n' a rn w).
Theorem notifBad_pres_tfs (m : Mode) (n n' : Network)
(a : ActDiscNet) (i : nat) (rn : reachableNet n)
(w : n -NA- a -NA> n') :
notifBadPathNet i n -> currModeNet m i n' -> ~failSafe m ->
notifBadPathNet i n' \/ (exists t, tfs m t i n' (reachNetDisc n n' a rn w)).
Lemma tfs_pres_not_currSince m t i n n' p a
(w : n -NA- a -NA> n') : tfs m t i n p ->
tfs m t i n' (reachNetDisc n n' a p w) \/
(forall m' t' p', ~currSince m' t' i n p').
Theorem instant_insuff_bad (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-[baseMode m, basePosition l], l0, r-]) adaptNotif i n p -> ~failSafe m ->
~sufficient m r -> currSince m t i n p -> adaptNotif < t ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n
\/ notifBadPathNet i n \/ exists t, tfs m t i n p.
Theorem deliv_next_suff (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
nextSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
adaptNotif < t' -> t' < t -> sufficient m r.
Theorem insuff_react (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
currSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
forall q : adaptNotif < t', t' < t -> ~sufficient m r -> ~failSafe m ->
exists x, minusTime t' adaptNotif (Rlt_le adaptNotif t' q) <= (time x) /\
tfs m x i n p.
(rn : reachableNet n) (w : n -NA- a -NA> n') :
badOvlpStateNet i n -> listeningStateNet i n' ->
currModeNet m i n ->
exists t, tfs m t i n' (reachNetDisc n n' a rn w).
Theorem notifBad_pres_tfs (m : Mode) (n n' : Network)
(a : ActDiscNet) (i : nat) (rn : reachableNet n)
(w : n -NA- a -NA> n') :
notifBadPathNet i n -> currModeNet m i n' -> ~failSafe m ->
notifBadPathNet i n' \/ (exists t, tfs m t i n' (reachNetDisc n n' a rn w)).
Lemma tfs_pres_not_currSince m t i n n' p a
(w : n -NA- a -NA> n') : tfs m t i n p ->
tfs m t i n' (reachNetDisc n n' a p w) \/
(forall m' t' p', ~currSince m' t' i n p').
Theorem instant_insuff_bad (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t : Time) (i : nat) (p : reachableNet n) :
delivered ([-[baseMode m, basePosition l], l0, r-]) adaptNotif i n p -> ~failSafe m ->
~sufficient m r -> currSince m t i n p -> adaptNotif < t ->
incomingNetNotif [baseDistance r, baseMode m, basePosition l] zeroTime i n
\/ notifBadPathNet i n \/ exists t, tfs m t i n p.
Theorem deliv_next_suff (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
nextSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
adaptNotif < t' -> t' < t -> sufficient m r.
Theorem insuff_react (n : Network) (m : Mode) (l l0 : Position)
(r : Distance) (t t' : Time) (i : nat) (p : reachableNet n) :
currSince m t i n p ->
delivered ([-[baseMode m, basePosition l], l0, r-]) t' i n p ->
forall q : adaptNotif < t', t' < t -> ~sufficient m r -> ~failSafe m ->
exists x, minusTime t' adaptNotif (Rlt_le adaptNotif t' q) <= (time x) /\
tfs m x i n p.
This page has been generated by coqdoc