Commit 25b17828 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

NuSMV communication, simple parsing of the output

parent bb4857c1
:- module(
nusmv,
[
% grammar
ctl/1,
op(800, xfy, '/\\'),
op(900, xfy, '\\/'),
% commands
export_nusmv/1,
check_ctl/1
]
).
:- grammar(ctl).
ctl('EX'(E)) :-
ctl(E).
ctl('EF'(E)) :-
ctl(E).
ctl('EG'(E)) :-
ctl(E).
ctl('EU'(E, F)) :-
ctl(E),
ctl(F).
ctl('AX'(E)) :-
ctl(E).
ctl('AF'(E)) :-
ctl(E).
ctl('AG'(E)) :-
ctl(E).
ctl('AU'(E, F)) :-
ctl(E),
ctl(F).
ctl(not(E)) :-
ctl(E).
ctl(E /\ F) :-
ctl(E),
ctl(F).
ctl(E \/ F) :-
ctl(E),
ctl(F).
ctl(E) :-
object(E).
export_nusmv(OutputFile) :-
biocham_command,
type(OutputFile, output_file),
......@@ -351,25 +400,22 @@ reserved('E').
reserved('U').
reserved('AF').
reserved('EF').
reserved('AG').
reserved('EG').
reserved('xor').
reserved('AX').
reserved('R').
reserved('EX').
reserved(Atom) :-
ctl_unary_op(Atom).
reserved('xor').
reserved('R').
ctl_unary_op(Op) :-
memberchk(Op, ['AF', 'EF', 'AG', 'EG', 'AX', 'EX']).
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.'
......@@ -381,6 +427,67 @@ check_ctl(Query) :-
set input_file nusmv.smv\n\c
go\n\c
check_ctlspec -p "~a"\n\c
quit\n', [Query]),
quit\n', [Nusmv]),
close(Stream),
process_create(path('NuSMV'), ['-dcx', '-df', '-source', 'nusmv.cmd'], []).
process_create(
path('NuSMV'),
['-dcx', '-df', '-source', 'nusmv.cmd'],
[stdout(pipe(NusmvOut))]
),
parse_nusmv_out(NusmvOut).
translate_ctl_for_nusmv(A \/ B, Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
translate_ctl_for_nusmv(B, BB),
atomic_list_concat(['(', AA, ' | ', BB, ')'], Atom).
translate_ctl_for_nusmv(A /\ B, Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
translate_ctl_for_nusmv(B, BB),
atomic_list_concat(['(', AA, ' & ', BB, ')'], Atom).
translate_ctl_for_nusmv(not(A), Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
atomic_list_concat(['!', AA], Atom).
translate_ctl_for_nusmv('EU'(A), Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
translate_ctl_for_nusmv(B, BB),
atomic_list_concat(['E [', AA, ' U ', BB, ']'], Atom).
translate_ctl_for_nusmv('AU'(A), Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
translate_ctl_for_nusmv(B, BB),
atomic_list_concat(['A [', AA, ' U ', BB, ']'], Atom).
translate_ctl_for_nusmv(CTL, Atom) :-
CTL =.. [Operator, A],
ctl_unary_op(Operator),
!,
translate_ctl_for_nusmv(A, AA),
atomic_list_concat([Operator, AA], ' ', Atom).
translate_ctl_for_nusmv(Object, Atom) :-
make_nusmv_name(Object, Atom).
parse_nusmv_out(Out) :-
read_line_to_codes(Out, Codes),
(
Codes = end_of_file
->
close(Out)
;
Codes = [45, 45, 32 | _]
->
format('~s\n', [Codes]),
parse_nusmv_out(Out)
;
parse_nusmv_out(Out)
).
......@@ -2,12 +2,17 @@
:- begin_tests(nusmv).
test('nusmv') :-
test('export', [setup(set_a_dummy_model), cleanup(clear_model)]) :-
export_nusmv('unittest').
test('check_ctl', [setup(set_a_dummy_model), cleanup(clear_model)]) :-
check_ctl('AG'(not(c) \/ b)).
set_a_dummy_model :-
clear_model,
add_reaction(a => b),
add_reaction(a + b => c),
command(present(a)),
command(absent(c)),
export_nusmv('unittest').
command(absent(c)).
:- end_tests(nusmv).
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