Mefresa.Behaviour.MasterSlaveCoffee

In this module we show another example regarding the reasoning about synchronized transition systems. In particular, we retake the example from the Fiacre online tutorial 1 concerning the Master/Slave coffee orders.
1 http://projects.laas.fr/fiacre/doc/fiacre-tutorial.html

Require Export Mefresa.Behaviour.Net.
Set Implicit Arguments.

Master and Slave Coffee example

We model both the Slave and Master with our LTS datatype. Then, we specify how they communicated by means of synchronization vectors, and define the resulting Net object.
Examples regarding an instantiated and parametrized Net objects are shown.
Below, before moving the the modelling of the slavelts, we define a convenient notation expressing the satisfiabilty of a property p by a trace t.

Notation "t '|=' p" := (satisfies t p) (at level 3, left associativity).

Slave model


Definition mem : state_mem := nil.

Definition slv0 : lts_state := LTS_State 0 mem.
Definition slv1 : lts_state := LTS_State 1 mem.

Definition receiveCoffeeOrder (n:nat) : action :=
  Action (Message "order:MakeCoffee" Read (Val(n)::nil)) nil.

Function nCoffeeOrders n : actions :=
  match n with
    0 => receiveCoffeeOrder 0 :: nil
  | S m => receiveCoffeeOrder n :: nCoffeeOrders m
  end.

Definition receiveSandwichOrder : action :=
  Action (Message "order:MakeSandwich" Read nil) nil.

Definition slave_order_acts n : actions := receiveSandwichOrder :: nCoffeeOrders n.
Definition slave_ready_act : action := Action (Message "ready" Read nil) nil.
Definition slave_acts n : actions := slave_ready_act :: (slave_order_acts n).

Definition slave_sts : lts_states := slv0 :: slv1 :: nil.

Function slave_transitions slave_order_acts : transitions :=
  match slave_order_acts with
    nil => (slv0, slave_ready_act, slv1) :: nil
  | slave_act :: r => (slv1, slave_act, slv0) :: (slave_transitions r)
  end.

Definition slavelts n : LTS := mk_LTS slave_sts slv0 (slave_acts n)
                                  (slave_transitions (slave_order_acts n)).

The above mechanization should pose no doubt. Basically, it is a simple LTS composed by two lts_states, slv0 and slv1, and the actions specified by the slave_acts function. The transitions are achieved through the slave_transitions function, and everything is put together by slavelts definition.

Master model

The model of the masterlts follows the same rationale as discussed for slavelts.

Definition mst0 : lts_state := LTS_State 0 mem.
Definition mst1 : lts_state := LTS_State 1 mem.

Definition makeCoffeeOrder (n:nat) : action :=
  Action (Message "MakeCoffee" Emit (Val(n)::nil)) nil.

Function nMakeCoffeeOrders n : actions :=
  match n with
    0 => makeCoffeeOrder 0 :: nil
  | S m => makeCoffeeOrder n :: nMakeCoffeeOrders m
  end.

Definition makeSandwichOrder : action :=
  Action (Message "MakeSandwich" Emit nil) nil.

Definition master_order_acts n : actions := makeSandwichOrder :: nMakeCoffeeOrders n.
Definition master_ready_act : action := Action (Message "ready" Emit nil) nil.
Definition master_acts n : actions := master_ready_act :: (master_order_acts n).

Definition master_sts : lts_states := mst0 :: mst1 :: nil.

Function master_transitions master_order_acts :=
  match master_order_acts with
    nil => (slv0, master_ready_act, slv1) :: nil
  | master_act :: r => (slv1, master_act, slv0) :: (master_transitions r)
  end.

Definition masterlts n : LTS := mk_LTS master_sts mst0 (master_acts n)
                                  (master_transitions (master_order_acts n)).

Synchronization Vectors, and the overall Net

Having discussed the mechanization of the masterlts and slavelts, let us now see how they communicate with each other.

Definition synch_vectors :=
  [ <<"ready" , "ready">> -> "ready" ;
    <<"order:MakeSandwich", "MakeSandwich">> -> "order:Sandwich" ;
    <<"order:MakeCoffee" , "MakeCoffee">> -> "order:Coffee" ].

Finally, we can define the overall Net of our system: MasterSlaveCoffeeNet.

Definition MasterSlaveCoffeeNet n := mk_Net (([slavelts n; masterlts n]), synch_vectors).

Interleaving property

A rather simple property that we may expect to hold in our MasterSlaveCoffeeNet system, is that its execution is an infinite interleaving between "ready" and some "order" actions.
In order to prove this, we must first specify this interleaving behaviour. This is achieved by the interleaving predicate depicted below.

Inductive interleaving (X:Type) (Y:Type) (R:Y->X->Prop)
                       (a b : Y) : LList X -> Prop :=
   InterleavingOne: forall l' l a' b',
                           l = LCons a' (LCons b' l') ->
                           R a a' ->
                           R b b' ->
                           interleaving R a b l
 | InterleavingTwo: forall l' l a' b',
                           l = LCons b' (LCons a' l') ->
                           R a a' ->
                           R b b' ->
                           interleaving R a b l.


The above interleaving takes a relation R as parameter since we may want a different relation then equality. Further, we include two construtors in order to easily cope with the order by which the interleaving starts.

