Mefresa.Examples.AutonomicUseCase

Structural Reconfigurations: ICAS'2009 use case

For this example we will need to load a previously discussed example regarding the approach for coping with parametrized architectures.

Require Import Mefresa.Examples.ParamSpec.

Below, we model the scenario presented in 1, where structural reconfigurations were used to balance the saving of power consumption with a good quality of service.

1 Francoise Baude and Ludovic Henrio and Paul Naoumenko. Structural reconfiguration : an autonomic strategy for GCM components. ICAS 2009

Architecture modelling

Let us start by the modelling of the use case architecture

Definition p1 := Ident "Lights Control" :: Ident "Switched On Lights" :: nil.

Definition interfaces_LightComp :=
  Interface (Ident "Get") "" (app p1 ((Ident "Street Light")::nil)) External Server Functional Mandatory Singleton :: nil.

Definition LightComp :=
  Component (Ident "Street Light") p1 default_class Configuration nil interfaces_LightComp nil.

Definition p2 := Ident "Lights Control" :: Ident "Sensed Brightness Info" :: nil.
Definition interfaces_BrightComp :=
   Interface (Ident "Get") "" (app p2 ((Ident "Brightness Info")::nil)) External Server Functional Mandatory Singleton :: nil.

Definition interfaces_LCC :=
  Interface (Ident "Light Info") "" (app p1 ((Ident "Light Collector")::nil)) External Server Functional Mandatory Singleton ::
  Interface (Ident "Collect Light Info") "" (app p1 ((Ident "Light Collector")::nil)) External Client Functional Mandatory Singleton ::
  nil.

Definition LCC :=
  Component (Ident "Light Collector") p1 default_class Configuration nil interfaces_LCC nil.

Definition BrightComp :=
  Component (Ident "Brightness Info") p2 default_class Configuration nil interfaces_BrightComp nil.

Definition interfaces_SwonLights :=
  Interface (Ident "Light Info") "" p1 External Server Functional Mandatory Singleton ::
  Interface (Ident "Light Info") "" p1 Internal Client Functional Mandatory Singleton ::
  Interface (Ident "Add/Remove Light") "" p1 External Server Control Mandatory Singleton ::

  nil.

Definition b7 := Export (Ident "Lights Control" :: Ident "Switched On Lights" :: nil)
                        (Ident "Light Info")
                        (Ident "Light Collector") (Ident "Light Info").

Definition SwonLights :=
  Component (Ident "Switched On Lights") (Ident "Lights Control" :: nil)
            default_class Configuration (LCC ::nil) interfaces_SwonLights (b7 ::nil).

Definition interfaces_BRINFOCOLL :=
  Interface (Ident "Sensor Info") "" (app p2 ((Ident "Brightness Info Collector")::nil)) External Server Functional Mandatory Singleton ::
  Interface (Ident "Collect Sensor Info") "" (app p2 ((Ident "Brightness Info Collector")::nil)) External Client Functional Mandatory Singleton ::
  nil.

Definition BRINFOCOLL :=
  Component (Ident "Brightness Info Collector") p2 default_class Configuration nil interfaces_BRINFOCOLL nil.

Definition interfaces_SensedBrInfo :=
  Interface (Ident "Brightness Info") "" p1 External Server Functional Mandatory Singleton ::
  Interface (Ident "Brightness Info") "" p1 Internal Client Functional Mandatory Singleton ::
  Interface (Ident "Add/Remove Brightness Info") "" p1 External Server Control Mandatory Singleton ::

  nil.

Definition b3 := Export (Ident "Lights Control" :: Ident "Sensed Brightness Info" :: nil)
                        (Ident "Brightness Info")
                        (Ident "Brightness Info Collector") (Ident "Sensor Info").
Definition b4 := Normal (Ident "Lights Control" :: Ident "Sensed Brightness Info" :: nil)
                        (Ident "Brightness Info Collector") (Ident "Collect Sensor Info")
                        (Ident "Brightness Info1") (Ident "Get").
