Commit bb4857c1 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

First version calling NuSMV for check_ctl

parent 67bf374f
:- module(
nusmv,
[
export_nusmv/1
export_nusmv/1,
check_ctl/1
]
).
......@@ -273,8 +274,6 @@ inputs_to_condition(PositiveInputs, NegativeInputs, Condition) :-
)
).
nusmv_initial_state(present(_), 'TRUE').
......@@ -367,3 +366,21 @@ reserved('EX').
reserved('xor').
reserved('R').
check_ctl(Query) :-
biocham_command,
doc('
evaluates the \\argument{Query} on the current model by calling the
NuSMV model-checker.'
),
% FIXME better template, in $TMP, check if not existing, etc.
export_nusmv(nusmv),
open('nusmv.cmd', write, Stream),
format(Stream, '\c
set input_file nusmv.smv\n\c
go\n\c
check_ctlspec -p "~a"\n\c
quit\n', [Query]),
close(Stream),
process_create(path('NuSMV'), ['-dcx', '-df', '-source', 'nusmv.cmd'], []).
......@@ -39,7 +39,6 @@
- transfer_function.pl
*** Graphics files
*** Other files
- nusmv.pl
** Listing and editing reactions, influences and events
*** Reactions
- reaction_editor.pl
......@@ -78,9 +77,11 @@
- influence_graphs.pl
- graph_editor.pl
- graphviz.pl
** Numerical temporal properties
** Temporal properties
*** FOLTL(R) constraints, validity domains, sensitivity and robustness
- foltl.pl
*** CTL model-checking and revision
- nusmv.pl
* Index
- index
* Bibliography
......
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