Definition Rma (l:string) (act:action) : Prop :=
  match l, act with
    "ready", Action (Message l' _ct _lp) _asgns => "ready" = l'
  | "order", Action (Message l' _ct _lp) _asgns =>
      "order:Sandwich" = l' \/ "order:Coffee" = l'
  | _, _ => False
  end.

Above, the Rma definition is the interleaving relation that we shall be using for the rest of this module.s Basically, we just want to compare the labels of the involved actions.
For the sake of clarity, we demonstrate two examples illustrating the interleaving predicate in action.

Example interelaving_test:
  forall t a b,
  a = Action (Message "ready" Read nil) nil ->
  b = Action (Message "order:Sandwich" Read nil) nil ->
  t = LCons a (LCons b LNil)->
  t |= (Always (interleaving Rma "ready" "order")).
Proof.
  intros. subst.
  apply Always_LCons.
  Case "1/2".
    eapply InterleavingOne; [refl | ..]; compute; auto.
  Case "2/2".
Abort.

Example interelaving_test':
  forall t a b,
  a = Action (Message "ready" Read nil) nil ->
  b = Action (Message "order:Sandwich" Read nil) nil ->
  t = LCons a (LCons b (LCons b (LCons a LNil)))->
  t |= (Always (interleaving Rma "ready" "order")).
Proof.
  intros. subst.
  apply Always_LCons.
  Case "1/2".
    eapply InterleavingOne; [refl | ..]; compute; auto.
  Case "2/2".
    apply Always_LCons.
    SCase "1/2".
    eapply InterleavingTwo; [refl | ..]; compute; auto.
Abort.

A first Master/Coffee proof

The fiacre online tutorial 1 exemplified a system with three kinds of coffee: 0, 1 and 2. Below, we prove that from all states, all Net_Traces of an instantiated MasterSlaveCoffeeNet with three kinds of coffee, satisfy an infinite interleaving behaviour.

Module InstantiatedExample.

Theorem Infinite_ready_interleaving:
  forall t q,
   Net_Trace (MasterSlaveCoffeeNet 2) q t ->
   t |= (Always (interleaving Rma "ready" "order")).
Proof.
  cofix;
  intros t q Ht; inversion Ht; subst.
  Case "1/3 : case of an LTS trace. reductio ad absurdum".
    clear Ht.
    discriminate H0.
  Case "2/3 : case of a empty Net trace. reductio ad absurdum".
    clear Ht.
    inversion H; subst. clear H.
    unfold synch_vectors in *.
    inversion H1; [discriminate | subst].
    inversion H0 ;subst. clear H0.
    inversion H5; [discriminate | subst].
    inversion H0; subst. clear H0.
    inversion H7; [subst | discriminate].
    clear H5 H7 H0 H1.
    destruct H4 as [Hs0 | [Hs1 | Hf]]; subst; try inversion Hf;
    destruct H6 as [Hm0 | [Hm1 | Hf']]; subst; try inversion Hf'.
      SCase "1/4 : Current state is attainable, but no valid synch. vectors".
        absurd (net_target_states (MasterSlaveCoffeeNet 2) (Net_State [slv0; mst0])
             (<< "ready", "ready" >> -> "ready") = []).
        SSCase "absurd: False case".
          simpl; discriminate.
        SSCase "absurd: True case".
          apply H3. left; auto.
      SCase "2/4: Current state is not attainable. Proof by contradiction". Focus.
        clear -SCase SCase H2.
        simpl in H2.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SCase SCase H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3 as
        [Hs1 | [Hs2 | [Hs3 | Hf] ]];
        subst; try inversion Hf; simpl in *; inversion H4; subst;
        (assert (False);
          [ apply H; compute; auto | fromfalse]).
      SCase "3/4: Current state is not attainable. Proof by contradiction".
        clear -SCase SCase H2.
        simpl in H2.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SCase SCase H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3 as
        [Hs1 | [Hs2 | [Hs3 | Hf] ]];
        subst; try inversion Hf; simpl in *; inversion H4; subst;
        (assert (False);
          [ apply H; compute; auto | fromfalse]).
      SCase "4/4: Current state is attainable, but no valid synch. vectors". Focus.
        absurd (net_target_states (MasterSlaveCoffeeNet 2) (Net_State [slv1; mst1])
             (<< "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich") = []).
        SSCase "absurd: False case".
          simpl; discriminate.
        SSCase "absurd: True case".
          apply H3. right. left; auto.
    Case "3/3 : case of lcons Net trace. Prove the interleaving!".
      clear Ht.
      inversion H; subst. clear H.
      inversion H1; [discriminate | subst]. clear H1.
      inversion H0; subst. clear H0.
      inversion H7; [discriminate | subst].
      inversion H0; subst.
      inversion H8; [subst | discriminate].
      clear H0 H9 H8 H7.
      simpl in H4; simpl in H1.
      simpl in H2.
      destruct H1 as [Hs0 | [Hs1 | Hf]]; subst; try inversion Hf;
      destruct H4 as [Hm0 | [Hm1 | Hf']]; subst; try inversion Hf'.
      SCase "1/4 : Current state is attainable". Focus.
        clear H2.
        unfold synch_vectors in H3.
        destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst;
        try inversion Hf; compute in H5; inversion H5;
        [ subst | fromfalse]. clear H5.
        inversion H; subst. clear H.
        apply Always_LCons.
        SSCase "1/2 : interleaving". Focus.
          inversion H6; subst.
          SSSCase "1/3".
            discriminate.
          SSSCase "2/3".
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 2)
       (Net_State [LTS_State 1 []; LTS_State 1 []])
             (<< "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich") = []).
          SSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSCase "absurd: True case".
            apply H3. right. left. auto.
        SSSCase "3/3".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          SSSSCase "1/4 : Synch. Vector order sandwich".
            clear H3 H5.
            apply InterleavingOne with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Sandwich" Emit []) []));
                        auto.
            refl. simpl. left; auto.
          SSSSCase "2/4 : Synch. Vector order coffee".
            clear H3 H5.
            apply InterleavingOne with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 2]) [])).
                        refl. refl. simpl. right. refl.

          SSSSCase "3/4". Focus.
            clear H3 H5.
            inversion H4; subst.
            apply InterleavingOne with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 1]) [])).
                        refl. refl. simpl. right. refl.
          SSSSCase "4/4".
            clear H3 H5.
            destruct H4 as [Ha | Hf];
             try inversion Hf; inversion Ha; subst; clear Ha.
             apply InterleavingOne with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 0]) [])).
                        refl. refl. simpl. right. refl.
        SSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 1 []; LTS_State 1 []])).
          clear Infinite_ready_interleaving.
          exact H6.
      SCase "2/4 : Current state is not attainable. Proof by contradiction".
        clear -Case SCase H2. Focus.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3 as
             [Ha | [Ha | [Ha | Hf]]];
             try inversion Hf; inversion Ha; subst;
             clear H H0; inversion H4; clear - SCase SCase Case H;
        (assert (False);
          [ apply H; compute; auto | fromfalse]).
      SCase "3/4 : Current state is not attainable. Proof by contradiction".
        clear -Case SCase H2.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3 as
             [Ha | [Ha | [Ha | Hf]]];
             try inversion Hf; inversion Ha; subst;
             clear H H0; inversion H4; clear - SCase SCase Case H;
        (assert (False);
          [ apply H; compute; auto | fromfalse]).
      SSCase "4/4 : Current state is attainable".
        clear H2.
        unfold synch_vectors in H3.
        destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst;
        [ compute in H5; inversion H5 | idtac | idtac | try inversion Hf].
        SSSCase "1/2". Focus.
          compute in H5; inversion H5; [subst | fromfalse].
          clear H5.
          inversion H; subst. clear H.
        apply Always_LCons.
        SSSSCase "1/2 : interleaving". Focus.
          inversion H6; [discriminate | ..]; subst.
          SSSSSCase "1/2". Focus.
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 2)
       (Net_State [LTS_State 0 []; LTS_State 0 []])
             (<< "ready", "ready" >> -> "ready") = []).
          SSSSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSSSCase "absurd: True case".
            apply H3. left. auto.
        SSSSSCase "2/2".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          clear H3 H5.
          apply InterleavingTwo with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Sandwich" Emit []) []));
                        auto.
          refl. simpl. left; auto.
        SSSSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 0 []; LTS_State 0 []])).
          clear Infinite_ready_interleaving.
          exact H6.
        SSSCase "2/2".
        compute in H5.
        destruct H5 as
             [Ha | [Ha | [Ha | Hf]]];
             try inversion Hf; inversion Ha; clear Ha; subst.
        SSSSCase "1/9".
        apply Always_LCons.
        SSSSSCase "1/2 : interleaving". Focus.
          inversion H6; [discriminate | ..]; subst.
          SSSSSSCase "1/2". Focus.
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 2)
       (Net_State [LTS_State 0 []; LTS_State 0 []])
             (<< "ready", "ready" >> -> "ready") = []).
          SSSSSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSSSSCase "absurd: True case".
            apply H3. left. auto.
        SSSSSSCase "2/2".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          clear H3 H5.
          apply InterleavingTwo with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 2]) []));
                        auto.
          refl. simpl. right; auto.
        SSSSSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 0 []; LTS_State 0 []])).
          clear Infinite_ready_interleaving.
          exact H6.
        SSSSCase "2/9".
        apply Always_LCons.
        SSSSSCase "1/2 : interleaving". Focus.
          inversion H6; [discriminate | ..]; subst.
          SSSSSSCase "1/2". Focus.
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 2)
       (Net_State [LTS_State 0 []; LTS_State 0 []])
             (<< "ready", "ready" >> -> "ready") = []).
          SSSSSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSSSSCase "absurd: True case".
            apply H3. left. auto.
        SSSSSSCase "2/2".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          clear H3 H5.
          apply InterleavingTwo with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 1]) []));
                        auto.
          refl. simpl. right; auto.
        SSSSSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 0 []; LTS_State 0 []])).
          clear Infinite_ready_interleaving.
          exact H6.
        SSSSCase "3/9".
        apply Always_LCons.
        SSSSSCase "1/2 : interleaving". Focus.
          inversion H6; [discriminate | ..]; subst.
          SSSSSSCase "1/2". Focus.
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 2)
       (Net_State [LTS_State 0 []; LTS_State 0 []])
             (<< "ready", "ready" >> -> "ready") = []).
          SSSSSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSSSSCase "absurd: True case".
            apply H3. left. auto.
        SSSSSSCase "2/2".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          clear H3 H5.
          apply InterleavingTwo with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 0]) []));
                        auto.
          refl. simpl. right; auto.
        SSSSSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 0 []; LTS_State 0 []])).
          clear Infinite_ready_interleaving.
          exact H6.
