Library InterfaceLanguage
This file was written by Colm Bhandal, PhD student, Foundations and Methods group,
School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
Require Import ComhCoq.Extras.LibTactics.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
A timed element is a vector of base values, along with a timestamp.
Record TimedEl : Type := mkTimedEl
{
msg : list BaseType;
stamp : Time
}.
Notation "<( m , t )>" := (mkTimedEl m t) (at level 40).
{
msg : list BaseType;
stamp : Time
}.
Notation "<( m , t )>" := (mkTimedEl m t) (at level 40).
Equality is decidable on timed elements.
Lemma eqDecTimedEl : eqDec TimedEl.
A timed list is a list of timed elements.
Definition TimedList : Type := list TimedEl.
Inductive ActTimedList :=
| atlDel :> Delay -> ActTimedList
| atlIn : list BaseType -> ActTimedList
| atlOut : list BaseType -> ActTimedList.
Notation "v ?? " := (atlIn v) (at level 30).
Notation "v !! " := (atlOut v) (at level 30).
Reserved Notation "l -tl- a -tl> l'" (at level 75).
Inductive ActTimedList :=
| atlDel :> Delay -> ActTimedList
| atlIn : list BaseType -> ActTimedList
| atlOut : list BaseType -> ActTimedList.
Notation "v ?? " := (atlIn v) (at level 30).
Notation "v !! " := (atlOut v) (at level 30).
Reserved Notation "l -tl- a -tl> l'" (at level 75).
The operational semantics for timed lists. Note that the law "buff" will have
to be defined separately for each of the sub-type lists individually,
because it is parametrised on a time T.
Inductive stepTimedList : TimedList -> ActTimedList -> TimedList -> Prop :=
If the head of the list has timed out (zero time) then it can be output.
| stepTlFwdHd : forall (v : list BaseType) (l : TimedList),
<(v, zeroTime)> :: l -tl- v!! -tl> l
<(v, zeroTime)> :: l -tl- v!! -tl> l
If the tail can evolve by outputting an element, then the whole list can evolve as
such.
| stepTlFwd : forall (l l' : TimedList) (v1 : list BaseType) (e : TimedEl),
l -tl- v1!! -tl> l' -> e :: l -tl- v1!! -tl> e :: l'
l -tl- v1!! -tl> l' -> e :: l -tl- v1!! -tl> e :: l'
The empty list can delay by any amount and stay as the empty list.
| stepTlDelEmp : forall d : Delay, [] -tl- d -tl> []
If the tail can delay by d, and the timestamp on the head is t + d, then the
whole list evolves by the tail delaying and the head element timestap reducing to t.
Note that this differs slightly from the formulation on paper, which asserts that the
timestamp of the head element is t >= d, and then the resulting timestamp is t - d.
The reason for this alternative formulation is to avoid subtraction of delays/times.
| stepTlDel : forall (l l' : TimedList) (d : Delay) (v : list BaseType) (t t' : Time),
l -tl- d -tl> l' -> t = t' +dt+ d -> <(v, t)> :: l -tl- d -tl>
<(v, t')> :: l'
where "l -tl- a -tl> l'" := (stepTimedList l a l').
l -tl- d -tl> l' -> t = t' +dt+ d -> <(v, t)> :: l -tl- d -tl>
<(v, t')> :: l'
where "l -tl- a -tl> l'" := (stepTimedList l a l').
The delay action preserves the size of a timed list.
Lemma delPresSizeTL : forall (l l' : TimedList) (d : Delay),
l -tl- d -tl> l' -> length l = length l'.
l -tl- d -tl> l' -> length l = length l'.
If ☐ delays to l', then l' = ☐
Lemma empLeftDelTL : forall (l' : TimedList) (d : Delay),
[] -tl- d -tl> l' -> l' = [].
[] -tl- d -tl> l' -> l' = [].
If l delays to ☐, then l = ☐
Lemma empRightDelTL : forall (l : TimedList) (d : Delay),
l -tl- d -tl> [] -> l = [].
l -tl- d -tl> [] -> l = [].
If a timed list l can delay by d to l' which in turn can delay by d' to l'',
then l can delay by d+d' to l''.
Lemma delAddTL : forall (l l' l'' : TimedList) (d d' : Delay),
l -tl- d -tl> l' -> l' -tl- d' -tl> l'' ->
l -tl- d +d+ d' -tl> l''.
Lemma timedList_timeout_enabled v l :
<( v, zeroTime )> _: l -> exists l', l -tl- v !! -tl> l'.
Lemma timedList_del_le l l' d v t q :
l -tl- atlDel d -tl> l' -> <( v, t )> _: l ->
<( v, minusTime t d q )> _: l'.
Reserved Notation "l -il- a -il> l'" (at level 75).
Reserved Notation "l -ol- a -ol> l'" (at level 75).
Reserved Notation "l -nl- a -nl> l'" (at level 75).
l -tl- d -tl> l' -> l' -tl- d' -tl> l'' ->
l -tl- d +d+ d' -tl> l''.
Lemma timedList_timeout_enabled v l :
<( v, zeroTime )> _: l -> exists l', l -tl- v !! -tl> l'.
Lemma timedList_del_le l l' d v t q :
l -tl- atlDel d -tl> l' -> <( v, t )> _: l ->
<( v, minusTime t d q )> _: l'.
Reserved Notation "l -il- a -il> l'" (at level 75).
Reserved Notation "l -ol- a -ol> l'" (at level 75).
Reserved Notation "l -nl- a -nl> l'" (at level 75).
Syntactially, an input list is essentially a timed list.
Record InputList : Type := mkInputList {inList : TimedList}.
Syntactially, an input list is essentially a timed list.
Record OutputList : Type := mkOutputList {outList : TimedList}.
Syntactially, an input list is essentially a timed list.
Record NotifList : Type := mkNotifList {notifList : TimedList}.
Semantics for the input list.
Inductive stepInputList : InputList -> ActTimedList -> InputList -> Prop :=
Buffer a message and stamp it with zero time.
| stepIlBuff : forall (l : TimedList) (v : list BaseType),
mkInputList l -il- v ?? -il> mkInputList (<(v, zeroTime)> :: l)
mkInputList l -il- v ?? -il> mkInputList (<(v, zeroTime)> :: l)
Delay causes all the messages in the list to be lost. In other words,
any list can delay and become the empty list.
| stepIlDel : forall (l : InputList) (d : Delay),
l -il- d -il> mkInputList []
l -il- d -il> mkInputList []
Lift the timed list semantics to these specialised semantics.
| stepIlLift : forall (l l' : TimedList) (a : ActTimedList),
l -tl- a -tl> l' -> mkInputList l -il- a -il> mkInputList l'
where "l -il- a -il> l'" := (stepInputList l a l').
Open Scope nat_scope.
l -tl- a -tl> l' -> mkInputList l -il- a -il> mkInputList l'
where "l -il- a -il> l'" := (stepInputList l a l').
Open Scope nat_scope.
The size of a list is non-increasing for an input list.
Lemma delNonIncSizeIL : forall (l l' : InputList) (d : Delay),
l -il- d -il> l' -> length (inList l') <= length (inList l).
l -il- d -il> l' -> length (inList l') <= length (inList l).
If an input list l can delay by d to l' which in turn can delay by d' to l'',
then l can delay by d+d' to l''.
Lemma delAddInput : forall (l l' l'' : InputList) (d d' : Delay),
l -il- d -il> l' -> l' -il- d' -il> l'' ->
l -il- d +d+ d' -il> l''.
l -il- d -il> l' -> l' -il- d' -il> l'' ->
l -il- d +d+ d' -il> l''.
An input list l is action enabled for the action a iff
there is some derivative list l' such that l transitions to l' via a.
Definition actEnabledInList (l : InputList) (a : ActTimedList) : Prop :=
exists l', l -il- a -il> l'.
exists l', l -il- a -il> l'.
An input list can always input a message.
Lemma inListInEnabled : forall (l : InputList) (v : list BaseType),
actEnabledInList l (v??).
Inductive stepOutputList : OutputList -> ActTimedList -> OutputList -> Prop :=
actEnabledInList l (v??).
Inductive stepOutputList : OutputList -> ActTimedList -> OutputList -> Prop :=
Buffer a message and stamp it with a timestamp of msgLatency.
| stepOlBuff : forall (l : TimedList) (v : list BaseType),
mkOutputList l -ol- v?? -ol> mkOutputList (<(v, msgLatency)> :: l)
mkOutputList l -ol- v?? -ol> mkOutputList (<(v, msgLatency)> :: l)
Lift the timed list semantics to these specialised semantics.
| stepOlLift : forall (l l' : TimedList) (a : ActTimedList),
l -tl- a -tl> l' -> mkOutputList l -ol- a -ol> mkOutputList l'
where "l -ol- a -ol> l'" := (stepOutputList l a l').
Lemma delAddOutput : forall (l l' l'' : OutputList) (d d' : Delay),
l -ol- d -ol> l' -> l' -ol- d' -ol> l'' ->
l -ol- d +d+ d' -ol> l''.
Inductive stepNotifList : NotifList -> ActTimedList -> NotifList -> Prop :=
l -tl- a -tl> l' -> mkOutputList l -ol- a -ol> mkOutputList l'
where "l -ol- a -ol> l'" := (stepOutputList l a l').
Lemma delAddOutput : forall (l l' l'' : OutputList) (d d' : Delay),
l -ol- d -ol> l' -> l' -ol- d' -ol> l'' ->
l -ol- d +d+ d' -ol> l''.
Inductive stepNotifList : NotifList -> ActTimedList -> NotifList -> Prop :=
Buffer a message and stamp it with a timestamp of adaptNotif.
| stepNlBuff : forall (l : TimedList) (v : list BaseType),
mkNotifList l -nl- v?? -nl> mkNotifList (<(v, adaptNotif)> :: l)
mkNotifList l -nl- v?? -nl> mkNotifList (<(v, adaptNotif)> :: l)
If the tail can delay to some l', and the head has timed out, then the whole
list can delay to l', essentially dropping the head.
| stepNlDrop : forall (l : TimedList) (l' : NotifList)
(d : Delay) (v : list BaseType), mkNotifList l -nl- d -nl> l' ->
mkNotifList (<(v, zeroTime)> :: l) -nl- d -nl> l'
| stepNlDelAdd : forall (l l' l'' : NotifList) (d d' : Delay),
l -nl- d -nl> l' -> l' -nl- d' -nl> l'' ->
l -nl- (d +d+ d') -nl> l''
(d : Delay) (v : list BaseType), mkNotifList l -nl- d -nl> l' ->
mkNotifList (<(v, zeroTime)> :: l) -nl- d -nl> l'
| stepNlDelAdd : forall (l l' l'' : NotifList) (d d' : Delay),
l -nl- d -nl> l' -> l' -nl- d' -nl> l'' ->
l -nl- (d +d+ d') -nl> l''
Lift the timed list semantics to these specialised semantics.
| stepNlLift : forall (l l' : TimedList) (a : ActTimedList),
l -tl- a -tl> l' -> mkNotifList l -nl- a -nl> mkNotifList l'
where "l -nl- a -nl> l'" := (stepNotifList l a l').
Open Scope R_scope.
Lemma notifList_del_le ln ln' d v t q :
ln -nl- atlDel d -nl> ln' -> <( v, t )> _: notifList ln ->
<( v, minusTime t d q )> _: notifList ln'.
Lemma timeSplit_inputList l l'' (d d' d'' : Delay) :
l -il- d'' -il> l'' -> d'' = d +d+ d' ->
exists l', l -il- d -il> l' /\ l' -il- d' -il> l''.
Lemma timeSplit_outputList l l'' (d d' d'' : Delay) :
l -ol- d'' -ol> l'' -> d'' = d +d+ d' ->
exists l', l -ol- d -ol> l' /\ l' -ol- d' -ol> l''.
Lemma timeSplit_notifList l l'' (d d' d'' : Delay) :
l -nl- d'' -nl> l'' -> d'' = d +d+ d' ->
exists l', l -nl- d -nl> l' /\ l' -nl- d' -nl> l''.
Record Interface : Type := mkInterface
{
li : InputList;
lo : OutputList;
ln : NotifList
}.
l -tl- a -tl> l' -> mkNotifList l -nl- a -nl> mkNotifList l'
where "l -nl- a -nl> l'" := (stepNotifList l a l').
Open Scope R_scope.
Lemma notifList_del_le ln ln' d v t q :
ln -nl- atlDel d -nl> ln' -> <( v, t )> _: notifList ln ->
<( v, minusTime t d q )> _: notifList ln'.
Lemma timeSplit_inputList l l'' (d d' d'' : Delay) :
l -il- d'' -il> l'' -> d'' = d +d+ d' ->
exists l', l -il- d -il> l' /\ l' -il- d' -il> l''.
Lemma timeSplit_outputList l l'' (d d' d'' : Delay) :
l -ol- d'' -ol> l'' -> d'' = d +d+ d' ->
exists l', l -ol- d -ol> l' /\ l' -ol- d' -ol> l''.
Lemma timeSplit_notifList l l'' (d d' d'' : Delay) :
l -nl- d'' -nl> l'' -> d'' = d +d+ d' ->
exists l', l -nl- d -nl> l' /\ l' -nl- d' -nl> l''.
Record Interface : Type := mkInterface
{
li : InputList;
lo : OutputList;
ln : NotifList
}.
Equality is decidable on interfaces.
Lemma eqDecInterface : eqDec Interface.
Actions for the interface semantics. We have delay, input of a list of base values
on a channel, output of the same, and finally output of a list of base values on a
channel augmented with coverage information.
Inductive ActInter :=
| aiDel :> Delay -> ActInter
| aiIn : Channel -> list BaseType -> ActInter
| aiOut : Channel -> list BaseType -> ActInter
| aiDel :> Delay -> ActInter
| aiIn : Channel -> list BaseType -> ActInter
| aiOut : Channel -> list BaseType -> ActInter
The final parameter is the coverage.
| aiOutCov : Channel -> list BaseType -> Distance -> ActInter.
Notation "c !I!" := (aiOut c []) (at level 30).
Notation "c {? v" := (aiIn c v) (at level 30).
Notation "c {! v" := (aiOut c v) (at level 30).
Notation "c _! v !_ r" := (aiOutCov c v r) (at level 30).
Reserved Notation "i -i- a -i> i'" (at level 75).
Notation "c !I!" := (aiOut c []) (at level 30).
Notation "c {? v" := (aiIn c v) (at level 30).
Notation "c {! v" := (aiOut c v) (at level 30).
Notation "c _! v !_ r" := (aiOutCov c v r) (at level 30).
Reserved Notation "i -i- a -i> i'" (at level 75).
The semantics for the interface.
Inductive stepInter : Interface -> ActInter -> Interface -> Prop :=
| stepIntDel : forall (l1 l1': InputList) (l2 l2': OutputList)
(l3 l3' : NotifList) (d : Delay), l1 -il- d -il> l1' ->
l2 -ol- d -ol> l2' -> l3 -nl- d -nl> l3' ->
(mkInterface l1 l2 l3) -i- d -i> (mkInterface l1' l2' l3')
| stepIntBuffIn : forall (l1 l1': InputList) (l2 : OutputList)
(l3 : NotifList) (v : list BaseType), l1 -il- v?? -il> l1' ->
(mkInterface l1 l2 l3) -i- chanIOEnv {? v -i> (mkInterface l1' l2 l3)
| stepIntFwdIn : forall (l1 l1': InputList) (l2 : OutputList)
(l3 : NotifList) (v : list BaseType), l1 -il- v!! -il> l1' ->
(mkInterface l1 l2 l3) -i- chanInProc {! v -i> (mkInterface l1' l2 l3)
| stepIntBuffOut : forall (l1 : InputList) (l2 l2' : OutputList)
(l3 : NotifList) (v : list BaseType), l2 -ol- v?? -ol> l2' ->
(mkInterface l1 l2 l3) -i- chanOutProc {? v -i> (mkInterface l1 l2' l3)
| stepIntFwdOut : forall (l1 : InputList) (l2 l2' : OutputList)
(l3 l3' : NotifList) (v : list BaseType) (r : Distance),
l2 -ol- v!! -ol> l2' -> l3 -nl- ((baseDistance r) :: v) ?? -nl> l3' ->
(mkInterface l1 l2 l3) -i- chanIOEnv _! v !_ r -i> (mkInterface l1 l2' l3')
| stepIntFwdNotif : forall (l1 : InputList) (l2 : OutputList)
(l3 l3' : NotifList) (v : list BaseType), l3 -nl- v!! -nl> l3' ->
(mkInterface l1 l2 l3) -i- chanAN {! v -i> (mkInterface l1 l2 l3')
where "i -i- a -i> i'" := (stepInter i a i').
| stepIntDel : forall (l1 l1': InputList) (l2 l2': OutputList)
(l3 l3' : NotifList) (d : Delay), l1 -il- d -il> l1' ->
l2 -ol- d -ol> l2' -> l3 -nl- d -nl> l3' ->
(mkInterface l1 l2 l3) -i- d -i> (mkInterface l1' l2' l3')
| stepIntBuffIn : forall (l1 l1': InputList) (l2 : OutputList)
(l3 : NotifList) (v : list BaseType), l1 -il- v?? -il> l1' ->
(mkInterface l1 l2 l3) -i- chanIOEnv {? v -i> (mkInterface l1' l2 l3)
| stepIntFwdIn : forall (l1 l1': InputList) (l2 : OutputList)
(l3 : NotifList) (v : list BaseType), l1 -il- v!! -il> l1' ->
(mkInterface l1 l2 l3) -i- chanInProc {! v -i> (mkInterface l1' l2 l3)
| stepIntBuffOut : forall (l1 : InputList) (l2 l2' : OutputList)
(l3 : NotifList) (v : list BaseType), l2 -ol- v?? -ol> l2' ->
(mkInterface l1 l2 l3) -i- chanOutProc {? v -i> (mkInterface l1 l2' l3)
| stepIntFwdOut : forall (l1 : InputList) (l2 l2' : OutputList)
(l3 l3' : NotifList) (v : list BaseType) (r : Distance),
l2 -ol- v!! -ol> l2' -> l3 -nl- ((baseDistance r) :: v) ?? -nl> l3' ->
(mkInterface l1 l2 l3) -i- chanIOEnv _! v !_ r -i> (mkInterface l1 l2' l3')
| stepIntFwdNotif : forall (l1 : InputList) (l2 : OutputList)
(l3 l3' : NotifList) (v : list BaseType), l3 -nl- v!! -nl> l3' ->
(mkInterface l1 l2 l3) -i- chanAN {! v -i> (mkInterface l1 l2 l3')
where "i -i- a -i> i'" := (stepInter i a i').
An interface i is action enabled for the action a iff
there is some derivative interface i' such that i transitions to i' via a.
Definition actEnabledInter (i : Interface) (a : ActInter) : Prop :=
exists i', i -i- a -i> i'.
exists i', i -i- a -i> i'.
incomingInter v i means v is in the incoming list of the interface i.
Inductive incomingInter (v : list BaseType) : Interface -> Prop :=
iciWitness (li : InputList) (lo : OutputList) (ln : NotifList) :
<( v, zeroTime )> _: inList li ->
incomingInter v (mkInterface li lo ln).
iciWitness (li : InputList) (lo : OutputList) (ln : NotifList) :
<( v, zeroTime )> _: inList li ->
incomingInter v (mkInterface li lo ln).
An interface is enabled on a discrete action if it can perform a corresponding
action. The actions in question can be input or output, but there will be no case
for tau because interfaces can't do a tau action.
Inductive discActEnabledInter : DiscAct -> Interface -> Prop :=
| daeiIn : forall (c : Channel) (v : list BaseType) (i i' : Interface),
i -i- c {? v -i> i' -> discActEnabledInter (c ;? v) i
| daeiOut : forall (c : Channel) (v : list BaseType) (i i' : Interface),
i -i- c {! v -i> i' -> discActEnabledInter (c ;! v) i.
| daeiIn : forall (c : Channel) (v : list BaseType) (i i' : Interface),
i -i- c {? v -i> i' -> discActEnabledInter (c ;? v) i
| daeiOut : forall (c : Channel) (v : list BaseType) (i i' : Interface),
i -i- c {! v -i> i' -> discActEnabledInter (c ;! v) i.
An interface is always enabled on an input on the channel chanIOEnv.
Theorem interfaceInEnabled : forall (i : Interface) (v : list BaseType),
actEnabledInter i (chanIOEnv {? v).
Lemma delAddInter : forall (i i' i'' : Interface) (d d' : Delay),
i -i- d -i> i' -> i' -i- d' -i> i'' ->
i -i- d +d+ d' -i> i''.
Conjecture outList_received_in : forall (l l' : OutputList) (v : list BaseType),
l -ol- v ?? -ol> l' -> <(v, msgLatency)> _: outList l'.
Conjecture inList_received_in : forall (l l' : InputList) (v : list BaseType),
l -il- v ?? -il> l' -> <(v, msgLatency)> _: inList l'.
Conjecture notifList_received_in : forall (l l' : NotifList) (v : list BaseType),
l -nl- v ?? -nl> l' -> <(v, msgLatency)> _: notifList l'.
Lemma inList_pres_input v l l' a :
<( v, zeroTime )> _: inList l -> l -il- a -il> l' ->
<( v, zeroTime )> _: inList l' \/ a = v !!.
Lemma inList_inter_pres_input v lix lox lnx lix' lox' lnx' a :
(forall d, a <> aiDel d) -> <(v, zeroTime )> _: inList lix ->
mkInterface lix lox lnx -i- a -i> mkInterface lix' lox' lnx' ->
<(v, zeroTime )> _: inList lix' \/
a = chanInProc{! v.
Lemma timeSplit_inter (h h'' : Interface) (d d' d'' : Delay) :
h -i- d'' -i> h'' -> d'' = d +d+ d' ->
exists h', h -i- d -i> h' /\ h' -i- d' -i> h''.
Lemma notif_timeout_enabled_aux v lnx :
<( v, zeroTime )> _: notifList lnx ->
exists lnx', lnx -nl- (v !!) -nl> lnx'.
Lemma notif_timeout_enabled v lix lox lnx :
<( v, zeroTime )> _: notifList lnx ->
discActEnabledInter (chanAN ;! v) (mkInterface lix lox lnx).
Lemma interface_outProc_in (h : Interface) (v : list BaseType) :
discActEnabledInter (chanOutProc ;? v) h.
Lemma inter_mStable_in_not h h' : h -i- chanMStable {! [] -i> h' -> False.
Lemma inter_abort_in_not h h' :
h -i- chanAbort {?[] -i> h' -> False.
Lemma outList_in_input_pres v u t lo lo' :
<( v, t )> _: outList lo -> outList lo -tl- u ?? -tl> outList lo' ->
<( v, t )> _: outList lo'.
Lemma outList_in_output_pres v u t lo lo' :
<( v, t )> _: outList lo -> outList lo -tl- u !! -tl> outList lo' ->
0 < t -> <( v, t )> _: outList lo'.
actEnabledInter i (chanIOEnv {? v).
Lemma delAddInter : forall (i i' i'' : Interface) (d d' : Delay),
i -i- d -i> i' -> i' -i- d' -i> i'' ->
i -i- d +d+ d' -i> i''.
Conjecture outList_received_in : forall (l l' : OutputList) (v : list BaseType),
l -ol- v ?? -ol> l' -> <(v, msgLatency)> _: outList l'.
Conjecture inList_received_in : forall (l l' : InputList) (v : list BaseType),
l -il- v ?? -il> l' -> <(v, msgLatency)> _: inList l'.
Conjecture notifList_received_in : forall (l l' : NotifList) (v : list BaseType),
l -nl- v ?? -nl> l' -> <(v, msgLatency)> _: notifList l'.
Lemma inList_pres_input v l l' a :
<( v, zeroTime )> _: inList l -> l -il- a -il> l' ->
<( v, zeroTime )> _: inList l' \/ a = v !!.
Lemma inList_inter_pres_input v lix lox lnx lix' lox' lnx' a :
(forall d, a <> aiDel d) -> <(v, zeroTime )> _: inList lix ->
mkInterface lix lox lnx -i- a -i> mkInterface lix' lox' lnx' ->
<(v, zeroTime )> _: inList lix' \/
a = chanInProc{! v.
Lemma timeSplit_inter (h h'' : Interface) (d d' d'' : Delay) :
h -i- d'' -i> h'' -> d'' = d +d+ d' ->
exists h', h -i- d -i> h' /\ h' -i- d' -i> h''.
Lemma notif_timeout_enabled_aux v lnx :
<( v, zeroTime )> _: notifList lnx ->
exists lnx', lnx -nl- (v !!) -nl> lnx'.
Lemma notif_timeout_enabled v lix lox lnx :
<( v, zeroTime )> _: notifList lnx ->
discActEnabledInter (chanAN ;! v) (mkInterface lix lox lnx).
Lemma interface_outProc_in (h : Interface) (v : list BaseType) :
discActEnabledInter (chanOutProc ;? v) h.
Lemma inter_mStable_in_not h h' : h -i- chanMStable {! [] -i> h' -> False.
Lemma inter_abort_in_not h h' :
h -i- chanAbort {?[] -i> h' -> False.
Lemma outList_in_input_pres v u t lo lo' :
<( v, t )> _: outList lo -> outList lo -tl- u ?? -tl> outList lo' ->
<( v, t )> _: outList lo'.
Lemma outList_in_output_pres v u t lo lo' :
<( v, t )> _: outList lo -> outList lo -tl- u !! -tl> outList lo' ->
0 < t -> <( v, t )> _: outList lo'.
This page has been generated by coqdoc