Commit a5116975 authored by Maxime Perrotin's avatar Maxime Perrotin

Ada backend can import or export the internal state

parent 91ff4f48
......@@ -121,6 +121,10 @@ def _process(process, simu=False, **kwargs):
SHARED_LIB = True
LPREFIX = process_name + u'_ctxt'
# taste-properties module-specific flag for the Ada backend:
# import the state data from an external module
import_context = kwargs["ppty_check"] if "ppty_check" in kwargs else ""
# When building a shared library (with simu=True), generate a "mini-cv"
# for aadl2glueC to create the code interfacing with asn1scc
minicv = ['-- Automatically generated by OpenGEODE - do NOT modify!']
......@@ -274,8 +278,19 @@ LD_LIBRARY_PATH=. opengeode-simulator
process_level_decl.append('end record;')
process_level_decl.append('{ctxt}: {ctxt}_Ty;'.format(ctxt=LPREFIX))
if simu:
# Export the context, so that it can be manipulated from outside
# (in practice used by the "properties" module.
process_level_decl.append(u'pragma export (C, {ctxt}, "{ctxt}");'
.format(ctxt=LPREFIX))
# Exhaustive simulation needs a backup of the context to quickly undo
process_level_decl.append('{ctxt}_bk: {ctxt}_Ty;'.format(ctxt=LPREFIX))
process_level_decl.append(u'{ctxt}_bk: {ctxt}_Ty;'
.format(ctxt=LPREFIX))
elif import_context:
# Possibility to have the context defined outside the module
# in order for a model checker to view/modify internals without any
# copy at runtime
process_level_decl.append(u'pragma import (C, ctxt, "{}_ctxt");'
.format(import_context))
process_level_decl.append('CS_Only : constant Integer := {};'
.format(len(process.transitions)))
......
......@@ -36,50 +36,52 @@ dcl seqof t_seqof;
CALL writeln( 'Orchestrator startup');
/* CIF NEXTSTATE (445, 152), (67, 35) */
NEXTSTATE wait;
/* CIF STATE (693, 94), (70, 35) */
/* CIF STATE (733, 94), (70, 35) */
STATE running;
/* CIF INPUT (693, 149), (70, 35) */
/* CIF INPUT (733, 149), (70, 35) */
INPUT *;
/* CIF NEXTSTATE (693, 204), (70, 35) */
/* CIF NEXTSTATE (733, 204), (70, 35) */
NEXTSTATE wait;
ENDSTATE;
/* CIF STATE (445, 152), (67, 35) */
STATE wait;
/* CIF INPUT (190, 207), (70, 35) */
/* CIF INPUT (120, 207), (70, 35) */
INPUT pulse(t);
/* CIF DECISION (190, 262), (70, 50) */
/* CIF DECISION (120, 262), (70, 50) */
DECISION t;
/* CIF ANSWER (145, 332), (70, 23) */
/* CIF ANSWER (75, 332), (70, 23) */
(0):
/* CIF NEXTSTATE (145, 375), (70, 35) */
/* CIF NEXTSTATE (75, 375), (70, 35) */
NEXTSTATE wait;
/* CIF ANSWER (235, 332), (70, 23) */
/* CIF ANSWER (165, 332), (70, 23) */
else:
/* CIF NEXTSTATE (235, 375), (70, 35) */
/* CIF NEXTSTATE (165, 375), (70, 35) */
NEXTSTATE running;
ENDDECISION;
/* CIF INPUT (373, 207), (83, 35) */
/* CIF INPUT (371, 207), (83, 35) */
INPUT arr(seqof);
/* CIF TASK (314, 262), (202, 35) */
/* CIF TASK (312, 262), (202, 35) */
TASK counter := (counter + 1) mod 4;
/* CIF DECISION (355, 317), (121, 50) */
/* CIF DECISION (353, 317), (121, 50) */
DECISION seqof = {4,4,4,4}
and counter = 0;
/* CIF ANSWER (336, 387), (70, 23) */
(true):
/* CIF ANSWER (426, 387), (70, 23) */
/* CIF PROCEDURECALL (245, 430), (250, 35) */
CALL writeln( 'Property should be checked');
/* CIF ANSWER (522, 387), (70, 23) */
(false):
/* CIF TASK (409, 430), (103, 35) */
/* CIF TASK (506, 430), (103, 35) */
TASK seqof(1) := 1;
ENDDECISION;
/* CIF NEXTSTATE (380, 480), (70, 35) */
/* CIF NEXTSTATE (378, 480), (70, 35) */
NEXTSTATE -;
/* CIF INPUT (532, 207), (83, 35) */
/* CIF INPUT (629, 207), (83, 35) */
INPUT paramless;
/* CIF TASK (525, 262), (97, 38) */
TASK counter := 0,
/* CIF TASK (619, 262), (104, 38) */
TASK counter := 4,
t := 1;
/* CIF NEXTSTATE (539, 320), (70, 35) */
/* CIF NEXTSTATE (636, 320), (70, 35) */
NEXTSTATE running;
ENDSTATE;
ENDPROCESS orchestrator;
......
with orchestrator;
with orchestrator_stop_conditions;
with asn1_iterators;
use asn1_iterators;
with TASTE_BasicTypes;
use TASTE_BasicTypes;
with ada.text_io;
use ada.text_io;
procedure test is
count : natural := 0;
function check(errno: out natural) return boolean is
res : Boolean := false;
begin
put_line("checking properties");
errno := 0;
return orchestrator_stop_conditions.pproperty_0;
res := orchestrator_stop_conditions.pproperty_0;
count := count + 1;
return res;
end;
procedure check_and_report is
errno: Natural := 0;
begin
if check(errno) then
put_line("Property " & errno'img & " is not verified");
end if;
end;
procedure exhaust_pulse is
pulse_it : T_Int_pkg.Instance;
asn1_p : aliased asn1SccT_Int;
begin
for each of pulse_it loop
asn1_p := asn1SccT_Int'(asn1SccT_Int(each));
orchestrator.pulse(asn1_p'access);
check_and_report;
end loop;
end;
procedure exhaust_arr is
arr_it : T_SeqOf_pkg.Instance;
asn1_p : aliased asn1SccT_SeqOf;
begin
for each of arr_it loop
asn1_p.Length := each.Length;
for idx in 1..asn1_p.Length loop
asn1_p.Data(idx) := asn1SccT_Int'(asn1SccT_Int(each.Data(idx)));
end loop;
orchestrator.arr(asn1_p'access);
check_and_report;
end loop;
end;
errno: Natural := 0;
begin
put_line("hello");
orchestrator.startup;
if check(errno) then
put_line("Property " & errno'img & " is not verified");
end if;
check_and_report;
exhaust_pulse;
exhaust_arr;
put_line("Executed" & count'img & " functions");
end;
Markdown is supported
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