Commit bcfdf1b4 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

traces not removed at proper point

parent 100192ed
......@@ -102,6 +102,7 @@ export_nusmv_stream_reactions(Stream) :-
findall(
(Reactants, [], Products, []),
(
% FIXME we do not take care of reversible reactions
item([kind: reaction, item: Item]),
reaction(Item, _, Reactants, Products)
),
......@@ -513,7 +514,13 @@ check_ctl_impl(Query, some, NusmvCX, BoolSem, Result) :-
).
% stores the counter-example trace from NuSMV
% argument is a list, with R, then molecules in enumerate_all_molecules order
:- dynamic(trace/1).
check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
retractall(trace(_)),
translate_ctl_for_nusmv(Query, NusmvQuery),
% FIXME better template, in $TMP, check if not existing, etc.
export_nusmv_file(nusmv, BoolSem),
......@@ -629,16 +636,11 @@ parse_nusmv_out(Out, NusmvCX, Result) :-
parse_nusmv_out(Out, NusmvCX, Result)
).
% stores the counter-example trace from NuSMV
% argument is a list, with R, then molecules in enumerate_all_molecules order
:- dynamic(trace/1).
parse_nusmv_out_trace(Out) :-
% -- as demonstrated by the following execution sequence
read_line_to_codes(Out, [0'-, 0'-, 0' | _]),
!,
read_line_to_codes(Out, [0'N, 0'a, 0'm, 0'e, 0'\t | _]),
retractall(trace(_)),
read_string(Out, "\n", "\r", _End, InitialString),
state_string_to_trace(InitialString, InitialTrace),
assertz(trace(InitialTrace)),
......
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