Commit 087e6e92 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

added some shortcuts

parent cd620813
......@@ -16,7 +16,6 @@
% Only for separate compilation/linting
:- use_module(reaction_rules).
:- use_module(ctl).
export_nusmv(OutputFile) :-
......@@ -451,6 +450,7 @@ check_ctl(Query) :-
:- biocham(a + b => a).
:- biocham(check_ctl('EX'(not(a) \/ 'EG'(not(b))), nusmv_counter_example:yes)).
:- biocham(check_ctl('EG'(not(b)), nusmv_counter_example:yes)).
:- biocham(check_ctl(reachable(b), nusmv_counter_example:yes)).
:- doc('\\end{example}').
......@@ -525,6 +525,18 @@ translate_ctl_for_nusmv(A -> B, Atom) :-
translate_ctl_for_nusmv(B, BB),
atomic_list_concat(['(!', AA, ' | ', BB, ')'], Atom).
translate_ctl_for_nusmv(reachable(A), Atom) :-
!,
translate_ctl_for_nusmv('EF'(A), Atom).
translate_ctl_for_nusmv(oscil(A), Atom) :-
!,
translate_ctl_for_nusmv('AG'('EF'(A) /\ 'EF'(not(A))), Atom).
translate_ctl_for_nusmv(checkpoint(A, B), Atom) :-
!,
translate_ctl_for_nusmv('EU'(not(A), B), Atom).
translate_ctl_for_nusmv(A \/ B, Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
......
:- use_module(library(plunit)).
% not necessary, except for separate compilation
:- use_module(reaction_rules).
:- use_module(ctl).
:- begin_tests(revision).
% condition(flag(slow_test, true, true)),
......
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