Library EntAuxDefs
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
*************************** Specialised Imports
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.EntityLanguage.
Require Import ComhCoq.ProtAuxDefs.
Inductive liftProcEnt (X : ProcTerm -> Prop) : Entity -> Prop :=
| lifpe (p : ProcTerm) (l : Position) (h : Interface) (k : ModeState) :
X p -> liftProcEnt X ([|p, l, h, k|]).
Definition bcWaitStateEnt (m : Mode) (x : Time) : Entity -> Prop :=
liftProcEnt (bcWaitStateProt m x).
Definition sleepingStateEnt : Entity -> Prop :=
liftProcEnt sleepingStateProt.
Definition bcReadyStateEnt (m : Mode) (l : Position) : Entity -> Prop :=
liftProcEnt (bcReadyStateProt m l).
Definition dormantStateEnt : Entity -> Prop :=
liftProcEnt dormantStateProt.
Definition tfsStartStateEnt : Entity -> Prop :=
liftProcEnt tfsStartStateProt.
Definition initStateEnt (m : Mode) : Entity -> Prop :=
liftProcEnt (initStateProt m).
Definition ovReadyStateEnt (m : Mode) (t : Time) (l : Position) : Entity -> Prop :=
liftProcEnt (ovReadyStateProt m t l).
Definition switchCurrStateEnt : Entity -> Prop :=
liftProcEnt switchCurrStateProt.
Definition switchListenStateEnt : Entity -> Prop :=
liftProcEnt switchListenStateProt.
Definition tfsListenStateEnt := liftProcEnt tfsListenStateProt.
Definition ovAbortStateEnt := liftProcEnt ovAbortStateProt.
Definition tfsBcStateEnt := liftProcEnt tfsBcStateProt.
Definition switchBcStateEnt m := liftProcEnt (switchBcStateProt m).
Definition ovWaitStateEnt (m : Mode) (t x y : Time) : Entity -> Prop :=
liftProcEnt (ovWaitStateProt m t x y).
Definition tfsCurrStateEnt := liftProcEnt tfsCurrStateProt.
Definition tfsNextStateEnt m := liftProcEnt (tfsNextStateProt m).
Definition listeningStateEnt : Entity -> Prop :=
liftProcEnt listeningStateProt.
Definition currCompStateEnt (m : Mode) (r : Distance) : Entity -> Prop :=
liftProcEnt (currCompStateProt m r).
Definition pausedStateEnt := liftProcEnt pausedStateProt.
Definition abortOvlpStateEnt := liftProcEnt abortOvlpStateProt.
Definition badOvlpStateEnt := liftProcEnt badOvlpStateProt.
Definition nextEqStateEnt m m' := liftProcEnt (nextEqStateProt m m').
Definition currEqStateEnt m m'' := liftProcEnt (currEqStateProt m m'').
Definition gotMsgStateEnt m l := liftProcEnt (gotMsgStateProt m l).
Definition gotRangeStateEnt m r := liftProcEnt (gotRangeStateProt m r).
Definition currPincCheckStateEnt m m'' r := liftProcEnt (currPincCheckStateProt m m'' r).
Definition nextPincCheckStateEnt m m'' r := liftProcEnt (nextPincCheckStateProt m m'' r).
Definition rangeBadStateEnt m := liftProcEnt (rangeBadStateProt m).
Definition broadcastStateEnt := liftProcEnt broadcastStateProt.
Definition overlapStateEnt : Entity -> Prop :=
liftProcEnt overlapStateProt.
Definition nextSinceStateEnt : Entity -> Prop :=
liftProcEnt nextSinceStateProt.
Definition tfsStateEnt : Entity -> Prop :=
liftProcEnt tfsStateProt.
Definition switchStateEnt : Entity -> Prop :=
liftProcEnt switchStateProt.
Definition listenerStateEnt : Entity -> Prop :=
liftProcEnt listenerStateProt.
Inductive msgBadPathEnt : Entity -> Prop :=
| mbpMsg p l h k m'' m l' : gotMsgStateProt m'' l' p -> currModeMState k = m ->
possiblyIncompatible m m'' (dist2d l l' -nn- speedMax *nn* msgLatency)
-> msgBadPathEnt ([| p, l, h, k|])
| mbpRng p l h k m'' m r : gotRangeStateProt m'' r p -> currModeMState k = m ->
possiblyIncompatible m m'' r -> msgBadPathEnt ([|p, l, h, k|])
| mbpBad p l h k : badOvlpStateProt p -> msgBadPathEnt ([|p, l, h, k|]).
Inductive notifBadPathEnt : Entity -> Prop :=
| nbpRng p l h k m : rangeBadStateProt m p -> currModeMState k = m ->
notifBadPathEnt ([|p, l, h, k|])
| nbpBad p l h k : badOvlpStateProt p -> notifBadPathEnt ([|p, l, h, k|]).
Inductive msgAbortPathEnt : Entity -> Prop :=
| mapMsg p l h k m'' m m' l' :
let r' := dist2d l l' -nn- speedMax *nn* msgLatency in
gotMsgStateProt m'' l' p -> currModeMState k = m ->
~possiblyIncompatible m m'' r' ->
nextModeMState k = Some m' ->
possiblyIncompatible m' m'' r' ->
msgAbortPathEnt ([|p, l, h, k|])
| mapGrng p l h k m'' m m' r : gotRangeStateProt m'' r p -> currModeMState k = m ->
~possiblyIncompatible m m'' r -> nextModeMState k = Some m' ->
possiblyIncompatible m' m'' r -> msgAbortPathEnt ([|p, l, h, k|])
| mapCuco p l h k m'' m' r : currCompStateProt m'' r p -> nextModeMState k = Some m' ->
possiblyIncompatible m' m'' r -> msgAbortPathEnt ([|p, l, h, k|])
| mapAbort p l h k : abortOvlpStateProt p -> msgAbortPathEnt ([|p, l, h, k|]).
Inductive notifAbortPathEnt : Entity -> Prop :=
| napRng p l h k m m' : rangeBadStateProt m' p -> currModeMState k = m -> m <> m' ->
nextModeMState k = Some m' -> notifAbortPathEnt ([|p, l, h, k|])
| napCuok p l h k m' : currOKStateProt m' p -> nextModeMState k = Some m' ->
notifAbortPathEnt ([|p, l, h, k|])
| napAbort p l h k : abortOvlpStateProt p -> notifAbortPathEnt ([|p, l, h, k|]).
incomingEnt v e means v is in the incoming list of the interface of e.
Inductive incomingEnt (v : list BaseType) : Entity -> Prop :=
| incent P l h K : incomingInter v h -> incomingEnt v ([|P, l, h, K|]).
Parameter reachableEnt : Entity -> Prop.
Parameter nextModeEnt : Mode -> Entity -> Prop.
Parameter inPosEnt : Position -> Entity -> Prop.
| incent P l h K : incomingInter v h -> incomingEnt v ([|P, l, h, K|]).
Parameter reachableEnt : Entity -> Prop.
Parameter nextModeEnt : Mode -> Entity -> Prop.
Parameter inPosEnt : Position -> Entity -> Prop.
An entity is initial if its consitutent process is
initial and its mode state is a stable, failSafe mode.
Inductive initialEnt : Entity -> Prop :=
initEnt p l h m : initialProc p -> failSafe m ->
initialEnt ([|p, l, h, m|]).
initEnt p l h m : initialProc p -> failSafe m ->
initialEnt ([|p, l, h, m|]).
This page has been generated by coqdoc