Commit 44454aae authored by Bechir Zalila's avatar Bechir Zalila

* Test cases for the AO4AADL frontend

	(By Sihem Loukil)
parent 10f84b1e
tests/test_ocarina_help
tests/test_ocarina_config
tests/test_ocarina_gpr
tests/test_ao4aadl_lexer
tests/test_ao4aadl_parser
tests/osate-flow-impls/FlowImpls.aadl
tests/osate-flow-impl-modes/FlowImplModes.aadl
tests/osate2-t02/t2.aadl
......
This diff is collapsed.
-----------
-- Data --
----------
data Integer_Type
properties
Data_Model::Data_Representation => integer;
end Integer_Type;
data String_Type
properties
Data_Model::Data_Representation => string;
Data_Model::Dimension => (100);
end String_Type;
-----------------
-- Subprograms --
-----------------
subprogram Check_Validity_Spg
features
NumCard : in parameter Integer_Type;
Valid : out parameter String_Type;
NotValid : out parameter String_Type;
end Check_Validity_Spg;
subprogram Check_Code_Spg
features
NumCard : in parameter Integer_Type;
Code : in parameter Integer_Type;
OK : out parameter String_Type;
RestoreCode : out parameter String_Type;
RejectedCard : out parameter String_Type;
end Check_Code_Spg;
subprogram Check_Spg
features
NumCard : in parameter Integer_Type;
Valid : out parameter String_Type;
NotValid : out parameter String_Type;
Code : in parameter Integer_Type;
OK : out parameter String_Type;
RestoreCode : out parameter String_Type;
RejectedCard : out parameter String_Type;
end Check_Spg;
subprogram implementation Check_Validity_Spg.Impl
properties
source_language => Ada95;
source_name => "Bank.Check_Validity_Spg";
end Check_Validity_Spg.Impl;
subprogram implementation Check_Code_Spg.Impl
properties
source_language => Ada95;
source_name => "Bank.Check_Code_Spg";
end Check_Code_Spg.Impl;
subprogram implementation Check_Spg.Impl
calls{
CV_Spg : subprogram Check_Validity_Spg.Impl;
CC_Spg : subprogram Check_Code_Spg.Impl;
};
connections
parameter NumCard -> CV_Spg.NumCard;
parameter NumCard -> CC_Spg.NumCard;
parameter CV_Spg.Valid -> Valid;
parameter CV_Spg.NotValid -> NotValid;
parameter Code -> CC_Spg.Code;
parameter CC_Spg.OK -> OK;
parameter CC_Spg.RestoreCode -> RestoreCode;
parameter CC_Spg.RejectedCard -> RejectedCard;
end Check_Spg.Impl;
-----------------
-- Threads --
-----------------
thread ValidationTh
features
NumCard_in_V : in event data port Integer_Type;
Code_in_V : in event data port Integer_Type;
NumCard_out_V : out event data port Integer_Type;
OK_out_V : out event data port String_Type;
RestoreCode_out_V : out event data port String_Type;
RejectedCard_out_V : out event data port String_Type;
Valid_out_V : out event data port String_Type;
NotValid_out_V : out event data port String_Type;
end ValidationTh;
thread implementation ValidationTh.Impl
calls {
C_Spg : subprogram Check_Spg.Impl;
};
connections
parameter NumCard_in_V -> C_Spg.NumCard;
parameter C_Spg.Valid -> Valid_out_V;
parameter C_Spg.NotValid -> NotValid_out_V;
parameter Code_in_V -> C_Spg.Code;
parameter C_Spg.OK -> OK_out_V;
parameter C_Spg.RestoreCode -> RestoreCode_out_V;
parameter C_Spg.RejectedCard -> RejectedCard_out_V;
properties
Initialize_Entrypoint => "Msgs.Welcome_Validation_TH";
Dispatch_Protocol => Sporadic;
Period => 1000 Ms;
Compute_Execution_time => 0 ms .. 3 ms;
Deadline => 1000 ms;
Cheddar_Properties::Fixed_Priority => 2;
annex ao4aadl {**
aspect CheckCode {
pointcut Verification (): call outport (RestoreCode_out_V (..));
advice around(): Verification(){
variables{
counter: Integer_Type;
message: String_Type;
}
initially{
counter:=1;
message:="Card Rejected!";
}
if (counter = 3){
RejectedCard_out_V ? (message);
counter := 1;
}
else{
proceed ();
counter := counter + 1;
}
}
}
aspect CheckConstraints {
pointcut VerificationAmount (session_id: Integer_Type, amount: Integer_Type):
call subprogram (C_Spg (..)) && args (session_id, amount, ..);
advice around(session_id: IntegerType, amount: IntegerType):
VerificationAmount(session_id, amount){
variables{
amount_Day: Integer_Type;
amount_Week: Integer_Type;
message : String_Type;}
initially { message := "";}
getAmount_Day!(session_id, amount_Day);
if (amount_Day + amount > 100 ){
message := "You can not debit more then 100 DT per day!";
RejectedCard_out_V !(message);
}
else{
getAmount_Week!(session_id, amount_Week);
if (amount_Week + amount > 400 ){
message := "You can not debit more then 400 DT per week!";
RejectedCard_out_V !(message);
}
else {
proceed (session_id, amount);}}}}
aspect Logging {
pointcut Log (session_id: Integer_Type, amount: Integer_Type):
execution subprogram (Debit (..))
&& args (session_id, amount, ..);
advice after(session_id: Integer_Type, amount: Integer_Type):
Log(session_id, amount){
sendSMS!(session_id, amount);
}}
**};
end ValidationTh.Impl;
process Customer
features
NumCard_in_C : in event data port Integer_Type;
Code_in_C : in event data port Integer_Type;
NumCard_out_C : out event data port Integer_Type;
OK_out_C : out event data port String_Type;
RestoreCode_out_C : out event data port String_Type;
RejectedCard_out_C : out event data port String_Type;
Valid_out_C : out event data port String_Type;
NotValid_out_C : out event data port String_Type;
end Customer;
process implementation Customer.Impl
subcomponents
Validation : thread ValidationTh.Impl;
connections
event data port NumCard_in_C -> Validation.NumCard_in_V;
event data port Code_in_C -> Validation.Code_in_V;
event data port Validation.NumCard_out_V -> NumCard_out_C;
event data port Validation.OK_out_V -> OK_out_C;
event data port Validation.RestoreCode_out_V -> RestoreCode_out_C;
event data port Validation.RejectedCard_out_V -> RejectedCard_out_C;
event data port Validation.Valid_out_V -> Valid_out_C;
event data port Validation.NotValid_out_V -> NotValid_out_C;
end Customer.Impl;
---------------
-- Processor --
---------------
processor the_processor
end the_processor;
processor implementation the_processor.Impl
properties
Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
Cheddar_Properties::Scheduler_Quantum => 0 Ms;
Cheddar_Properties::Preemptive_Scheduler => true;
end the_processor.Impl;
system Bank
end Bank;
system implementation Bank.others
subcomponents
node_customer : process Customer.Impl
{Deployment::Channel_Address => 2;
Deployment::Process_Id => 1200;};
CPU : processor the_processor.Impl
{Deployment::Execution_Platform => LEON_ORK;};
properties
actual_processor_binding => reference CPU applies to node_customer;
END Bank.others;
-----------
-- Data --
----------
data Integer_Type
properties
Data_Model::Data_Representation => integer;
end Integer_Type;
data String_Type
properties
Data_Model::Data_Representation => string;
Data_Model::Dimension => (100);
end String_Type;
-----------------
-- Subprograms --
-----------------
subprogram Check_Validity_Spg
features
NumCard : in parameter Integer_Type;
Valid : out parameter String_Type;
NotValid : out parameter String_Type;
end Check_Validity_Spg;
subprogram Check_Code_Spg
features
NumCard : in parameter Integer_Type;
Code : in parameter Integer_Type;
OK : out parameter String_Type;
RestoreCode : out parameter String_Type;
RejectedCard : out parameter String_Type;
end Check_Code_Spg;
subprogram Check_Spg
features
NumCard : in parameter Integer_Type;
Valid : out parameter String_Type;
NotValid : out parameter String_Type;
Code : in parameter Integer_Type;
OK : out parameter String_Type;
RestoreCode : out parameter String_Type;
RejectedCard : out parameter String_Type;
end Check_Spg;
subprogram implementation Check_Validity_Spg.Impl
properties
source_language => Ada95;
source_name => "Bank.Check_Validity_Spg";
end Check_Validity_Spg.Impl;
subprogram implementation Check_Code_Spg.Impl
properties
source_language => Ada95;
source_name => "Bank.Check_Code_Spg";
end Check_Code_Spg.Impl;
subprogram implementation Check_Spg.Impl
calls{
CV_Spg : subprogram Check_Validity_Spg.Impl;
CC_Spg : subprogram Check_Code_Spg.Impl;
};
connections
parameter NumCard -> CV_Spg.NumCard;
parameter NumCard -> CC_Spg.NumCard;
parameter CV_Spg.Valid -> Valid;
parameter CV_Spg.NotValid -> NotValid;
parameter Code -> CC_Spg.Code;
parameter CC_Spg.OK -> OK;
parameter CC_Spg.RestoreCode -> RestoreCode;
parameter CC_Spg.RejectedCard -> RejectedCard;
end Check_Spg.Impl;
-----------------
-- Threads --
-----------------
thread ValidationTh
features
NumCard_in_V : in event data port Integer_Type;
Code_in_V : in event data port Integer_Type;
NumCard_out_V : out event data port Integer_Type;
OK_out_V : out event data port String_Type;
RestoreCode_out_V : out event data port String_Type;
RejectedCard_out_V : out event data port String_Type;
Valid_out_V : out event data port String_Type;
NotValid_out_V : out event data port String_Type;
end ValidationTh;
thread implementation ValidationTh.Impl
calls {
C_Spg : subprogram Check_Spg.Impl;
};
connections
parameter NumCard_in_V -> C_Spg.NumCard;
parameter C_Spg.Valid -> Valid_out_V;
parameter C_Spg.NotValid -> NotValid_out_V;
parameter Code_in_V -> C_Spg.Code;
parameter C_Spg.OK -> OK_out_V;
parameter C_Spg.RestoreCode -> RestoreCode_out_V;
parameter C_Spg.RejectedCard -> RejectedCard_out_V;
properties
Initialize_Entrypoint => "Msgs.Welcome_Validation_TH";
Dispatch_Protocol => Sporadic;
Period => 1000 Ms;
Compute_Execution_time => 0 ms .. 3 ms;
Deadline => 1000 ms;
Cheddar_Properties::Fixed_Priority => 2;
annex ao4aadl {**
aspect CheckCode {
pointcut Verification (): call outport (RestoreCode_out_V (..));
advice around(): Verification(){
variables{
counter: Integer_Type;
message: String_Type;
}
initially{
counter:=1;
message:="Card Rejected!";
}
if (counter = 3){
RejectedCard_out_V ! (message);
}
else{
proceed();
counter := counter + 1;
}
}
}
**};
end ValidationTh.Impl;
process Customer
features
NumCard_in_C : in event data port Integer_Type;
Code_in_C : in event data port Integer_Type;
NumCard_out_C : out event data port Integer_Type;
OK_out_C : out event data port String_Type;
RestoreCode_out_C : out event data port String_Type;
RejectedCard_out_C : out event data port String_Type;
Valid_out_C : out event data port String_Type;
NotValid_out_C : out event data port String_Type;
end Customer;
process implementation Customer.Impl
subcomponents
Val : thread ValidationTh.Impl;
connections
event data port NumCard_in_C -> Val.NumCard_in_V;
event data port Code_in_C -> Val.Code_in_V;
event data port Val.NumCard_out_V -> NumCard_out_C;
event data port Val.OK_out_V -> OK_out_C;
event data port Val.RestoreCode_out_V -> RestoreCode_out_C;
event data port Val.RejectedCard_out_V -> RejectedCard_out_C;
event data port Val.Valid_out_V -> Valid_out_C;
event data port Val.NotValid_out_V -> NotValid_out_C;
end Customer.Impl;
---------------
-- Processor --
---------------
processor the_processor
end the_processor;
processor implementation the_processor.Impl
properties
Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
Cheddar_Properties::Scheduler_Quantum => 0 Ms;
Cheddar_Properties::Preemptive_Scheduler => true;
end the_processor.Impl;
system Bank
end Bank;
system implementation Bank.others
subcomponents
customer : process Customer.Impl
{Deployment::Channel_Address => 2;
Deployment::Process_Id => 1200;};
CPU : processor the_processor.Impl
{Deployment::Execution_Platform => LEON_ORK;};
properties
actual_processor_binding => reference CPU applies to customer;
END Bank.others;
----------
-- Data --
----------
data Integer_Type
properties
Data_Model::Data_Representation => integer;
end Integer_Type;
data String_Type
properties
Data_Model::Data_Representation => string;
Data_Model::Dimension => (100);
end String_Type;
-----------------
-- Subprograms --
-----------------
subprogram Operation_Spg
features
SessionID: in parameter Integer_Type;
NumCard : in parameter Integer_Type;
Cmd : in parameter Integer_Type;
Amount : in parameter Integer_Type;
Result : out parameter String_Type;
end Operation_Spg;
subprogram implementation Operation_Spg.Impl
calls{
Debit_Op : subprogram Debit.Impl;
Credit_Op : subprogram Credit.Impl;
};
connections
parameter SessionID -> Debit_Op.SessionID;
parameter SessionID -> Credit_Op.SessionID;
parameter Amount -> Debit_Op.Amount;
parameter Amount -> Credit_Op.Amount;
parameter NumCard -> Debit_Op.NumCard;
parameter NumCard -> Credit_Op.NumCard;
parameter Debit_Op.Result -> Result;
parameter Credit_Op.Result -> Result;
properties
source_language => rtsj;
source_name => "Bank.Operation_Spg";
end Operation_Spg.Impl;
subprogram Debit
features
SessionID : in parameter Integer_Type;
NumCard : in parameter Integer_Type;
Amount : in parameter Integer_Type;
Result : out parameter String_Type;
end Debit;
subprogram Credit
features
SessionID : in parameter Integer_Type;
NumCard : in parameter Integer_Type;
Amount : in parameter Integer_Type;
Result : out parameter String_Type;
end Credit;
subprogram implementation Debit.Impl
properties
source_language => rtsj;
source_name => "Bank.Debit_Spg";
end Debit.Impl;
subprogram implementation Credit.Impl
properties
source_language => rtsj;
source_name => "Bank.Credit_Spg";
end Credit.Impl;
-------------
-- Threads --
-------------
thread AccountTh
features
NumCard_in_AT : in event data port Integer_Type;
Cmd_in_AT : in event data port Integer_Type;
SessionID_in_AT : in event data port Integer_Type;
Amount_in_AT : in event data port Integer_Type;
Result_out_AT : out event data port String_Type;
end AccountTh;
thread implementation AccountTh.Impl
calls {
Do_Op_Spg : subprogram Operation_Spg.Impl;
};
connections
parameter NumCard_in_AT -> Do_Op_Spg.NumCard;
parameter Cmd_in_AT -> Do_Op_Spg.Cmd;
parameter SessionID_in_AT -> Do_Op_Spg.SessionID;
parameter Amount_in_AT -> Do_Op_Spg.Amount;
parameter Do_Op_Spg.Result -> Result_out_AT;
properties
Initialize_Entrypoint => "Msgs.Welcome_Account_TH";
Dispatch_Protocol => Periodic;
Period => 1000 Ms;
Compute_Execution_time => 0 ms .. 3 ms;
Deadline => 1000 ms;
Cheddar_Properties::Fixed_Priority => 3;
annex ao4aadl {**
aspect CheckConstraints {
pointcut VerificationAmount (session_id:Integer_Type, amount:Integer_Type): call subprogram (Debit (..)) && args(session_id, amount, ..);
advice around(session_id:Integer_Type, amount:Integer_Type): VerificationAmount(session_id, amount){
variables{
amount_Day: Integer_Type;
amount_Week: Integer_Type;
message:String_Type;
}
getAmount_Day!(session_id, amount_Day);
if((amount_Day+amount)>100){
message:="you can not debit more then 100 DT per day!";
Result_out_AT!(message);
}
else{
getAmount_Week!(session_id, amount_Week);
if((amount_Week+amount)>400){
message:="you can not debit more then 400 DT per week!";
Result_out_AT!(message);
}
else{
proceed(session_id,amount);
}
}
}
}
aspect Logging {
pointcut Log (session_id:Integer_Type, amount:Integer_Type): execution subprogram (Debit (..)) && args(session_id, amount, ..);
advice after(session_id:Integer_Type, amount:Integer_Type): Log(session_id, amount){
sendSMS!(session_id,amount);
}
}
**};
end AccountTh.Impl;
process Account
features
NumCard_in_A : in event data port Integer_Type;
Cmd_in_A : in event data port Integer_Type;
SessionID_in_A : in event data port Integer_Type;
Amount_in_A : in event data port Integer_Type;
Result_out_A : out event data port String_Type;
end Account;
process implementation Account.Impl
subcomponents
AC : thread AccountTh.Impl;
connections
event data port NumCard_in_A -> AC.NumCard_in_AT;
event data port Cmd_in_A -> AC.Cmd_in_AT;
event data port SessionID_in_A -> AC.SessionID_in_AT;
event data port Amount_in_A -> AC.Amount_in_AT;
event data port AC.Result_out_AT -> Result_out_A;
end Account.Impl;
---------------
-- Processor --
---------------
processor the_processor
end the_processor;
processor implementation the_processor.Impl
properties
Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
Cheddar_Properties::Scheduler_Quantum => 0 Ms;
Cheddar_Properties::Preemptive_Scheduler => true;
end the_processor.Impl;
system Bank
end Bank;
system implementation Bank.others
subcomponents
account : process Account.Impl
{Deployment::Channel_Address => 2;
Deployment::Process_Id => 1200;};
CPU : processor the_processor.Impl
{Deployment::Execution_Platform => LEON_ORK;};
properties
actual_processor_binding => reference CPU applies to account;
END Bank.others;
SYSTEM Bank
END Bank;
SYSTEM IMPLEMENTATION Bank.others
SUBCOMPONENTS
Customer : PROCESS Bank_P::Customer.impl;
AccountData : PROCESS Bank_P::AccountData.impl;
Account : PROCESS Bank_P::Account.impl;
CONNECTIONS
EVENT DATA PORT Customer.Request_out-> AccountData.Request_in;
EVENT DATA PORT Customer.NumCard_out -> AccountData.NumCard_in;
EVENT DATA PORT AccountData.session_id_out -> Customer.session_id_in;
EVENT DATA PORT Customer.session_id_out-> Account.session_id_in;
EVENT DATA PORT Customer.cmd_out -> Account.cmd_in;
EVENT DATA PORT Customer.amount_out ->Account.amount_in;
EVENT DATA PORT Account.result_out -> Customer.result_in;
END Bank.others;
PACKAGE Bank_P
PUBLIC
PROCESS Customer
FEATURES
NumCard_in : IN EVENT DATA PORT Integer_Type;
Code_in : IN EVENT DATA PORT Integer_Type;
result_in : IN EVENT DATA PORT Integer_Type;
session_id_in : IN EVENT DATA PORT Integer_Type;
NumCard_out : OUT EVENT DATA PORT Integer_Type;
cmd_out : OUT EVENT DATA PORT Integer_Type;
amount_out: OUT EVENT DATA PORT Integer_Type;
session_id_out : OUT EVENT DATA PORT Integer_Type;
Request_out : OUT EVENT DATA PORT Integer_Type;
END Customer;
PROCESS IMPLEMENTATION Customer.impl
SUBCOMPONENTS
GUI: THREAD GUIThread.Impl;
validation: THREAD ValidationThread.Impl;
CONNECTIONS
EVENT DATA PORT NumCard_in -> GUI.NumCard_in;
EVENT DATA PORT Code_in -> GUI.Code_in;
EVENT DATA PORT result_in -> GUI.result_in;
EVENT DATA PORT session_id_in -> validation.session_id_in;
EVENT DATA PORT validation.NumCard_out -> NumCard_out;
EVENT DATA PORT GUI.session_id_out -> session_id_out ;
EVENT DATA PORT GUI.cmd_out -> cmd_out;
EVENT DATA PORT GUI.amount_out -> amount_out;
EVENT DATA PORT validation.Request_out-> Request_out;
EVENT DATA PORT GUI.Control_out-> validation.Request_in;
EVENT DATA PORT GUI.NumCard_out-> validation.NumCard_in;
EVENT DATA PORT GUI.Code_out-> validation.Code_in;
EVENT DATA PORT validation.session_id_out-> GUI.session_id_in;
EVENT DATA PORT validation.Ok_out-> GUI.Ok_in;
EVENT DATA PORT validation.RestoreCode_out-> GUI.RestoreCode_in;
EVENT DATA PORT validation.RejectedCard_out-> GUI.RejectedCard_in;
END Customer.impl;
PROCESS AccountData
FEATURES
Request_in : IN EVENT DATA PORT Integer_Type;
NumCard_in : IN EVENT DATA PORT Integer_Type;
session_id_out : OUT EVENT DATA PORT Integer_Type;
END AccountData;
PROCESS IMPLEMENTATION AccountData.impl
SUBCOMPONENTS
AccountDataT: THREAD AccountDataThread.Impl;
CONNECTIONS
EVENT DATA PORT Request_in -> AccountDataT.Request_in;
EVENT DATA PORT NumCard_in -> AccountDataT.NumCard_in;
EVENT DATA PORT AccountDataT.session_id_out ->session_id_out;
END AccountData.impl;
PROCESS Account
FEATURES
cmd_in : IN EVENT DATA PORT Integer_Type;
amount_in : IN EVENT DATA PORT Integer_Type;
session_id_in : IN EVENT DATA PORT Integer_Type;
result_out : OUT EVENT DATA PORT Integer_Type;
END Account;
PROCESS IMPLEMENTATION Account.impl
SUBCOMPONENTS
AccountT: THREAD AccountThread.Impl;
CONNECTIONS
EVENT DATA PORT cmd_in -> AccountT.cmd_in;
EVENT DATA PORT amount_in -> AccountT.amount_in;
EVENT DATA PORT AccountT.result_out -> result_out;
EVENT DATA PORT session_id_in -> AccountT.session_id_in ;
END Account.impl;
THREAD GUIThread
FEATURES
NumCard_in: IN EVENT DATA PORT Integer_Type;
Code_in: IN EVENT DATA PORT Integer_Type;
result_in: IN EVENT DATA PORT Integer_Type;
RejectedCard_in: IN EVENT DATA PORT Integer_Type;
OK_in: IN EVENT DATA PORT Integer_Type;
RestoreCode_in: IN EVENT DATA PORT Integer_Type;
session_id_in: IN EVENT DATA PORT Integer_Type;
Control_out: OUT EVENT DATA PORT Integer_Type;
NumCard_out: OUT EVENT DATA PORT Integer_Type;
Code_out: OUT EVENT DATA PORT Integer_Type;
cmd_out: OUT EVENT DATA PORT Integer_Type;
amount_out: OUT EVENT DATA PORT Integer_Type;
session_id_out: OUT EVENT DATA PORT Integer_Type;
END GUIThread;
THREAD IMPLEMENTATION GUIThread.impl
PROPERTIES
Dispatch_protocol => Sporadic;