Qed.

End InstantiatedExample.

Reasoning on a parametrized MasterSlaveCoffeeNet

Above, we demonstrated how we can reason about MasterSlaveCoffeeNet. Yet, we did it on an instantiated system. Clearly, it would be more interesting to do so on a parametrized system. Below, we show how we can reason about the same property on a non-instantiated system. Alas, there are still some auxiliary lemmas that are admitted. Yet, we informally discuss why we are confident of their veracity.

Lemma net_target_states_from_q0q0':
  forall sv n,
    In sv
      [
       << "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich";
       << "order:MakeCoffee", "MakeCoffee" >> -> "order:Coffee"] ->
    (get_list_snd
         (net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv0; mst0]) sv)) =
         [].
Proof.
  induction n; intros.
  Case "1/2: Base case". Focus.
    destruct H as [Hs | [Hc | Hf]]; try inversion Hf; subst; refl.
  Case "2/2: Induction step".
    assert (get_list_snd
        (net_target_states (MasterSlaveCoffeeNet n)
           (Net_State [slv0; mst0]) sv) = []).
      apply IHn; auto.
    clear IHn.
    rewrite <- H0.
    apply f_equal.
    apply f_equal. refl.
Qed.

Lemma net_target_states_from_q0q0:
  forall n,
    (get_list_snd
         (net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv0; mst0]) (<< "ready", "ready" >> -> "ready"))) =
         [Net_State [slv1; mst1]].
