MultiModalProducerConsumer

AADL-BA example

-- AADL-BA-FrontEnd
 
-- Copyright © 2011 TELECOM ParisTech and CNRS
 
-- TELECOM ParisTech/LTCI

-- Authors: see AUTHORS
 
-- This program is free software: you can redistribute it and/or modify 
-- it under the terms of the Eclipse Public License as published by Eclipse,
-- either version 1.0 of the License, or (at your option) any later version.
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-- Eclipse Public License for more details.
-- You should have received a copy of the Eclipse Public License
-- along with this program.  If not, see 
-- http://www.eclipse.org/org/documents/epl-v10.php

package MultiModalPingPong
public

-- we suppose we have 123 components, ping or pong

with data_model;
with base_types;

---------------------------------------------------------------------
-- INTERFACES
---------------------------------------------------------------------

data components_number
  properties
	data_model::data_representation => integer;
end components_number;

data sequence_number
  properties
	data_model::data_representation => integer;
end sequence_number;

data component_id
  properties
	data_model::data_representation => integer;
end component_id;

data message_type
-- PING/PONG
  properties
	data_model::data_representation => string;
	data_model::enumerators => ("PING", "PONG");
end message_type;

data payload
-- type + recipient + sequence
  properties
	data_model::data_representation => struct;
end payload;

data implementation payload.impl
-- type + recipient + sequence
  subcomponents
    t: data message_type;
    r: data component_id;
    s: data sequence_number;
end payload.impl;

data role_switch
-- to_ping/to_pong
  properties
	data_model::data_representation => string;
	data_model::enumerators => ("to_ping", "to_pong", "to_disconnect");
end role_switch;

data mode_switch_cmd
  properties
	data_model::data_representation => struct;
	data_model::base_type => (classifier (role_switch), classifier(component_id));
	data_model::element_names => ("to_role","c_id");
end mode_switch_cmd;

data implementation mode_switch_cmd.impl
  subcomponents
    to_role: data role_switch;
    c_id: data component_id;
end mode_switch_cmd.impl;

data ping_result
-- success/failure
  properties
	data_model::data_representation => string;
	data_model::enumerators => ("failure", "success");
end ping_result;

---------------------------------------------------------------------
-- CPING ROLE DEFINITION
---------------------------------------------------------------------

thread Cping_t
  features
	emit: out event data port payload.impl;
  	result: out data port ping_result; 
    receive: in event data port payload.impl;
  properties
    dispatch_protocol => timed;
    period => 100 ms;
end Cping_t;

thread implementation Cping_t.impl
subcomponents
  the_ping_msg : data payload.impl;
  received_msg : data payload.impl;
  recipient_array : data component_id[122];
  message_array : data sequence_number[122];
  my_id: data component_id;
  counter: data base_types::integer;

annex behavior_specification {**

  states
    standby : initial complete final state;
    busy : complete state;
    validation : state;
  
  transitions
-- TODO: init recipient_array  
    busy -[ on dispatch ]-> busy { result := "failure" };
    standby -[ on dispatch ]-> busy { for(i : component_id in recipient_array)
    					{
    						the_ping_msg.t :="PING";
    						the_ping_msg.r := i;
    						set_muid!(the_ping_msg.s);
    						message_array[i] := the_ping_msg.s;
    						emit!(the_ping_msg)
    					}
    				};
    standby -[ on dispatch receive ]-> standby {receive?};
    busy -[ on dispatch receive]-> validation {receive?(received_msg)};
    validation -[ received_msg.t="PONG" and received_msg.s = message_array[received_msg.r] ]-> 
    				standby { result := "success"; counter:=counter+1};
    validation -[ received_msg.t!="PONG" or received_msg.s != message_array[received_msg.r]]-> busy;
    busy -[on dispatch timeout 80 ms]-> standby { result := "failure" };

  **};
end Cping_t.impl;

subprogram set_muid
  features
    uid: out parameter sequence_number; -- should be unique at system's scale
end set_muid;

---------------------------------------------------------------------
-- CPONG ROLE DEFINITION
---------------------------------------------------------------------

thread Cpong_t
  features
 	emit: out event data port payload.impl;
    receive: in event data port payload.impl;
  properties
    dispatch_protocol => sporadic;
end Cpong_t;

thread implementation Cpong_t.impl
  subcomponents
    received_ping: data payload.impl;
  annex behavior_specification {**
    states
      available: initial complete final state;
    
    transitions -- TODO: specify the buffer size of receive=2
      available -[ on dispatch receive ]-> 
    		available{receive?(received_ping); received_ping.t:="PONG";emit!(received_ping)};
  **};
end Cpong_t.impl;

---------------------------------------------------------------------
-- COMPONENTS DEFINITION
---------------------------------------------------------------------

