Commit 0eab21f6 authored by Sylvain Soliman's avatar Sylvain Soliman

use option/3 for check_ctl options

parent ded6969b
......@@ -4,7 +4,9 @@ option(
error_epsilon_relative: 1e-6,
initial_step_size: 1e-6,
maximum_step_size: 1e-2,
precision: 5
precision: 5,
nusmv_initial_states: all,
nusmv_counter_example: no
).
function MA(k) = k * product(S * O in [reactants], O ^ S).
......
......@@ -3,13 +3,13 @@
[
% grammar
ctl/1,
ctl_option/1,
op(800, xfy, '/\\'),
op(900, xfy, '\\/'),
% options
nusmv_initial_states/1,
nusmv_counter_example/1,
% commands
export_nusmv/1,
check_ctl/2,
check_ctl/1
]
).
......@@ -418,38 +418,39 @@ ctl_unary_op(Op) :-
memberchk(Op, ['AF', 'EF', 'AG', 'EG', 'AX', 'EX']).
check_ctl(Query, Options) :-
% TODO see if biocham option/3 could be better
biocham_command(*),
:- grammar(nusmv_counter_example).
nusmv_counter_example(yes).
% Default. Set in library/initial.bc
nusmv_counter_example(no).
:- grammar(nusmv_initial_states).
nusmv_initial_states(some).
% Default. Set in library/initial.bc
nusmv_initial_states(all).
check_ctl(Query) :-
biocham_command,
doc('
evaluates the \\argument{Query} on the current model by calling the
NuSMV model-checker.
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.
the \\texttt{nusmv_initial_states} option.
'),
type(Query, ctl),
type(Options, *(ctl_option)),
check_ctl(Query, Options, Result),
option(nusmv_initial_states, nusmv_initial_states, NusmvInitialState,
'Consider that a query is true if verified for all/some initial states.'),
option(nusmv_counter_example, nusmv_counter_example, NusmvCX,
'Compute a counter-example for a query when possible.'),
check_ctl_impl(Query, NusmvInitialState, NusmvCX, Result),
format('~w is ~w\n', [Query, Result]).
:- doc('The \\texttt{cx} option activates counter-example computation, while
the \\texttt{Ei} option evaluates if the query is true for some (instead of
all) initial states.').
:- grammar(ctl_option).
ctl_option('cx').
ctl_option('Ei').
check_ctl(Query) :-
biocham_command,
doc('calls check_ctl with no options.'),
type(Query, ctl),
check_ctl(Query, []).
:- doc('\\begin{example}\n').
:- biocham_silent(clear_model).
......@@ -457,14 +458,13 @@ check_ctl(Query) :-
:- biocham(absent(b)).
:- 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))), nusmv_counter_example:yes)).
:- biocham(check_ctl('EG'(not(b)), nusmv_counter_example:yes)).
:- doc('\\end{example}').
check_ctl(Query, Options, Result) :-
select('Ei', Options, OtherOptions),
!,
check_ctl(not(Query), OtherOptions, NotResult),
check_ctl_impl(Query, some, NusmvCX, Result) :-
check_ctl_impl(not(Query), all, NusmvCX, NotResult),
(
NotResult == 'true'
->
......@@ -478,14 +478,14 @@ check_ctl(Query, Options, Result) :-
).
check_ctl(Query, Options, Result) :-
check_ctl_impl(Query, all, NusmvCX, Result) :-
translate_ctl_for_nusmv(Query, NusmvQuery),
% FIXME better template, in $TMP, check if not existing, etc.
export_nusmv(nusmv),
open('nusmv.cmd', write, Stream),
write(Stream, 'set input_file nusmv.smv\ngo\n'),
(
memberchk('cx', Options)
NusmvCX == 'yes'
->
write(Stream, 'set default_trace_plugin 2\nset counter_examples 1\n')
;
......@@ -498,9 +498,9 @@ check_ctl(Query, Options, Result) :-
['-df', '-source', 'nusmv.cmd'],
[stdin(null), stdout(pipe(NusmvOut))]
),
parse_nusmv_out(NusmvOut, Options, Result),
parse_nusmv_out(NusmvOut, NusmvCX, Result),
(
memberchk('cx', Options),
NusmvCX == 'yes',
trace(_)
->
write('Trace:\n'),
......@@ -560,7 +560,7 @@ translate_ctl_for_nusmv(Object, Atom) :-
make_nusmv_name(Object, Atom).
parse_nusmv_out(Out, Options, Result) :-
parse_nusmv_out(Out, NusmvCX, Result) :-
read_line_to_codes(Out, Codes),
(
Codes = end_of_file
......@@ -583,7 +583,7 @@ parse_nusmv_out(Out, Options, Result) :-
Result = 'error'
),
(
memberchk('cx', Options)
NusmvCX == 'yes'
->
parse_nusmv_out_trace(Out)
;
......@@ -591,7 +591,7 @@ parse_nusmv_out(Out, Options, Result) :-
),
close(Out)
;
parse_nusmv_out(Out, Options, Result)
parse_nusmv_out(Out, NusmvCX, Result)
).
% stores the counter-example trace from NuSMV
......@@ -601,6 +601,7 @@ parse_nusmv_out(Out, Options, Result) :-
parse_nusmv_out_trace(Out) :-
% -- as demonstrated by the following execution sequence
read_line_to_codes(Out, [0'-, 0'-, 0' | _]),
!,
read_line_to_codes(Out, [0'N, 0'a, 0'm, 0'e, 0'\t | _]),
retractall(trace(_)),
read_string(Out, "\n", "\r", _End, InitialString),
......@@ -620,6 +621,9 @@ parse_nusmv_out_trace(Out) :-
fail
).
parse_nusmv_out_trace(Out) :-
read_line_to_codes(Out, end_of_file).
state_string_to_trace(String, Trace) :-
split_string(String, "\t", "\t", [_ | Trace]).
......@@ -16,7 +16,7 @@ test(
true(Result == 'false')
]
) :-
nusmv:check_ctl('AG'(not(c) \/ b), [], Result).
nusmv:check_ctl_impl('AG'(not(c) \/ b), all, no, Result).
test('export_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :-
......@@ -30,7 +30,7 @@ test(
true(Result == 'false')
]
) :-
nusmv:check_ctl('AG'(not(c) \/ b), [], Result).
nusmv:check_ctl_impl('AG'(not(c) \/ b), all, no, Result).
test(
......@@ -42,10 +42,10 @@ test(
cleanup(clear_model)
]
) :-
assertion(nusmv:check_ctl('EG'('R') /\ 'P', [], true)),
assertion(nusmv:check_ctl('EF'('AG'('R' /\ not('P'))), [], true)),
assertion(nusmv:check_ctl('EF'('AG'(not('R') /\ not('P'))), [], true)),
assertion(nusmv:check_ctl('EF'('AG'(not('R') /\ 'P')), [], false)).
assertion(nusmv:check_ctl_impl('EG'('R') /\ 'P', all, no, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'('R' /\ not('P'))), all, no, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ not('P'))), all, no, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ 'P')), all, no, false)).
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