Proof.
  induction n; intros.
  Case "1/2: Base case".
    refl.
  Case "2/2: Induction step".
    rewrite <- IHn.
    apply f_equal.
    apply f_equal. refl.
Qed.

The above lemmas simply demonstrate that, from the initial state Net_State slv0; mst0, we can either reach Net_State [slv1; mst1], if using << "ready", "ready" >> -> "ready" as synchronization vector (lemma [net_target_states_from_q0q0]), or we do not reach any state if using other synchronization vectors (lemma [net_target_states_from_q0q0']).

Lemma MasterSlaveCoffeeNet_allowed_actions_from_q1q1_n_ready_fact:
   forall n,
     (allowed_actions_from_sv_element [slavelts n; masterlts n]
              [slv1; mst1] [sync_notation "ready"; sync_notation "ready"]) = [[]; []].
Proof.
  induction n; [refl|..].
  simpl in *.
  rewrite IHn. refl.
Qed.

Lemma net_target_states_from_q1q1':
  forall n,
    (net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv1; mst1])
    (<< "ready", "ready" >> -> "ready")) = [].
Proof.
  induction n; intros.
  Case "1/2: Base case".
    refl.
  Case "2/2: Induction step".
    unfold MasterSlaveCoffeeNet.
    unfold net_target_states;
    fold net_target_states.
    replace ((allowed_actions_from_sv_element [slavelts (S n); masterlts (S n)]
        [slv1; mst1] [sync_notation "ready"; sync_notation "ready"]))
    with [[]; (nil:actions)].
    SCase "Continue proof with replacement".
      refl.
    SCase "prove sound replacement".
      symmetry.
      apply MasterSlaveCoffeeNet_allowed_actions_from_q1q1_n_ready_fact.
Qed.

Lemma net_target_states_from_q1q1' states that, from Net_State slv1; mst1, we do not reach any state if using the ("ready", "ready"

Lemma allowed_actions_from_q1q1_sandwich_fact:
  forall n,
    (allowed_actions_from_sv_element [slavelts n; masterlts n]
         [slv1; mst1] [sync_notation "order:MakeSandwich"; sync_notation "MakeSandwich"]) =
    [[Action (Message "order:MakeSandwich" Read []) []];
     [Action (Message "MakeSandwich" Emit []) []]].
Proof.
  induction n; [refl | ..].
  simpl in *. rewrite IHn. refl.
Qed.

Lemma allowed_actions_from_q1q1_sandwich_fact follows the rationale of the MasterSlaveCoffeeNet_allowed_actions_from_q1q1_n_ready_fact lemma but w.r.t. the MakeSandwich action.

Set Implicit Arguments.
Inductive allowed_actions_from_q1q1_coffee :
                     nat -> list (list action) -> Prop :=
  | Coffee0: allowed_actions_from_q1q1_coffee 0
             [[Action (Message "order:MakeCoffee" Read [Val 0]) []];
             [Action (Message "MakeCoffee" Emit [Val 0]) []]]

  | CoffeeN: forall n (l:list (list action)) (lread lemit:list action),
             l = lread :: lemit :: nil ->
             forall lreadt lemitt,
             lread = Action (Message "order:MakeCoffee" Read [Val n]) [] :: lreadt->
             lemit = Action (Message "MakeCoffee" Emit [Val n]) [] :: lemitt ->
             allowed_actions_from_q1q1_coffee (n-1) [lreadt; lemitt] ->
             allowed_actions_from_q1q1_coffee n l.

Dealing with the action involving MakeCoffee requires a bit more care as it includes a parameter. Above, we defined the predicate allowed_actions_from_q1q1_coffee, defining the allowed MakeCoffee actions w.r.t. to the parameter n used for MasterSlaveCoffeeNet.

Lemma allowed_actions_from_sv_elements_coffee_fact:
  forall n,
  allowed_actions_from_q1q1_coffee n
    (allowed_actions_from_sv_element
      [slavelts n; masterlts n] [slv1; mst1]
      [sync_notation "order:MakeCoffee"; sync_notation "MakeCoffee"]).
Proof.
  induction n.
  Case "1/2".
    simpl. apply Coffee0.
  Case "2/2".
    unfold slv1 in *; unfold mst1 in *.
    simpl in *.
    eapply CoffeeN with
   (lread:=Action (Message "order:MakeCoffee" Read [Val (S n)]) []
          :: lts_allowed_actions_with_label (LTS_State 1 mem) (slave_transitions (nCoffeeOrders n)) (SyncElement "order:MakeCoffee"))
   (lemit:=Action (Message "MakeCoffee" Emit [Val (S n)]) []
  :: lts_allowed_actions_with_label (LTS_State 1 mem)
       (master_transitions (nMakeCoffeeOrders n)) (SyncElement "MakeCoffee")); auto.
  simpl.
  replace (n-0) with n.
  exact IHn. clear IHn.
  induction n; [refl | ..].
  rewrite IHn. simpl. refl.
Qed.

Lemma allowed_actions_from_sv_elements_coffee_fact depicts the first proof involving the allowed_actions_from_q1q1_coffee predicate.


Inductive valid_coffee_combination : nat -> list (list action) -> Prop :=
  | VC0: valid_coffee_combination 0 [[Action (Message "order:MakeCoffee" Read [Val 0]) [];
                                    Action (Message "MakeCoffee" Emit [Val 0]) []]]
| VCN: forall l h t n, l = h :: t ->
                       h = [Action (Message "order:MakeCoffee" Read [Val n]) [];
                            Action (Message "MakeCoffee" Emit [Val n]) [] ] ->
                       valid_coffee_combination (n-1) t ->
                       valid_coffee_combination n l.

The net_target_states function computes the combination of possible actions that may occur at each LTS (slavelts and masterlts) composing the Net object MasterSlaveCoffeeNet. The above predicate valid_coffee_combination specifies the valid combinations w.r.t. the MakeCoffee actions.

