Mefresa.GCM.Examples

Example of a primitive component

Require Import Mefresa.GCM.Component.

The definitions below represent the structure of the Primitive Component example giving in 1, pp. 9

Definition default_class := "org.mefresa.defaultimpl".

Definition PrimitivePath := (Ident "PrimitiveExample") :: nil.
Definition Primitive : component :=
  Component (Ident "PrimitiveExample") nil default_class Configuration nil
  ((Interface (Ident "m1") "sig1" PrimitivePath External Server Functional Optional Singleton ) ::
   (Interface (Ident "m2") "sig2" PrimitivePath External Server Functional Optional Singleton ) ::
   (Interface (Ident "m3") "sig3" PrimitivePath External Server Functional Optional Singleton ) ::
   (Interface (Ident "m4") "sig4" PrimitivePath External Client Functional Mandatory Singleton ) ::
   (Interface (Ident "m5") "sig5" PrimitivePath External Client Functional Mandatory Singleton ) :: nil)
  nil.

Example of a composite component

The definitions below represent the structure of a composite component

Definition CompositePath := (Ident "CompositeExample") :: nil.
Definition PrimitiveAPath := (Ident "CompositeExample") :: (Ident "PrimitiveA") :: nil.
Definition PrimitiveA : component :=
  Component (Ident "PrimitiveA") CompositePath default_class Configuration nil
  ((Interface (Ident "S1") "sig1" PrimitiveAPath External Server Functional Optional Singleton ) ::
  (Interface (Ident "C1") "sig2" PrimitiveAPath External Client Functional Mandatory Singleton ) ::
  (Interface (Ident "C2") "sig3" PrimitiveAPath External Client Functional Mandatory Singleton ) ::
  nil)
  nil.

Definition PrimitiveB : component :=
  Component (Ident "PrimitiveB") CompositePath default_class Configuration nil
  ((Interface (Ident "S1") "sig1" PrimitiveAPath External Server Functional Optional Singleton ) ::
   (Interface (Ident "C1") "sig2" PrimitiveAPath External Client Functional Mandatory Singleton ) :: nil)
   nil.

Definition Composite : component :=
  Component (Ident "CompositeExample") nil default_class Configuration
  (PrimitiveA :: PrimitiveB :: nil)
  ((Interface (Ident "S") "sig1" CompositePath External Server Functional Optional Singleton ) ::
  (Interface (Ident "S") "sig1" CompositePath Internal Client Functional Optional Singleton ) ::
  (Interface (Ident "M") "sig2" CompositePath External Client Functional Optional Multicast ) ::
  (Interface (Ident "M") "sig2" CompositePath Internal Server Functional Optional Singleton ) ::
  (Interface (Ident "C") "sig3" CompositePath External Client Functional Mandatory Singleton ) ::
  (Interface (Ident "C") "sig3" CompositePath Internal Client Functional Mandatory Singleton ) ::
  nil)
  ((Export CompositePath (Ident "S") (Ident "PrimitiveA") (Ident "S1")) ::
  (Import CompositePath (Ident "M") (Ident "PrimitiveA") (Ident "C1")) ::
  (Normal CompositePath (Ident "PrimitiveA") (Ident "C2") (Ident "PrimitiveB") (Ident "S1")) ::
  (Import CompositePath (Ident "C") (Ident "PrimitiveB") (Ident "C1")) ::
  nil).