Commit 341327d1 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

Proper command and tests, with parsing of NuSMV result

parent 7a846124
......@@ -414,8 +414,6 @@ ctl_unary_op(Op) :-
check_ctl(Query) :-
biocham_command,
type(Query, ctl),
translate_ctl_for_nusmv(Query, Nusmv),
doc('
evaluates the \\argument{Query} on the current model by calling the
NuSMV model-checker.
......@@ -428,6 +426,13 @@ check_ctl(Query) :-
self-transition issued from our imperfect asynchronous to synchronous
translation.
'),
type(Query, ctl),
check_ctl(Query, Result),
format('~w is ~w\n', [Query, Result]).
check_ctl(Query, Result) :-
translate_ctl_for_nusmv(Query, Nusmv),
% FIXME better template, in $TMP, check if not existing, etc.
export_nusmv(nusmv),
open('nusmv.cmd', write, Stream),
......@@ -442,7 +447,7 @@ check_ctl(Query) :-
['-dcx', '-df', '-source', 'nusmv.cmd'],
[stdout(pipe(NusmvOut))]
),
parse_nusmv_out(NusmvOut).
parse_nusmv_out(NusmvOut, Result).
translate_ctl_for_nusmv(A \/ B, Atom) :-
......@@ -485,17 +490,31 @@ translate_ctl_for_nusmv(Object, Atom) :-
make_nusmv_name(Object, Atom).
parse_nusmv_out(Out) :-
parse_nusmv_out(Out, Result) :-
read_line_to_codes(Out, Codes),
(
Codes = end_of_file
->
close(Out)
close(Out),
Result = 'error'
;
% "-- "
Codes = [45, 45, 32 | _]
->
format('~s\n', [Codes]),
parse_nusmv_out(Out)
close(Out),
(
% "is true"
append(_, [105, 115, 32, 116, 114, 117, 101], Codes)
->
Result = 'true'
;
% "is false"
append(_, [105, 115, 32, 102, 97, 108, 115, 101], Codes)
->
Result = 'false'
;
Result = 'error'
)
;
parse_nusmv_out(Out)
parse_nusmv_out(Out, Result)
).
:- use_module(library(plunit)).
% not necessary, except for separate compilation
:- use_module(reaction_rules).
:- use_module(influence_rules).
:- begin_tests(nusmv).
test('export_reac', [setup(set_a_dummy_reaction_model), cleanup(clear_model)]) :-
export_nusmv('unittest').
test('check_ctl_reac', [setup(set_a_dummy_reaction_model), cleanup(clear_model)]) :-
check_ctl('AG'(not(c) \/ b)).
test(
'check_ctl_reac',
[
setup(set_a_dummy_reaction_model),
cleanup(clear_model),
true(Result == 'false')
]
) :-
nusmv:check_ctl('AG'(not(c) \/ b), Result).
test('export_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :-
export_nusmv('unittest').
test('check_ctl_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :-
check_ctl('AG'(not(c) \/ b)).
test(
'check_ctl_infl',
[
setup(set_a_dummy_influence_model),
cleanup(clear_model),
true(Result == 'false')
]
) :-
nusmv:check_ctl('AG'(not(c) \/ b), Result).
set_a_dummy_reaction_model :-
clear_model,
......@@ -21,6 +40,7 @@ set_a_dummy_reaction_model :-
command(present(a)),
command(absent(c)).
set_a_dummy_influence_model :-
clear_model,
add_influence(a -> b),
......
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