Lemma combineN_coffee_orders_fact:
  forall n l,
   allowed_actions_from_q1q1_coffee n l ->
   valid_coffee_combination n (exclude_incompatible_parameter_messages
                                 (treat_emissions (combineN l) [slv1; mst1])).
Proof.
Admitted.

As expected, we need to prove that, provided that we have allowed MakeCoffee actions, we can show that valid_coffee_combination for combination of compatible synchronized actions.
Proving this lemma is a bit tricky as it involves several definitions. Still, the main problem is that when doing induction on l, we dont quite get something useful w.r.t the allowed_actions_from_q1q1_coffee predicate...

Inductive all_the_same (X:Type) (e:X) : list X -> Prop :=
  | AllEmpty: all_the_same e nil
  | AllStep : forall h t l, l = h::t -> e=h -> all_the_same e t -> all_the_same e l.

As the name indicates, the all_the_same predicate defines lists whose elements are all equal to the parameter e. Below, we show a rather trivial fact that shall be useful at a later stage.

Lemma all_the_same_fact:
  forall (X:Type) (e:X) l,
    all_the_same e l ->
    forall x, In x l ->
    x=e.
Proof.
  induction l; intros.
  Case "1/2".
    fromfalse.
  Case "2/2".
    destruct H0; subst.
    SCase "1/2".
      inversion H; subst.
      inversion H0; subst; refl.
    SCase "2/2".
      apply IHl; auto.
      inversion H; subst.
      inversion H1; subst; auto.
Qed.

Lemma net_target_states_from_q1q1:
  forall sv n,
    In sv
      [
       << "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich";
       << "order:MakeCoffee", "MakeCoffee" >> -> "order:Coffee"] ->
    (all_the_same (Net_State [slv0; mst0]) (get_list_snd
         (net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv1; mst1]) sv))).
Proof.
  induction n; intros.
  Case "1/2: Base case".
    destruct H as [Hs | [Hc | Hf]]; try inversion Hf; subst; simpl;
    (eapply AllStep; eauto; apply AllEmpty).
  Case "2/2: Induction step".
    unfold MasterSlaveCoffeeNet in *.
    unfold net_target_states in *;
    fold net_target_states in *.
    destruct H as [Hs | [Hc | Hf]]; subst; try inversion Hf.
    SCase "Sandwich order".
      admit.
    SCase "Coffee order".
      pose (allowed_actions_from_sv_elements_coffee_fact (S n)) as Hf.
      pose (combineN_coffee_orders_fact Hf) as Hf2.
Admitted.

The above lemma net_target_states_from_q1q1 attempts to show that forall n, activating one of the synchronization vectors regarding the order of one kind of coffee or a sandwich, the Net_States that can be attained are all equal to Net_State slv0; mst0.
Establishing the subgoal for Sandwich orders should pose no special issue, as there is no parameter involved. For the Coffer order however, we need to use Hf2. From valid_coffee_combination we ought to be able to derive that we always attain Net_State slv0; mst0.

Lemma not_attainable_q0q0_q0q1:
  forall n, ~ attainable (MasterSlaveCoffeeNet n) [] (Net_State [slv0; mst0])
                       (Net_State [slv0; mst1]).
Proof.
  intro. intro. inversion H; subst. clear H0.
  inversion H1; subst.
  unfold synch_vectors in H2.
  destruct H2 as [Hr | Hr]; subst.
  Case "1/2 : Synch. vector ready". Focus.
    rewrite net_target_states_from_q0q0 in H4; auto.
    destruct H4 as [Hq1 | Hf]; [subst | fromfalse].
    inversion H5; subst. clear H0.
    inversion H2; subst.
    unfold synch_vectors in H3.
    destruct H3 as [Hr | Hr]; subst.
    rewrite net_target_states_from_q1q1' in H6; auto.
    assert (all_the_same (Net_State [slv0; mst0]) (get_list_snd
          (net_target_states (MasterSlaveCoffeeNet n)
             (Net_State [slv1; mst1]) sv))) as Hy.
      apply net_target_states_from_q1q1 with (sv:=sv) (n:=n); auto.
    assert (qn = Net_State [slv0; mst0]) as Hs.
      induction ((get_list_snd
          (net_target_states (MasterSlaveCoffeeNet n)
             (Net_State [slv1; mst1]) sv))); [fromfalse|..].
      destruct H6.
      SCase "Head case". Focus.
        subst.
        clear -Hy Case SCase.
        inversion Hy; subst. inversion H; subst; auto.
      SCase "Tail case".
        apply IHl; auto.
        inversion Hy. inversion H3; subst; auto.
    inversion H7; subst.
    discriminate H8.
    apply H0. compute. auto.
  Case "2/2 : Synch. vectors orders".
    rewrite net_target_states_from_q0q0' in H4; auto.
Qed.

Lemma not_attainable_q0q0_q1q0:
  forall n, ~ attainable (MasterSlaveCoffeeNet n) [] (Net_State [slv0; mst0])
                       (Net_State [slv1; mst0]).
Proof.
  intro. intro. inversion H; subst. clear H0.
  inversion H1; subst.
  unfold synch_vectors in H2.
  destruct H2 as [Hr | Hr]; subst.
  Case "1/2 : Synch. vector ready". Focus.
    rewrite net_target_states_from_q0q0 in H4; auto.
    destruct H4 as [Hq1 | Hf]; [subst | fromfalse].
    inversion H5; subst. clear H0.
    inversion H2; subst.
    unfold synch_vectors in H3.
    destruct H3 as [Hr | Hr]; subst.
    rewrite net_target_states_from_q1q1' in H6; auto.
    assert (qn = Net_State [slv0; mst0]) as Hs.
      pose (net_target_states_from_q1q1 n Hr ).
      eapply all_the_same_fact; eauto.
    subst.
    inversion H7; subst.
    clear - Case H0.
    apply H0. compute. auto.
  Case "2/2 : Synch. vectors orders".
    rewrite net_target_states_from_q0q0' in H4; auto.
