Commit 67bf374f authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain
Browse files

removed NuSMV use of DEFINE, added __valid variable

parent ba63b18d
......@@ -45,7 +45,8 @@ export_nusmv_stream_reactions(Stream) :-
length(Reactions, ReactionCount),
enumerate_molecules(Molecules),
export_initial_state_reactions(Stream, Molecules, ReactionCount),
export_reactions(Stream, Molecules, Reactions).
export_reactions(Stream, Molecules, Reactions),
export_valid_reactions(Stream, Reactions).
......@@ -57,9 +58,8 @@ export_initial_state_reactions(Stream, Molecules, ReactionCount) :-
;
format(atom(NextStates), '1..~d', [ReactionCount])
),
format(Stream, 'DEFINE allreactions := ~a;\n\n', [NextStates]),
write(Stream, 'VAR\n'),
write(Stream, 'R: allreactions;\n'),
format(Stream, 'R: ~a;\n', [NextStates]),
\+ (
member(Molecule, Molecules),
\+ (
......@@ -67,11 +67,12 @@ export_initial_state_reactions(Stream, Molecules, ReactionCount) :-
format(Stream, '~a: boolean;\n', [Name])
)
),
write(Stream, '\n\c
write(Stream, '__valid: boolean;\n'),
format(Stream, '\n\c
ASSIGN
init(R) := allreactions;
next(R) := allreactions;\n
').
init(R) := ~a;
next(R) := ~a;\n
', [NextStates, NextStates]).
export_reactions(Stream, Molecules, Reactions) :-
......@@ -106,15 +107,7 @@ next(~a) := case
)
->
format(Stream, ' R = ~d: case\n', [ReactionIndex]),
findall(
ReactantName,
(
member(_ * Reactant, Reactants),
make_nusmv_name(Reactant, ReactantName)
),
ReactantNames
),
atomic_list_concat(ReactantNames, ' & ', Condition),
reactants_to_condition(Reactants, Condition),
format(Stream, ' \c
(~a): ~a;
TRUE: ~a;
......@@ -131,6 +124,42 @@ next(~a) := case
', [Name]).
export_valid_reactions(Stream, Reactions) :-
write(Stream, 'init(__valid) := TRUE;\n'),
write(Stream, 'next(__valid) := case\n'),
findall(
ParenthesizedCondition,
(
member((Reactants, _Products), Reactions),
reactants_to_condition(Reactants, Condition),
atomic_list_concat(['(', Condition, ')'], ParenthesizedCondition)
),
Conditions
),
atomic_list_concat(Conditions, ' | ', AReactionIsEnabled),
format(Stream, ' !(~a): TRUE;\n', [AReactionIsEnabled]),
forall(
nth1(ReactionIndex, Reactions, (Reactants, _Products)),
(
reactants_to_condition(Reactants, Condition),
format(Stream, ' R = ~d & !(~a): FALSE;\n', [ReactionIndex, Condition])
)
),
write(Stream, ' TRUE: TRUE;\n esac;\n').
reactants_to_condition(Reactants, Condition) :-
findall(
ReactantName,
(
member(_ * Reactant, Reactants),
make_nusmv_name(Reactant, ReactantName)
),
ReactantNames
),
atomic_list_concat(ReactantNames, ' & ', Condition).
export_nusmv_stream_influences(Stream) :-
write(Stream, 'MODULE main\n'),
findall(
......
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