Commit 168e24e1 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Update the model checker backend

use the latest API of asn1-iterators
parent 688a4805
...@@ -35,13 +35,13 @@ end if;''' ...@@ -35,13 +35,13 @@ end if;'''
exhaust_procedure = '''procedure exhaust_<interface> is exhaust_procedure = '''procedure exhaust_<interface> is
<if(param)><interface>_it : <sort>_pkg.Instance;<endif> <if(param)><interface>_it : <sort>_pkg.Instance;<endif>
event : Event_ty(<interface>); event : Event_ty(<interface>_pi);
S_Hash : Hash_Type; S_Hash : Hash_Type;
begin begin
backup_ctxt := Process_Ctxt; backup_ctxt := Process_Ctxt;
<if(param)> <if(param)>
for each of <interface>_it loop for each of <interface>_it loop
event.<interface>_param := each; <sort>_pkg.To_ASN1(each, event.<interface>_param);
<model>.<interface>(event.<interface>_param'access); <model>.<interface>(event.<interface>_param'access);
count := count + 1; count := count + 1;
S_Hash := Add_to_graph(event => event); S_Hash := Add_to_graph(event => event);
...@@ -64,8 +64,8 @@ end if;''' ...@@ -64,8 +64,8 @@ end if;'''
checker_template = '''with <model>; checker_template = '''with <model>;
use <model>; use <model>;
with <model>_stop_conditions; with <model>_stop_conditions;
with asn1_iterators; with asn1_iterators.iterators;
use asn1_iterators; use asn1_iterators.iterators;
<asn1_modules;separator="\n"> <asn1_modules;separator="\n">
......
...@@ -16,7 +16,7 @@ Author: Maxime.Perrotin@esa.int ...@@ -16,7 +16,7 @@ Author: Maxime.Perrotin@esa.int
__author__ = "Maxime Perrotin" __author__ = "Maxime Perrotin"
__license__ = "LGPL v3" __license__ = "LGPL v3"
__version__ = "1.0.4" __version__ = "1.1.0"
__url__ = "http://taste.tuxfamily.org" __url__ = "http://taste.tuxfamily.org"
import os import os
......
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