Mefresa.Behaviour.GCMExample

In this module we put the LTS, Net and traces in the context of the GCM.

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

Simple GCM example

Queue process : size 2, one method m0, taking one parameter

Definition queue_transitions : transitions :=
[ (LTS_State 0 [], Action (Message "Q_m1" Read [Var("v1")]) [], LTS_State 1 []) ;
   (LTS_State 1 [], Action (Message "Q_m1" Read [Var("v2")]) [], LTS_State 2 []) ;
   (LTS_State 2 [], Action (Message "Q_m1" Read [Var("v3")]) [], LTS_State 3 []) ;

   (LTS_State 3 [], Action (Message "Error" Emit [Var("v3")]) [], LTS_State 3 []) ;

   (LTS_State 2 [], Action (Message "Serve_m1" Emit [Var("v1")]) [AssignmentVar "v2" "v1"], LTS_State 1 []) ;
   (LTS_State 1 [], Action (Message "Serve_m1" Emit [Var("v1")]) [], LTS_State 0 [])
].

Definition queue_states : lts_states :=
  [LTS_State 0 [] ; LTS_State 1 []; LTS_State 2 [] ; LTS_State 3 []].

Definition queue_mem : state_mem :=
  ("v1", 0) :: ("v2", 0) :: ("v3", 0) :: nil.
Definition queue_init : lts_state := LTS_State 0 queue_mem.

Definition queue_actions : actions :=
  [ Action (Message "Q_m1" Read [Var("v1")]) [] ;
    Action (Message "Q_m1" Read [Var("v2")]) [] ;
    Action (Message "Q_m1" Read [Var("v3")]) [] ;
    Action (Message "Error" Emit [Var("v3")]) [] ;
    Action (Message "Serve_m1" Emit [Var("v1")]) [AssignmentVar "v2" "v1"] ;
    Action (Message "Serve_m1" Emit [Var("v1")]) []
  ].

Definition queue : LTS :=
  mk_LTS queue_states queue_init queue_actions queue_transitions.

Body process : one method m0

Definition body_transitions : transitions :=
  [ (LTS_State 0 [], Action (Message "Serve_m1" Read [Var("v1")]) [], LTS_State 1 []) ;
    (LTS_State 1 [], Action (Message "Call_m1" Emit [Var("v1")]) [] , LTS_State 2 []) ;
    (LTS_State 2 [], Action (Message "R_m1" Read [Var("v1")]) [] , LTS_State 0 [])
  ].

Definition body_states : lts_states :=
  [LTS_State 0 [] ; LTS_State 1 [] ; LTS_State 2 []].

Definition body_mem : state_mem := ("v1", 0) :: nil.
Definition body_init : lts_state := LTS_State 0 body_mem.

Definition body_actions : actions :=
  [ Action (Message "Serve_m1" Read [Var("v1")]) [] ;
    Action (Message "Call_m1" Emit [Var("v1")]) [] ;
    Action (Message "R_m1" Read [Var("v1")]) []
  ].

Definition body : LTS :=
  mk_LTS body_states body_init body_actions body_transitions.

JMX process : two jmx indicators, MemoryStatus (encoded by 1), and Device Status (encoded by 21 and 22)

Overall model: Process Synchronization

Definition synch_vectors : list SynchronizationVector :=
  [ << "Q_m1" , "-" , "-" >> -> "Q_m1" ;
    << "Serve_m1", "Serve_m1", "-" >> -> "Serve_m1" ;
    << "-" , "Call_m1" , "Call_m1" >> -> "Call_m1" ;
    << "-" , "R_m1" , "R_m1" >> -> "R_m1" ;
    << "Error" , "-" , "-" >> -> "Error" ].

Definition gcm_component : Net :=
  mk_Net ([queue ; body ; jmx ], synch_vectors ).

Experimental : parametrized Body process

A simple body process is depicted in this section. For the sake of simplicity, it only takes one parameter.

