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;