Definition b5 := Normal (Ident "Lights Control" :: Ident "Sensed Brightness Info" :: nil)
                        (Ident "Brightness Info Collector") (Ident "Collect Sensor Info")
                        (Ident "Brightness Info2") (Ident "Get").
Definition b6 := Normal (Ident "Lights Control" :: Ident "Sensed Brightness Info" :: nil)
                        (Ident "Brightness Info Collector") (Ident "Collect Sensor Info")
                        (Ident "Brightness Info3") (Ident "Get").

Definition SensedBrInfo :=
  Component (Ident "Sensed Brightness Info") (Ident "Lights Control" :: nil)
            default_class Configuration
            (BRINFOCOLL :: (generate_from_template BrightComp 3) )
            interfaces_SensedBrInfo
            (b3 ::b4 ::b5 ::b6 ::nil).

Definition interfaces_LightControlComp :=
  Interface (Ident "Collect Brightness Info") "" (Ident "Lights Control" :: nil) External Server Functional Mandatory Singleton ::
  Interface (Ident "Collect Brightness Info") "" (Ident "Lights Control" :: nil) Internal Client Functional Mandatory Singleton ::
  Interface (Ident "Collect Light Info") "" (Ident "Lights Control" :: nil) External Server Functional Mandatory Singleton ::
  Interface (Ident "Collect Light Info") "" (Ident "Lights Control" :: nil) Internal Client Functional Mandatory Singleton ::
  nil.

Definition b1 := Export (Ident "Lights Control" :: nil)
                        (Ident "Collect Brightness Info")
                        (Ident "Sensed Brightness Info") (Ident "Brightness Info").
Definition b2 := Export (Ident "Lights Control" :: nil)
                        (Ident "Collect Light Info")
                        (Ident "Switched On Lights") (Ident "Light Info").

Definition LightControlComp :=
  Component (Ident "Lights Control") nil default_class Configuration

            (SwonLights :: SensedBrInfo :: nil)

            interfaces_LightControlComp

            (b1 ::b2 ::nil).

The scenario starts with the creation of the component system. At the beginning there are no LIGHTCOMP in the SWONLIGHTS, as we suppose that no light has been switched on. Further, we consider that already three existing BRIGHTCOMPs in the SENSEDBRINFO.

Definition LightsControlUseCaseArchitecture :=
Component (Ident "Root") root "null" Configuration (LightControlComp ::nil) nil nil.

Proving well-formedness

We can prove that this initial configuration is indeed well formed in the following manner.

Lemma LightsControlUseCase_is_well_formed:
  well_formed LightsControlUseCaseArchitecture.