process ping_or_pong
  features
  	to_ping: in event port;
  	to_pong: in event port;
  	result: out data port ping_result; 
  	emit: out event data port payload.impl;
  	receive: in event data port payload.impl;
  modes
    not_connected: initial mode;
    ping_m: mode;
    pong_m: mode;
    ping_m-[to_pong]->not_connected;
    pong_m-[to_ping]->not_connected;
    not_connected-[to_ping]->ping_m;
    not_connected-[to_pong]->pong_m;
  
end ping_or_pong;

process implementation ping_or_pong.impl
subcomponents
    the_ping: thread Cping_t.impl in modes (ping_m);
    the_pong: thread Cpong_t.impl in modes (pong_m);
  connections
    cnx1: port the_ping.emit -> emit in modes (ping_m);
    cnx2: port receive -> the_ping.receive in modes (ping_m);
    cnx3: port the_pong.emit -> emit in modes (pong_m);
    cnx4: port receive -> the_pong.receive in modes (pong_m);
    cnx5: port the_ping.result -> result in modes (ping_m);
end ping_or_pong.impl; 

---------------------------------------------------------------------
-- SYSTEM DEFINITION
---------------------------------------------------------------------

system global_sys
  features
    mode_switch_p: in event data port mode_switch_cmd;
end global_sys;

system implementation global_sys.impl
  subcomponents
    the_components: process ping_or_pong.impl[123];
    the_controller: process controller_process.impl;
  connections
    cnx1: port the_components.emit -> the_components.receive {connection_pattern =>((one_to_all));};
    cnx3: port mode_switch_p->the_controller.mode_switch_p;
end global_sys.impl;

process controller_process
  features
    mode_switch_p: in event data port mode_switch_cmd;
end controller_process;

process implementation controller_process.impl
  subcomponents
    the_controller: thread controller_thread.impl;
    the_components: data components_array.impl;
  connections
    cnx: port mode_switch_p -> the_controller.mode_switch_p;
    cnx2: data access the_components->the_controller.components;
end controller_process.impl;

thread controller_thread
  features
    mode_switch_p: in event data port mode_switch_cmd.impl;
    to_ping: out event port[123];
    to_pong: out event port[123];
    components: requires data access components_array.impl;
  properties
    dispatch_protocol => sporadic;
end controller_thread;

thread implementation controller_thread.impl
  subcomponents
    last_cmd: data mode_switch_cmd.impl;
    mode_switch: subprogram controller_subprogram.impl;
    result: data base_types::integer;
    
  annex behavior_specification {**
    states
      idle: initial complete state;
      exec: state;
      close: final state;
    
    transitions
      exec -[last_cmd.to_role="to_ping"]-> idle {for(i : base_types::integer in 0 .. result)
                                                    {
                                                        to_ping[last_cmd.c_id]!
                                                    };
                                                    last_cmd.to_role:=""
                                                };
      idle -[on dispatch mode_switch_p]-> idle 
                                           {
                                               mode_switch_p?(last_cmd);
                                               mode_switch!(last_cmd.to_role,last_cmd.c_id,result, components)
                                           };
  **};
end controller_thread.impl;

subprogram controller_subprogram
  features
    dest_mode: in parameter role_switch;
    c_id: in parameter component_id;
    result: out parameter base_types::integer; -- value_range 0..2;
    components: requires data access components_array.impl;
end controller_subprogram;

subprogram implementation controller_subprogram.impl
  annex behavior_specification {**
    states
      s_ini: initial state;
      s_fini: final state;
    transitions -- TODO : not the same event name for to_ping and to_disconnected.
      s_ini -[dest_mode="to_disconnect" and components.c[c_id].role="pong"]-> s_fini 
                             {
                                 result:=2;
                                 components.c[c_id].role:="not_connected"
                             };
      s_ini -[dest_mode="to_disconnect" and components.c[c_id].role="ping"]-> s_fini
                             {
                                 result:=2;
                                 components.c[c_id].role:="not_connected"
                             };
      s_ini -[dest_mode="to_ping" and components.c[c_id].role="not_connected"]-> s_fini
                             {
                                 result:=1;
                                 components.c[c_id].role:="ping"
                             };
      s_ini -[dest_mode="to_pong" and components.c[c_id].role="not_connected"]-> s_fini
                             {
                                 result:=1;
                                 components.c[c_id].role:="pong"
                             };
  **};
end controller_subprogram.impl;

-- TODO: init data of each component

data c_id_and_role
  properties
	data_model::data_representation => struct;
end c_id_and_role;

data implementation c_id_and_role.impl
  subcomponents
    c_id: data component_id;
    role: data base_types::string;
end c_id_and_role.impl;

data components_array
  properties
    data_model::data_representation => array;
end components_array;

data implementation components_array.impl
  subcomponents
    c: data c_id_and_role.impl[123];
end components_array.impl;

end MultiModalPingPong;