Qed.

The two above lemmas, not_attainable_q0q0_q1q0 and not_attainable_q0q0_q0q1 simply show that we cannot attain these Net_States.

Lemma from_q1q1_target_states:
  forall n,
  net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv1; mst1])
  (<< "order:MakeCoffee", "MakeCoffee" >> -> "order:Coffee") <> [].
Proof.
  induction n. discriminate.
Admitted.

Lemma from_q0q0_target_states:
  forall n,
  net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv0; mst0])
  (<< "ready", "ready" >> -> "ready") <> [].
Proof.
  induction n; [discriminate | idtac].
  assert (
    (get_list_snd
         (net_target_states (MasterSlaveCoffeeNet (S n)) (Net_State [slv0; mst0]) (<< "ready", "ready" >> -> "ready"))) =
         [Net_State [slv1; mst1]]) as Ha.
    apply net_target_states_from_q0q0.
  intro.
  rewrite H in Ha.
  simpl in Ha. congruence.
Qed.

The above two lemmas from_q1q1_target_states and from_q0q0_target_states regard the fact that we necessarily reach Net_States, departing the the specified Net_State and activating the indicated SV.
Proving this kind of lemma involving the orders of Coffee is more complicated since it involves the parameter n.

Lemma net_target_states_fromq0q0_output:
  forall n,
  (net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv0; mst0])
  (<< "ready", "ready" >> -> "ready")) = ((Action (Message "ready" Emit nil) nil), Net_State [slv1; mst1]) :: nil.
Proof.
  induction n; intros.
  Case "1/2: Base case".
    refl.
  Case "2/2: Induction step".
    rewrite <- IHn.
    apply f_equal.
    apply f_equal. refl.
Qed.

The above lemma, net_target_states_fromq0q0_output acts a simple rewrite rule that we shall use below.

Lemma from_q0q0_target_states_interleaving:
  forall ga q' n l, In (ga, q')
       (net_target_states (MasterSlaveCoffeeNet n)
          (Net_State [slv0; mst0]) (<< "ready", "ready" >> -> "ready")) ->
          Net_Trace (MasterSlaveCoffeeNet n) q' l ->
        interleaving Rma "ready" "order" (LCons ga l).
Proof.
  intros.
  rewrite net_target_states_fromq0q0_output in H.
  destruct H as [Ha | Hf]; [inversion Ha; subst | fromfalse].
  clear Ha.
  inversion H0; subst.
  Case "1/3 : pLTS trace".
    discriminate.
  Case "2/3 : pNet empty trace". Focus.
    clear H3 H0.
    inversion H1; subst. clear H1.
    inversion H; subst. clear H.
    assert (net_target_states (MasterSlaveCoffeeNet n) (Net_State [slv1; mst1])
           (<< "order:MakeCoffee", "MakeCoffee" >> -> "order:Coffee") <> []) as Ha.
      apply from_q1q1_target_states.
    assert (False) as Hf.
      apply Ha. apply H4. right. right. left; auto.
    inversion Hf.
  Case "3/3 : pNet LCons trace".
    clear H3 H0.
Admitted.

Lemma from_q0q0_target_states_interleaving' sv:
  forall n,
  (sv = (<<"order:MakeSandwich", "MakeSandwich">> -> "order:Sandwich") \/
            sv = (<<"order:MakeCoffee" , "MakeCoffee">> -> "order:Coffee" )) ->
  (net_target_states (MasterSlaveCoffeeNet n)
          (Net_State [slv0; mst0]) sv) = [].
Proof.
Admitted.

Lemma from_q1q1_target_states_interleaving:
  forall ga q' n l, In (ga, q')
       (net_target_states (MasterSlaveCoffeeNet n)
          (Net_State [slv1; mst1]) (<< "ready", "ready" >> -> "ready")) ->
        interleaving Rma "ready" "order" (LCons ga l).
Proof.
  Admitted.

Lemma from_q1q1_target_states_interleaving' sv:
  forall n,
  (sv = (<<"order:MakeSandwich", "MakeSandwich">> -> "order:Sandwich") \/
            sv = (<<"order:MakeCoffee" , "MakeCoffee">> -> "order:Coffee" )) ->
  (net_target_states (MasterSlaveCoffeeNet n)
          (Net_State [slv1; mst1]) sv) = [].
Proof.
Admitted.

The above four lemmas, from_q0q0_target_states_interleaving, from_q0q0_target_states_interleaving', from_q1q1_target_states_interleaving and from_q1q1_target_states_interleaving' serve as helpers for our main goal, depicted below by theorem Infinite_ready_interleaving.
The function net_target_states returns values of type list (action * net_state), symbolizing the resulting global action, and the respective attained state. Since, one synchronization vector may trigger several actions among the constituents LTSs, we need to return a list.
This may not be the best solution for easing proofs. Perhaps using different data structures would facilitate proofs..
Below, directly or indirectly, we use the above lemmas to establish our main theorem.

Theorem Infinite_ready_interleaving:
  forall n t q,
   Net_Trace (MasterSlaveCoffeeNet n) q t ->
   t |= (Always (interleaving Rma "ready" "order")).