Proof.
  firstorder.
  apply WellFormedComponent; simpl; intros; auto.
  inversion H; try fromfalse.
  subst.
  clear.
  apply WellFormedComponent; simpl; intros.
  Case "Well Formed Sub Components".
    Focus.
    destruct H as [H1 | [H2 | H3]]; subst.
    SCase "Well Formed SwonLights".
      Focus.
      unfold SwonLights.
      apply WellFormedComponent; simpl; intros; auto.
      Focus.
      destruct H; try fromfalse; subst.
      SSCase "Well Formed SwonLights Sub Components".
        unfold LCC.
        apply WellFormedComponent; simpl; intros; auto; try fromfalse.
        unfold interfaces_LCC.
        apply WellFormedInterfaces_Step with
          (i:=Interface (Ident "Light Info") "" (p1 ++ Ident "Light Collector" :: nil)%list External Server Functional Mandatory Singleton)
          (r:=Interface (Ident "Collect Light Info") "" (p1 ++ Ident "Light Collector" :: nil)%list External Client Functional Mandatory Singleton :: nil); auto.
        SSSCase "Interfaces have unique Id x Acc pair".
          apply UniquePairs_Step with (int:=Interface (Ident "Light Info") "" (p1 ++ Ident "Light Collector" :: nil)%list External Server Functional Mandatory Singleton)
                                      (r:=Interface (Ident "Collect Light Info") "" (p1 ++ Ident "Light Collector" :: nil)%list External Client Functional Mandatory Singleton :: nil); simpl; auto.
          SSSSCase "Not In in the Remaining of the List".
            eapply NotInPairStep; auto.
            apply NotInPair_Nil; auto.
          SSSSCase "Unique Pairs".
            eapply UniquePairs_Step;auto; simpl.
            apply NotInPair_Nil; auto.
            apply UniquePairs_Base;auto.
        SSSCase "Well Formed LCC Interfaces".
          eapply WellFormedInterfaces_Step; auto.
          eapply UniquePairs_Step; auto; simpl.
          apply NotInPair_Nil;auto.
          apply UniquePairs_Base; auto.
      SSCase "Well Formed SwonLights Interfaces".
        unfold interfaces_SwonLights. Focus.
        eapply WellFormedInterfaces_Step; auto.
        eapply UniquePairs_Step; auto; simpl.
        eapply NotInPairStep; auto.
        eapply NotInPairStep; auto.
        eapply NotInPair_Nil;auto.
        eapply UniquePairs_Step; auto; simpl.
        eapply NotInPairStep; auto.
        eapply NotInPair_Nil;auto.
        eapply UniquePairs_Step; auto; simpl.
        eapply NotInPair_Nil;auto.
        eapply UniquePairs_Base; auto.
        eapply WellFormedInterfaces_Step; auto.
        eapply UniquePairs_Step; auto; simpl.
        eapply NotInPairStep; auto.
        eapply NotInPair_Nil;auto.
        eapply UniquePairs_Step; auto; simpl.
        eapply NotInPair_Nil;auto.
        eapply UniquePairs_Base; auto.
        eapply WellFormedInterfaces_Step; auto.
        eapply UniquePairs_Step; auto; simpl.
        eapply NotInPair_Nil;auto.
        eapply UniquePairs_Base; auto.
     SSCase "Well Formed SwonLights Bindings".
       intro; intro.
       destruct H; subst; try fromfalse.
       unfold b7; simpl.
       unfold interfaces_SwonLights.
       unfold LCC. unfold interfaces_LCC.
       unfold p1.
       simpl.
       unfold export_binding; simpl; auto.
   SCase "Well Formed Sub Component SensedBrInfo".
     unfold SensedBrInfo.
     apply WellFormedComponent; intros.
     SSCase "Well Formed Sub Components".
       destruct H; subst.
       SSSCase "Well Formed BRINFOCOLL".
         unfold BRINFOCOLL.
         apply WellFormedComponent; simpl; intros; auto; try inversion H.
         unfold interfaces_BRINFOCOLL.
         eapply WellFormedInterfaces_Step; auto.
         SSSSCase "Unique Pair Id x Acc".
           eapply UniquePairs_Step; auto; simpl.
           eapply NotInPairStep; auto.
           eapply NotInPair_Nil; auto.
           eapply UniquePairs_Step; auto; simpl.
           eapply NotInPair_Nil;auto.
           eapply UniquePairs_Base;auto.
           eapply WellFormedInterfaces_Step;auto.
           eapply UniquePairs_Step;auto; simpl.
           eapply NotInPair_Nil;auto.
           eapply UniquePairs_Base;auto.
      SSSCase "Well Formed Generated Components".
        assert (well_formed_component BrightComp).
          Focus.
          unfold BrightComp.
          apply WellFormedComponent; simpl; intros; auto; try inversion H0.
          unfold interfaces_BrightComp.
          apply WellFormedInterfaces_Step with
                (i:=Interface (Ident "Get") "" (p2 ++ Ident "Brightness Info" :: nil)%list External Server Functional Mandatory Singleton)
                (r:=nil);auto.
          eapply UniquePairs_Step; auto; simpl.
          eapply NotInPair_Nil; auto.
          eapply UniquePairs_Base;auto.
        assert (well_formed_components (generate_from_template BrightComp 3)).
          apply template_generation_produces_well_formed_components with (c:=BrightComp) (n:=3);auto.
        eauto.
    SSCase "Unique Ids of SensedBrInfo Sub Components".
      change ((Component (Ident "Sensed Brightness Info")
     (Ident "Lights Control" :: nil) default_class Configuration
     (BRINFOCOLL :: generate_from_template BrightComp 3)
     interfaces_SensedBrInfo (b3 :: b4 :: b5 :: b6 :: nil) ->subComponents)%comp) with (BRINFOCOLL :: generate_from_template BrightComp 3).
     eapply Unique_Step;auto.
     SSSCase "Id of the Head does not clash with the Remaining".
       unfold BRINFOCOLL.
       change (Component (Ident "Brightness Info Collector") p2 default_class Configuration nil
       interfaces_BRINFOCOLL nil ->id)%comp with (Ident "Brightness Info Collector") .
       simpl.
       eapply NotInStep; auto.
       eapply NotInStep; auto.
       eapply NotInStep; auto.
     SSSCase "Unique Ids of the Remaining".
       unfold BrightComp.
       simpl.
       eapply Unique_Step;auto.
       eapply NotInStep; auto.
       eapply NotInStep; auto.
       eapply Unique_Step;auto.
       eapply NotInStep; auto.
   SSCase "Well Formed SensedBrInfo Interfaces".
     simpl.
     unfold interfaces_SensedBrInfo.
     eapply WellFormedInterfaces_Step; auto.
     SSSCase "Unique Pairs Id x Acc".
       eapply UniquePairs_Step;auto;simpl.
       eapply NotInPairStep;auto.
       eapply NotInPairStep;auto.
       eapply NotInPair_Nil;auto.
       eapply UniquePairs_Step;auto;simpl.
       eapply NotInPairStep;auto.
       eapply NotInPair_Nil;auto.
       eapply UniquePairs_Step;auto;simpl.
       eapply NotInPair_Nil;auto.
       eapply UniquePairs_Base;auto.
       eapply WellFormedInterfaces_Step; auto.
       eapply UniquePairs_Step;auto;simpl.
       eapply NotInPairStep;auto.
       eapply NotInPair_Nil;auto.
       eapply UniquePairs_Step;auto;simpl.
       eapply NotInPair_Nil;auto.
       eapply UniquePairs_Base;auto.
       eapply WellFormedInterfaces_Step; auto.
       eapply UniquePairs_Step;auto;simpl.
       eapply NotInPair_Nil;auto.
       eapply UniquePairs_Base;auto.
   SSCase "Well Formed SensedBrInfo Bindings".
     Focus.
     change (well_formed_bindings
  (Component (Ident "Sensed Brightness Info")
     (Ident "Lights Control" :: nil) default_class Configuration
     (BRINFOCOLL :: generate_from_template BrightComp 3)
     interfaces_SensedBrInfo (b3 :: b4 :: b5 :: b6 :: nil) ->bindings)%comp
  (Component (Ident "Sensed Brightness Info")
     (Ident "Lights Control" :: nil) default_class Configuration
     (BRINFOCOLL :: generate_from_template BrightComp 3)
     interfaces_SensedBrInfo (b3 :: b4 :: b5 :: b6 :: nil) ->subComponents)%comp
  (Component (Ident "Sensed Brightness Info")
     (Ident "Lights Control" :: nil) default_class Configuration
     (BRINFOCOLL :: generate_from_template BrightComp 3)
     interfaces_SensedBrInfo (b3 :: b4 :: b5 :: b6 :: nil) ->interfaces)%comp) with
     (well_formed_bindings (b3 :: b4 :: b5 :: b6 :: nil) (BRINFOCOLL :: generate_from_template BrightComp 3) interfaces_SensedBrInfo).
     intro; intro.
     destruct H as [Hb3 | [Hb4 | [Hb5| [ Hb6 | Hbnil ]]]]; subst.
     SSSCase "b3 is a Valid Binding".
       unfold b3; unfold BRINFOCOLL; unfold interfaces_SensedBrInfo; simpl.
       unfold interfaces_BRINFOCOLL; simpl.
       unfold export_binding.
       simpl; auto.
     SSSCase "b4 is a Valid Binding".
       unfold generate_from_template; unfold BrightComp; simpl.
       unfold nat_to_string; simpl.
       unfold normal_binding; simpl; auto.
     SSSCase "b5 is a Valid Binding".
       unfold generate_from_template; unfold BrightComp; simpl.
       unfold nat_to_string; simpl.
       unfold normal_binding; simpl; auto.
     SSSCase "b6 is a Valid Binding".
       unfold generate_from_template; unfold BrightComp; simpl.
       unfold nat_to_string; simpl.
       unfold normal_binding; simpl; auto.
     SSSCase "Congruence of binding".
       inversion Hbnil.
    SCase "Component does not Exit".
      inversion H3.
  Case "Unique Ids".
    unfold SwonLights; unfold SensedBrInfo;
    eapply Unique_Step; simpl; auto.
    unfold nat_to_string; simpl.
    eapply NotInStep; auto.
  Case "Well Formed Interfaces".
    unfold interfaces_LightControlComp. Focus.
    eapply WellFormedInterfaces_Step;auto.
    SCase "Unique Pair Id x Acc".
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPairStep;auto.
      eapply NotInPairStep;auto.
      eapply NotInPairStep;auto.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPairStep;auto.
      eapply NotInPairStep;auto.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPairStep;auto.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Base;auto.
      eapply WellFormedInterfaces_Step;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPairStep;auto.
      eapply NotInPairStep;auto.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPairStep;auto.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Base;auto.
      eapply WellFormedInterfaces_Step;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPairStep;auto.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Base;auto.
      eapply WellFormedInterfaces_Step;auto.
      eapply UniquePairs_Step;auto;simpl.
      eapply NotInPair_Nil;auto.
      eapply UniquePairs_Base;auto.
  Case "Well Formed Bindings".
    unfold b1; unfold b2; unfold SwonLights;
    unfold SensedBrInfo; unfold interfaces_LightControlComp;
    simpl; auto.
    unfold nat_to_string; simpl.
    intro; intro.
    destruct H as [Hb1 | [Hb2 | HbNil]]; subst;
    unfold interfaces_SwonLights;
    unfold interfaces_SensedBrInfo; simpl.
    unfold export_binding; simpl; auto.
    unfold export_binding; simpl; auto.
    inversion HbNil.
