Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
TASTE
kazoo
Commits
991344f4
Commit
991344f4
authored
Jun 25, 2021
by
Maxime Perrotin
Browse files
Update test case for model checking
parent
475dbe04
Changes
3
Hide whitespace changes
Inline
Side-by-side
test/iterators/work/simulation/mcsrc/properties.adb
View file @
991344f4
...
...
@@ -28,6 +28,7 @@ package body Properties is
Event
:
in
out
asn1sccObservable_Event
;
Id
:
out
Natural
;
Success
:
out
Boolean
)
is
Observer_State_Status
:
asn1SccObserver_State_Kind
;
begin
Id
:=
0
;
-- Restore the state of the observer, and execute it
...
...
@@ -35,13 +36,14 @@ package body Properties is
-- Put_Line ("[OBS] Context set to: " & GSER.Image (My_Observer.Ctxt));
-- Set the observer's monitors
My_Observer
.
Observe
(
Full_State
.
User_State
,
Event
);
Observer_State_Status
:=
My_Observer
.
Observe
(
Full_State
.
User_State
,
Event
);
-- Read the modified state from the observer
Event
:=
My_Observer
.
Event
;
Full_State
.
User_state
:=
My_Observer
.
St
;
Full_State
.
My_Observer_State
:=
My_Observer
.
Ctxt
;
-- Simple stop condition:
Success
:=
(
My_Observer
.
Ctxt
.
State
=
My_Observer_Datamodel
.
asn1SccEnd_Success
);
Success
:=
(
Observer_State_Status
=
asn1SccError_State
);
-- My_Observer.Ctxt.State = My_Observer_Datamodel.asn1SccEnd_Success);
if
Success
then
Put_Line
(
"Stop condition found"
);
end
if
;
...
...
test/iterators/work/simulation/observer/observer.asn
View file @
991344f4
...
...
@@ -86,6 +86,14 @@ BEGIN
env, another-function, orchestrator, simulator-gui
}
-- Current observer state flag (used by model checkers)
Observer-State-Kind ::= ENUMERATED {
regular-state,
error-state,
ignore-state,
success-state
}
-- Event related to the execution of a PI or call of a RI in the functional code
Function-Event ::= CHOICE {
another-function Another-Function-Event,
...
...
@@ -132,7 +140,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 {
all-done,
step-2, wait}
Orchestrator-States ::= ENUMERATED {step-2, wait
, all-done
}
Orchestrator-Context ::= SEQUENCE {
state Orchestrator-States,
...
...
test/iterators/work/simulation/observer/observer.pr
View file @
991344f4
...
...
@@ -29,7 +29,7 @@ foo;
connect c and r;
/* CIF PROCESS (259, 87), (150, 75) */
process my_observer;
/* CIF TEXT (0, 57), (256, 2
16
) */
/* CIF TEXT (0, 57), (256, 2
48
) */
monitor st System_State;
monitor event Observable_Event;
...
...
@@ -41,8 +41,11 @@ foo;
renames st.another_function.param1;
dcl p1 T_Int;
successstates good;
errorstates corrupted;
/* CIF ENDTEXT */
/* CIF procedure (1
61
, 457), (106, 35) */
/* CIF procedure (1
49
, 457), (106, 35) */
procedure Discard_Event;
/* CIF START (182, 39), (70, 35) */
START;
...
...
@@ -51,163 +54,145 @@ foo;
/* CIF return (199, 149), (35, 35) */
return ;
endprocedure;
/* CIF procedure (2
145
, 1
5
2), (70, 35) */
/* CIF procedure (2
74
, 12
0
), (70, 35) */
procedure observe;
/* CIF TEXT (28
5
, 48), (3
1
3, 1
20
) */
/* CIF TEXT (28
8
, 48), (33
7
, 1
36
) */
-- this procedure could be generated automatically,
-- and be read-only.
fpar in/out model System_State,
in/out last_event Observable_Event;
returns Observer_State_Kind;
dcl curr_status Observer_State_Kind := regular_state;
/* CIF ENDTEXT */
/* CIF START (
609
, 1
53
), (70, 35) */
/* CIF START (
782
, 1
18
), (70, 35) */
START;
/* CIF task (
575, 208
), (137, 40) */
/* CIF task (
748, 173
), (137, 40) */
task st := model,
Event := Last_Event;
/* CIF PROCEDURECALL (
490
, 2
68
), (308, 35) */
/* CIF PROCEDURECALL (
663
, 2
33
), (308, 35) */
call writeln('[observer] Event: ', present(event));
/* CIF decision (
587, 323
), (113, 50) */
/* CIF decision (
760, 288
), (113, 50) */
decision present(event);
/* CIF ANSWER (9
7
, 3
93
), (93, 24) */
/* CIF ANSWER (
25
9, 3
58
), (93, 24) */
(input_event):
/* CIF PROCEDURECALL (
0
, 4
37
), (289, 35) */
/* CIF PROCEDURECALL (
162
, 4
02
), (289, 35) */
call writeln('FROM: ', event.input_event.source);
/* CIF PROCEDURECALL (
0
, 4
92
), (289, 35) */
/* CIF PROCEDURECALL (
162
, 4
57
), (289, 35) */
call writeln('TO: ', event.input_event.dest);
/* CIF ANSWER (
393
, 3
93
), (103, 24) */
/* CIF ANSWER (
555
, 3
58
), (103, 24) */
(output_event):
/* CIF PROCEDURECALL (
300
, 4
37
), (290, 35) */
/* CIF PROCEDURECALL (
462
, 4
02
), (290, 35) */
call writeln('FROM: ', event.output_event.source);
/* CIF PROCEDURECALL (
300
, 4
92
), (289, 35) */
/* CIF PROCEDURECALL (
463
, 4
57
), (289, 35) */
call writeln('TO: ', event.output_event.dest);
/* CIF ANSWER (
629
, 3
93
), (114, 24) */
/* CIF ANSWER (
791
, 3
58
), (114, 24) */
(system_startup):
/* CIF PROCEDURECALL (
601
, 4
37
), (169, 35) */
/* CIF PROCEDURECALL (
764
, 4
02
), (169, 35) */
call writeln('system startup');
/* CIF ANSWER (
827
, 3
93
), (78, 24) */
/* CIF ANSWER (
989
, 3
58
), (78, 24) */
(no_event):
/* CIF PROCEDURECALL (
781
, 4
37
), (169, 35) */
/* CIF PROCEDURECALL (
944
, 4
02
), (169, 35) */
call writeln('no_event');
/* CIF ANSWER (
984
, 3
93
), (123, 24) */
/* CIF ANSWER (
1146
, 3
58
), (123, 24) */
(unhandled_input):
/* CIF PROCEDURECALL (
974
, 4
37
), (142, 35) */
/* CIF PROCEDURECALL (
1137
, 4
02
), (142, 35) */
call writeln('Lost input');
enddecision;
/* CIF return (
626
, 5
43
), (35, 35) */
return ;
/* CIF return (
799
, 5
08
), (35, 35) */
return
call observer_status
;
endprocedure;
/* CIF START (5
89
, 96), (70, 35) */
/* CIF START (5
56
, 96), (70, 35) */
START;
/* CIF NEXTSTATE (5
82
, 151), (83, 35) */
/* CIF NEXTSTATE (5
49
, 151), (83, 35) */
NEXTSTATE first_state;
/* CIF state (
1169
, 2
37
), (97, 40) */
/* CIF state (
864
, 2
45
), (97, 40) */
state fourth_state;
/* CIF provided (
1121, 297
), (193, 79) */
/* CIF provided (
816, 305
), (193, 79) */
provided output do_something(p)
from orchestrator
to another_function
/* CIF comment (1
337
, 3
08
), (146, 56) */
/* CIF comment (1
032
, 3
16
), (146, 56) */
comment 'intercept the output
and modify the value
of the parameter';
/* CIF decision (
1182, 396
), (70, 50) */
/* CIF decision (
877, 404
), (70, 50) */
decision p = 42;
/* CIF ANSWER (
1117
, 4
66
), (70, 24) */
/* CIF ANSWER (
812
, 4
74
), (70, 24) */
(true):
/* CIF task (
1117
, 51
0
), (70, 35) */
/* CIF task (
812
, 51
8
), (70, 35) */
task p := 99;
/* CIF NEXTSTATE (
1109
, 5
65
), (85, 35) */
/* CIF NEXTSTATE (
804
, 5
73
), (85, 35) */
NEXTSTATE fifth_state;
/* CIF ANSWER (12
17
, 4
66
), (70, 24) */
/* CIF ANSWER (
9
12, 4
74
), (70, 24) */
(false):
/* CIF NEXTSTATE (
1205
, 51
0
), (92, 35) */
NEXTSTATE
unexpec
ted;
/* CIF NEXTSTATE (
900
, 51
8
), (92, 35) */
NEXTSTATE
corrup
ted;
enddecision;
endstate;
/* CIF state (
1371
, 9
0
), (88, 35) */
/* CIF state (
868
, 9
8
), (88, 35) */
state third_state;
/* CIF input (1495, 147), (70, 35) */
input Foo (pr);
/* CIF output (1495, 202), (70, 35) */
output foo (pr);
/* CIF NEXTSTATE (1495, 252), (70, 35) */
NEXTSTATE -;
/* CIF provided (1132, 145), (173, 72) */
/* CIF provided (827, 153), (173, 72) */
provided output paramesstogui
from orchestrator;
/* CIF NEXTSTATE (
1169
, 2
37
), (97, 40) */
/* CIF NEXTSTATE (
864
, 2
45
), (97, 40) */
NEXTSTATE fourth_state;
endstate;
/* CIF state (1
8
08, 43
7
), (87, 35) */
/* CIF state (1
2
08, 43
0
), (87, 35) */
state sixth_state;
/* CIF provided (1
7
92, 4
92
), (121, 50) */
provided actual_val =
100
;
/* CIF NEXTSTATE (1
8
04, 5
62
), (95, 35) */
NEXTSTATE
end_success
;
/* CIF provided (1
1
92, 4
85
), (121, 50) */
provided actual_val =
99
;
/* CIF NEXTSTATE (1
2
04, 5
55
), (95, 35) */
NEXTSTATE
corrupted
;
endstate;
/* CIF state (1
8
26,
88
), (145, 57) */
/* CIF state (1
2
26,
131
), (145, 57) */
state fifth_state;
/* CIF provided (1
8
06,
165
), (184, 68) */
/* CIF provided (1
2
06,
208
), (184, 68) */
provided input do_something(val)
to another_function
/* CIF comment (2013, 163), (134, 72) */
comment 'intercept the input
before execution
(=post-output)
alter it again';
/* CIF decision (1848, 253), (99, 68) */
decision val = 99;
/* CIF ANSWER (1821, 343), (62, 24) */
(true):
/* CIF task (1805, 387), (93, 35) */
task val := val + 1;
/* CIF NEXTSTATE (1808, 437), (87, 35) */
to another_function;
/* CIF decision (1248, 296), (99, 68) */
decision val;
/* CIF ANSWER (1221, 386), (62, 24) */
(/= 42):
/* CIF NEXTSTATE (1208, 430), (87, 35) */
NEXTSTATE sixth_state;
/* CIF ANSWER (1
9
37, 3
43
), (70, 24) */
(fa
lse
)
:
/* CIF NEXTSTATE (1
9
25,
387
), (92, 35) */
NEXTSTATE
unexpecte
d;
/* CIF ANSWER (1
3
37, 3
86
), (70, 24) */
e
lse:
/* CIF NEXTSTATE (1
3
25,
430
), (92, 35) */
NEXTSTATE
Goo
d;
enddecision;
endstate;
/* CIF state (2
42
, 314), (92, 35) */
state
unexpec
ted;
/* CIF state (2
30
, 314), (92, 35) */
state
corrup
ted;
endstate;
/* CIF state (266, 262), (95, 35) */
state
end_success
;
state
good
;
endstate;
/* CIF state (40
3
, 39
4
), (101, 34) */
/* CIF state (
5
40, 39
2
), (101, 34) */
state second_state;
/* CIF provided (
335
, 44
9
), (239, 45) */
/* CIF provided (
472
, 44
7
), (239, 45) */
provided st.orchestrator.magic_number = 42;
/* CIF NEXTSTATE (
404
, 51
4
), (101, 35) */
/* CIF NEXTSTATE (
541
, 51
2
), (101, 35) */
NEXTSTATE third_state;
endstate;
/* CIF state (
404
, 28
4
), (101, 35) */
/* CIF state (
541
, 28
2
), (101, 35) */
state Wait_count;
/* CIF provided (412, 339), (85, 35) */
provided count = 3
/* CIF comment (521, 336), (136, 56) */
comment 'Called immediately
if true';
/* CIF NEXTSTATE (403, 394), (101, 34) */
/* CIF provided (549, 337), (85, 35) */
provided count = 3;
/* CIF NEXTSTATE (540, 392), (101, 34) */
NEXTSTATE second_state;
endstate;
/* CIF state (5
82
, 151), (83, 35) */
/* CIF state (5
49
, 151), (83, 35) */
state first_state;
/* CIF provided (
385
, 20
8
), (139, 56) */
/* CIF provided (
522
, 20
6
), (139, 56) */
provided input pulse
to orchestrator
/* CIF comment (
551
, 21
6
), (111, 40) */
/* CIF comment (
688
, 21
4
), (111, 40) */
comment 'Called AFTER
the input';
/* CIF NEXTSTATE (
404
, 28
4
), (101, 35) */
/* CIF NEXTSTATE (
541
, 28
2
), (101, 35) */
NEXTSTATE Wait_count;
/* CIF provided (672, 206), (148, 40) */
provided unhandled input
pulse to orchestrator;
/* CIF NEXTSTATE (712, 266), (70, 35) */
NEXTSTATE -;
endstate;
endprocess my_observer;
endblock;
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment