Commit 97906db1 authored by David Rosenblueth's avatar David Rosenblueth

NuSMV for influence models

parent 9b0d5a25
......@@ -33,7 +33,8 @@ biocham: platform/current swipl-biocham $(MODULES) toc.org Makefile
biocham_debug: platform/current swipl-biocham $(MODULES) $(TEST_MODULES) \
toc.org Makefile
$(SWIPL) -o biocham_debug \
--goal='(leash(-all),initialize)' -c $(MODULES) $(TEST_MODULES)
--goal='(leash(-all),leash(+call),initialize)' -c $(MODULES) $(TEST_MODULES)
swipl-biocham: swipl-biocham.o \
modules/graphviz/graphviz_swiprolog.o \
......
:- module(
influence_editor,
[
s/0,
% Commands
add_influence/1,
list_influences/0,
......@@ -8,10 +9,21 @@
is_influence_model/0,
check_influence_model/0,
list_model_influences/0,
influence/6
influence/6,
enumerate_molecules_influences/1
]
).
s :-
biocham_command,
write('id parent kind item\n'),
models:item(W,X,Y,Z),
write(W), write(' '),
write(X), write(' '),
write(Y), write(' '),
write(Z), write(' '), nl, fail.
s.
:- devdoc('\\section{Commands}').
......@@ -154,3 +166,24 @@ list_enumeration([H], H) :-
list_enumeration([H | List], (H, Enum)) :-
list_enumeration(List, Enum).
%-----------------
enumerate_molecules_influences(Molecules) :-
setof(
Molecule,
enumerate_molecule_influences(Molecule),
Molecules
).
enumerate_molecule_influences(Molecule) :-
item([kind: influence, item: Item]),
influence(Item, _Force, PositiveInputs, NegativeInputs, _Sign, Output),
(
member( Molecule, PositiveInputs)
;
member( Molecule, NegativeInputs)
;
Molecule = Output
).
......@@ -25,6 +25,18 @@ no_false_initial_state :-
export_nusmv_stream(Stream) :-
(
is_reaction_model
->
export_nusmv_stream_reactions(Stream)
;
is_influence_model
->
export_nusmv_stream_influences(Stream)
).
export_nusmv_stream_reactions(Stream) :-
write(Stream, 'MODULE main\n'),
findall(
(Reactants, Products),
......@@ -36,11 +48,12 @@ export_nusmv_stream(Stream) :-
),
length(Reactions, ReactionCount),
enumerate_molecules(Molecules),
export_initial_state(Stream, Molecules, ReactionCount),
export_initial_state_reactions(Stream, Molecules, ReactionCount),
export_reactions(Stream, Molecules, Reactions).
export_initial_state(Stream, Molecules, ReactionCount) :-
export_initial_state_reactions(Stream, Molecules, ReactionCount) :-
write(Stream, 'VAR\n'),
(
no_false_initial_state
......@@ -129,6 +142,130 @@ next(~a) := case
', [Name]).
%-----------------------new----------------------
export_nusmv_stream_influences(Stream) :-
write(Stream, 'MODULE main\n'),
findall(
i(Force,PositiveInputs,NegativeInputs,Sign,Output),
(
item([kind: influence, item: Item]), %
influence(Item, Force, PositiveInputs, NegativeInputs, Sign, Output)
),
Influences
),
length(Influences, InfluenceCount),
enumerate_molecules_influences(Molecules),
export_initial_state_influences(Stream, Molecules, InfluenceCount),
export_influences(Stream, Molecules, Influences).
export_initial_state_influences(Stream, Molecules, InfluenceCount) :-
write(Stream, 'VAR\n'),
(
no_false_initial_state
->
FirstState = 1
;
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
->
NextStates = '1'
;
format(atom(NextStates), '1..~d', [InfluenceCount])
),
format(Stream, '\c
ASSIGN
init(I) := ~d;
next(I) := ~a;
', [FirstState, NextStates]).
export_influences(Stream, Molecules, Influences) :-
\+ (
member(Molecule, Molecules),
\+ (
export_molecule_influences(Stream, Molecule, Influences)
)
).
export_molecule_influences(Stream, Molecule, Influences) :-
make_nusmv_name(Molecule, Name),
get_initial_state(Molecule, InitialState),
nusmv_initial_state(InitialState, NusmvInitialState),
format(Stream, '\c
init(~a) := FALSE;
next(~a) := case
I = 0: ~a;
', [Name, Name, NusmvInitialState]),
\+ (
nth1(InfluenceIndex, Influences, i(_Force,PositiveInputs,NegativeInputs,Sign,Output)),
\+ (
Molecule = Output %
-> %
(
(
Sign = +
->
Result = 'TRUE'
;
Sign = -
->
Result = 'FALSE'
)
->
format(Stream, ' I = ~d: case\n', [InfluenceIndex]),
inputs_to_condition( PositiveInputs, NegativeInputs, Condition ),
format(Stream, ' \c
(~a): ~a;
TRUE: ~a;
esac;
', [Condition, Result, Name])
)
;
true
)
),
format(Stream, ' \c
TRUE: ~a;
esac;
', [Name]).
atomic_negation_concat(NegativeInput, NegativeInputp) :-
atomic_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)
)
).
nusmv_initial_state(present(_), 'TRUE').
nusmv_initial_state(absent, 'FALSE').
......
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