Qed.

Handling reconfigurations

Setting up the scene

Having our initial architecture proved well formed by theorem LightsControlUseCase_is_well_formed, we can now proceed to a structural reconfiguration.

First, we shall define some high level operations.

Function Mk_normal_multicast (p:path)
                   (icc:ident) (iic:ident)
                   (ics:ident) (n:nat) (iis:ident) : operation :=
  match n with
    0 => Done
  | 1 => Mk_binding (Normal p icc iic (suffix_ident ics 1) iis)
  | S m => (Mk_binding (Normal p icc iic (suffix_ident ics n) iis)) ;
           Mk_normal_multicast p icc iic ics m iis
  end.

Function Mk_components (lc: list component) : operation :=
  match lc with
    nil => Done
  | Component i p ic cl lc li lb :: r =>
     (Mk_component i p ic cl lc li lb) ;
     Mk_components r
  end.

The purpose of the above operations ,Mk_components and Mk_normal_multicast, should raise no doubt. We can put them in operation by the following manner.

Function add_lights_reconfig (n:nat) : operation :=
  Mk_components (generate_from_template LightComp n);
  Mk_normal_multicast (LCC ->path%comp)
                      (LCC ->id%comp) (Ident "Collect Light Info")
                      (LightComp ->id%comp) n (Ident "Get").

