Commit e40f945a authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain


parent 56270914
......@@ -418,8 +418,16 @@ check_ctl(Query) :-
translate_ctl_for_nusmv(Query, Nusmv),
evaluates the \\argument{Query} on the current model by calling the
NuSMV model-checker.'
NuSMV model-checker.
As is usual in Model-Checking, the query is evaluated for all possible
initial states (\texttt{Ai} in Biocham v3).
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
self-transition issued from our imperfect asynchronous to synchronous
% FIXME better template, in $TMP, check if not existing, etc.
open('nusmv.cmd', write, Stream),
......@@ -454,13 +462,13 @@ 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('EU'(A, B), 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('AU'(A, B), Atom) :-
translate_ctl_for_nusmv(A, AA),
translate_ctl_for_nusmv(B, BB),
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment