Commit 7e171c2b authored by Sylvain Soliman's avatar Sylvain Soliman
Browse files

David's faithful NuSMV implementation of BIOCHAM's boolean transition systems (no loop yet)

parent fedab03a
......@@ -90,233 +90,200 @@ export_nusmv_stream(Stream) :-
export_nusmv_stream_reactions(Stream) :-
write(Stream, 'MODULE main\n\n'),
findall(
(Reactants, Products),
(Reactants, [], Products, []),
(
item([kind: reaction, item: Item]),
reaction(Item, _, Reactants, Products)
),
Reactions
),
length(Reactions, ReactionCount),
enumerate_molecules(Molecules),
export_initial_state_reactions(Stream, Molecules, ReactionCount),
export_reactions(Stream, Molecules, Reactions),
export_valid_reactions(Stream, Reactions).
enumerate_all_molecules(Molecules),
export_initial_state(Stream, Molecules),
export_transitions(Stream, Molecules, Reactions).
export_initial_state_reactions(Stream, Molecules, ReactionCount) :-
enumerate_all_molecules(Molecules) :-
(
ReactionCount < 2
enumerate_molecules(ReactionMolecules)
->
NextStates = '1'
true
;
format(atom(NextStates), '1..~d', [ReactionCount])
ReactionMolecules = []
),
write(Stream, 'VAR\n'),
format(Stream, 'R: ~a;\n', [NextStates]),
\+ (
member(Molecule, Molecules),
\+ (
make_nusmv_name(Molecule, Name),
format(Stream, '~a: boolean;\n', [Name])
)
(
enumerate_molecules_influences(InfluenceMolecules)
->
true
;
InfluenceMolecules = []
),
write(Stream, '__valid: boolean;\n'),
format(Stream, '\n\c
ASSIGN
init(R) := ~a;
next(R) := ~a;\n
', [NextStates, NextStates]).
union(ReactionMolecules, InfluenceMolecules, Molecules).
export_reactions(Stream, Molecules, Reactions) :-
\+ (
export_initial_state(Stream, Molecules) :-
forall(
member(Molecule, Molecules),
\+ (
export_molecule_reactions(Stream, Molecule, Reactions)
)
).
export_molecule_reactions(Stream, Molecule, Reactions) :-
make_nusmv_name(Molecule, Name),
get_initial_state(Molecule, InitialState),
nusmv_initial_state(InitialState, NusmvInitialState),
format(Stream, '\c
init(~a) := ~a;
next(~a) := case
', [Name, NusmvInitialState, Name]),
\+ (
nth1(ReactionIndex, Reactions, (Reactants, Products)),
\+ (
(
(
member((_ * Molecule), Products)
->
Result = 'TRUE'
;
member((_ * Molecule), Reactants)
->
Result = '{FALSE, TRUE}'
)
->
format(Stream, ' R = ~d: case\n', [ReactionIndex]),
reactants_to_condition(Reactants, Condition),
format(Stream, ' \c
(~a): ~a;
TRUE: ~a;
esac;
', [Condition, Result, Name])
(
make_nusmv_name(Molecule, Name),
format(Stream, 'VAR ~a: boolean;\n', [Name]),
get_initial_state(Molecule, InitialState),
nusmv_initial_state(InitialState, NusmvInitialState),
format(Stream, 'INIT ~a in ~a;~n', [Name, NusmvInitialState])
)
;
true
)
),
format(Stream, ' \c
TRUE: ~a;
esac;\n
', [Name]).
nl(Stream).
export_valid_reactions(Stream, Reactions) :-
write(Stream, 'init(__valid) := TRUE;\n'),
write(Stream, 'next(__valid) := case\n'),
export_nusmv_stream_influences(Stream) :-
write(Stream, 'MODULE main\n\n'),
findall(
ParenthesizedCondition,
(PositiveInputs, NegativeInputs, [Output], []),
(
member((Reactants, _Products), Reactions),
reactants_to_condition(Reactants, Condition),
atomic_list_concat(['(', Condition, ')'], ParenthesizedCondition)
item([kind: influence, item: Item]),
influence(Item, _Force, PositiveInputs, NegativeInputs, '+', Output)
),
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])
)
PInfluences
),
write(Stream, ' TRUE: TRUE;\n esac;\n').
reactants_to_condition(Reactants, Condition) :-
findall(
ReactantName,
(PositiveInputs, NegativeInputs, [], [Output]),
(
member(_ * ReactantName, Reactants)
item([kind: influence, item: Item]),
influence(Item, __Force, PositiveInputs, NegativeInputs, '-', Output)
),
ReactantNames
NInfluences
),
objects_to_condition(ReactantNames, Condition).
append(PInfluences, NInfluences, Influences),
enumerate_all_molecules(Molecules),
export_initial_state(Stream, Molecules),
export_transitions(Stream, Molecules, Influences).
:- dynamic(allmolecules/1).
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(
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_transitions(Stream, Molecules, Reactions) :-
retractall(allmolecules(_)),
assertz(allmolecules(Molecules)),
write(Stream, 'TRANS '),
maplist(reaction_to_trans, Reactions, Trans),
atomic_list_concat(Trans, ' | ', TransOred),
write(Stream, TransOred),
nl(Stream).
export_initial_state_influences(Stream, Molecules, InfluenceCount) :-
write(Stream, 'VAR\n'),
reaction_to_trans((PositiveInputs, NegativeInputs, Products, Degraded), Trans) :-
(
InfluenceCount < 2
PositiveInputs == []
->
NextStates = '1'
PositiveNames = [],
NusmvPositive = 'TRUE'
;
format(atom(NextStates), '1..~d', [InfluenceCount])
maplist(reactant_to_name, PositiveInputs, PositiveNames),
apply_and_join(
[make_nusmv_name],
PositiveNames,
' & ',
NusmvPositive
)
),
format(Stream, 'I: ~a;\n', [NextStates]),
\+ (
member(Molecule, Molecules),
\+ (
make_nusmv_name(Molecule, Name),
format(Stream, '~a: boolean;\n', [Name])
(
NegativeInputs == []
->
NegativeNames = [],
NusmvNegative = 'TRUE'
;
maplist(reactant_to_name, NegativeInputs, NegativeNames),
apply_and_join(
[make_nusmv_name, prepend_not],
NegativeNames,
' & ',
NusmvNegative
)
),
format(Stream, '\c
ASSIGN
init(I) := ~a;
next(I) := ~a;
', [NextStates, NextStates]).
export_influences(Stream, Molecules, Influences) :-
\+ (
member(Molecule, Molecules),
\+ (
export_molecule_influences(Stream, Molecule, Influences)
(
Products == []
->
ProductNames = [],
NusmvProducts = 'TRUE'
;
maplist(reactant_to_name, Products, ProductNames),
apply_and_join(
[make_nusmv_name, surround_next],
ProductNames,
' & ',
NusmvProducts
)
),
(
Degraded == []
->
DegradedNames = [],
NusmvDegraded = 'TRUE'
;
maplist(reactant_to_name, Degraded, DegradedNames),
apply_and_join(
[make_nusmv_name, surround_next, prepend_not],
DegradedNames,
' & ',
NusmvDegraded
)
),
allmolecules(Molecules),
subtract(Molecules, PositiveNames, NoPositive),
subtract(NoPositive, NegativeNames, NoNegative),
subtract(NoNegative, ProductNames, NoProducts),
subtract(NoProducts, DegradedNames, OtherMolecules),
(
OtherMolecules == []
->
NusmvOthers = 'TRUE'
;
apply_and_join(
[make_nusmv_name, equiv_next],
OtherMolecules,
' & ',
NusmvOthers
)
),
atomic_list_concat(
[NusmvPositive, NusmvNegative, NusmvProducts, NusmvDegraded, NusmvOthers],
' & ',
Trans
).
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) := ~a;
next(~a) := case
', [Name, NusmvInitialState, Name]),
\+ (
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]).
apply_and_join([], List, Join, Result) :-
atomic_list_concat(List, Join, Result).
apply_and_join([Function | Functions], List, Join, Result) :-
maplist(Function, List, NewList),
apply_and_join(Functions, NewList, Join, Result).
atomic_negation_concat(NegativeInput, NegativeInputp) :-
atomic_concat('!', NegativeInput, NegativeInputp).
surround_next(Atom, Next) :-
format(atom(Next), 'next(~a)', [Atom]).
inputs_to_condition(PositiveInputs, NegativeInputs, Condition) :-
maplist(atomic_negation_concat, NegativeInputs, NegativeInputsp),
append(PositiveInputs, NegativeInputsp, Inputs),
objects_to_condition(Inputs, Condition).
prepend_not(Atom, Not) :-
format(atom(Not), '!~a', [Atom]).
equiv_next(Atom, Equiv) :-
format(atom(Equiv), '(~a <-> next(~a))', [Atom, Atom]).
reactants_to_condition(Reactants, Condition) :-
apply_and_join([reactant_to_name, make_nusmv_name], Reactants, ' & ', Condition).
reactant_to_name(_ * Name, Name) :-
!.
reactant_to_name(Name, Name).
objects_to_condition(Objects, Condition) :-
apply_and_join(make_nusmv_name, Objects, ' & ', Condition).
nusmv_initial_state(present(_), 'TRUE').
......@@ -417,11 +384,6 @@ check_ctl(Query, Options) :-
As is usual in Model-Checking, the query is evaluated for all possible
initial states (\\texttt{Ai} in Biocham v3). This can be changed via
the \\texttt{Ei} option.
Note that a specific state variable \\texttt{_valid} can be used to check
that a state does not come from the application of a spurious
self-transition issued from our imperfect asynchronous to synchronous
translation.
'),
type(Query, ctl),
type(Options, *(ctl_option)),
......@@ -452,7 +414,6 @@ check_ctl(Query) :-
:- biocham(a => b).
:- biocham(a + b => a).
:- biocham(check_ctl('EX'(not(a) \/ 'EG'(not(b))))).
:- biocham(check_ctl('EX'(not(a) \/ 'EG'(not(b) /\ '_valid')))).
:- doc('\\end{example}').
......@@ -499,7 +460,7 @@ check_ctl(Query, Options, Result) :-
trace(_)
->
write('Trace:\n'),
enumerate_molecules(Molecules),
enumerate_all_molecules(Molecules),
findall(T, trace(T), Trace),
forall(
member(Line, [['R' | Molecules] | Trace]),
......@@ -590,7 +551,7 @@ parse_nusmv_out(Out, Options, Result) :-
).
% stores the counter-example trace from NuSMV
% argument is a list, with R, then molecules in enumerate_molecules order
% argument is a list, with R, then molecules in enumerate_all_molecules order
:- dynamic(trace/1).
parse_nusmv_out_trace(Out) :-
......
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