Commit fedab03a authored by Thierry Martinez's avatar Thierry Martinez

Fixed: Quoting of conditions in SMV influences

parent 197cfed1
......@@ -207,14 +207,17 @@ reactants_to_condition(Reactants, Condition) :-
findall(
ReactantName,
(
member(_ * Reactant, Reactants),
make_nusmv_name(Reactant, ReactantName)
member(_ * ReactantName, Reactants)
),
ReactantNames
),
atomic_list_concat(ReactantNames, ' & ', Condition).
objects_to_condition(ReactantNames, Condition).
objects_to_condition(Objects, Condition) :-
maplist(make_nusmv_name, Objects, ObjectNames),
atomic_list_concat(ObjectNames, ' & ', Condition).
export_nusmv_stream_influences(Stream) :-
write(Stream, 'MODULE main\n'),
findall(
......@@ -309,22 +312,9 @@ atomic_negation_concat(NegativeInput, NegativeInputp) :-
inputs_to_condition(PositiveInputs, NegativeInputs, Condition) :-
(
NegativeInputs = []
->
atomic_list_concat(PositiveInputs, ' & ', Condition)
;
maplist(atomic_negation_concat, NegativeInputs, NegativeInputsp),
atomic_list_concat(NegativeInputsp, ' & ', NegativeCondition),
(
PositiveInputs = []
->
Condition = NegativeCondition
;
atomic_list_concat(PositiveInputs, ' & ', PositiveCondition),
atomic_list_concat([PositiveCondition,NegativeCondition], ' & ', Condition)
)
).
maplist(atomic_negation_concat, NegativeInputs, NegativeInputsp),
append(PositiveInputs, NegativeInputsp, Inputs),
objects_to_condition(Inputs, Condition).
......@@ -498,10 +488,10 @@ check_ctl(Query, Options, Result) :-
),
format(Stream, 'check_ctlspec -p "~a"\nquit\n', [NusmvQuery]),
close(Stream),
process_create(
call_subprocess(
path('NuSMV'),
['-df', '-source', 'nusmv.cmd'],
[stdout(pipe(NusmvOut))]
[stdin(null), stdout(pipe(NusmvOut))]
),
parse_nusmv_out(NusmvOut, Options, Result),
(
......
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