Proof.
  induction n;
  
  cofix;
  intros t q Ht.
  Case "Base case".
    inversion Ht.
    SCase "1/3".
      clear Ht.
      discriminate H0.
    SCase "2/3". Focus.
      clear Ht.
      inversion H; subst. clear H.
      unfold synch_vectors in *.
      inversion H1; [discriminate | subst].
      inversion H0 ;subst. clear H0.
      inversion H5; [discriminate | subst].
      inversion H0; subst. clear H0.
      inversion H7; [subst | discriminate].
      clear H5 H7 H0 H1.
      destruct H4 as [Hs0 | [Hs1 | Hf]]; subst; try inversion Hf;
      destruct H6 as [Hm0 | [Hm1 | Hf']]; subst; try inversion Hf'.
      SSCase "1/4 : Current state is attainable, but no valid synch. vectors".
        absurd (net_target_states (MasterSlaveCoffeeNet 0) (Net_State [slv0; mst0])
             (<< "ready", "ready" >> -> "ready") = []).
        SSSCase "absurd: False case".
          simpl; discriminate.
        SSSCase "absurd: True case".
          apply H3. left; auto.
      SSCase "2/4: Current state is not attainable. Proof by contradiction". Focus.
        clear -SSCase SCase Case H2.
        simpl in H2.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
      SSCase "3/4: Current state is not attainable. Proof by contradiction". Focus.
        clear -SSCase SCase Case H2.
        simpl in H2.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
      SSCase "4/4: Current state is attainable, but no valid synch. vectors". Focus.
        absurd (net_target_states (MasterSlaveCoffeeNet 0) (Net_State [slv1; mst1])
             (<< "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich") = []).
        SSSCase "absurd: False case".
          simpl; discriminate.
        SSSCase "absurd: True case".
          apply H3. right. left; auto.
    SCase "3/3". Focus.
      clear Ht. subst.
      inversion H; subst. clear H.
      inversion H1; [discriminate | subst]. clear H1.
      inversion H0; subst. clear H0.
      inversion H7; [discriminate | subst].
      inversion H0; subst.
      inversion H8; [subst | discriminate].
      clear H0 H9 H8 H7.
      simpl in H4; simpl in H1.
      simpl in H2.
      destruct H1 as [Hs0 | [Hs1 | Hf]]; subst; try inversion Hf;
      destruct H4 as [Hm0 | [Hm1 | Hf']]; subst; try inversion Hf'.
      SSCase "1/4 : Current state is attainable". Focus.
        clear H2.
        unfold synch_vectors in H3.
        destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst;
        try inversion Hf; compute in H5; inversion H5;
        [ subst | fromfalse]. clear H5.
        inversion H; subst. clear H.
        apply Always_LCons.
        SSSCase "1/2 : interleaving". Focus.
          inversion H6; subst.
          SSSSCase "1/3".
            discriminate.
          SSSSCase "2/3".
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 0)
       (Net_State [LTS_State 1 []; LTS_State 1 []])
             (<< "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich") = []).
          SSSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSSCase "absurd: True case".
            apply H3. right. left. auto.
        SSSSCase "3/3".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          SSSSSCase "1/2 : Synch. Vector order sandwich".
            clear H3 H5.
            apply InterleavingOne with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Sandwich" Emit []) []));
                        auto.
            refl. simpl. left; auto.
          SSSSSCase "2/2 : Synch. Vector order coffee".
            apply InterleavingOne with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 0]) [])).
                        refl. refl. simpl. right. refl.
        SSSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 1 []; LTS_State 1 []])).
          clear Infinite_ready_interleaving.
          exact H6.
      SSCase "2/4 : Current state is not attainable. Proof by contradiction".
        clear -Case SCase SSCase H2.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
      SSCase "3/4 : Current state is not attainable. Proof by contradiction".
        clear -Case SCase SSCase H2.
        inversion H2; subst.
        inversion H0; subst. clear H0.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse. clear H2 H.
        destruct H4; [subst| fromfalse].
        inversion H5; subst. clear H H5.
        inversion H0; subst.
        unfold synch_vectors in H1.
        destruct H1 as [Hr | [Hs | [Hc| Hf]]]; try inversion Hf; subst;
        simpl in *; try fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
        destruct H3; [subst | fromfalse].
        clear H0. inversion H4. clear - SSCase SCase Case H.
        assert (False).
          apply H. compute. auto.
        fromfalse.
      SSCase "4/4 : Current state is attainable".
        clear H2.
        unfold synch_vectors in H3.
        destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst;
        [ compute in H5; inversion H5 | idtac | idtac | try inversion Hf].
        SSSCase "1/2". Focus.
          compute in H5; inversion H5; [subst | fromfalse].
          clear H5.
          inversion H; subst. clear H.
        apply Always_LCons.
        SSSSCase "1/2 : interleaving". Focus.
          inversion H6; [discriminate | ..]; subst.
          SSSSSCase "1/2". Focus.
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 0)
       (Net_State [LTS_State 0 []; LTS_State 0 []])
             (<< "ready", "ready" >> -> "ready") = []).
          SSSSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSSSCase "absurd: True case".
            apply H3. left. auto.
        SSSSSCase "2/2".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          clear H3 H5.
          apply InterleavingTwo with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Sandwich" Emit []) []));
                        auto.
          refl. simpl. left; auto.
        SSSSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 0 []; LTS_State 0 []])).
          clear Infinite_ready_interleaving.
          exact H6.
        SSSCase "2/2". Focus.
        compute in H5; inversion H5; [subst | fromfalse].
          clear H5.
          inversion H; subst. clear H.
        apply Always_LCons.
        SSSSCase "1/2 : interleaving". Focus.
          inversion H6; [discriminate | ..]; subst.
          SSSSSCase "1/2". Focus.
            inversion H; subst.
            unfold synch_vectors in *.
            absurd (net_target_states (MasterSlaveCoffeeNet 0)
       (Net_State [LTS_State 0 []; LTS_State 0 []])
             (<< "ready", "ready" >> -> "ready") = []).
          SSSSSSCase "absurd: False case".
            simpl. discriminate.
          SSSSSSCase "absurd: True case".
            apply H3. left. auto.
        SSSSSCase "2/2".
          inversion H; subst.
          unfold synch_vectors in H3.
          destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst; try inversion Hf;
          simpl in H5; inversion H5; subst; try fromfalse;
          inversion H3; subst.
          clear H3 H5.
          apply InterleavingTwo with (l':=l0)
                        (a':=(Action (Message "ready" Emit []) []))
                        (b':=(Action (Message "order:Coffee" Emit [Val 0]) []));
                        auto.
          refl. simpl. right; auto.
        SSSSCase "2/2 : Recursion".
          apply Infinite_ready_interleaving with
                (q:=(Net_State [LTS_State 0 []; LTS_State 0 []])).
          clear Infinite_ready_interleaving.
          exact H6.
  Case "2/2 : Induction step".
    inversion Ht; subst.
    SCase "1/3 : pLTS trace => proof by contradiction".
      discriminate H0.
    SCase "2/3 : pNet Empty trace => proof by contradiction". Focus.
      inversion H; subst. clear H.
      unfold synch_vectors in *.
      inversion H1; [discriminate | subst].
      inversion H0 ;subst. clear H0.
      inversion H5; [discriminate | subst].
      inversion H0; subst. clear H0.
      inversion H7; [subst | discriminate].
      clear H5 H7 H0 H1.
      destruct H4 as [Hs0 | [Hs1 | Hf]]; subst; try inversion Hf;
      destruct H6 as [Hm0 | [Hm1 | Hf']]; subst; try inversion Hf'.
      SSCase "1/4 : Current state is attainable, but no valid synch. vectors". Focus.
        absurd (net_target_states (MasterSlaveCoffeeNet (S n)) (Net_State [slv0; mst0])
             (<< "ready", "ready" >> -> "ready") = []).
        SSSCase "absurd: False case".
          apply from_q0q0_target_states.
        SSSCase "absurd: True case".
          apply H3. left; auto.
      SSCase "2/4: Current state is not attainable. Reductio ad absurdum". Focus.
        clear -SSCase SCase Case H2.
        absurd (attainable (MasterSlaveCoffeeNet (S n)) []
                (init_net_state (MasterSlaveCoffeeNet (S n)))
                (Net_State [slv0; mst1])); auto.
          apply not_attainable_q0q0_q0q1.
      SSCase "3/4: Current state is not attainable. Reductio ad absurdum". Focus.
        clear -SSCase SCase Case H2.
        absurd (attainable (MasterSlaveCoffeeNet (S n)) []
                (init_net_state (MasterSlaveCoffeeNet (S n)))
                (Net_State [slv1; mst0])); auto.
          apply not_attainable_q0q0_q1q0.
      SSCase "4/4 : Current state is attainable, but no valid synch. vectors".
        clear H2.
        absurd (net_target_states (MasterSlaveCoffeeNet (S n))
          (Net_State [slv1; mst1])
          (<< "order:MakeCoffee", "MakeCoffee" >> -> "order:Coffee") = []);
        [idtac | apply H3; intuition].
        apply from_q1q1_target_states.
    SCase "3/3 : pNet LCons trace". Focus.
      clear Ht.
      inversion H; subst. clear H.
      inversion H1; [discriminate | subst]. clear H1.
      inversion H0; subst. clear H0.
      inversion H7; [discriminate | subst].
      inversion H0; subst.
      inversion H8; [subst | discriminate].
      clear H0 H9 H8 H7.
      simpl in H4; simpl in H1.
      simpl in H2.
      destruct H1 as [Hs0 | [Hs1 | Hf]]; subst; try inversion Hf;
      destruct H4 as [Hm0 | [Hm1 | Hf']]; subst; try inversion Hf'.
      SSCase "1/4 : Current state is attainable". Focus.
        clear H2.
        unfold synch_vectors in H3.
        destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst;
        try inversion Hf.
        SSSCase "1/3 : Synch. vector: ready". Focus.
          apply Always_LCons;
            [ idtac
            | apply Infinite_ready_interleaving with (q:=q'); exact H6 ].
          clear Infinite_ready_interleaving.
          apply from_q0q0_target_states_interleaving with
                  (n:=S n) (q':=q'); auto.
        SSSCase "2/3 : Synch. vector: makesandwich".
          rewrite from_q0q0_target_states_interleaving' with
             (sv:=(<< "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich")) in H5.
          fromfalse.
          left. refl.
        SSSCase "3/3 : Synch. vector: makeCoffee".
          rewrite from_q0q0_target_states_interleaving' with
             (sv:=(<< "order:MakeCoffee", "MakeCoffee" >> -> "order:Coffee")) in H5.
          fromfalse.
          right. refl.
      SSCase "2/4 : Current state is not attainable".
        clear - Case SCase SSCase H2.
        apply not_attainable_q0q0_q1q0 in H2.
        fromfalse.
      SSCase "3/4 : Current state is not attainable".
        clear - Case SCase SSCase H2.
        apply not_attainable_q0q0_q0q1 in H2.
        fromfalse.
      SSCase "4/4 : Current state is attainable".
        clear H2.
        unfold synch_vectors in H3.
        destruct H3 as [Hr | [Hs | [Hc | Hf]]]; subst;
        try inversion Hf.
        SSSCase "1/3 : Synch. vector: ready". Focus.
          apply Always_LCons;
            [ idtac
            | apply Infinite_ready_interleaving with (q:=q'); exact H6 ].
          clear Infinite_ready_interleaving.
          apply from_q1q1_target_states_interleaving with
                  (n:=S n) (q':=q'); auto.
        SSSCase "2/3 : Synch. vector: makesandwich".
          rewrite from_q1q1_target_states_interleaving' with
             (sv:=(<< "order:MakeSandwich", "MakeSandwich" >> -> "order:Sandwich")) in H5.
          fromfalse.
          left. refl.
        SSSCase "3/3 : Synch. vector: makeCoffee".
          rewrite from_q1q1_target_states_interleaving' with
             (sv:=(<< "order:MakeCoffee", "MakeCoffee" >> -> "order:Coffee")) in H5.
          fromfalse.
          right. refl.
Qed.