Library SoftwareLanguage
This file was written by Colm Bhandal, PhD student, Foundations and Methods group,
School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
The software component of the language is here defined.
Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import Decidable.
Require Import ListSet.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.ComhBasics.
Inductive Name := bcWaitN | sleepingN | bcReadyN | dormantN | initN |
ovWaitN | ovReadyN | switchBcN | switchCurrN | switchListenN | ovAbortN |
tfsStartN | tfsNextN | tfsCurrN | tfsBcN | tfsListenN | listeningN | checkRangeN |
rangeBadN | currEqN | badOvlpN | currOKN | nextEqN | abortOvlpN | gotMsgN |
gotRangeN | currPincCheckN | currCompN | nextPincCheckN | pausedN.
Equality is decidable on names.
Lemma eqDecName : eqDec Name.
Inductive ProcTerm : Type :=
| nilProc : ProcTerm
| outPrefix : Channel -> list Exp -> ProcTerm -> ProcTerm
| inPrefix : Channel -> list Var -> ProcTerm -> ProcTerm
| ifThen : BoolExp -> ProcTerm -> ProcTerm
| sum : ProcTerm -> ProcTerm -> ProcTerm
| parComp : ProcTerm -> ProcTerm -> ProcTerm
| app : Name -> list Exp -> ProcTerm
| del : Exp -> ProcTerm -> ProcTerm.
Inductive ProcTerm : Type :=
| nilProc : ProcTerm
| outPrefix : Channel -> list Exp -> ProcTerm -> ProcTerm
| inPrefix : Channel -> list Var -> ProcTerm -> ProcTerm
| ifThen : BoolExp -> ProcTerm -> ProcTerm
| sum : ProcTerm -> ProcTerm -> ProcTerm
| parComp : ProcTerm -> ProcTerm -> ProcTerm
| app : Name -> list Exp -> ProcTerm
| del : Exp -> ProcTerm -> ProcTerm.
Process language syntactic sugar.
Notation "c $< l >$ ? P" := (inPrefix c l P) (at level 41, right associativity).
Notation "c $< l >$ ! P" := (outPrefix c l P) (at level 41, right associativity).
Notation "c ? P" := (inPrefix c [] P) (at level 41, right associativity).
Notation "c ! P" := (outPrefix c [] P) (at level 41, right associativity).
Notation "B $> P" := (ifThen B P) (at level 41, right associativity).
Notation "P $+$ Q" := (sum P Q) (at level 50).
Notation "P $||$ Q" := (parComp P Q) (at level 45, right associativity).
Notation "h $( l )$" := (app h l) (at level 41, right associativity).
Notation " $< E >$ P " := (del E P) (at level 41, right associativity).
Notation "c $< l >$ ! P" := (outPrefix c l P) (at level 41, right associativity).
Notation "c ? P" := (inPrefix c [] P) (at level 41, right associativity).
Notation "c ! P" := (outPrefix c [] P) (at level 41, right associativity).
Notation "B $> P" := (ifThen B P) (at level 41, right associativity).
Notation "P $+$ Q" := (sum P Q) (at level 50).
Notation "P $||$ Q" := (parComp P Q) (at level 45, right associativity).
Notation "h $( l )$" := (app h l) (at level 41, right associativity).
Notation " $< E >$ P " := (del E P) (at level 41, right associativity).
A name applied to the empty list is a process term, which can just be
specified using the name.
Coercion liftNameProc (n : Name) : ProcTerm := n $([])$.
Equality is decidable on ProcTerms.
Lemma eqDecProcTerm : eqDec ProcTerm.
Definition vM := (var 0).
Definition vMF := (var 1).
Definition vM' := (var 2).
Definition vM'' := (var 3).
Definition vL := (var 4).
Definition vL' := (var 5).
Definition vT := (var 6).
Definition vT' := (var 7).
Definition vR := (var 8).
Definition vX := (var 9).
Definition vY := (var 10).
Definition bcWait (m x : Exp) := chanTrans? sleepingN $+$ $<x>$chanPos$<vL>$? bcReadyN $([m, eVar vL])$ $+$ chanWake$<vM>$? bcWaitN $([eVar vM, liftTimeExp zeroTime])$.
Definition sleeping := chanWake$<vM>$? bcWaitN $([eVar vM, liftTimeExp zeroTime])$ $+$ chanTrans? sleepingN.
Definition bcReady (m l : Exp) := chanOutProc$<[m, l]>$!bcWaitN $([m, (ePeriod m)])$.
Definition dormant := chanMNext$<vM'>$? initN $(eVar vM')$ $+$ chanAbort? dormantN $+$ chanBad? tfsStartN.
Definition init (m' : Exp) := chanMCurr$<vM>$? ovWaitN $([m', (eAdd (eWaitTime vM m') (ePeriod m')), liftTimeExp zeroTime])$.
Definition ovWait (m' t x y : Exp) := chanAbort? ovAbortN $+$ chanBad? tfsStartN $+$ $<y>$chanPos$<vL>$? ovReadyN $([m', t, eVar vL])$ $+$ $<x>$chanPause!switchBcN $(m')$.
Definition ovReady (m' t l : Exp) := chanOutProc$<[m', l]>$!ovWaitN $([m', (eSubtract t (ePeriod m')), (ePeriod m')])$.
Definition switchBc (m' : Exp) := chanWake$<m'>$!switchCurrN.
Definition switchCurr := chanMCurr!switchListenN.
Definition switchListen := chanUnpause!dormantN.
Definition tfsStart := chanMCurr$<vM>$? tfsNextN $(eVar vM)$.
Definition tfsNext (m : Exp) := chanMNext$<eFailSafeSucc m>$!tfsCurrN $+$ chanMStable!tfsNextN $(m)$.
Definition tfsCurr := chanAbort? tfsCurrN $+$ chanBad? tfsCurrN $+$ chanMCurr!tfsBcN.
Definition tfsBc := chanTrans!tfsListenN.
Definition tfsListen := chanAbort? tfsListenN $+$ chanBad? tfsListenN $+$ chanUnpause!dormantN.
Definition ovAbort := chanMStable!dormantN.
Definition listening := chanAN$<[vR, vM'']>$? checkRangeN $([eVar vM'', eVar vR])$ $+$ chanInProc$<[vM'', vL']>$? gotMsgN $([eVar vM'', eVar vL'])$ $+$ chanPause? pausedN $+$ chanUnpause? listeningN.
Definition vM := (var 0).
Definition vMF := (var 1).
Definition vM' := (var 2).
Definition vM'' := (var 3).
Definition vL := (var 4).
Definition vL' := (var 5).
Definition vT := (var 6).
Definition vT' := (var 7).
Definition vR := (var 8).
Definition vX := (var 9).
Definition vY := (var 10).
Definition bcWait (m x : Exp) := chanTrans? sleepingN $+$ $<x>$chanPos$<vL>$? bcReadyN $([m, eVar vL])$ $+$ chanWake$<vM>$? bcWaitN $([eVar vM, liftTimeExp zeroTime])$.
Definition sleeping := chanWake$<vM>$? bcWaitN $([eVar vM, liftTimeExp zeroTime])$ $+$ chanTrans? sleepingN.
Definition bcReady (m l : Exp) := chanOutProc$<[m, l]>$!bcWaitN $([m, (ePeriod m)])$.
Definition dormant := chanMNext$<vM'>$? initN $(eVar vM')$ $+$ chanAbort? dormantN $+$ chanBad? tfsStartN.
Definition init (m' : Exp) := chanMCurr$<vM>$? ovWaitN $([m', (eAdd (eWaitTime vM m') (ePeriod m')), liftTimeExp zeroTime])$.
Definition ovWait (m' t x y : Exp) := chanAbort? ovAbortN $+$ chanBad? tfsStartN $+$ $<y>$chanPos$<vL>$? ovReadyN $([m', t, eVar vL])$ $+$ $<x>$chanPause!switchBcN $(m')$.
Definition ovReady (m' t l : Exp) := chanOutProc$<[m', l]>$!ovWaitN $([m', (eSubtract t (ePeriod m')), (ePeriod m')])$.
Definition switchBc (m' : Exp) := chanWake$<m'>$!switchCurrN.
Definition switchCurr := chanMCurr!switchListenN.
Definition switchListen := chanUnpause!dormantN.
Definition tfsStart := chanMCurr$<vM>$? tfsNextN $(eVar vM)$.
Definition tfsNext (m : Exp) := chanMNext$<eFailSafeSucc m>$!tfsCurrN $+$ chanMStable!tfsNextN $(m)$.
Definition tfsCurr := chanAbort? tfsCurrN $+$ chanBad? tfsCurrN $+$ chanMCurr!tfsBcN.
Definition tfsBc := chanTrans!tfsListenN.
Definition tfsListen := chanAbort? tfsListenN $+$ chanBad? tfsListenN $+$ chanUnpause!dormantN.
Definition ovAbort := chanMStable!dormantN.
Definition listening := chanAN$<[vR, vM'']>$? checkRangeN $([eVar vM'', eVar vR])$ $+$ chanInProc$<[vM'', vL']>$? gotMsgN $([eVar vM'', eVar vL'])$ $+$ chanPause? pausedN $+$ chanUnpause? listeningN.
States for handling notification
Definition checkRange (m'' r : Exp) := (bSufficient m'' r $> listeningN) $+$ !~(bSufficient (m'') (r)) $> rangeBadN $(m'')$.
Definition rangeBad (m'' : Exp) := chanMCurr$<vM>$? currEqN $([eVar vM, m''])$.
Definition currEq (m m'' : Exp) := (m =b= m'') $> badOvlpN $+$ !~(m =b= m'') $> currOKN $(m'')$.
Definition badOvlp := chanBad!listeningN.
Definition currOK (m'' : Exp) := chanMStable? listeningN $+$ chanMNext$<vM'>$? nextEqN $([eVar vM', m''])$.
Definition nextEq (m' m'' : Exp) := (m' =b= m'') $> abortOvlpN $+$ !~(m' =b= m'') $> listeningN.
Definition abortOvlp := chanAbort!listeningN.
States for handling messages
Definition gotMsg (m'' l' : Exp) := chanPos$<vL>$? gotRangeN $([m'', (|vL , l'| (-) speedMax (.) msgLatency)])$.
Definition gotRange (m'' r : Exp) := chanMCurr$<vM>$? currPincCheckN $([eVar vM, m'', r])$.
Definition currPincCheck (m m'' r : Exp) := !~bPossInc m m'' r $> currCompN $([m'', r])$ $+$ bPossInc m m'' r $> badOvlpN.
Definition currComp (m'' r : Exp) := chanMStable? listeningN $+$ chanMNext$<vM'>$? nextPincCheckN $([eVar vM', m'', r])$.
Definition nextPincCheck (m' m'' r : Exp) := !~bPossInc m' m'' r $> listeningN $+$ bPossInc m' m'' r $> abortOvlpN.
Definition paused := chanUnpause? listeningN.
Notation "( a , b )" := (pair a b).
Definition def (n : Name) : (list Var * ProcTerm) :=
match n with
| bcWaitN => ([vM, vX], bcWait (eVar vM) (eVar vX))
| sleepingN => ([], sleeping)
| bcReadyN => ([vM, vL ], bcReady (eVar vM) (eVar vL) )
| dormantN => ([], dormant)
| initN => ([vM'], init (eVar vM'))
| ovWaitN => ([vM', vT, vY], ovWait (eVar vM') (eVar vT) (eVar vT) (eVar vY))
| ovReadyN => ([vM', vT, vL], ovReady (eVar vM') (eVar vT) (eVar vL))
| switchBcN => ([vM'], switchBc (eVar vM'))
| switchCurrN => ([], switchCurr)
| switchListenN => ([], switchListen)
| ovAbortN => ([], ovAbort)
| tfsStartN => ([], tfsStart)
| tfsNextN => ([vM], tfsNext (eVar vM))
| tfsCurrN => ([], tfsCurr)
| tfsBcN => ([], tfsBc)
| tfsListenN => ([], tfsListen)
| listeningN => ([], listening)
| checkRangeN => ([vM'', vR], checkRange (eVar vM'') (eVar vR))
| rangeBadN => ([vM''], rangeBad (eVar vM''))
| currEqN => ([vM, vM''], currEq (eVar vM) (eVar vM''))
| badOvlpN => ([], badOvlp)
| currOKN => ([vM''], currOK (eVar vM''))
| nextEqN => ([vM', vM''], nextEq (eVar vM') (eVar vM''))
| abortOvlpN => ([], abortOvlp)
| gotMsgN => ([vM'', vL'], gotMsg (eVar vM'') (eVar vL'))
| gotRangeN => ([vM'', vR], gotRange (eVar vM'') (eVar vR))
| currPincCheckN => ([vM, vM'', vR], currPincCheck (eVar vM) (eVar vM'') (eVar vR))
| currCompN => ([vM'', vR], currComp (eVar vM'') (eVar vR))
| nextPincCheckN => ([vM', vM'', vR], nextPincCheck (eVar vM') (eVar vM'') (eVar vR))
| pausedN => ([], paused)
end.
The protocol process is the parallel composition of the three processes below.
Notice that we could have defined this process via the def relation. However,
the def relation is only necessary for recursive references, of which there are
none here i.e. procProtocol is not on the right hand side of any of the def
equations. Hence there is no need to use the def relation, which in any case would
have made for more cumbersome developments later on.
Definition procProtocol := sleeping $||$ dormant $||$ listening.
Fixpoint subProcTerm (s : Subst) (t : ProcTerm) : ProcTerm :=
match t with
| nilProc => nilProc
| outPrefix c l t' => outPrefix c (listSub s l) (subProcTerm s t')
| inPrefix c l t' => inPrefix c l (subProcTerm (resetSub s l) t')
| ifThen b t' => ifThen (subBoolExp s b) (subProcTerm s t')
| sum t1 t2 => sum (subProcTerm s t1) (subProcTerm s t2)
| parComp t1 t2 => parComp (subProcTerm s t1) (subProcTerm s t2)
| app n l => app n (listSub s l)
| del e t' => del (subExp s e) (subProcTerm s t')
end.
Inductive Act :=
| actDisc :> DiscAct -> Act
| actTime :> Delay -> Act.
Fixpoint subProcTerm (s : Subst) (t : ProcTerm) : ProcTerm :=
match t with
| nilProc => nilProc
| outPrefix c l t' => outPrefix c (listSub s l) (subProcTerm s t')
| inPrefix c l t' => inPrefix c l (subProcTerm (resetSub s l) t')
| ifThen b t' => ifThen (subBoolExp s b) (subProcTerm s t')
| sum t1 t2 => sum (subProcTerm s t1) (subProcTerm s t2)
| parComp t1 t2 => parComp (subProcTerm s t1) (subProcTerm s t2)
| app n l => app n (listSub s l)
| del e t' => del (subExp s e) (subProcTerm s t')
end.
Inductive Act :=
| actDisc :> DiscAct -> Act
| actTime :> Delay -> Act.
The duration of an action. A discrete action has duration 0,
while a delay has a duration equal to the amount of the delay.
Definition durationSoft (a : Act) : Time :=
match a with
| actDisc _ => zeroTime
| actTime d => d
end.
Inductive stepDiscProc : ProcTerm -> DiscAct -> ProcTerm -> Prop :=
| stepDpOut : forall (c : Channel) (l1 : list Exp) (l2 : list BaseType) (p : ProcTerm),
evalExpLists l1 l2 -> stepDiscProc (outPrefix c l1 p) (outAct c l2) p
match a with
| actDisc _ => zeroTime
| actTime d => d
end.
Inductive stepDiscProc : ProcTerm -> DiscAct -> ProcTerm -> Prop :=
| stepDpOut : forall (c : Channel) (l1 : list Exp) (l2 : list BaseType) (p : ProcTerm),
evalExpLists l1 l2 -> stepDiscProc (outPrefix c l1 p) (outAct c l2) p
If the list of base values l1 matches the list of variables l2 in length, then
it can be input across the channel in question, and the resulting term is the
guraded term with all occurences of variables in the list l2 replaced by their
base value counterparts in l1.
| stepDpIn : forall (c : Channel) (l1 : list BaseType) (l2 : list Var) (p : ProcTerm),
length l1 = length l2 -> stepDiscProc (inPrefix c l2 p) (inAct c l1)
(subProcTerm (listsToSub l2 (listBaselistExp l1)) p)
| stepDpThen : forall (b : BoolExp) (p p' : ProcTerm) (d : DiscAct),
stepDiscProc p d p' -> evalBoolExpFunTot b = true ->
stepDiscProc (ifThen b p) d p'
| stepDpChoiceL : forall (p1 p2 p' : ProcTerm) (d : DiscAct),
stepDiscProc p1 d p' -> stepDiscProc (sum p1 p2) d p'
| stepDpChoiceR : forall (p1 p2 p' : ProcTerm) (d : DiscAct),
stepDiscProc p2 d p' -> stepDiscProc (p1 $+$ p2) d p'
| stepDpParL : forall (p p' q : ProcTerm) (d : DiscAct),
stepDiscProc p d p' -> stepDiscProc (parComp p q) d (parComp p' q)
| stepDpParR : forall (q q' p : ProcTerm) (d : DiscAct),
stepDiscProc q d q' -> stepDiscProc (parComp p q) d (parComp p q')
| stepDpSyncLR : forall (p p' q q' : ProcTerm) (c : Channel) (l : list BaseType),
stepDiscProc p (outAct c l) p' -> stepDiscProc q (inAct c l) q' ->
stepDiscProc (parComp p q) tauAct (parComp p' q')
| stepDpSyncRL : forall (p p' q q' : ProcTerm) (c : Channel) (l : list BaseType),
stepDiscProc p (inAct c l) p' -> stepDiscProc q (outAct c l) q' ->
stepDiscProc (parComp p q) tauAct (parComp p' q')
| stepDpApp : forall (n : Name) (l1 : list Var) (l2 : list Exp) (p p' : ProcTerm) (d : DiscAct),
def n = pair l1 p -> stepDiscProc (subProcTerm (listsToSub l1 l2) p) d p' ->
stepDiscProc (app n l2) d p'
| stepDpTimeOut : forall (p p' : ProcTerm) (d : DiscAct) (e : Exp),
stepDiscProc p d p' -> evalExpFunTime e = Some zeroTime -> stepDiscProc (del e p) d p'.
Inductive sort : DiscAct -> Delay -> ProcTerm -> Prop :=
| sortOut : forall (c : Channel) (l1 : list Exp) (l2 : list BaseType)
(p : ProcTerm) (d : Delay),
evalExpLists l1 l2 -> sort (outAct c l2) d (outPrefix c l1 p)
| sortIn : forall (c : Channel) (l1 : list Var) (l2 : list BaseType)
(p : ProcTerm) (d : Delay), length l1 = length l2 ->
sort (inAct c l2) d (inPrefix c l1 p)
| sortThen : forall (p : ProcTerm) (b : BoolExp) (a : DiscAct) (d : Delay),
evalBoolExp b true -> sort a d p -> sort a d (ifThen b p)
| sortSumL : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p1 -> sort a d (sum p1 p2)
| sortSumR : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p2 -> sort a d (sum p1 p2)
| sortParCompL : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p1 -> sort a d (parComp p1 p2)
| sortParCompR : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p2 -> sort a d (parComp p1 p2)
| sortApp : forall (p : ProcTerm) (a : DiscAct) (d : Delay)
(n : Name) (l1 : list Var) (l2 : list Exp),
def n = pair l1 p -> sort a d (subProcTerm (listsToSub l1 l2) p) -> sort a d (app n l2)
| sortDel : forall (e : Exp) (t : Time) (d : Delay) (p : ProcTerm) (a : DiscAct),
evalExpFunTime e = Some t -> sort a d p -> sort a (addDelayTime t d) (del e p).
Inductive discActEnabled (p : ProcTerm) (a : DiscAct) : Prop :=
dae : forall p' : ProcTerm, stepDiscProc p a p' -> discActEnabled p a.
Open Scope R_scope.
Inductive stepTimedProc : ProcTerm -> Delay -> ProcTerm -> Prop :=
| stepTpNil : forall d : Delay, stepTimedProc nilProc d nilProc
| stepTpOut : forall (d : Delay) (c : Channel) (l : list Exp) (p : ProcTerm),
stepTimedProc (outPrefix c l p) d (outPrefix c l p)
| stepTpIn : forall (d : Delay) (c : Channel) (l : list Var) (p : ProcTerm),
stepTimedProc (inPrefix c l p) d (inPrefix c l p)
| stepTpIfTrue : forall (p p' : ProcTerm) (d : Delay) (b : BoolExp),
stepTimedProc p d p' -> evalBoolExpFunTot b = true ->
stepTimedProc (ifThen b p) d p'
| stepTpIfFalse : forall (p : ProcTerm) (d : Delay) (b : BoolExp),
evalBoolExpFunTot b = false -> stepTimedProc (ifThen b p) d (ifThen b p)
| stepTpSum : forall (p1 p2 p1' p2' : ProcTerm) (d : Delay),
stepTimedProc p1 d p1' -> stepTimedProc p2 d p2' ->
stepTimedProc (sum p1 p2) d (sum p1' p2')
length l1 = length l2 -> stepDiscProc (inPrefix c l2 p) (inAct c l1)
(subProcTerm (listsToSub l2 (listBaselistExp l1)) p)
| stepDpThen : forall (b : BoolExp) (p p' : ProcTerm) (d : DiscAct),
stepDiscProc p d p' -> evalBoolExpFunTot b = true ->
stepDiscProc (ifThen b p) d p'
| stepDpChoiceL : forall (p1 p2 p' : ProcTerm) (d : DiscAct),
stepDiscProc p1 d p' -> stepDiscProc (sum p1 p2) d p'
| stepDpChoiceR : forall (p1 p2 p' : ProcTerm) (d : DiscAct),
stepDiscProc p2 d p' -> stepDiscProc (p1 $+$ p2) d p'
| stepDpParL : forall (p p' q : ProcTerm) (d : DiscAct),
stepDiscProc p d p' -> stepDiscProc (parComp p q) d (parComp p' q)
| stepDpParR : forall (q q' p : ProcTerm) (d : DiscAct),
stepDiscProc q d q' -> stepDiscProc (parComp p q) d (parComp p q')
| stepDpSyncLR : forall (p p' q q' : ProcTerm) (c : Channel) (l : list BaseType),
stepDiscProc p (outAct c l) p' -> stepDiscProc q (inAct c l) q' ->
stepDiscProc (parComp p q) tauAct (parComp p' q')
| stepDpSyncRL : forall (p p' q q' : ProcTerm) (c : Channel) (l : list BaseType),
stepDiscProc p (inAct c l) p' -> stepDiscProc q (outAct c l) q' ->
stepDiscProc (parComp p q) tauAct (parComp p' q')
| stepDpApp : forall (n : Name) (l1 : list Var) (l2 : list Exp) (p p' : ProcTerm) (d : DiscAct),
def n = pair l1 p -> stepDiscProc (subProcTerm (listsToSub l1 l2) p) d p' ->
stepDiscProc (app n l2) d p'
| stepDpTimeOut : forall (p p' : ProcTerm) (d : DiscAct) (e : Exp),
stepDiscProc p d p' -> evalExpFunTime e = Some zeroTime -> stepDiscProc (del e p) d p'.
Inductive sort : DiscAct -> Delay -> ProcTerm -> Prop :=
| sortOut : forall (c : Channel) (l1 : list Exp) (l2 : list BaseType)
(p : ProcTerm) (d : Delay),
evalExpLists l1 l2 -> sort (outAct c l2) d (outPrefix c l1 p)
| sortIn : forall (c : Channel) (l1 : list Var) (l2 : list BaseType)
(p : ProcTerm) (d : Delay), length l1 = length l2 ->
sort (inAct c l2) d (inPrefix c l1 p)
| sortThen : forall (p : ProcTerm) (b : BoolExp) (a : DiscAct) (d : Delay),
evalBoolExp b true -> sort a d p -> sort a d (ifThen b p)
| sortSumL : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p1 -> sort a d (sum p1 p2)
| sortSumR : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p2 -> sort a d (sum p1 p2)
| sortParCompL : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p1 -> sort a d (parComp p1 p2)
| sortParCompR : forall (p1 p2 : ProcTerm) (a : DiscAct) (d : Delay),
sort a d p2 -> sort a d (parComp p1 p2)
| sortApp : forall (p : ProcTerm) (a : DiscAct) (d : Delay)
(n : Name) (l1 : list Var) (l2 : list Exp),
def n = pair l1 p -> sort a d (subProcTerm (listsToSub l1 l2) p) -> sort a d (app n l2)
| sortDel : forall (e : Exp) (t : Time) (d : Delay) (p : ProcTerm) (a : DiscAct),
evalExpFunTime e = Some t -> sort a d p -> sort a (addDelayTime t d) (del e p).
Inductive discActEnabled (p : ProcTerm) (a : DiscAct) : Prop :=
dae : forall p' : ProcTerm, stepDiscProc p a p' -> discActEnabled p a.
Open Scope R_scope.
Inductive stepTimedProc : ProcTerm -> Delay -> ProcTerm -> Prop :=
| stepTpNil : forall d : Delay, stepTimedProc nilProc d nilProc
| stepTpOut : forall (d : Delay) (c : Channel) (l : list Exp) (p : ProcTerm),
stepTimedProc (outPrefix c l p) d (outPrefix c l p)
| stepTpIn : forall (d : Delay) (c : Channel) (l : list Var) (p : ProcTerm),
stepTimedProc (inPrefix c l p) d (inPrefix c l p)
| stepTpIfTrue : forall (p p' : ProcTerm) (d : Delay) (b : BoolExp),
stepTimedProc p d p' -> evalBoolExpFunTot b = true ->
stepTimedProc (ifThen b p) d p'
| stepTpIfFalse : forall (p : ProcTerm) (d : Delay) (b : BoolExp),
evalBoolExpFunTot b = false -> stepTimedProc (ifThen b p) d (ifThen b p)
| stepTpSum : forall (p1 p2 p1' p2' : ProcTerm) (d : Delay),
stepTimedProc p1 d p1' -> stepTimedProc p2 d p2' ->
stepTimedProc (sum p1 p2) d (sum p1' p2')
For this law we need to assert that for all actions a that can be done by
p within d units of time, the complementary action cannot be performed by q
within that time.
| stepTpPar : forall (p q p' q': ProcTerm) (d : Delay),
stepTimedProc p d p' -> stepTimedProc q d q' ->
(forall a : DiscAct, sort a d p -> ~sort (a^) d q) ->
stepTimedProc (parComp p q) d (parComp p' q')
| stepTpApp : forall (n : Name) (l1 : list Var) (l2 : list Exp) (p p' : ProcTerm) (d : Delay),
def n = pair l1 p -> stepTimedProc (subProcTerm (listsToSub l1 l2) p) d p' ->
stepTimedProc (app n l2) d p'
| stepTpDelAdd : forall (p p' : ProcTerm) (d : Delay) (e : Exp) (t : Time),
stepTimedProc p d p' -> evalExpFunTime e = Some t ->
stepTimedProc (del e p) (t +dt+ d) p'
| stepTpDelSub : forall (p : ProcTerm) (d : Delay) (e : Exp) (t : Time)
(H : d <= t), evalExpFunTime e = Some t ->
stepTimedProc (del e p) d (del (minusTime t d H) p)
stepTimedProc p d p' -> stepTimedProc q d q' ->
(forall a : DiscAct, sort a d p -> ~sort (a^) d q) ->
stepTimedProc (parComp p q) d (parComp p' q')
| stepTpApp : forall (n : Name) (l1 : list Var) (l2 : list Exp) (p p' : ProcTerm) (d : Delay),
def n = pair l1 p -> stepTimedProc (subProcTerm (listsToSub l1 l2) p) d p' ->
stepTimedProc (app n l2) d p'
| stepTpDelAdd : forall (p p' : ProcTerm) (d : Delay) (e : Exp) (t : Time),
stepTimedProc p d p' -> evalExpFunTime e = Some t ->
stepTimedProc (del e p) (t +dt+ d) p'
| stepTpDelSub : forall (p : ProcTerm) (d : Delay) (e : Exp) (t : Time)
(H : d <= t), evalExpFunTime e = Some t ->
stepTimedProc (del e p) d (del (minusTime t d H) p)
If the guard is ill formed, we just let the process idle.
| stepTpDelIll : forall (p : ProcTerm) (d : Delay) (e : Exp),
evalExpFunTime e = None -> stepTimedProc (del e p) d (del e p).
Inductive stepProc (t : ProcTerm) : Act -> ProcTerm -> Prop :=
| stepPDisc : forall (a : DiscAct) (t' : ProcTerm),
stepDiscProc t a t' -> stepProc t a t'
| stepPTimed : forall (d : Delay) (t' : ProcTerm),
stepTimedProc t d t' -> stepProc t d t'.
Notation "p1 -PA- a -PA> p2" := (stepDiscProc p1 a p2) (left associativity, at level 50).
Notation "p1 -PD- d -PD> p2" := (stepTimedProc p1 d p2) (left associativity, at level 50).
Notation "p1 -P- a -P> p2" := (stepProc p1 a p2) (left associativity, at level 50).
evalExpFunTime e = None -> stepTimedProc (del e p) d (del e p).
Inductive stepProc (t : ProcTerm) : Act -> ProcTerm -> Prop :=
| stepPDisc : forall (a : DiscAct) (t' : ProcTerm),
stepDiscProc t a t' -> stepProc t a t'
| stepPTimed : forall (d : Delay) (t' : ProcTerm),
stepTimedProc t d t' -> stepProc t d t'.
Notation "p1 -PA- a -PA> p2" := (stepDiscProc p1 a p2) (left associativity, at level 50).
Notation "p1 -PD- d -PD> p2" := (stepTimedProc p1 d p2) (left associativity, at level 50).
Notation "p1 -P- a -P> p2" := (stepProc p1 a p2) (left associativity, at level 50).
Two processes are related if either they are equal or if there is a transition
linking them.
Inductive stepProcRefl : ProcTerm -> ProcTerm -> Prop :=
| stprRefl : forall p : ProcTerm, stepProcRefl p p
| stprTrans : forall (p1 p2 : ProcTerm) (a : Act),
p1 -P- a -P> p2 -> stepProcRefl p1 p2.
Notation "p1 -P=> p2" := (stepProcRefl p1 p2) (at level 50).
Inductive timedActEnabled (p : ProcTerm) (d : Delay) : Prop :=
tae : forall p' : ProcTerm, stepTimedProc p d p' -> timedActEnabled p d.
| stprRefl : forall p : ProcTerm, stepProcRefl p p
| stprTrans : forall (p1 p2 : ProcTerm) (a : Act),
p1 -P- a -P> p2 -> stepProcRefl p1 p2.
Notation "p1 -P=> p2" := (stepProcRefl p1 p2) (at level 50).
Inductive timedActEnabled (p : ProcTerm) (d : Delay) : Prop :=
tae : forall p' : ProcTerm, stepTimedProc p d p' -> timedActEnabled p d.
If the left component of a sum is dae, then so is the entire sum.
Lemma daeSumL : forall (a : DiscAct) (p1 p2 : ProcTerm),
discActEnabled p1 a -> discActEnabled (p1 $+$ p2) a.
discActEnabled p1 a -> discActEnabled (p1 $+$ p2) a.
If the right component of a sum is dae, then so is the entire sum.
Lemma daeSumR : forall (a : DiscAct) (p1 p2 : ProcTerm),
discActEnabled p2 a -> discActEnabled (p1 $+$ p2) a.
discActEnabled p2 a -> discActEnabled (p1 $+$ p2) a.
If the left component of a sum is dae, then so is the entire sum.
Lemma daeParL : forall (a : DiscAct) (p1 p2 : ProcTerm),
discActEnabled p1 a -> discActEnabled (p1 $||$ p2) a.
discActEnabled p1 a -> discActEnabled (p1 $||$ p2) a.
If the right component of a sum is dae, then so is the entire sum.
Lemma daeParR : forall (a : DiscAct) (p1 p2 : ProcTerm),
discActEnabled p2 a -> discActEnabled (p1 $||$ p2) a.
discActEnabled p2 a -> discActEnabled (p1 $||$ p2) a.
If the body of a process definition is discActEnabled, then so is the application.
Lemma daeApp : forall (a : DiscAct) (x : list Var) (l : list Exp)
(h : Name) (p : ProcTerm), def h = (x, p) ->
discActEnabled (subProcTerm (listsToSub x l) p) a ->
discActEnabled (h $(l)$) a.
(h : Name) (p : ProcTerm), def h = (x, p) ->
discActEnabled (subProcTerm (listsToSub x l) p) a ->
discActEnabled (h $(l)$) a.
More cumbersome version but it fills in the variable list x and the process p automatically by
extracting them from the process definition of p.
Lemma daeAppAuto : forall (a : DiscAct) (l : list Exp) (h : Name),
discActEnabled (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) a ->
discActEnabled (h $(l)$) a.
discActEnabled (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) a ->
discActEnabled (h $(l)$) a.
If the then branch of an ifThen construct is discActEnabled for an action a,
and the guard evaluates to true, then the whole construct is dae by action a.
Theorem daeThenBranch : forall (a : DiscAct) (b : BoolExp) (p : ProcTerm),
evalBoolExp b true -> discActEnabled p a -> discActEnabled (b $> p) a.
evalBoolExp b true -> discActEnabled p a -> discActEnabled (b $> p) a.
If p is discActEnabled for an action a, and the guard times out,
then the whole construct is dae by action a.
Theorem daeTimeout : forall (a : DiscAct) (e : Exp) (p : ProcTerm),
evalExpFunTime e = Some zeroTime -> discActEnabled p a ->
discActEnabled ($<e>$ p) a.
evalExpFunTime e = Some zeroTime -> discActEnabled p a ->
discActEnabled ($<e>$ p) a.
All input prefixed terms are timed action enabled on all times.
Lemma taeIn : forall (d : Delay) (c : Channel) (l : list Var) (p : ProcTerm),
timedActEnabled (c $<l>$ ? p) d.
timedActEnabled (c $<l>$ ? p) d.
All output prefixed terms are timed action enabled on all times.
Lemma taeOut : forall (d : Delay) (c : Channel) (l : list Exp) (p : ProcTerm),
timedActEnabled (c $<l>$ ! p) d.
timedActEnabled (c $<l>$ ! p) d.
If both components of a sum are timedActEnabled, then so is the whole sum.
Lemma taeSum : forall (d : Delay) (p1 p2 : ProcTerm),
timedActEnabled p1 d -> timedActEnabled p2 d ->
timedActEnabled (p1 $+$ p2) d.
timedActEnabled p1 d -> timedActEnabled p2 d ->
timedActEnabled (p1 $+$ p2) d.
If the body of a process definition is timedActEnabled, then so is the application.
Lemma taeApp : forall (d : Delay) (x : list Var) (l : list Exp)
(h : Name) (p : ProcTerm), def h = (x, p) ->
timedActEnabled (subProcTerm (listsToSub x l) p) d ->
timedActEnabled (h $(l)$) d.
(h : Name) (p : ProcTerm), def h = (x, p) ->
timedActEnabled (subProcTerm (listsToSub x l) p) d ->
timedActEnabled (h $(l)$) d.
More cumbersome version but it fills in the variable list x and the process p automatically by
extracting them from the process definition of p.
Lemma taeAppAuto : forall (d : Delay) (l : list Exp) (h : Name),
timedActEnabled (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) d ->
timedActEnabled (h $(l)$) d.
timedActEnabled (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) d ->
timedActEnabled (h $(l)$) d.
If the then branch of an ifThen construct is timedActEnabled for an amount d,
then the whole construct can delay by this amount.
Theorem taeThenBranch : forall (d : Delay) (b : BoolExp) (p : ProcTerm),
timedActEnabled p d -> timedActEnabled (b $> p) d.
timedActEnabled p d -> timedActEnabled (b $> p) d.
If a process p is guarded by a value that is timed out, then all actions available
to p within d are available to the guarded p within that time d.
Lemma sortTimeOut : forall (e : Exp) (d : Delay) (p : ProcTerm) (a : DiscAct),
evalExpFunTime e = Some zeroTime -> sort a d p -> sort a d (del e p).
evalExpFunTime e = Some zeroTime -> sort a d p -> sort a d (del e p).
If a process is enabled on a discrete action a other than tau,
then forall delays d, a is in sort d for that process.
Lemma enabledInSort : forall (a : DiscAct) (d : Delay) (p : ProcTerm),
discActEnabled p a -> a <> tauAct -> sort a d p.
Lemma enabledInSort_in (c : Channel) (v : list BaseType) (d : Delay) (p : ProcTerm) :
discActEnabled p (c ;? v) -> sort (c ;? v) d p.
Lemma enabledInSort_out (c : Channel) (v : list BaseType) (d : Delay) (p : ProcTerm) :
discActEnabled p (c ;!v) -> sort (c ;! v) d p.
discActEnabled p a -> a <> tauAct -> sort a d p.
Lemma enabledInSort_in (c : Channel) (v : list BaseType) (d : Delay) (p : ProcTerm) :
discActEnabled p (c ;? v) -> sort (c ;? v) d p.
Lemma enabledInSort_out (c : Channel) (v : list BaseType) (d : Delay) (p : ProcTerm) :
discActEnabled p (c ;!v) -> sort (c ;! v) d p.
If we can prove sort a d p, then the action a is either an input of some vector
or the output of some vector.
Lemma sortInOrOut : forall (a : DiscAct) (d : Delay) (p : ProcTerm),
sort a d p -> exists v : list BaseType, exists c : Channel,
a = c ;? v \/ a = c ;! v.
sort a d p -> exists v : list BaseType, exists c : Channel,
a = c ;? v \/ a = c ;! v.
If an action is in sort d of p, then it is also in sort d + d' of p.
Theorem sortAddR : forall (a : DiscAct) (d d' : Delay) (p : ProcTerm),
sort a d p -> sort a (d +d+ d') p.
sort a d p -> sort a (d +d+ d') p.
If an action is in sort d of p, then it is also in sort d' + d of p.
Theorem sortAddL : forall (a : DiscAct) (d d' : Delay) (p : ProcTerm),
sort a d p -> sort a (d' +d+ d) p.
sort a d p -> sort a (d' +d+ d) p.
If an action is in sort d of p, then it is also in sort t + d of p.
Theorem sortAddTime : forall (a : DiscAct) (d : Delay) (t : Time) (p : ProcTerm),
sort a d p -> sort a (t +dt+ d) p.
sort a d p -> sort a (t +dt+ d) p.
If sort a d p and d' <= d, then sort a d' p.
Theorem sortLe : forall (a : DiscAct) (d d' : Delay) (p : ProcTerm),
sort a d p -> d <= d' -> sort a d' p.
Ltac evalExp_evalExpFunTime_step := match goal with
[V : ?e |_| baseTime ?t |- _] => apply evalExp_evalExpFunTime in V end.
sort a d p -> d <= d' -> sort a d' p.
Ltac evalExp_evalExpFunTime_step := match goal with
[V : ?e |_| baseTime ?t |- _] => apply evalExp_evalExpFunTime in V end.
If a is in sort d' of p' and p transitions to p' by d, then a is in the sort
d + d' of p.
Theorem sortDeriv : forall (a : DiscAct) (d d' : Delay) (p p' : ProcTerm),
sort a d' p' -> p -PD- d -PD> p' -> sort a (d +d+ d') p.
Lemma sort_minus_guard a d' d t H p :
sort a d' ($<eBase (baseTime (minusTime (nonneg (time t))
(pos (delay d)) H))>$ p) ->
sort a (d +d+ d') ($<eBase (baseTime t)>$ p).
Lemma evalExpFunTime_time t :
evalExpFunTime (eBase (baseTime t)) = Some t.
Lemma sort_guard_eval_eq a d e1 e2 p :
sort a d ($<e1>$ p) ->
evalExpFunTime e1 = evalExpFunTime e2 ->
sort a d ($<e2>$ p).
sort a d' p' -> p -PD- d -PD> p' -> sort a (d +d+ d') p.
Lemma sort_minus_guard a d' d t H p :
sort a d' ($<eBase (baseTime (minusTime (nonneg (time t))
(pos (delay d)) H))>$ p) ->
sort a (d +d+ d') ($<eBase (baseTime t)>$ p).
Lemma evalExpFunTime_time t :
evalExpFunTime (eBase (baseTime t)) = Some t.
Lemma sort_guard_eval_eq a d e1 e2 p :
sort a d ($<e1>$ p) ->
evalExpFunTime e1 = evalExpFunTime e2 ->
sort a d ($<e2>$ p).
A version of sortDeriv but as an equivalence rather than an implication.
Corollary sortDerivEquiv (a : DiscAct) (d d' : Delay) (p p' : ProcTerm) :
p -PD- d -PD> p' -> (sort a d' p' <-> sort a (d +d+ d') p).
Require Import ComhCoq.Extras.LibTactics.
Open Scope R_scope.
Theorem sort_complete d a p :
a <> tauAct /\ (discActEnabled p a \/
exists d' p', delay d' < delay d /\ p -PD- d' -PD> p' /\ discActEnabled p' a)
-> sort a d p.
p -PD- d -PD> p' -> (sort a d' p' <-> sort a (d +d+ d') p).
Require Import ComhCoq.Extras.LibTactics.
Open Scope R_scope.
Theorem sort_complete d a p :
a <> tauAct /\ (discActEnabled p a \/
exists d' p', delay d' < delay d /\ p -PD- d' -PD> p' /\ discActEnabled p' a)
-> sort a d p.
If a parallel construct delays to another process then the resulting process is
itself a parallel construct, whose terms either match the original or are related
to the original via a single transition.
Theorem parStructPres : forall (p1 p2 p' : ProcTerm) (a : Act),
p1 $||$ p2 -P- a -P> p' -> exists p1', exists p2',
p' = p1' $||$ p2' /\ p1 -P=> p1' /\ p2 -P=> p2'.
p1 $||$ p2 -P- a -P> p' -> exists p1', exists p2',
p' = p1' $||$ p2' /\ p1 -P=> p1' /\ p2 -P=> p2'.
Parallel structural preservation for the reflexive transition relation.
Theorem parStructPres2 : forall (p1 p2 p' : ProcTerm),
p1 $||$ p2 -P=> p' -> exists p1', exists p2',
p' = p1' $||$ p2' /\ p1 -P=> p1' /\ p2 -P=> p2'.
p1 $||$ p2 -P=> p' -> exists p1', exists p2',
p' = p1' $||$ p2' /\ p1 -P=> p1' /\ p2 -P=> p2'.
Whenever a process p can do a silent action, it cannot do a delay.
Theorem maximalProgressProc : forall (p : ProcTerm) (d : Delay),
discActEnabled p tauAct -> ~timedActEnabled p d.
discActEnabled p tauAct -> ~timedActEnabled p d.
In this case, we show a contradiction because the guard is assumed both
to be greater than the delay d and also to have timed out to 0.
Contradiction: Guard timed out but also ill formed.
If a process p can delay by d'' to become p'', and there is some d, d' such
that d'' = d + d', then there is some p' such that p can delay by d to get to p',
and p' can delay by d' to p''.
Theorem timeSplit : forall (p p'' : ProcTerm) (d d' d'' : Delay),
p -PD- d'' -PD> p'' -> d'' = d +d+ d' -> exists p',
p -PD- d -PD> p' /\ p' -PD- d' -PD> p''.
p -PD- d'' -PD> p'' -> d'' = d +d+ d' -> exists p',
p -PD- d -PD> p' /\ p' -PD- d' -PD> p''.
Case d0 <= t, then we can proceed via del sub.
Case t < d0, then we split the delay d into (d0 - t) and d', and we proceed
via the induction hypothesis and delAdd.
Now we do the case where the entire delay is less than the guard, in which case
we can proceed via delSub twice.
If p can delay by d, then p can delay by any d' strictly less than d.
Lemma delShortenStrict : forall (p : ProcTerm) (d d' : Delay),
timedActEnabled p d -> d' < d -> timedActEnabled p d'.
timedActEnabled p d -> d' < d -> timedActEnabled p d'.
If p can delay by d, then p can delay by any d' less than or equal d.
Lemma delShorten : forall (p : ProcTerm) (d d' : Delay),
timedActEnabled p d -> d' <= d -> timedActEnabled p d'.
Lemma taeSumEx (p1 p2 : ProcTerm) : (exists d, timedActEnabled p1 d) ->
(exists d, timedActEnabled p2 d) -> exists d, timedActEnabled (p1 $+$ p2) d.
timedActEnabled p d -> d' <= d -> timedActEnabled p d'.
Lemma taeSumEx (p1 p2 : ProcTerm) : (exists d, timedActEnabled p1 d) ->
(exists d, timedActEnabled p2 d) -> exists d, timedActEnabled (p1 $+$ p2) d.
If a process can delay to another process, then all discrete actions available
to the original process are available to the derivative.
Theorem persistence : forall (p p' : ProcTerm) (d : Delay) (a : DiscAct),
p -PD- d -PD> p' -> discActEnabled p a -> discActEnabled p' a.
p -PD- d -PD> p' -> discActEnabled p a -> discActEnabled p' a.
If a process p can delay by d'' to become p'', then there is some p', d, d' such
that d'' = d + d' and p can delay by d to get to p' and p' can delay by d' to p''.
Theorem timeSplitEx : forall (p p'' : ProcTerm) (d'' : Delay),
p -PD- d'' -PD> p'' -> exists p', exists d, exists d',
d'' = d +d+ d' /\ p -PD- d -PD> p' /\ p' -PD- d' -PD> p''.
p -PD- d'' -PD> p'' -> exists p', exists d, exists d',
d'' = d +d+ d' /\ p -PD- d -PD> p' /\ p' -PD- d' -PD> p''.
If a guarded process can delay by d, and the guard evaluates to some t, then
the guarded construct can delay by that same d.
Lemma taeDelWf : forall (d : Delay) (e : Exp) (t : Time) (p : ProcTerm),
evalExpFunTime e = Some t -> timedActEnabled p d -> timedActEnabled ($<e>$ p) d.
evalExpFunTime e = Some t -> timedActEnabled p d -> timedActEnabled ($<e>$ p) d.
If the guarded process in a delay guard construct is enabled on d, then so is
the entire construct. We prove this by a case analysis on the well formedness of the
evaluation of the guard expression. If it is well formed, then it evaluates to some t,
and so we can apply taeDelWf. Otherwise, we can simply apply the constructor for ill
formed delay guarded processes.
Theorem taeDel : forall (d : Delay) (e : Exp) (p : ProcTerm),
timedActEnabled p d -> timedActEnabled ($<e>$ p) d.
timedActEnabled p d -> timedActEnabled ($<e>$ p) d.
A single step of the full automation tactic for "eventually discrete guarded sum" terms.
Ltac taeAutoSing := match goal with
| [ |- timedActEnabled ?P _ ] =>
match P with
| _ $< _ >$ ? _ => apply taeIn
| _ $< _ >$ ! _ => apply taeOut
| _ $> _ => apply taeThenBranch
| _ $+$ _ => apply taeSum
| _ $(_)$ => apply taeAppAuto; simpl
| $< _ >$ _ => apply taeDel
end
end.
| [ |- timedActEnabled ?P _ ] =>
match P with
| _ $< _ >$ ? _ => apply taeIn
| _ $< _ >$ ! _ => apply taeOut
| _ $> _ => apply taeThenBranch
| _ $+$ _ => apply taeSum
| _ $(_)$ => apply taeAppAuto; simpl
| $< _ >$ _ => apply taeDel
end
end.
A tactic that will automatically prove that certain processes are time
action enabled. It does this by repeatedly drilling into the process until it finds
either input or output prefixed terms, at which point the delay proof is simple.
Obviously, this will only work for a certain class of processes that are, let's say
"eventually discrete guarded sums" i.e. if they were put in some sort of normal form,
with all the applications expanded to their definitions, then they would be sums of
input or output prefixed terms.
Ltac taeAuto := repeat taeAutoSing.
Every application of a name to a vector can progress by a delay. To prove this
we need to use heavy automation tactics rather than step through all 30 names
individually. The automation tactic we use is taeAuto.
Theorem delApp : forall (h : Name) (l : list Exp),
exists d, timedActEnabled (h $(l)$) d.
Reserved Notation "t %; p" (at level 50).
exists d, timedActEnabled (h $(l)$) d.
Reserved Notation "t %; p" (at level 50).
minGuard t P roughly says that t is less than or equal to the smallest delay
guard encountered in an expansion of P- by expansion of P what is meant is a recursive
drilling into unguarded terms until the resulting process contains only guarded terms.
Inductive minGuard : Delay -> ProcTerm -> Prop :=
| mgNil : forall (d : Delay), d %; nilProc
| mgIn : forall (d : Delay) (p : ProcTerm) (c : Channel) (l : list Var), d %; (c $< l >$ ? p)
| mgOut : forall (d : Delay) (p : ProcTerm) (c : Channel) (l : list Exp), d %; (c $< l >$ ! p)
| mgIfTrue : forall (d : Delay) (p : ProcTerm) (b : BoolExp),
d %; p -> evalBoolExp b true -> d %; (b $> p)
| mgIfFalse : forall (d : Delay) (p : ProcTerm) (b : BoolExp),
evalBoolExpFunTot b = false -> d %; (b $> p)
| mgSumL : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d1 <= d2 -> d1 %; (p $+$ q)
| mgSumR : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d2 < d1 -> d2 %; (p $+$ q)
| mgParL : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d1 <= d2 -> d1 %; (p $||$ q)
| mgParR : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d2 < d1 -> d2 %; (p $||$ q)
| mgApp : forall (d : Delay) (p : ProcTerm) (h : Name) (l1 : list Var) (l2 : list Exp),
def h = pair l1 p -> d %; (subProcTerm (listsToSub l1 l2) p) -> d %; (h $(l2)$)
| mgDelEval : forall (d : Delay) (t : Time) (p : ProcTerm) (e : Exp),
evalExpFunTime e = Some t -> d <= t -> d %; ($< e >$ p)
| mgDelIll : forall (d : Delay) (p : ProcTerm) (e : Exp),
evalExpFunTime e = None -> d %; ($< e >$ p)
| mgDelTimeout : forall (d : Delay) (p : ProcTerm) (e : Exp),
evalExpFunTime e = Some zeroTime -> d %; p -> d %; ($< e >$ p)
where "d %; p" := (minGuard d p).
| mgNil : forall (d : Delay), d %; nilProc
| mgIn : forall (d : Delay) (p : ProcTerm) (c : Channel) (l : list Var), d %; (c $< l >$ ? p)
| mgOut : forall (d : Delay) (p : ProcTerm) (c : Channel) (l : list Exp), d %; (c $< l >$ ! p)
| mgIfTrue : forall (d : Delay) (p : ProcTerm) (b : BoolExp),
d %; p -> evalBoolExp b true -> d %; (b $> p)
| mgIfFalse : forall (d : Delay) (p : ProcTerm) (b : BoolExp),
evalBoolExpFunTot b = false -> d %; (b $> p)
| mgSumL : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d1 <= d2 -> d1 %; (p $+$ q)
| mgSumR : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d2 < d1 -> d2 %; (p $+$ q)
| mgParL : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d1 <= d2 -> d1 %; (p $||$ q)
| mgParR : forall (d1 d2 : Delay) (p q : ProcTerm),
d1 %; p -> d2 %; q -> d2 < d1 -> d2 %; (p $||$ q)
| mgApp : forall (d : Delay) (p : ProcTerm) (h : Name) (l1 : list Var) (l2 : list Exp),
def h = pair l1 p -> d %; (subProcTerm (listsToSub l1 l2) p) -> d %; (h $(l2)$)
| mgDelEval : forall (d : Delay) (t : Time) (p : ProcTerm) (e : Exp),
evalExpFunTime e = Some t -> d <= t -> d %; ($< e >$ p)
| mgDelIll : forall (d : Delay) (p : ProcTerm) (e : Exp),
evalExpFunTime e = None -> d %; ($< e >$ p)
| mgDelTimeout : forall (d : Delay) (p : ProcTerm) (e : Exp),
evalExpFunTime e = Some zeroTime -> d %; p -> d %; ($< e >$ p)
where "d %; p" := (minGuard d p).
If t2 is minGuard p, then all t1 <= t2 are also minGuard p. Follows by induction, the only
"interesting" case being mgDelEval, in which case we use the transitivity of the Rle relation to
prove this property.
Lemma minGuardLe : forall (d1 d2 : Delay) (p : ProcTerm),
d2 %; p -> d1 <= d2 -> d1 %; p.
d2 %; p -> d1 <= d2 -> d1 %; p.
If we can show that minGuard d p, then for all actions, sort a d p implies
p being able to actually perform the action a now.
Theorem sortMinGuard1 : forall (a : DiscAct) (d : Delay) (p : ProcTerm),
d %; p -> sort a d p -> discActEnabled p a.
d %; p -> sort a d p -> discActEnabled p a.
If we can show that minGuard d p, then for all actions, sort a d p is equivalent to
p being able to actually perform the action a now.
Theorem sortMinGuard2 : forall (a : DiscAct) (d : Delay) (p : ProcTerm),
d %; p -> a <> tauAct -> (sort a d p <-> discActEnabled p a).
d %; p -> a <> tauAct -> (sort a d p <-> discActEnabled p a).
All input prefixed terms are minGuarded by any delay.
Lemma mgInEx : forall (c : Channel) (l : list Var) (p : ProcTerm),
exists d, d %; (c $<l>$ ? p).
exists d, d %; (c $<l>$ ? p).
All output prefixed terms are minGuarded by any delay.
Lemma mgOutEx : forall (c : Channel) (l : list Exp) (p : ProcTerm),
exists d, d %; (c $<l>$ ! p).
exists d, d %; (c $<l>$ ! p).
If both components of a sum are have some minGuard, then so does the whole sum.
Lemma mgSumEx : forall (p1 p2 : ProcTerm),
(exists d1, d1 %; p1) -> (exists d2, d2 %; p2) ->
exists d, d %; (p1 $+$ p2).
(exists d1, d1 %; p1) -> (exists d2, d2 %; p2) ->
exists d, d %; (p1 $+$ p2).
If the body of a process definition is minGuard d, then so is the application.
Lemma mgAppEx : forall (x : list Var) (l : list Exp) (h : Name) (p : ProcTerm),
def h = (x, p) -> (exists d, d %; (subProcTerm (listsToSub x l) p)) ->
exists d, d %; (h $(l)$).
def h = (x, p) -> (exists d, d %; (subProcTerm (listsToSub x l) p)) ->
exists d, d %; (h $(l)$).
More cumbersome version but it fills in the variable list x and the process p automatically by
extracting them from the process definition of p.
Lemma mgAppAutoEx : forall (l : list Exp) (h : Name),
(exists d, d %; (subProcTerm (listsToSub (fst (def h)) l) (snd (def h)))) ->
exists d, d %; (h $(l)$).
(exists d, d %; (subProcTerm (listsToSub (fst (def h)) l) (snd (def h)))) ->
exists d, d %; (h $(l)$).
If the then branch of an ifThen construct is minGuard for some amount d,
then the whole construct is for some amount also.
Lemma mgThenBranchEx : forall (b : BoolExp) (p : ProcTerm),
(exists d, d %; p) -> (exists d, d %; (b $> p)).
(exists d, d %; p) -> (exists d, d %; (b $> p)).
If p has a minGuard, then so does the guarded term with p as the guarded process.
Lemma mgDelEx : forall (e : Exp) (p : ProcTerm),
(exists d, d %; p) -> exists d, d %; ($<e>$p).
(exists d, d %; p) -> exists d, d %; ($<e>$p).
A single step of the full automation tactic for "eventually discrete guarded sum" terms.
This should prove that any such term has some minGuard.
Ltac mgAutoSing := match goal with
| [ |- exists _, _ %; ?P] =>
match P with
| _ $< _ >$ ? _ => apply mgInEx
| _ $< _ >$ ! _ => apply mgOutEx
| _ $> _ => apply mgThenBranchEx
| _ $+$ _ => apply mgSumEx
| _ $(_)$ => apply mgAppAutoEx; simpl
| $< _ >$ _ => apply mgDelEx
end
end.
Ltac mgAuto := repeat mgAutoSing.
| [ |- exists _, _ %; ?P] =>
match P with
| _ $< _ >$ ? _ => apply mgInEx
| _ $< _ >$ ! _ => apply mgOutEx
| _ $> _ => apply mgThenBranchEx
| _ $+$ _ => apply mgSumEx
| _ $(_)$ => apply mgAppAutoEx; simpl
| $< _ >$ _ => apply mgDelEx
end
end.
Ltac mgAuto := repeat mgAutoSing.
For every application there is some delay that is a minGuard of that application.
Theorem minGuardExistsBody (h : Name) (l : list Exp) :
exists d, d %; (h $(l)$).
exists d, d %; (h $(l)$).
For every application there is some delay that is a minGuard of that application.
Theorem minGuardExists (p : ProcTerm) :
exists d, d %; p.
exists d, d %; p.
An action that is involved in the sort relation is not the tau action.
Lemma sortNotTau (a : DiscAct) (p : ProcTerm) (d : Delay) :
sort a d p -> a <> tauAct.
sort a d p -> a <> tauAct.
The precondition for parallel delay can be replaced with a simpler precondition
as long as the delay in question is a minGuard of both components of the parallel.
Theorem parPrecMgEquiv : forall (p q : ProcTerm) (d : Delay),
d %; p -> d %; q -> (
(forall a : DiscAct, sort a d p -> ~sort (a^) d q) <->
(forall a : DiscAct, a <> tauAct -> discActEnabled p a -> ~discActEnabled q (a^))).
Open Scope nat_scope.
d %; p -> d %; q -> (
(forall a : DiscAct, sort a d p -> ~sort (a^) d q) <->
(forall a : DiscAct, a <> tauAct -> discActEnabled p a -> ~discActEnabled q (a^))).
Open Scope nat_scope.
This is a the set of channels stamped with natural numbers. The natural number
indicates the number of arguments that will be output on that channel.
Definition ChanStamped := (Channel * nat)%type.
Returns p x -> l where def h = x, p.
Definition unfoldApp (h : Name) (l : list Exp) :=
let (x, p) := def h in (subProcTerm (listsToSub x l) p).
let (x, p) := def h in (subProcTerm (listsToSub x l) p).
We want a way to symbolically collect all the output actions a process can do.
For each output, we just record the channel on which it occurs and the number
of arguments output, hence the collection is symbolic rather than literal.
Combined with a similar computation for input channels, this will be used to
construct a decision procedure as to whether processes can synchronise or not.
Inductive outListProc : ProcTerm -> list ChanStamped -> Prop :=
| outlNil : outListProc nilProc []
| outlOutEval (p : ProcTerm) (l : list Exp) (l' : list BaseType)
(c : Channel) : evalExpLists l l' -> outListProc (c $< l >$ ! p) [(c, length l)]
| outlOutIll (p : ProcTerm) (l : list Exp) (c : Channel) :
(forall l', ~evalExpLists l l') -> outListProc (c $< l >$ ! p) []
| outlIn (p : ProcTerm) (l : list Var) (c : Channel) :
outListProc (c $< l >$ ? p) []
| outlIfTrue (b : BoolExp) (p : ProcTerm) (l : list ChanStamped) :
evalBoolExp b true -> outListProc p l -> outListProc (b $> p) l
| outlIfFalse (b : BoolExp) (p : ProcTerm) :
evalBoolExpFunTot b = false -> outListProc (b $> p) []
| outlSum (p q : ProcTerm) (l1 l2 : list ChanStamped) :
outListProc p l1 -> outListProc q l2 -> outListProc (p $+$ q) (l1 ++ l2)
| outlPar (p q : ProcTerm) (l1 l2 : list ChanStamped) :
outListProc p l1 -> outListProc q l2 -> outListProc (p $||$ q) (l1 ++ l2)
| outlApp (h : Name) (l : list Exp) (l' : list ChanStamped) :
outListProc (unfoldApp h l) l' -> outListProc (h $( l )$) l'
| outlDelTimeout (p : ProcTerm) (e : Exp) (l : list ChanStamped) :
evalExpFunTime e = Some zeroTime -> outListProc p l -> outListProc ($< e >$ p) l
| outlDelGuard (p : ProcTerm) (e : Exp) :
evalExpFunTime e <> Some zeroTime -> outListProc ($< e >$ p) [].
| outlNil : outListProc nilProc []
| outlOutEval (p : ProcTerm) (l : list Exp) (l' : list BaseType)
(c : Channel) : evalExpLists l l' -> outListProc (c $< l >$ ! p) [(c, length l)]
| outlOutIll (p : ProcTerm) (l : list Exp) (c : Channel) :
(forall l', ~evalExpLists l l') -> outListProc (c $< l >$ ! p) []
| outlIn (p : ProcTerm) (l : list Var) (c : Channel) :
outListProc (c $< l >$ ? p) []
| outlIfTrue (b : BoolExp) (p : ProcTerm) (l : list ChanStamped) :
evalBoolExp b true -> outListProc p l -> outListProc (b $> p) l
| outlIfFalse (b : BoolExp) (p : ProcTerm) :
evalBoolExpFunTot b = false -> outListProc (b $> p) []
| outlSum (p q : ProcTerm) (l1 l2 : list ChanStamped) :
outListProc p l1 -> outListProc q l2 -> outListProc (p $+$ q) (l1 ++ l2)
| outlPar (p q : ProcTerm) (l1 l2 : list ChanStamped) :
outListProc p l1 -> outListProc q l2 -> outListProc (p $||$ q) (l1 ++ l2)
| outlApp (h : Name) (l : list Exp) (l' : list ChanStamped) :
outListProc (unfoldApp h l) l' -> outListProc (h $( l )$) l'
| outlDelTimeout (p : ProcTerm) (e : Exp) (l : list ChanStamped) :
evalExpFunTime e = Some zeroTime -> outListProc p l -> outListProc ($< e >$ p) l
| outlDelGuard (p : ProcTerm) (e : Exp) :
evalExpFunTime e <> Some zeroTime -> outListProc ($< e >$ p) [].
We want a way to symbolically collect all the input actions a process can do.
For each input, we just record the channel on which it occurs and the number
of arguments input, hence the collection is symbolic rather than literal.
Combined with a similar computation for output channels, this will be used to
construct a decision procedure as to whether processes can synchronise or not.
Inductive inListProc : ProcTerm -> list ChanStamped -> Prop :=
| inlNil : inListProc nilProc []
| inlOut (p : ProcTerm) (l : list Exp) (c : Channel) :
inListProc (c $< l >$ ! p) []
| inlIn (p : ProcTerm) (l : list Var) (c : Channel) :
inListProc (c $< l >$ ? p) [(c, length l)]
| inlIfTrue (b : BoolExp) (p : ProcTerm) (l : list ChanStamped) :
evalBoolExp b true -> inListProc p l -> inListProc (b $> p) l
| inlIfFalse (b : BoolExp) (p : ProcTerm) :
evalBoolExpFunTot b = false -> inListProc (b $> p) []
| inlSum (p q : ProcTerm) (l1 l2 : list ChanStamped) :
inListProc p l1 -> inListProc q l2 -> inListProc (p $+$ q) (l1 ++ l2)
| inlPar (p q : ProcTerm) (l1 l2 : list ChanStamped) :
inListProc p l1 -> inListProc q l2 -> inListProc (p $||$ q) (l1 ++ l2)
| inlApp (h : Name) (l : list Exp) (l' : list ChanStamped) :
inListProc (unfoldApp h l) l' -> inListProc (h $( l )$) l'
| inlDelTimeout (p : ProcTerm) (e : Exp) (l : list ChanStamped) :
evalExpFunTime e = Some zeroTime -> inListProc p l -> inListProc ($< e >$ p) l
| inlDelGuard (p : ProcTerm) (e : Exp) :
evalExpFunTime e <> Some zeroTime -> inListProc ($< e >$ p) [].
| inlNil : inListProc nilProc []
| inlOut (p : ProcTerm) (l : list Exp) (c : Channel) :
inListProc (c $< l >$ ! p) []
| inlIn (p : ProcTerm) (l : list Var) (c : Channel) :
inListProc (c $< l >$ ? p) [(c, length l)]
| inlIfTrue (b : BoolExp) (p : ProcTerm) (l : list ChanStamped) :
evalBoolExp b true -> inListProc p l -> inListProc (b $> p) l
| inlIfFalse (b : BoolExp) (p : ProcTerm) :
evalBoolExpFunTot b = false -> inListProc (b $> p) []
| inlSum (p q : ProcTerm) (l1 l2 : list ChanStamped) :
inListProc p l1 -> inListProc q l2 -> inListProc (p $+$ q) (l1 ++ l2)
| inlPar (p q : ProcTerm) (l1 l2 : list ChanStamped) :
inListProc p l1 -> inListProc q l2 -> inListProc (p $||$ q) (l1 ++ l2)
| inlApp (h : Name) (l : list Exp) (l' : list ChanStamped) :
inListProc (unfoldApp h l) l' -> inListProc (h $( l )$) l'
| inlDelTimeout (p : ProcTerm) (e : Exp) (l : list ChanStamped) :
evalExpFunTime e = Some zeroTime -> inListProc p l -> inListProc ($< e >$ p) l
| inlDelGuard (p : ProcTerm) (e : Exp) :
evalExpFunTime e <> Some zeroTime -> inListProc ($< e >$ p) [].
If l and l' are both out lists of p, then l is equal to l'.
Theorem outListUnique (l l' : list ChanStamped) (p : ProcTerm) :
outListProc p l -> outListProc p l' -> l = l'.
outListProc p l -> outListProc p l' -> l = l'.
If l and l' are both out lists of p, then l is equal to l'.
Theorem inListUnique (l l' : list ChanStamped) (p : ProcTerm) :
inListProc p l -> inListProc p l' -> l = l'.
Definition chanStampedNil : list ChanStamped := [].
inListProc p l -> inListProc p l' -> l = l'.
Definition chanStampedNil : list ChanStamped := [].
All output prefixed terms have an associated output list.
Lemma outListInEx : forall (c : Channel) (l : list Var) (p : ProcTerm),
{l' : list ChanStamped | outListProc (c $<l>$ ? p) l'}.
{l' : list ChanStamped | outListProc (c $<l>$ ? p) l'}.
All output prefixed terms have an associated output list.
Lemma outListOutEx : forall (c : Channel) (l : list Exp) (p : ProcTerm),
{ l' : list ChanStamped |outListProc (c $<l>$ ! p) l'}.
{ l' : list ChanStamped |outListProc (c $<l>$ ! p) l'}.
If both components of a sum have some output list, then so does the whole sum.
Lemma outListSumEx : forall (p1 p2 : ProcTerm),
{l1 | outListProc p1 l1} -> {l2 | outListProc p2 l2} ->
{l | outListProc (p1 $+$ p2) l}.
{l1 | outListProc p1 l1} -> {l2 | outListProc p2 l2} ->
{l | outListProc (p1 $+$ p2) l}.
If the body of a process definition has an output list, then so does the application.
Lemma outListAppIndEx : forall (x : list Var) (l : list Exp) (h : Name) (p : ProcTerm),
def h = (x, p) -> {l' | outListProc (subProcTerm (listsToSub x l) p) l'} ->
{l' | outListProc (h $(l)$) l'}.
def h = (x, p) -> {l' | outListProc (subProcTerm (listsToSub x l) p) l'} ->
{l' | outListProc (h $(l)$) l'}.
More cumbersome version but it fills in the variable list x and the
process p automatically by extracting them from the process definition of p.
Lemma outListAppAutoEx : forall (l : list Exp) (h : Name),
{l' | outListProc (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) l'} ->
{l' | outListProc (h $(l)$) l'}.
{l' | outListProc (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) l'} ->
{l' | outListProc (h $(l)$) l'}.
If the then branch of an ifThen construct has some outListProc,
then the whole construct has one also.
Lemma outListThenBranchEx : forall (b : BoolExp) (p : ProcTerm),
{l | outListProc p l} -> {l | outListProc (b $> p) l}.
{l | outListProc p l} -> {l | outListProc (b $> p) l}.
If p has an output list, then so does the guarded term with p as
the guarded process.
Lemma outListDelEx : forall (e : Exp) (p : ProcTerm),
{l | outListProc p l} -> {l | outListProc ($<e>$p) l}.
{l | outListProc p l} -> {l | outListProc ($<e>$p) l}.
A single step of the full automation tactic for "eventually discrete guarded sum" terms.
This should prove that any such term has some minGuard.
Ltac outListAutoSing := match goal with
| [ |- {_ | outListProc ?P _}] =>
match P with
| _ $< _ >$ ? _ => apply outListInEx
| _ $< _ >$ ! _ => apply outListOutEx
| _ $> _ => apply outListThenBranchEx
| _ $+$ _ => apply outListSumEx
| _ $(_)$ => apply outListAppAutoEx; simpl
| $< _ >$ _ => apply outListDelEx
end
end.
Ltac outListAuto := repeat outListAutoSing.
Theorem outListAppEx (h : Name) (l : list Exp) :
{l' : list ChanStamped | outListProc (h $(l)$) l'}.
Theorem outListEx (p : ProcTerm) : {l : list ChanStamped | outListProc p l}.
| [ |- {_ | outListProc ?P _}] =>
match P with
| _ $< _ >$ ? _ => apply outListInEx
| _ $< _ >$ ! _ => apply outListOutEx
| _ $> _ => apply outListThenBranchEx
| _ $+$ _ => apply outListSumEx
| _ $(_)$ => apply outListAppAutoEx; simpl
| $< _ >$ _ => apply outListDelEx
end
end.
Ltac outListAuto := repeat outListAutoSing.
Theorem outListAppEx (h : Name) (l : list Exp) :
{l' : list ChanStamped | outListProc (h $(l)$) l'}.
Theorem outListEx (p : ProcTerm) : {l : list ChanStamped | outListProc p l}.
All input prefixed terms have an associated input list.
Lemma inListInEx : forall (c : Channel) (l : list Var) (p : ProcTerm),
{l' : list ChanStamped | inListProc (c $<l>$ ? p) l'}.
{l' : list ChanStamped | inListProc (c $<l>$ ? p) l'}.
All input prefixed terms have an associated input list.
Lemma inListOutEx : forall (c : Channel) (l : list Exp) (p : ProcTerm),
{ l' : list ChanStamped |inListProc (c $<l>$ ! p) l'}.
{ l' : list ChanStamped |inListProc (c $<l>$ ! p) l'}.
If both components of a sum have some input list, then so does the whole sum.
Lemma inListSumEx : forall (p1 p2 : ProcTerm),
{l1 | inListProc p1 l1} -> {l2 | inListProc p2 l2} ->
{l | inListProc (p1 $+$ p2) l}.
{l1 | inListProc p1 l1} -> {l2 | inListProc p2 l2} ->
{l | inListProc (p1 $+$ p2) l}.
If the body of a process definition has an input list, then so does the application.
Lemma inListAppIndEx : forall (x : list Var) (l : list Exp) (h : Name) (p : ProcTerm),
def h = (x, p) -> {l' | inListProc (subProcTerm (listsToSub x l) p) l'} ->
{l' | inListProc (h $(l)$) l'}.
def h = (x, p) -> {l' | inListProc (subProcTerm (listsToSub x l) p) l'} ->
{l' | inListProc (h $(l)$) l'}.
More cumbersome version but it fills in the variable list x and the
process p automatically by extracting them from the process definition of p.
Lemma inListAppAutoEx : forall (l : list Exp) (h : Name),
{l' | inListProc (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) l'} ->
{l' | inListProc (h $(l)$) l'}.
{l' | inListProc (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) l'} ->
{l' | inListProc (h $(l)$) l'}.
If the then branch of an ifThen construct has some inListProc,
then the whole construct has one also.
Lemma inListThenBranchEx : forall (b : BoolExp) (p : ProcTerm),
{l | inListProc p l} -> {l | inListProc (b $> p) l}.
{l | inListProc p l} -> {l | inListProc (b $> p) l}.
If p has an input list, then so does the guarded term with p as
the guarded process.
Lemma inListDelEx : forall (e : Exp) (p : ProcTerm),
{l | inListProc p l} -> {l | inListProc ($<e>$p) l}.
{l | inListProc p l} -> {l | inListProc ($<e>$p) l}.
A single step of the full automation tactic for "eventually discrete guarded sum" terms.
This should prove that any such term has some minGuard.
Ltac inListAutoSing := match goal with
| [ |- {_ | inListProc ?P _}] =>
match P with
| _ $< _ >$ ? _ => apply inListInEx
| _ $< _ >$ ! _ => apply inListOutEx
| _ $> _ => apply inListThenBranchEx
| _ $+$ _ => apply inListSumEx
| _ $(_)$ => apply inListAppAutoEx; simpl
| $< _ >$ _ => apply inListDelEx
end
end.
Ltac inListAuto := repeat inListAutoSing.
Theorem inListAppEx (h : Name) (l : list Exp) :
{l' : list ChanStamped | inListProc (h $(l)$) l'}.
Theorem inListEx (p : ProcTerm) : {l : list ChanStamped | inListProc p l}.
Lemma eqDecChanStamped (c1 c2 : ChanStamped) :
{c1 = c2} + {c1 <> c2}.
| [ |- {_ | inListProc ?P _}] =>
match P with
| _ $< _ >$ ? _ => apply inListInEx
| _ $< _ >$ ! _ => apply inListOutEx
| _ $> _ => apply inListThenBranchEx
| _ $+$ _ => apply inListSumEx
| _ $(_)$ => apply inListAppAutoEx; simpl
| $< _ >$ _ => apply inListDelEx
end
end.
Ltac inListAuto := repeat inListAutoSing.
Theorem inListAppEx (h : Name) (l : list Exp) :
{l' : list ChanStamped | inListProc (h $(l)$) l'}.
Theorem inListEx (p : ProcTerm) : {l : list ChanStamped | inListProc p l}.
Lemma eqDecChanStamped (c1 c2 : ChanStamped) :
{c1 = c2} + {c1 <> c2}.
It is decidable whether or not an element is in a list of stamped channels.
Lemma inChanStampedDec (s : ChanStamped) (l : list ChanStamped) :
{s _: l} + {~s _: l}.
{s _: l} + {~s _: l}.
If a stamped channel is in the output list of a process, then that process is
enabled on an action that matches the stamped channel.
Theorem outListEnabled (c : Channel) (p : ProcTerm) (l : list ChanStamped)
(n : nat) : outListProc p l -> (c, n) _: l ->
exists v, length v = n /\ discActEnabled p (c ;! v).
Theorem inListEnabled (c : Channel) (p : ProcTerm) (l : list ChanStamped)
(v : list BaseType): inListProc p l -> (c, length v) _: l ->
discActEnabled p (c ;? v).
(n : nat) : outListProc p l -> (c, n) _: l ->
exists v, length v = n /\ discActEnabled p (c ;! v).
Theorem inListEnabled (c : Channel) (p : ProcTerm) (l : list ChanStamped)
(v : list BaseType): inListProc p l -> (c, length v) _: l ->
discActEnabled p (c ;? v).
An existential version of the above.
Corollary inListEnabledEx (c : Channel) (p : ProcTerm) (l : list ChanStamped)
(n : nat): inListProc p l -> (c, n) _: l -> exists v, length v = n /\
discActEnabled p (c ;? v).
(n : nat): inListProc p l -> (c, n) _: l -> exists v, length v = n /\
discActEnabled p (c ;? v).
If a process is enabled on an output action then there is a matching stamped
channel in the output list of that process.
Theorem enabledOutList (c : Channel) (p : ProcTerm) (l : list ChanStamped)
(v : list BaseType) : outListProc p l -> discActEnabled p (c ;! v) ->
(c, (length v)) _: l.
(v : list BaseType) : outListProc p l -> discActEnabled p (c ;! v) ->
(c, (length v)) _: l.
If a process is enabled on an input action then there is a matching stamped
channel in the input list of that process.
Theorem enabledInList (c : Channel) (p : ProcTerm) (l : list ChanStamped)
(v : list BaseType) : inListProc p l -> discActEnabled p (c ;? v) ->
(c, (length v)) _: l.
(v : list BaseType) : inListProc p l -> discActEnabled p (c ;? v) ->
(c, (length v)) _: l.
A way of checking for no synchronisations between p and q by performing intersections
on their input/output and output/input lists and checking that they evaluate to empty lists.
Inductive noSync (p q : ProcTerm) : Prop :=
nosync : forall (l1 l2 l1' l2' : list ChanStamped),
inListProc p l1 -> outListProc p l2 -> inListProc q l1' -> outListProc q l2' ->
set_inter eqDecChanStamped l1 l2' = [] -> set_inter eqDecChanStamped l2 l1' = []
-> noSync p q.
Theorem noSyncDec (p q : ProcTerm) :
decidable (noSync p q).
nosync : forall (l1 l2 l1' l2' : list ChanStamped),
inListProc p l1 -> outListProc p l2 -> inListProc q l1' -> outListProc q l2' ->
set_inter eqDecChanStamped l1 l2' = [] -> set_inter eqDecChanStamped l2 l1' = []
-> noSync p q.
Theorem noSyncDec (p q : ProcTerm) :
decidable (noSync p q).
The precondition for parallel delay can be replaced with a simpler precondition
involving the input and output lists, as long as the delay in question is a minGuard
of both components of the parallel.
Theorem parPrecMgEquiv2 : forall (p q : ProcTerm) (d : Delay),
d %; p -> d %; q -> (
(forall a : DiscAct, sort a d p -> ~sort (a^) d q) <->
noSync p q).
Lemma minGuardCommon (p q : ProcTerm) : exists d,
d %; p /\ d %; q.
Lemma taeCommon (p1 p2 : ProcTerm) :
(exists d, timedActEnabled p1 d) -> (exists d, timedActEnabled p2 d) ->
(exists d, timedActEnabled p1 d /\ timedActEnabled p2 d).
d %; p -> d %; q -> (
(forall a : DiscAct, sort a d p -> ~sort (a^) d q) <->
noSync p q).
Lemma minGuardCommon (p q : ProcTerm) : exists d,
d %; p /\ d %; q.
Lemma taeCommon (p1 p2 : ProcTerm) :
(exists d, timedActEnabled p1 d) -> (exists d, timedActEnabled p2 d) ->
(exists d, timedActEnabled p1 d /\ timedActEnabled p2 d).
If a process p is time act enabled on d, then it is time act enabled on
any minGuard d' of p less than d.
Lemma taeMinGuardCommon (p1 p2 : ProcTerm) :
(exists d, timedActEnabled p1 d) -> (exists d, timedActEnabled p2 d) ->
(exists d, timedActEnabled p1 d /\ timedActEnabled p2 d /\ d %; p1 /\ d %; p2).
(exists d, timedActEnabled p1 d) -> (exists d, timedActEnabled p2 d) ->
(exists d, timedActEnabled p1 d /\ timedActEnabled p2 d /\ d %; p1 /\ d %; p2).
If the noSync predicate is not true, then there exists some specific synchronisation
between the component processes.
Lemma noSyncNotExistsSync (p q : ProcTerm) : ~noSync p q ->
exists a, discActEnabled p a /\ discActEnabled q (a^).
exists a, discActEnabled p a /\ discActEnabled q (a^).
If both list are empty, then we get a contradiction.
Otherwise we just take the head of the list as a witness.
Definition progress (p : ProcTerm) : Prop :=
discActEnabled p tauAct \/ exists d, timedActEnabled p d.
All input prefixed terms can progress.
Lemma progressIn : forall (c : Channel) (l : list Var) (p : ProcTerm),
progress (c $<l>$ ? p).
progress (c $<l>$ ? p).
All output prefixed terms can progress.
Lemma progressOut : forall (c : Channel) (l : list Exp) (p : ProcTerm),
progress (c $<l>$ ! p).
progress (c $<l>$ ! p).
If both components of a sum can progress, then so can the whole sum.
Lemma progressSum : forall (p1 p2 : ProcTerm),
progress p1 -> progress p2 -> progress (p1 $+$ p2).
progress p1 -> progress p2 -> progress (p1 $+$ p2).
If the body of a process definition can progress, then so can the application.
Lemma progressAppInd : forall (x : list Var) (l : list Exp) (h : Name) (p : ProcTerm),
def h = (x, p) -> progress (subProcTerm (listsToSub x l) p) ->
progress (h $(l)$).
def h = (x, p) -> progress (subProcTerm (listsToSub x l) p) ->
progress (h $(l)$).
More cumbersome version but it fills in the variable list x and the
process p automatically by extracting them from the process definition of p.
Lemma progressAppAuto : forall (l : list Exp) (h : Name),
progress (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) ->
progress (h $(l)$).
progress (subProcTerm (listsToSub (fst (def h)) l) (snd (def h))) ->
progress (h $(l)$).
If the then branch of an ifThen construct can progress,
then the whole construct can also.
Lemma progressThenBranch : forall (b : BoolExp) (p : ProcTerm),
progress p -> progress (b $> p).
Open Scope R_scope.
progress p -> progress (b $> p).
Open Scope R_scope.
If p can progress, then so can the guarded term with p as
the guarded process.
Lemma progressDel : forall (e : Exp) (p : ProcTerm),
progress p -> progress ($<e>$p).
progress p -> progress ($<e>$p).
A single step of the full automation tactic for "eventually discrete guarded sum" terms.
This should prove that any such term can progress.
Ltac progressAutoSing := match goal with
| [ |- progress ?P] =>
match P with
| _ $< _ >$ ? _ => apply progressIn
| _ $< _ >$ ! _ => apply progressOut
| _ $> _ => apply progressThenBranch
| _ $+$ _ => apply progressSum
| _ $(_)$ => apply progressAppAuto; simpl
| $< _ >$ _ => apply progressDel
end
end.
Ltac progressAuto := repeat progressAutoSing.
Theorem progressApp (h : Name) (l : list Exp) :
progress (h $(l)$).
| [ |- progress ?P] =>
match P with
| _ $< _ >$ ? _ => apply progressIn
| _ $< _ >$ ! _ => apply progressOut
| _ $> _ => apply progressThenBranch
| _ $+$ _ => apply progressSum
| _ $(_)$ => apply progressAppAuto; simpl
| $< _ >$ _ => apply progressDel
end
end.
Ltac progressAuto := repeat progressAutoSing.
Theorem progressApp (h : Name) (l : list Exp) :
progress (h $(l)$).
A software process can always do either a tau action or it can delay by some amount
d.
Theorem progressSoft : forall (p : ProcTerm),
progress p.
progress p.
If a process cannot perform a tau action, then it can delay by some amount. This is
a direct corollary of progress.
Corollary patienceSoft (p : ProcTerm) : ~discActEnabled p tauAct -> exists d,
timedActEnabled p d.
Lemma delProc_minus_guard t d d' H p p' e :
$< minusTime t (delay d) H >$ p -PD- d' -PD> p' ->
$< e >$ p -PD- d +d+ d' -PD> p'.
timedActEnabled p d.
Lemma delProc_minus_guard t d d' H p p' e :
$< minusTime t (delay d) H >$ p -PD- d' -PD> p' ->
$< e >$ p -PD- d +d+ d' -PD> p'.
If p can delay to p' and p' can delay to p'',
then p can delay to p'' by the sum of the two original delays.
Theorem delAddSoft (p p' p'' : ProcTerm) (d d' : Delay) :
p -PD- d -PD> p' -> p' -PD- d' -PD> p'' -> p -PD- d +d+ d' -PD> p''.
p -PD- d -PD> p' -> p' -PD- d' -PD> p'' -> p -PD- d +d+ d' -PD> p''.
The passage of time in this universe is linear, i.e. any process can delay by an amount d to
at most one derivative process.
Theorem timeDeterminacySoft (p p1' p2' : ProcTerm) (d : Delay) :
p -PD- d -PD> p1' -> p -PD- d -PD> p2' -> p1' = p2'.
Lemma del_triple_sort p1 p2 p3 p d : p1 $||$ p2 $||$ p3 -PD- d -PD> p ->
(forall a : DiscAct, sort a d p1 -> ~sort (a^) d p2) /\
(forall a : DiscAct, sort a d p1 -> ~sort (a^) d p3) /\
(forall a : DiscAct, sort a d p2 -> ~sort (a^) d p3).
Lemma parTriple_disc_intro1 p1 p2 p3 p1' a :
p1 -PA- a -PA> p1' ->
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2 $||$ p3.
Lemma parTriple_disc_intro2 p1 p2 p3 p2' a :
p2 -PA- a -PA> p2' ->
p1 $||$ p2 $||$ p3 -PA- a -PA> p1 $||$ p2' $||$ p3.
Lemma parTriple_disc_intro3 p1 p2 p3 p3' a :
p3 -PA- a -PA> p3' ->
p1 $||$ p2 $||$ p3 -PA- a -PA> p1 $||$ p2 $||$ p3'.
Lemma parTriple_dae_intro1 p1 p2 p3 a :
discActEnabled p1 a -> discActEnabled (p1 $||$ p2 $||$ p3) a.
Lemma parTriple_dae_intro2 p1 p2 p3 a :
discActEnabled p2 a -> discActEnabled (p1 $||$ p2 $||$ p3) a.
Lemma parTriple_dae_intro3 p1 p2 p3 a :
discActEnabled p3 a -> discActEnabled (p1 $||$ p2 $||$ p3) a.
p -PD- d -PD> p1' -> p -PD- d -PD> p2' -> p1' = p2'.
Lemma del_triple_sort p1 p2 p3 p d : p1 $||$ p2 $||$ p3 -PD- d -PD> p ->
(forall a : DiscAct, sort a d p1 -> ~sort (a^) d p2) /\
(forall a : DiscAct, sort a d p1 -> ~sort (a^) d p3) /\
(forall a : DiscAct, sort a d p2 -> ~sort (a^) d p3).
Lemma parTriple_disc_intro1 p1 p2 p3 p1' a :
p1 -PA- a -PA> p1' ->
p1 $||$ p2 $||$ p3 -PA- a -PA> p1' $||$ p2 $||$ p3.
Lemma parTriple_disc_intro2 p1 p2 p3 p2' a :
p2 -PA- a -PA> p2' ->
p1 $||$ p2 $||$ p3 -PA- a -PA> p1 $||$ p2' $||$ p3.
Lemma parTriple_disc_intro3 p1 p2 p3 p3' a :
p3 -PA- a -PA> p3' ->
p1 $||$ p2 $||$ p3 -PA- a -PA> p1 $||$ p2 $||$ p3'.
Lemma parTriple_dae_intro1 p1 p2 p3 a :
discActEnabled p1 a -> discActEnabled (p1 $||$ p2 $||$ p3) a.
Lemma parTriple_dae_intro2 p1 p2 p3 a :
discActEnabled p2 a -> discActEnabled (p1 $||$ p2 $||$ p3) a.
Lemma parTriple_dae_intro3 p1 p2 p3 a :
discActEnabled p3 a -> discActEnabled (p1 $||$ p2 $||$ p3) a.
This page has been generated by coqdoc