Commit 9ed796d3 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

Removed fake initial state for influences too

parent 25b17828
......@@ -227,15 +227,6 @@ export_nusmv_stream_influences(Stream) :-
export_initial_state_influences(Stream, Molecules, InfluenceCount) :-
write(Stream, 'VAR\n'),
FirstState = 0,
format(Stream, 'I: ~d..~d;\n', [FirstState, InfluenceCount]),
\+ (
member(Molecule, Molecules),
\+ (
make_nusmv_name(Molecule, Name),
format(Stream, '~a: boolean;\n', [Name])
)
),
(
InfluenceCount < 2
->
......@@ -243,11 +234,19 @@ export_initial_state_influences(Stream, Molecules, InfluenceCount) :-
;
format(atom(NextStates), '1..~d', [InfluenceCount])
),
format(Stream, 'I: ~a;\n', [NextStates]),
\+ (
member(Molecule, Molecules),
\+ (
make_nusmv_name(Molecule, Name),
format(Stream, '~a: boolean;\n', [Name])
)
),
format(Stream, '\c
ASSIGN
init(I) := ~d;
init(I) := ~a;
next(I) := ~a;
', [FirstState, NextStates]).
', [NextStates, NextStates]).
export_influences(Stream, Molecules, Influences) :-
\+ (
......@@ -263,10 +262,9 @@ export_molecule_influences(Stream, Molecule, Influences) :-
get_initial_state(Molecule, InitialState),
nusmv_initial_state(InitialState, NusmvInitialState),
format(Stream, '\c
init(~a) := FALSE;
init(~a) := ~a;
next(~a) := case
I = 0: ~a;
', [Name, Name, NusmvInitialState]),
', [Name, NusmvInitialState, Name]),
\+ (
nth1(InfluenceIndex, Influences, i(_Force,PositiveInputs,NegativeInputs,Sign,Output)),
\+ (
......
......@@ -2,17 +2,30 @@
:- begin_tests(nusmv).
test('export', [setup(set_a_dummy_model), cleanup(clear_model)]) :-
test('export_reac', [setup(set_a_dummy_reaction_model), cleanup(clear_model)]) :-
export_nusmv('unittest').
test('check_ctl', [setup(set_a_dummy_model), cleanup(clear_model)]) :-
check_ctl('AG'(not(c) \/ b)).
test('check_ctl_reac', [setup(set_a_dummy_reaction_model), cleanup(clear_model)]) :-
check_ctl('AG'(not(c) \/ b)).
set_a_dummy_model :-
test('export_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :-
export_nusmv('unittest').
test('check_ctl_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :-
check_ctl('AG'(not(c) \/ b)).
set_a_dummy_reaction_model :-
clear_model,
add_reaction(a => b),
add_reaction(a + b => c),
command(present(a)),
command(absent(c)).
set_a_dummy_influence_model :-
clear_model,
add_influence(a -> b),
add_influence((a, b) -< c),
command(present(a)),
command(present(c)).
:- end_tests(nusmv).
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