Proving the reconfiguration correct

Lemma adding_3_lights:
   exists s, add_lights_reconfig 3 / LightsControlUseCaseArchitecture ~~~>* Done / s.
Proof.
  eexists.
  unfold add_lights_reconfig; simpl.
  unfold nat_to_string; simpl.
  eapply rsc_step.
  apply SSeq1.
  apply SSeq2.
  apply SMakeComponent; intuition.
  unfold p1; unfold LightsControlUseCaseArchitecture.
  unfold valid_component_path; simpl.
  unfold LightControlComp.
  unfold b1; unfold b2.
  unfold SwonLights; unfold SensedBrInfo.
  unfold interfaces_SwonLights; unfold interfaces_LightControlComp.
  simpl.
  unfold nat_to_string; simpl.
  unfold interfaces_SensedBrInfo; simpl.
  unfold BRINFOCOLL; simpl.
  eapply ValidN; auto.
  simpl.
  exists LightControlComp.
  simpl. auto.
  refl.
  simpl in *.
  eapply ValidN; auto.
  exists SwonLights. simpl.
  auto.
  simpl; auto.
  apply WellFormedComponent; simpl; auto; intros; try fromfalse.
  eapply WellFormedInterfaces_Step; auto.
  eapply UniquePairs_Step; auto; simpl.
  apply NotInPair_Nil; auto.
  apply UniquePairs_Base; auto.
  unfold no_id_clash; intros.
  unfold LightsControlUseCaseArchitecture in H;
  unfold p1 in H.
  simpl in *.
  inversion H; subst.
  unfold LCC.
  eapply NotInStep; auto.
  eapply rsc_step.
  apply SSeq1.
  apply SSeq2.
  apply SMakeComponent; intuition.
  unfold p1; unfold LightsControlUseCaseArchitecture.
  unfold valid_component_path; simpl.
  unfold LightControlComp.
  unfold b1; unfold b2.
  unfold SwonLights; unfold SensedBrInfo.
  unfold interfaces_SwonLights; unfold interfaces_LightControlComp.
  simpl.
  unfold nat_to_string; simpl.
  unfold interfaces_SensedBrInfo; simpl.
  unfold BRINFOCOLL; simpl.
  eapply ValidN; auto.
  simpl.
  exists LightControlComp.
  simpl. auto.
  refl.
  simpl in *.
  eapply ValidN; auto.
  exists SwonLights. simpl.
  auto.
  simpl; auto.
  apply WellFormedComponent; simpl; auto; intros; try fromfalse.
  eapply WellFormedInterfaces_Step; auto.
  eapply UniquePairs_Step; auto; simpl.
  apply NotInPair_Nil; auto.
  apply UniquePairs_Base; auto.
  unfold no_id_clash; intros.
  unfold LightsControlUseCaseArchitecture in H;
  unfold p1 in H.
  simpl in *.
  inversion H; subst.
  clear H.
  unfold LCC.
  eapply NotInStep; auto.
  eapply NotInStep; auto.
  eapply rsc_step.
  apply SSeq1.
  mstep.
  unfold p1; unfold LightsControlUseCaseArchitecture.
  unfold valid_component_path; simpl.
  unfold LightControlComp.
  unfold b1; unfold b2.
  unfold SwonLights; unfold SensedBrInfo.
  unfold interfaces_SwonLights; unfold interfaces_LightControlComp.
  simpl.
  unfold nat_to_string; simpl.
  unfold interfaces_SensedBrInfo; simpl.
  unfold BRINFOCOLL; simpl.
  eapply ValidN; auto.
  simpl.
  exists LightControlComp.
  simpl. auto.
  refl.
  simpl in *.
  eapply ValidN; auto.
  exists SwonLights. simpl.
  auto.
  simpl; auto.
  apply WellFormedComponent; simpl; auto; intros; try fromfalse.
  eapply WellFormedInterfaces_Step; auto.
  eapply UniquePairs_Step; auto; simpl.
  apply NotInPair_Nil; auto.
  apply UniquePairs_Base; auto.
  unfold no_id_clash; intros.
  unfold LightsControlUseCaseArchitecture in H;
  unfold p1 in H.
  simpl in *.
  inversion H; subst.
  clear H.
  unfold LCC.
  eapply NotInStep; auto.
  eapply NotInStep; auto.
  eapply NotInStep; auto.
