Library NARIncomp
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 Coq.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.EntityLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARMisc.
Theorem incomingNet_urgent (n n' : Network) (v : list BaseType) (i : nat) (d : Delay) :
reachableNet n -> incomingNet v i n -> ~n -ND- d -ND> n'.
Theorem incomp_incomingNet_bad (n n' : Network) (a : ActDiscNet) (l l' : Position) (i : nat)
(m m' : Mode) :
n -NA- a -NA> n' -> inPosNet l i n -> currModeNet m i n ->
incomingNet [baseMode m', basePosition l'] i n ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n' \/
msgBadPathNet i n'.
Theorem incomp_incomingNet_abort (n n' : Network) (a : ActDiscNet) (l l' : Position) (i : nat)
(m m' : Mode) : n -NA- a -NA> n' -> inPosNet l i n -> nextModeNet m i n ->
incomingNet [baseMode m', basePosition l'] i n ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n' \/ msgAbortPathNet i n'.
Theorem msgAbort_not_nextSince (n n' : Network) (a : ActDiscNet)
(i : nat) (rn : reachableNet n) :
msgAbortPathNet i n -> n -NA- a -NA> n' ->
msgAbortPathNet i n' \/ ~nextSinceStateNet i n'.
This case is almost identical to the case for notifAbortPath_not_nextSince.
Theorem instant_incomp_abort (n : Network) (t : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n -> 0 < t ->
received [baseMode m', basePosition l'] zeroTime i n p ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n \/
msgAbortPathNet i n.
If a message was received some non-zero time t' ago and for longer than this time
we have been pending transition to a mode which threatens to be incompatible with
the received mode, given our current position & adjusting for time, the we get a
contradiction.
Theorem incomp_abort (n : Network) (t t' : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p -> zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax *nn* msgLatency + speedMax*t' < possIncDist m m' ->
False.
Theorem instant_incomp_tfs (n : Network) (t : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> 0 < t ->
received [baseMode m', basePosition l'] zeroTime i n p ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n \/
msgBadPathNet i n \/ tfs m zeroTime i n p.
Theorem incomp_tfs (n : Network) (t t' : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p ->
zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax*nn*msgLatency + speedMax*t' < possIncDist m m' ->
tfs m t' i n p.
(m m' : Mode) (p : reachableNet n) :
nextSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p -> zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax *nn* msgLatency + speedMax*t' < possIncDist m m' ->
False.
Theorem instant_incomp_tfs (n : Network) (t : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n -> 0 < t ->
received [baseMode m', basePosition l'] zeroTime i n p ->
dist2d l l' -nn- speedMax *nn* msgLatency < possIncDist m m' ->
incomingNet [baseMode m', basePosition l'] i n \/
msgBadPathNet i n \/ tfs m zeroTime i n p.
Theorem incomp_tfs (n : Network) (t t' : Time) (l l' : Position) (i : nat)
(m m' : Mode) (p : reachableNet n) :
currSince m t i n p -> inPosNet l i n ->
received [baseMode m', basePosition l'] t' i n p ->
zeroTime < t' -> t' < t ->
dist2d l l' -nn- speedMax*nn*msgLatency + speedMax*t' < possIncDist m m' ->
tfs m t' i n p.
This page has been generated by coqdoc