Function n_transitions (tr:lts_state * action * lts_state) (param_domain:nat) :=
  match param_domain, tr with
    0 , (st, Action (Message l ct _) asgns, st') => (st, Action (Message l ct [Val 0]) asgns, st') :: nil
  | S m, (st, Action (Message l ct _) asgns, st') => (st, Action (Message l ct [Val m]) asgns, st') ::
                                                     n_transitions tr m
  end.

Function build_method_transitions (name:string) (n:nat) (arg_domain:nat) : transitions :=
  let ts := n_transitions (LTS_State 0 [], Action (Message (append "Serve_" name) Read []) [], LTS_State (n +1) []) arg_domain in
  let tc := n_transitions (LTS_State (n +1) [], Action (Message (append "Call_" name) Emit []) [], LTS_State (n +2) []) arg_domain in
  let tr := n_transitions (LTS_State (n +2) [], Action (Message (append "R_" name) Read []) [], LTS_State 0 []) arg_domain in
  app ts (app tc tr).

Function build_methods_transitions (method_names:list string) n arg_domain :=
  match method_names with
    nil => nil
  | m :: r => app (build_method_transitions m n arg_domain) (build_methods_transitions r (n +2) arg_domain)
  end.

The function build_methods_transitions computes the transitions resulting from the dealing with method invocation dispatch.

Function build_operation_transitions (operations:list (string * nat)) (index:nat) :=
  match operations with
    nil => nil
  | (op_name, arg_domain) :: r =>
     let ts := n_transitions (LTS_State 0 [], Action (Message (append "Serve_" op_name) Read []) [], LTS_State index []) arg_domain in
     let to := n_transitions (LTS_State index [], Action (Message op_name Emit []) [], LTS_State 0 []) arg_domain in
     app ts (app to (build_operation_transitions r (index +1)))
  end.

The function build_operation_transitions computes the transitions resulting from the dealing with non-functional operations invocation dispatch.

Function generate_n_states n :=
  match n with
    0 => nil
  | S n' => LTS_State n' [] :: generate_n_states n'
  end.

Lemma generate_n_states_len:
  forall n, List.length (generate_n_states n) = n.
Proof.
  induction n; auto.
  simpl.
  apply f_equal; auto.
Qed.

Above, a simple function generate_n_states generating lts_states, and the proof of a trivial fact about it.

Function n_actions (act:action) (arg_domain:nat) : actions :=
  match act, arg_domain with
    Action (Message l ct _) asgns, 0 => [Action (Message l ct [Val 0]) asgns]
  | Action (Message l ct _) asgns, S m => Action (Message l ct [Val m]) asgns ::
                                          n_actions act m
  end.

Function body_actions_from_methods (method_names:list string) (arg_domain:nat): actions :=
  match method_names with
    nil => nil
  | m :: r => let acs := n_actions (Action (Message (append "Serve_" m) Read []) []) arg_domain in
              let acc := n_actions (Action (Message (append "Call_" m) Emit []) []) arg_domain in
              let acr := n_actions (Action (Message (append "R_" m) Read []) []) arg_domain in
              app acs (app acc (app acr (body_actions_from_methods r arg_domain)))
  end.

Function body_actions_from_operations (ops:list (string * nat)) :=
  match ops with
    nil => nil
  | (op, n) :: r => let a := n_actions (Action (Message (append "Serve_" op) Read []) []) n in
                    let b := n_actions (Action (Message op Emit []) []) n in
                    app a (app b (body_actions_from_operations r))
  end.

Function body_LTS (method_names : list string)
                  (acts_params : parameters)
                  (operations : list (string * nat))
                  (method_arg_domain : nat) :=

    let param_method_transitions := build_methods_transitions method_names 0 method_arg_domain in
    let param_operation_transitions := build_operation_transitions operations ((2 * List.length method_names )+1) in
    let nstates := (2 * List.length method_names ) + (List.length operations ) + 1 in
    let LTSstates := generate_n_states nstates in
    let acts := app (body_actions_from_methods method_names method_arg_domain) (body_actions_from_operations operations) in

    mk_LTS LTSstates (LTS_State 0 []) acts (app param_method_transitions param_operation_transitions).