refl.
   eapply rsc_step.
   apply SSeqFinish.
   eapply rsc_step.
   apply SSeq2.
   apply SMakeBinding.
   simpl.
   unfold p1.
   unfold valid_component_binding. simpl.
   apply ValidComponentBinding_Step.
   eexists. split. refl.
   unfold valid_component_binding.
   simpl.
   unfold interfaces_SwonLights; unfold interfaces_LightControlComp; simpl.
   unfold p1.
   compute; auto.
   compute.
   intuition.
   inversion H0.
   unfold SensedBrInfo; simpl.
   refl.
   eapply rsc_step.
   apply SSeq2.
   apply SMakeBinding.
   simpl.
   unfold p1.
   unfold valid_component_binding. simpl.
   apply ValidComponentBinding_Step.
   eexists. split.
   refl.
   unfold valid_component_binding.
   simpl.
   unfold interfaces_SwonLights; unfold interfaces_LightControlComp; simpl.
   unfold p1.
   compute; auto.
   compute.
   intuition.
   inversion H0. inversion H.
   refl.
   eapply rsc_step.
   apply SMakeBinding.
   simpl.
   unfold p1.
   unfold valid_component_binding. simpl.
   apply ValidComponentBinding_Step. eexists. split.
   refl.
   unfold valid_component_binding.
   simpl.
   unfold interfaces_SwonLights; unfold interfaces_LightControlComp; simpl.
   unfold p1.
   compute; auto.
   compute.
   intuition.
   inversion H0. inversion H. inversion H0.
   refl.
   auto.
