Library ModeStateLanguage

This file was written by Colm Bhandal, PhD student, Foundations and Methods group, School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
*************************** Standard Imports

Require Import ComhCoq.Extras.LibTactics.


Require Import ComhCoq.GenTacs.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.StandardResults.



Syntax: a mode state is either a single stable mode, or the transition from one mode to another, with a certain amount of time remaining until the transition times out and the mode switch can be finalised.
Inductive ModeState : Type :=
  | sing :> Mode -> ModeState
  | transState : Mode -> Mode -> Time -> ModeState.
Notation "<| m , m' , t |>" := (transState m m' t) (at level 30).

Coerce a mode state to its current mode.
Coercion currModeMState (a : ModeState) : Mode :=
  match a with
  | sing m => m
  | <|m, m', d|> => m
  end.

Strip the next mode off the mode state, if it exists.
Definition nextModeMState (a : ModeState) : option Mode :=
  match a with
  | sing m => None
  | <|m, m', d|> => Some m'
  end.

Equality on mode states is decidable.
Lemma eqDecModeState : eqDec ModeState.

The actions of the mode state are: input/output of a mode on a channel, or delay.
Inductive ActModeState :=
  | amIn : Channel -> Mode -> ActModeState
  | amOut : Channel -> Mode -> ActModeState
  | amOutEmp : Channel -> ActModeState
  | amInEmp : Channel -> ActModeState
  | amDel :> Delay -> ActModeState.

Notation "c .? m" := (amIn c m) (at level 30).
Notation "c .! m" := (amOut c m) (at level 30).
Notation "c @! " := (amOutEmp c) (at level 30).
Notation "c @? " := (amInEmp c) (at level 30).

Reserved Notation "m -ms- a -ms> m'" (at level 75).

The semantics of the mode state language.
Inductive stepModeState : ModeState -> ActModeState -> ModeState -> Prop :=
  
A stable mode state can delay arbitrarily and remain unchanged.
  | stepMsDelSing : forall (m : Mode) (d : Delay),
    m -ms- d -ms> m
  | stepMsDelTout : forall (m m' : Mode) (d : Delay),
    <| m , m' , zeroTime |> -ms- d -ms> <| m , m' , zeroTime |>
  | stepMsDelGuard : forall (m m' : Mode) (d : Delay) (t t' : Time),
    t = t' +dt+ d -> <| m , m' , t |> -ms- d -ms> <| m , m' , t' |>
  | stepMsTimeout : forall (m m' : Mode) (t : Time) (d : Delay),
    t < d -> <| m , m' , t |> -ms- d -ms> <| m , m' , zeroTime |>
  | stepMsInit : forall (m m' : Mode) (p : m -mtr-> m'),
    m -ms- chanMNext .? m' -ms> <| m , m' , modeTransTime m m' p |>
  | stepMsSwitch : forall (m m' : Mode),
    <| m , m' , zeroTime |> -ms- chanMCurr @? -ms> m'
  | stepMsAbort : forall (m m' : Mode) (t : Time),
    <| m , m' , t |> -ms- chanMStable @? -ms> m
  | stepMsOutCurrSing : forall m : Mode, m -ms- chanMCurr .! m -ms> m
  | stepMsOutCurrTrans : forall (m m' : Mode) (t : Time),
    <| m , m' , t |> -ms- chanMCurr .! m -ms> <| m , m' , t |>
  | stepMsOutNext : forall (m m' : Mode) (t : Time),
    <| m , m' , t |> -ms- chanMNext .! m' -ms> <| m , m' , t |>
  | stepMsOutStable : forall m : Mode, m -ms- chanMStable @! -ms> m
  where "m -ms- a -ms> m'" := (stepModeState m a m').

A mode state is enabled on a discrete action if it can perform an input of a mode, an output of a mode or an output of nothing. The discrete action is then the corresponding input or output as a DiscAct rather than an ActModeState.
Inductive discActEnabledMState : DiscAct -> ModeState -> Prop :=
  | daemIn : forall (c : Channel) (m : Mode) (k k' : ModeState),
    k -ms- c .? m -ms> k' -> discActEnabledMState (c ;? [baseMode m]) k
  | daemOutMode : forall (c : Channel) (m : Mode) (k k' : ModeState),
    k -ms- c .! m -ms> k' -> discActEnabledMState (c ;! [baseMode m]) k
  | daemInEmp : forall (c : Channel) (k k' : ModeState),
    k -ms- c @? -ms> k' -> discActEnabledMState (c *?) k
  | daemOutEmp : forall (c : Channel) (k k' : ModeState),
    k -ms- c @! -ms> k' -> discActEnabledMState (c *!) k.


If <m1, m2, t> transitions by d to <m1', m2', t'> then either t' = 0, or t = t' + d.
Lemma delMStateTrans : forall (m1 m2 m1' m2' : Mode) (t t' : Time) (d : Delay),
  <| m1, m2, t |> -ms- d -ms> <| m1', m2', t' |> ->
  t' = zeroTime /\ t < d \/ t = t' +dt+ d.

Lemma delMStateTout : forall (m1 m2 : Mode) (a : ModeState) (d : Delay),
  <| m1, m2, zeroTime |> -ms- d -ms> a -> a = <| m1, m2, zeroTime |>.

If an MState can timeout in d then it can timeout in d + d'.
Lemma delMStateToutLengthen : forall (m1 m2 : Mode) (t : Time) (d d' : Delay),
  <| m1, m2, t |> -ms- d -ms> <| m1, m2, zeroTime |> ->
  <| m1, m2, t |> -ms- d +d+ d' -ms> <| m1, m2, zeroTime |>.

If an Mstate is transitioning and it delays, then it is still transitioning.
Lemma delMStatePresTrans : forall (m1 m2 : Mode) (a : ModeState) (d : Delay) (t : Time),
  <| m1, m2, t|> -ms- d -ms> a -> exists t', a = <| m1, m2, t'|>.

Two consecutive delays can be joined together into one delay, skipping the intermediate state. The final delay is the sum of the two original delays.
Lemma delAddMState : forall (a a' a'' : ModeState) (d d' : Delay),
  a -ms- d -ms> a' -> a' -ms- d' -ms> a'' ->
  a -ms- d +d+ d' -ms> a''.

Every mode state can delay by any amount d.
Lemma delEnabledMState : forall (a : ModeState) (d : Delay),
  exists a', a -ms- d -ms> a'.

Lemma curr_switch_mState (k k' : ModeState) (a : ActModeState) :
  k -ms- a -ms> k' -> currModeMState k <> currModeMState k' ->
  a = chanMCurr @?.

Lemma timeSplit_mState (k k'' : ModeState) (d d' d'' : Delay) :
  k -ms- d'' -ms> k'' -> d'' = d +d+ d' ->
  exists k', k -ms- d -ms> k' /\ k' -ms- d' -ms> k''.


Inductive unstable : ModeState -> Prop :=
  | unstbl m m' t : unstable (<| m , m' , t |>).

Lemma unstable_stable_in k : unstable k -> discActEnabledMState (chanMStable *?) k.

Lemma modeState_curr_enabled k :
  discActEnabledMState (chanMCurr ;! [baseMode (currModeMState k)]) k.

Lemma mState_stable_next_enabled k m' : currModeMState k -mtr-> m' ->
  discActEnabledMState (chanMStable*?) k \/
  discActEnabledMState (chanMNext;? [baseMode m']) k.

Lemma next_modeState_stable_not k k' m' :
  nextModeMState k = Some m' -> k -ms- chanMStable @! -ms> k' -> False.

Lemma modeState_abort_in_not k k' :
  k -ms- chanAbort @? -ms> k' -> False.

Lemma unstable_stable_out_not k : unstable k ->
  ~ discActEnabledMState (chanMStable *!) k.

Lemma nextMode_unstable k m : nextModeMState k = Some m ->
  unstable k.

This page has been generated by coqdoc