Commit c61f5134 authored by Sylvain Soliman's avatar Sylvain Soliman

NuSMV counter-example parsing

parent e1b6adb5
......@@ -12,6 +12,9 @@
]
).
% Only for separate compilation/linting
:- use_module(reaction_rules).
:- grammar(ctl).
......@@ -441,22 +444,34 @@ check_ctl(Query) :-
:- doc('\\end{example}').
check_ctl(Query, Result) :-
translate_ctl_for_nusmv(Query, Nusmv),
check_ctl(Query, [], Result).
check_ctl(Query, Options, 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),
format(Stream, '\c
write(Stream, '\c
set input_file nusmv.smv\n\c
go\n\c
go\n'),
(
memberchk('cx', Options)
->
write(Stream, 'set default_trace_plugin 2\nset counter_examples 1\n')
;
write(Stream, 'set counter_examples 0\n')
),
format(Stream, '\c
check_ctlspec -p "~a"\n\c
quit\n', [Nusmv]),
quit\n', [NusmvQuery]),
close(Stream),
process_create(
path('NuSMV'),
['-dcx', '-df', '-source', 'nusmv.cmd'],
['-df', '-source', 'nusmv.cmd'],
[stdout(pipe(NusmvOut))]
),
parse_nusmv_out(NusmvOut, Result).
parse_nusmv_out(NusmvOut, Options, Result).
translate_ctl_for_nusmv(A \/ B, Atom) :-
......@@ -499,7 +514,7 @@ translate_ctl_for_nusmv(Object, Atom) :-
make_nusmv_name(Object, Atom).
parse_nusmv_out(Out, Result) :-
parse_nusmv_out(Out, Options, Result) :-
read_line_to_codes(Out, Codes),
(
Codes = end_of_file
......@@ -508,22 +523,57 @@ parse_nusmv_out(Out, Result) :-
Result = 'error'
;
% "-- "
Codes = [45, 45, 32 | _]
Codes = [0'-, 0'-, 0' | _]
->
close(Out),
(
% "is true"
append(_, [105, 115, 32, 116, 114, 117, 101], Codes)
append(_, [0'i, 0's, 0' , 0't, 0'r, 0'u, 0'e], Codes)
->
Result = 'true'
;
% "is false"
append(_, [105, 115, 32, 102, 97, 108, 115, 101], Codes)
append(_, [0'i, 0's, 0' , 0'f, 0'a, 0'l, 0's, 0'e], Codes)
->
Result = 'false'
;
Result = 'error'
)
),
(
memberchk('cx', Options)
->
parse_nusmv_out_trace(Out)
;
true
),
close(Out)
;
parse_nusmv_out(Out, Result)
parse_nusmv_out(Out, Options, Result)
).
% stores the counter-example trace from NuSMV
% argument is a list, with R, then molecules in enumerate_molecules order
:- dynamic(trace/1).
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),
state_string_to_trace(InitialString, InitialTrace),
assertz(trace(InitialTrace)),
repeat,
read_line_to_codes(Out, _Constants),
read_line_to_codes(Out, _Inputs),
read_string(Out, "\n", "\r", End, StateString),
(
End = -1
->
!
;
state_string_to_trace(StateString, StateTrace),
assertz(trace(StateTrace)),
fail
).
state_string_to_trace(String, Trace) :-
split_string(String, "\t", "\t", [_ | Trace]).
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