Qed.

Lemma add_3_lights:
  forall s, add_lights_reconfig 3 / LightsControlUseCaseArchitecture ~~~>* Done / s ->
             well_formed s.
Proof.
  intros.
  assert (well_formed LightsControlUseCaseArchitecture).
    apply LightsControlUseCase_is_well_formed.
  apply validity with (s:=LightsControlUseCaseArchitecture) (a:=add_lights_reconfig 3); auto.
Qed.

More on parametrized architectures

More stuff to be needed later :-)

Definition primitive c := (c ->subComponents%comp) = nil /\
                          (c ->bindings%comp) = nil.

Definition no_clash_on_generation id n p s :=
  match get_scope p s with
    None => True
  | Some lc => forall c', In c' lc ->
                 forall m, m < n -> (c'->id%comp) <> (suffix_ident id m )
  end.

Lemma generate_0:
  forall c n, n = 0 -> generate_from_template c n = nil.
Proof.
  intros.
  functional induction generate_from_template c n; auto.
  inversion H.
Qed.

Lemma generate_1:
  forall c n, primitive c ->
              n = 1 -> generate_from_template c n =
          (Component (suffix_ident (c ->id%comp) 1)
                         (c ->path%comp) (c ->iclass%comp) (c ->controlLevel%comp)
                         (c ->subComponents%comp)
                         (update_interfaces_path (c ->interfaces%comp) (suffix_ident (c ->id%comp) n))
                         (c ->bindings%comp)) :: nil.
Proof.
  intros.
  functional induction generate_from_template c n.
  inversion H0. simpl in *.
  rewrite H0.
  assert (m = 0).
    inversion H0; auto.
  rewrite H1. simpl. refl.
  assert (False). Focus.
    destruct template.
    unfold primitive in H.
    simpl in H; subst.
    destruct l; auto.
    destruct l1; auto.
    destruct H; congruence.
    destruct H; congruence.
  inversion H0.
Qed.

Lemma generate_from_template_fact:
  forall c n, primitive c ->
              generate_from_template c (S n) =
              (Component (suffix_ident (c ->id%comp) (S n))
                         (c ->path%comp) (c ->iclass%comp) (c ->controlLevel%comp)
                         (c ->subComponents%comp)
                         (update_interfaces_path (c ->interfaces%comp) (suffix_ident (c ->id%comp) (S n)))
                         (c ->bindings%comp)) ::
                         generate_from_template c n.
Proof.
  induction n; intro.
  Case "n is 0".
    rewrite generate_1; auto.
    rewrite generate_0; auto.
  Case "n is not 0".
    assert (generate_from_template c (S n) =
      Component (suffix_ident (c ->id)%comp (S n))
        (c ->path)%comp (c->iclass%comp) (c ->controlLevel)%comp
        (c ->subComponents)%comp
        (update_interfaces_path (c ->interfaces)%comp
           (suffix_ident (c ->id)%comp (S n))) (c ->bindings)%comp
      :: generate_from_template c n).
      apply IHn; auto.
    clear IHn.
    destruct c; simpl in *.
    unfold primitive in H; simpl in H.
    destruct H; subst.
    refl.
Qed.