Commit f56ffc1a authored by Sylvain Soliman's avatar Sylvain Soliman

Add options to NuSMV's checks, for Ei and +-dcx, display trace if asked for

parent c61f5134
......@@ -3,11 +3,13 @@
[
% grammar
ctl/1,
ctl_option/1,
op(800, xfy, '/\\'),
op(900, xfy, '\\/'),
% commands
export_nusmv/1,
check_ctl/2,
check_ctl/1
]
).
......@@ -415,14 +417,16 @@ ctl_unary_op(Op) :-
memberchk(Op, ['AF', 'EF', 'AG', 'EG', 'AX', 'EX']).
check_ctl(Query) :-
biocham_command,
check_ctl(Query, Options) :-
% TODO see if biocham option/3 could be better
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).
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
......@@ -430,9 +434,27 @@ check_ctl(Query) :-
translation.
'),
type(Query, ctl),
check_ctl(Query, Result),
type(Options, *(ctl_option)),
check_ctl(Query, Options, 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).
:- biocham(present(a)).
......@@ -443,8 +465,22 @@ check_ctl(Query) :-
:- biocham(check_ctl('EX'(not(a) \/ 'EG'(not(b) /\ '_valid')))).
:- doc('\\end{example}').
check_ctl(Query, Result) :-
check_ctl(Query, [], Result).
check_ctl(Query, Options, Result) :-
select('Ei', Options, OtherOptions),
!,
check_ctl(not(Query), OtherOptions, NotResult),
(
NotResult == 'true'
->
Result = 'false'
;
NotResult == 'false'
->
Result = 'true'
;
Result = 'error'
).
check_ctl(Query, Options, Result) :-
......@@ -452,9 +488,7 @@ check_ctl(Query, Options, Result) :-
% FIXME better template, in $TMP, check if not existing, etc.
export_nusmv(nusmv),
open('nusmv.cmd', write, Stream),
write(Stream, '\c
set input_file nusmv.smv\n\c
go\n'),
write(Stream, 'set input_file nusmv.smv\ngo\n'),
(
memberchk('cx', Options)
->
......@@ -462,16 +496,33 @@ check_ctl(Query, Options, Result) :-
;
write(Stream, 'set counter_examples 0\n')
),
format(Stream, '\c
check_ctlspec -p "~a"\n\c
quit\n', [NusmvQuery]),
format(Stream, 'check_ctlspec -p "~a"\nquit\n', [NusmvQuery]),
close(Stream),
process_create(
path('NuSMV'),
['-df', '-source', 'nusmv.cmd'],
[stdout(pipe(NusmvOut))]
),
parse_nusmv_out(NusmvOut, Options, Result).
parse_nusmv_out(NusmvOut, Options, Result),
(
memberchk('cx', Options),
trace(_)
->
write('Trace:\n'),
enumerate_molecules(Molecules),
findall(T, trace(T), Trace),
forall(
member(Line, [['R' | Molecules] | Trace]),
(
atomic_list_concat(Line, '\t', Atom),
write(Atom),
nl
)
),
nl
;
true
).
translate_ctl_for_nusmv(A \/ B, Atom) :-
......
......@@ -16,7 +16,7 @@ test(
true(Result == 'false')
]
) :-
nusmv:check_ctl('AG'(not(c) \/ b), Result).
nusmv:check_ctl('AG'(not(c) \/ b), [], 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('AG'(not(c) \/ b), [], Result).
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