Commit 61d729b2 authored by Sylvain Soliman's avatar Sylvain Soliman
Browse files

positive/negative boolean semantics

parent f35655a1
...@@ -6,7 +6,8 @@ option( ...@@ -6,7 +6,8 @@ option(
maximum_step_size: 1e-2, maximum_step_size: 1e-2,
precision: 5, precision: 5,
nusmv_initial_states: all, nusmv_initial_states: all,
nusmv_counter_example: no nusmv_counter_example: no,
boolean_semantics: negative
). ).
function MA(k) = k * product(S * O in [reactants], O ^ S). function MA(k) = k * product(S * O in [reactants], O ^ S).
......
...@@ -8,6 +8,7 @@ ...@@ -8,6 +8,7 @@
% options % options
nusmv_initial_states/1, nusmv_initial_states/1,
nusmv_counter_example/1, nusmv_counter_example/1,
boolean_semantics/1,
% commands % commands
export_nusmv/1, export_nusmv/1,
check_ctl/1 check_ctl/1
...@@ -67,15 +68,21 @@ export_nusmv(OutputFile) :- ...@@ -67,15 +68,21 @@ export_nusmv(OutputFile) :-
exports the current Biocham set of reactions and initial state in an SMV exports the current Biocham set of reactions and initial state in an SMV
\\texttt{.smv} file. \\texttt{.smv} file.
'), '),
option(boolean_semantics, boolean_semantics, BoolSem,
'Use positive or negative boolean semantics for inhibitors.'),
export_nusmv_file(OutputFile, BoolSem).
export_nusmv_file(OutputFile, BoolSem) :-
automatic_suffix(OutputFile, '.smv', write, FilenameSmv), automatic_suffix(OutputFile, '.smv', write, FilenameSmv),
setup_call_cleanup( setup_call_cleanup(
open(FilenameSmv, write, Stream), open(FilenameSmv, write, Stream),
export_nusmv_stream(Stream), export_nusmv_stream(Stream, BoolSem),
close(Stream) close(Stream)
). ).
export_nusmv_stream(Stream) :- export_nusmv_stream(Stream, BoolSem) :-
( (
is_reaction_model is_reaction_model
-> ->
...@@ -83,7 +90,7 @@ export_nusmv_stream(Stream) :- ...@@ -83,7 +90,7 @@ export_nusmv_stream(Stream) :-
; ;
is_influence_model is_influence_model
-> ->
export_nusmv_stream_influences(Stream) export_nusmv_stream_influences(Stream, BoolSem)
). ).
...@@ -134,14 +141,20 @@ export_initial_state(Stream, Molecules) :- ...@@ -134,14 +141,20 @@ export_initial_state(Stream, Molecules) :-
nl(Stream). nl(Stream).
export_nusmv_stream_influences(Stream) :- export_nusmv_stream_influences(Stream, BoolSem) :-
write(Stream, 'MODULE main\n\n'), write(Stream, 'MODULE main\n\n'),
findall( findall(
(PositiveInputs, NegativeInputs, [Output | PositiveInputs], NegativeInputs), (PositiveInputs, NegativeInputs, [Output | PositiveInputs], NegativeInputs),
( (
item([kind: influence, item: Item]), item([kind: influence, item: Item]),
influence(Item, _Force, PositiveInputs, NegInputs, '+', Output), influence(Item, _Force, PositiveInputs, NegInputs, '+', Output),
subtract(NegInputs, [Output], NegativeInputs) (
BoolSem == positive
->
NegativeInputs = []
;
subtract(NegInputs, [Output], NegativeInputs)
)
), ),
PInfluences PInfluences
), ),
...@@ -149,7 +162,14 @@ export_nusmv_stream_influences(Stream) :- ...@@ -149,7 +162,14 @@ export_nusmv_stream_influences(Stream) :-
(PositiveInputs, NegativeInputs, PositiveInputs, [Output | NegativeInputs]), (PositiveInputs, NegativeInputs, PositiveInputs, [Output | NegativeInputs]),
( (
item([kind: influence, item: Item]), item([kind: influence, item: Item]),
influence(Item, __Force, PosInputs, NegativeInputs, '-', Output), influence(Item, __Force, PosInputs, NegInputs, '-', Output),
(
BoolSem == positive
->
NegativeInputs = []
;
NegativeInputs = NegInputs
),
subtract(PosInputs, [Output], PositiveInputs) subtract(PosInputs, [Output], PositiveInputs)
), ),
NInfluences NInfluences
...@@ -420,6 +440,13 @@ ctl_unary_op(Op) :- ...@@ -420,6 +440,13 @@ ctl_unary_op(Op) :-
memberchk(Op, ['AF', 'EF', 'AG', 'EG', 'AX', 'EX']). memberchk(Op, ['AF', 'EF', 'AG', 'EG', 'AX', 'EX']).
:- grammar(boolean_semantics).
boolean_semantics(positive).
% Default. Set in library/initial.bc
boolean_semantics(negative).
:- grammar(nusmv_counter_example). :- grammar(nusmv_counter_example).
nusmv_counter_example(yes). nusmv_counter_example(yes).
...@@ -450,7 +477,9 @@ check_ctl(Query) :- ...@@ -450,7 +477,9 @@ check_ctl(Query) :-
'Consider that a query is true if verified for all/some initial states.'), 'Consider that a query is true if verified for all/some initial states.'),
option(nusmv_counter_example, nusmv_counter_example, NusmvCX, option(nusmv_counter_example, nusmv_counter_example, NusmvCX,
'Compute a counter-example for a query when possible.'), 'Compute a counter-example for a query when possible.'),
check_ctl_impl(Query, NusmvInitialState, NusmvCX, Result), option(boolean_semantics, boolean_semantics, BoolSem,
'Use positive or negative boolean semantics for inhibitors.'),
check_ctl_impl(Query, NusmvInitialState, NusmvCX, BoolSem, Result),
format('~w is ~w\n', [Query, Result]). format('~w is ~w\n', [Query, Result]).
...@@ -465,8 +494,8 @@ check_ctl(Query) :- ...@@ -465,8 +494,8 @@ check_ctl(Query) :-
:- doc('\\end{example}'). :- doc('\\end{example}').
check_ctl_impl(Query, some, NusmvCX, Result) :- check_ctl_impl(Query, some, NusmvCX, BoolSem, Result) :-
check_ctl_impl(not(Query), all, NusmvCX, NotResult), check_ctl_impl(not(Query), all, NusmvCX, BoolSem, NotResult),
( (
NotResult == 'true' NotResult == 'true'
-> ->
...@@ -480,10 +509,10 @@ check_ctl_impl(Query, some, NusmvCX, Result) :- ...@@ -480,10 +509,10 @@ check_ctl_impl(Query, some, NusmvCX, Result) :-
). ).
check_ctl_impl(Query, all, NusmvCX, Result) :- check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
translate_ctl_for_nusmv(Query, NusmvQuery), translate_ctl_for_nusmv(Query, NusmvQuery),
% FIXME better template, in $TMP, check if not existing, etc. % FIXME better template, in $TMP, check if not existing, etc.
export_nusmv(nusmv), export_nusmv_file(nusmv, BoolSem),
open('nusmv.cmd', write, Stream), open('nusmv.cmd', write, Stream),
write(Stream, 'set input_file nusmv.smv\ngo\n'), write(Stream, 'set input_file nusmv.smv\ngo\n'),
( (
......
...@@ -16,7 +16,7 @@ test( ...@@ -16,7 +16,7 @@ test(
true(Result == 'false') true(Result == 'false')
] ]
) :- ) :-
nusmv:check_ctl_impl('AG'(not(c) \/ b), all, no, Result). nusmv:check_ctl_impl('AG'(not(c) \/ b), all, no, negative, Result).
test('export_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :- test('export_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :-
...@@ -30,7 +30,7 @@ test( ...@@ -30,7 +30,7 @@ test(
true(Result == 'false') true(Result == 'false')
] ]
) :- ) :-
nusmv:check_ctl_impl('AG'(not(c) \/ b), all, no, Result). nusmv:check_ctl_impl('AG'(not(c) \/ b), all, no, negative, Result).
test( test(
...@@ -42,10 +42,13 @@ test( ...@@ -42,10 +42,13 @@ test(
cleanup(clear_model) cleanup(clear_model)
] ]
) :- ) :-
assertion(nusmv:check_ctl_impl('EG'('R') /\ 'P', all, no, true)), assertion(nusmv:check_ctl_impl('EG'('R') /\ 'P', all, no, negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'('R' /\ not('P'))), all, no, true)), assertion(nusmv:check_ctl_impl('EF'('AG'('R' /\ not('P'))), all, no,
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ not('P'))), all, no, true)), negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ 'P')), all, no, false)). assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ not('P'))), all, no,
negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ 'P')), all, no,
negative, false)).
set_a_dummy_reaction_model :- set_a_dummy_reaction_model :-
......
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