Commit 419075b1 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Update model checking test case

parent f3593584
......@@ -27,6 +27,7 @@ PUBLIC
WITH interfaceview::IV::orchestrator;
WITH interfaceview::IV::simulator_gui;
WITH interfaceview::IV::another_function;
WITH ocarina_processors_x86;
WITH deploymentview::DV::Node1;
WITH Taste;
......@@ -44,6 +45,9 @@ SUBCOMPONENTS
IV_simulator_gui : SYSTEM interfaceview::IV::simulator_gui::simulator_gui.others {
Taste::FunctionName => "simulator_gui";
};
IV_another_function : SYSTEM interfaceview::IV::another_function::another_function.others {
Taste::FunctionName => "another_function";
};
demo : PROCESS deploymentview::DV::Node1::demo.others {
Taste::coordinates => "124694 58687 147018 75906";
Deployment::Port_Number => 0;
......@@ -54,6 +58,7 @@ SUBCOMPONENTS
PROPERTIES
Taste::APLC_Binding => (reference (demo)) APPLIES TO IV_orchestrator;
Taste::APLC_Binding => (reference (demo)) APPLIES TO IV_simulator_gui;
Taste::APLC_Binding => (reference (demo)) APPLIES TO IV_another_function;
Actual_Processor_Binding => (reference (x86_linux)) APPLIES TO demo;
END Node1.others;
......@@ -72,6 +77,6 @@ PROPERTIES
Taste::coordinates => "0 0 297000 210000";
Taste::version => "2.4";
Taste::interfaceView => "InterfaceView.aadl";
Taste::HWLibraries => ("/home/taste/tool-inst/share/ocarina/AADLv2/ocarina_components.aadl");
Taste::HWLibraries => ("../../../../tool-inst/share/ocarina/AADLv2/ocarina_components.aadl");
END deploymentview::DV;
......@@ -9,6 +9,7 @@ PACKAGE interfaceview::IV::orchestrator
PUBLIC
WITH interfaceview::IV::simulator_gui;
WITH interfaceview::IV::another_function;
WITH Taste;
WITH DataView;
WITH TASTE_IV_Properties;
......@@ -32,6 +33,16 @@ END RI_paramesstogui;
SUBPROGRAM IMPLEMENTATION RI_paramesstogui.others
END RI_paramesstogui.others;
SUBPROGRAM RI_do_something
FEATURES
param1 : IN PARAMETER DataView::T_UInt32 {
Taste::encoding => NATIVE;
};
END RI_do_something;
SUBPROGRAM IMPLEMENTATION RI_do_something.others
END RI_do_something.others;
SYSTEM orchestrator
FEATURES
PI_pulse : PROVIDES SUBPROGRAM ACCESS interfaceview::IV::orchestrator::PI_pulse.others {
......@@ -47,6 +58,12 @@ FEATURES
Taste::InterfaceName => "paramesstogui";
Taste::labelInheritance => "true";
};
RI_do_something : REQUIRES SUBPROGRAM ACCESS interfaceview::IV::another_function::PI_do_something.others {
Taste::coordinates => "195417 115007";
Taste::RCMoperationKind => any;
Taste::InterfaceName => "do_something";
Taste::labelInheritance => "true";
};
PROPERTIES
Source_Language => (SDL);
Taste::Active_Interfaces => any;
......@@ -64,6 +81,16 @@ WITH interfaceview::IV::orchestrator;
WITH Taste;
WITH DataView;
WITH TASTE_IV_Properties;
SUBPROGRAM PI_paramesstogui
PROPERTIES
Taste::Associated_Queue_Size => 1;
END PI_paramesstogui;
SUBPROGRAM IMPLEMENTATION PI_paramesstogui.others
PROPERTIES
Compute_Execution_Time => 0 ms .. 0 ms;
END PI_paramesstogui.others;
SUBPROGRAM RI_pulse
FEATURES
p1 : IN PARAMETER DataView::T_Int {
......@@ -74,27 +101,21 @@ END RI_pulse;
SUBPROGRAM IMPLEMENTATION RI_pulse.others
END RI_pulse.others;
SUBPROGRAM PI_paramesstogui
END PI_paramesstogui;
SUBPROGRAM IMPLEMENTATION PI_paramesstogui.others
PROPERTIES
Compute_Execution_Time => 0 ms .. 0 ms;
END PI_paramesstogui.others;
SYSTEM simulator_gui
FEATURES
PI_paramesstogui : PROVIDES SUBPROGRAM ACCESS interfaceview::IV::simulator_gui::PI_paramesstogui.others {
Taste::coordinates => "119740 83208";
Taste::RCMoperationKind => sporadic;
Taste::RCMperiod => 0 ms;
Taste::Deadline => 0 ms;
Taste::InterfaceName => "paramesstogui";
};
RI_pulse : REQUIRES SUBPROGRAM ACCESS interfaceview::IV::orchestrator::PI_pulse.others {
Taste::coordinates => "119740 66705";
Taste::RCMoperationKind => any;
Taste::InterfaceName => "pulse";
Taste::labelInheritance => "true";
};
PI_paramesstogui : PROVIDES SUBPROGRAM ACCESS interfaceview::IV::simulator_gui::PI_paramesstogui.others {
Taste::coordinates => "119740 83208";
Taste::RCMoperationKind => sporadic;
Taste::InterfaceName => "paramesstogui";
};
PROPERTIES
Source_Language => (GUI);
Taste::Active_Interfaces => any;
......@@ -105,11 +126,49 @@ END simulator_gui.others;
END interfaceview::IV::simulator_gui;
PACKAGE interfaceview::IV::another_function
PUBLIC
WITH Taste;
WITH DataView;
WITH TASTE_IV_Properties;
SUBPROGRAM PI_do_something
FEATURES
param1 : IN PARAMETER DataView::T_UInt32 {
Taste::encoding => NATIVE;
};
PROPERTIES
Taste::Associated_Queue_Size => 1;
END PI_do_something;
SUBPROGRAM IMPLEMENTATION PI_do_something.others
PROPERTIES
Compute_Execution_Time => 0 ms .. 0 ms;
END PI_do_something.others;
SYSTEM another_function
FEATURES
PI_do_something : PROVIDES SUBPROGRAM ACCESS interfaceview::IV::another_function::PI_do_something.others {
Taste::coordinates => "195324 130628";
Taste::RCMoperationKind => sporadic;
Taste::InterfaceName => "do_something";
};
PROPERTIES
Source_Language => (SDL);
Taste::Active_Interfaces => any;
END another_function;
SYSTEM IMPLEMENTATION another_function.others
END another_function.others;
END interfaceview::IV::another_function;
PACKAGE interfaceview::IV
PUBLIC
WITH interfaceview::IV::orchestrator;
WITH interfaceview::IV::simulator_gui;
WITH interfaceview::IV::another_function;
WITH Taste;
WITH DataView;
WITH TASTE_IV_Properties;
......@@ -127,6 +186,9 @@ SUBCOMPONENTS
simulator_gui : SYSTEM interfaceview::IV::simulator_gui::simulator_gui.others {
Taste::coordinates => "33291 42009 119740 110860";
};
another_function : SYSTEM interfaceview::IV::another_function::another_function.others {
Taste::coordinates => "174060 130628 254069 171430";
};
CONNECTIONS
simulator_gui_RI_pulse_orchestrator_PI_pulse : SUBPROGRAM ACCESS orchestrator.PI_pulse -> simulator_gui.RI_pulse {
Taste::coordinates => "119740 66705 136103 66705 136103 68382 157343 68382";
......@@ -134,6 +196,9 @@ CONNECTIONS
orchestrator_RI_paramesstogui_simulator_gui_PI_paramesstogui : SUBPROGRAM ACCESS simulator_gui.PI_paramesstogui -> orchestrator.RI_paramesstogui {
Taste::coordinates => "157343 81798 138541 81798 138541 83208 119740 83208";
};
orchestrator_RI_do_something_another_function_PI_do_something : SUBPROGRAM ACCESS another_function.PI_do_something -> orchestrator.RI_do_something {
Taste::coordinates => "195417 115007 195417 122817 195324 122817 195324 130628";
};
END interfaceview.others;
PROPERTIES
......
/* CIF PROCESS (250, 150), (150, 75) */
process Another_Function;
/* CIF START (148, 10), (70, 35) */
/* CIF TEXT (268, 0), (267, 111) */
-- Text area for declarations and comments
dcl param1 T_UInt32;
/* CIF ENDTEXT */
/* CIF START (148, 70), (70, 35) */
START;
/* CIF NEXTSTATE (148, 60), (70, 35) */
/* CIF NEXTSTATE (148, 120), (70, 35) */
NEXTSTATE one;
/* CIF state (148, 60), (70, 35) */
/* CIF state (148, 120), (70, 35) */
state one;
/* CIF input (127, 115), (107, 35) */
input do_something;
/* CIF NEXTSTATE (146, 170), (70, 35) */
NEXTSTATE one;
endstate;
/* CIF state (456, 10), (70, 35) */
state two;
/* CIF input (435, 65), (107, 35) */
input do_something;
/* CIF NEXTSTATE (454, 120), (70, 35) */
/* CIF input (100, 175), (160, 35) */
input do_something(param1);
/* CIF NEXTSTATE (145, 230), (70, 35) */
NEXTSTATE one;
endstate;
endprocess Another_Function;
\ No newline at end of file
......@@ -21,48 +21,53 @@ process Orchestrator;
input pulse(t);
/* CIF decision (496, 447), (70, 50) */
decision t = 2;
/* CIF ANSWER (451, 517), (70, 24) */
/* CIF ANSWER (420, 517), (70, 24) */
(true):
/* CIF output (430, 561), (110, 35) */
/* CIF output (400, 561), (110, 35) */
output paramesstogui;
/* CIF NEXTSTATE (451, 616), (70, 35) */
NEXTSTATE wait;
/* CIF NEXTSTATE (420, 616), (70, 35) */
NEXTSTATE step_2;
/* CIF ANSWER (552, 517), (70, 24) */
(false):
/* CIF NEXTSTATE (552, 561), (70, 35) */
NEXTSTATE step_2;
/* CIF output (521, 561), (130, 35) */
output do_something(42);
/* CIF NEXTSTATE (550, 611), (73, 35) */
NEXTSTATE all_done;
enddecision;
endstate;
/* CIF state (815, 543), (73, 35) */
state all_done;
endstate;
/* CIF state (999, 100), (67, 35) */
state wait;
/* CIF input (996, 155), (71, 35) */
input pulse(t);
/* CIF decision (986, 210), (89, 50) */
decision counter = 3;
/* CIF ANSWER (875, 280), (70, 24) */
/* CIF ANSWER (830, 280), (70, 24) */
(true):
/* CIF task (839, 324), (141, 35) */
/* CIF task (791, 324), (148, 35) */
task magic_number := 42;
/* CIF NEXTSTATE (875, 379), (70, 35) */
/* CIF NEXTSTATE (830, 379), (70, 35) */
NEXTSTATE Step_2;
/* CIF ANSWER (1068, 280), (70, 24) */
(false):
enddecision;
/* CIF decision (996, 430), (70, 50) */
decision t;
/* CIF ANSWER (914, 500), (70, 25) */
(4):
/* CIF task (878, 545), (141, 59) */
task counter := 3;
/* CIF ANSWER (1061, 500), (70, 25) */
else:
/* CIF task (1025, 545), (141, 59) */
task counter := 0,
/* CIF decision (1068, 324), (70, 50) */
decision t;
/* CIF ANSWER (986, 394), (70, 25) */
(4):
/* CIF task (950, 439), (141, 59) */
task counter := 3;
/* CIF ANSWER (1133, 394), (70, 25) */
else:
/* CIF task (1097, 439), (141, 59) */
task counter := 0,
magic_number := 0;
enddecision;
/* CIF task (1068, 514), (70, 35) */
task t := 0;
/* CIF NEXTSTATE (1068, 569), (70, 35) */
NEXTSTATE wait;
enddecision;
/* CIF task (996, 620), (70, 35) */
task t := 0;
/* CIF NEXTSTATE (996, 675), (70, 35) */
NEXTSTATE wait;
endstate;
endprocess Orchestrator;
\ No newline at end of file
......@@ -14,7 +14,7 @@ observer/my_observer.adb: observer/observer.pr observer/observer.asn
# gather dataviews needed to build an observer
observer/observer.asn: ../dataview/dataview-uniq.asn ../build/simulation.asn ../orchestrator/SDL/code/orchestrator_datamodel.asn # ../another_function/SDL/code/another_function_datamodel.asn
observer/observer.asn: ../dataview/dataview-uniq.asn ../build/simulation.asn ../orchestrator/SDL/code/orchestrator_datamodel.asn ../another_function/SDL/code/another_function_datamodel.asn
cat $^ > $@
clean:
......
......@@ -36,6 +36,9 @@ Simulation-DataView DEFINITIONS ::=
BEGIN
IMPORTS
-- ASN.1 modules used by thread another_function_do_something
T-UInt32 FROM TASTE-BasicTypes
-- ASN.1 modules used by thread orchestrator_pulse
T-Int FROM Iterators-Types
......@@ -44,17 +47,25 @@ BEGIN
-- Import generic integer type (used for timers)
T-UInt32 FROM TASTE-BasicTypes
-- Import the SDL function states needed for the global system state
Orchestrator-Context FROM Orchestrator-Datamodel
Another-function-Context FROM Another-function-Datamodel
Orchestrator-Context FROM Orchestrator-Datamodel
;
Another-Function-Event ::= CHOICE {
msg-in CHOICE {
do-something SEQUENCE { param1 T-UInt32 }
}
}
Orchestrator-Event ::= CHOICE {
msg-in CHOICE {
pulse SEQUENCE { p1 T-Int }
},
msg-out CHOICE {
do-something SEQUENCE { param1 T-UInt32 },
paramesstogui SEQUENCE { }
}
}
......@@ -72,13 +83,14 @@ BEGIN
-- List all the TASTE functions present in the system
PID ::= ENUMERATED {
env, orchestrator, simulator-gui
env, another-function, orchestrator, simulator-gui
}
-- Event related to the execution of a PI or call of a RI in the functional code
Function-Event ::= CHOICE {
orchestrator Orchestrator-Event,
simulator-gui Simulator-Gui-Event
another-function Another-Function-Event,
orchestrator Orchestrator-Event,
simulator-gui Simulator-Gui-Event
}
-- Event at interface level (PI or RI), including source and destination ID
......@@ -103,9 +115,11 @@ BEGIN
-- Global system state (excluding observers, which are defined later)
System-State ::= SEQUENCE {
-- Message queues
orchestrator-queue Events-Ty (SIZE (0..2)),
another-function-queue Events-Ty (SIZE (0..2)),
orchestrator-queue Events-Ty (SIZE (0..2)),
orchestrator Orchestrator-Context
another-function Another-function-Context,
orchestrator Orchestrator-Context
}
END
Orchestrator-Datamodel DEFINITIONS ::=
......@@ -114,7 +128,7 @@ IMPORTS
T-Null, T-Int, T-SeqOf FROM Iterators-Types
T-Int32, T-UInt32, T-Int8, T-UInt8, T-Boolean, T-Null-Record FROM TASTE-BasicTypes;
Orchestrator-States ::= ENUMERATED {step-2, wait}
Orchestrator-States ::= ENUMERATED {wait, all-done, step-2}
Orchestrator-Context ::= SEQUENCE {
state Orchestrator-States,
......@@ -125,3 +139,18 @@ Orchestrator-Context ::= SEQUENCE {
}
END
Another-function-Datamodel DEFINITIONS ::=
BEGIN
IMPORTS
T-Null, T-Int, T-SeqOf FROM Iterators-Types
T-Int32, T-UInt32, T-Int8, T-UInt8, T-Boolean, T-Null-Record FROM TASTE-BasicTypes;
Another-function-States ::= ENUMERATED {one}
Another-function-Context ::= SEQUENCE {
state Another-function-States,
init-done BOOLEAN,
param1 T-UInt32
}
END
......@@ -20,87 +20,169 @@ observe;
connect c and r;
/* CIF PROCESS (250, 87), (150, 75) */
process my_observer;
/* CIF TEXT (0, 57), (309, 104) */
/* CIF TEXT (0, 57), (256, 152) */
monitor st System_State;
monitor event Observable_Event;
dcl count T_Int renames st.orchestrator.counter;
dcl count T_Int
renames st.orchestrator.counter;
dcl actual_val T_UInt32
renames st.another_function.param1;
/* CIF ENDTEXT */
/* CIF procedure (1254, 63), (70, 35) */
/* CIF procedure (1390, 63), (70, 35) */
procedure observe;
/* CIF TEXT (38, 48), (313, 120) */
/* CIF TEXT (120, 48), (313, 120) */
-- this procedure could be generated automatically,
-- and be read-only.
fpar in/out model System_State,
in/out last_event Observable_Event;
/* CIF ENDTEXT */
/* CIF START (362, 153), (70, 35) */
/* CIF START (444, 153), (70, 35) */
START;
/* CIF task (328, 208), (137, 40) */
/* CIF task (410, 208), (137, 40) */
task st := model,
Event := Last_Event;
/* CIF return (379, 268), (35, 35) */
/* CIF PROCEDURECALL (325, 268), (308, 35) */
call writeln('[observer] Event: ', present(event));
/* CIF decision (422, 323), (113, 50) */
decision present(event);
/* CIF ANSWER (97, 393), (93, 24) */
(input_event):
/* CIF PROCEDURECALL (0, 437), (289, 35) */
call writeln('FROM: ', event.input_event.source);
/* CIF PROCEDURECALL (0, 492), (289, 35) */
call writeln('TO: ', event.input_event.dest);
/* CIF ANSWER (392, 393), (103, 24) */
(output_event):
/* CIF PROCEDURECALL (299, 437), (290, 35) */
call writeln('FROM: ', event.output_event.source);
/* CIF PROCEDURECALL (300, 492), (289, 35) */
call writeln('TO: ', event.output_event.dest);
/* CIF ANSWER (627, 393), (114, 24) */
(system_startup):
/* CIF PROCEDURECALL (600, 437), (169, 35) */
call writeln('system startup');
/* CIF ANSWER (825, 393), (78, 24) */
(no_event):
/* CIF PROCEDURECALL (780, 437), (169, 35) */
call writeln('no_event');
enddecision;
/* CIF return (461, 543), (35, 35) */
return ;
endprocedure;
/* CIF START (433, 78), (70, 35) */
/* CIF START (333, 88), (70, 35) */
START;
/* CIF PROCEDURECALL (388, 133), (159, 35) */
/* CIF PROCEDURECALL (288, 143), (159, 35) */
call writeln ('observer init');
/* CIF NEXTSTATE (426, 183), (83, 35) */
/* CIF NEXTSTATE (326, 193), (83, 35) */
NEXTSTATE first_state;
/* CIF state (1013, 111), (101, 35) */
/* CIF state (586, 370), (88, 35) */
state third_state;
/* CIF provided (548, 425), (173, 72) */
provided output paramesstogui
from orchestrator;
/* CIF PROCEDURECALL (455, 517), (359, 35) */
call writeln('[observer] detected output paramesstogui');
/* CIF NEXTSTATE (585, 567), (97, 40) */
NEXTSTATE fourth_state;
endstate;
/* CIF state (1149, 111), (101, 35) */
state second_state;
/* CIF provided (963, 168), (241, 35) */
/* CIF provided (1085, 166), (241, 35) */
provided st.orchestrator.magic_number = 42;
/* CIF PROCEDURECALL (904, 223), (359, 35) */
/* CIF PROCEDURECALL (1026, 221), (359, 35) */
call writeln ('[observer] step 2 passed (magic_number =42)');
/* CIF NEXTSTATE (1033, 273), (101, 35) */
/* CIF NEXTSTATE (1155, 271), (101, 35) */
NEXTSTATE third_state;
endstate;
/* CIF state (116, 218), (95, 35) */
/* CIF state (49, 262), (95, 35) */
state end_success;
endstate;
/* CIF state (1137, 316), (88, 35) */
state third_state;
/* CIF provided (1104, 371), (341, 136) */
provided event =
output_event : {
source orchestrator,
dest simulator_gui,
event orchestrator: msg_out : paramesstogui : {}
};
priority 2;
/* CIF PROCEDURECALL (1186, 538), (176, 35) */
call writeln ('SUCCESS(1)');
/* CIF NEXTSTATE (1226, 593), (95, 35) */
NEXTSTATE end_success;
/* CIF provided (526, 371), (525, 104) */
provided present(event) = output_event
and then event.output_event.dest = simulator_gui
and then present(event.output_event.event) = orchestrator
and then present(event.output_event.event.orchestrator.msg_out) = paramesstogui;
priority 3;
/* CIF PROCEDURECALL (701, 506), (176, 35) */
call writeln ('SUCCESS(2)');
/* CIF NEXTSTATE (741, 561), (95, 35) */
NEXTSTATE end_success;
/* CIF provided (1495, 371), (173, 72) */
provided output paramesstogui
from orchestrator;
priority 1;
/* CIF NEXTSTATE (1533, 474), (95, 40) */
/* CIF state (683, 128), (92, 35) */
state Wait_Count;
/* CIF provided (686, 183), (85, 35) */
provided count = 3
/* CIF comment (793, 179), (104, 40) */
comment 'Called AFTER
the input';
/* CIF PROCEDURECALL (578, 238), (300, 35) */
call writeln ('[observer] step 1 passed (counter=3)');
/* CIF NEXTSTATE (677, 293), (101, 35) */
NEXTSTATE second_state;
endstate;
/* CIF state (242, 503), (92, 35) */
state unexpected;
endstate;
/* CIF state (1320, 358), (85, 35) */
state fifth_state;
/* CIF provided (1278, 413), (168, 40) */
provided input do_something(val)
to another_function
/* CIF comment (1468, 397), (134, 72) */
comment 'intercept the input
before execution
(=post-output)
alter it again';
/* CIF decision (1328, 473), (70, 50) */
decision val = 99;
/* CIF ANSWER (1284, 543), (62, 24) */
(true):
/* CIF task (1268, 587), (93, 35) */
task val := val + 1;
/* CIF NEXTSTATE (1271, 637), (87, 35) */
NEXTSTATE sixth_state;
/* CIF ANSWER (1376, 543), (70, 24) */
(false):
/* CIF NEXTSTATE (1364, 587), (92, 35) */
NEXTSTATE unexpected;
enddecision;
endstate;
/* CIF state (1674, 356), (87, 35) */
state sixth_state;
/* CIF provided (1659, 411), (124, 35) */
provided actual_val = 100;
/* CIF NEXTSTATE (1673, 466), (95, 35) */
NEXTSTATE end_success;
endstate;
/* CIF state (426, 183), (83, 35) */
/* CIF state (953, 357), (97, 35) */
state fourth_state;
/* CIF provided (917, 412), (176, 56) */
provided output do_something(p)
from orchestrator
to another_function
/* CIF comment (1112, 421), (146, 56) */
comment 'intercept the output
and modify the value
of the parameter';
/* CIF PROCEDURECALL (825, 488), (359, 35) */
call writeln('[observer] detected output do_something');
/* CIF decision (970, 538), (70, 50) */
decision p = 42;
/* CIF ANSWER (925, 608), (70, 24) */
(true):
/* CIF task (925, 652), (70, 35) */
task p := 99;
/* CIF NEXTSTATE (917, 707), (85, 35) */
NEXTSTATE fifth_state;
/* CIF ANSWER (1025, 608), (70, 24) */
(false):
/* CIF NEXTSTATE (1013, 652), (92, 35) */
NEXTSTATE unexpected;
enddecision;
endstate;
/* CIF state (326, 193), (83, 35) */
state first_state;
/* CIF provided (425, 239), (85, 35) */
provided count;
/* CIF PROCEDURECALL (317, 294), (300, 35) */
call writeln ('[observer] step 1 passed (counter=3)');
/* CIF NEXTSTATE (416, 349), (101, 35) */
NEXTSTATE second_state;
/* CIF provided (305, 249), (113, 40) */
provided input pulse
to orchestrator
/* CIF comment (445, 249), (111, 40) */
comment 'Called BEFORE
the input';
/* CIF NEXTSTATE (312, 309), (101, 35) */
NEXTSTATE Wait_count;
endstate;
endprocess my_observer;
endblock;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment