Commit 14434ad2 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

3_inhib, ok

parent 430df94d
......@@ -14,6 +14,8 @@
]
).
:- use_module(ctl).
% Only for separate compilation/linting
:- use_module(reaction_rules).
......@@ -478,7 +480,8 @@ check_ctl_impl(Query, some, NusmvCX, BoolSem, Result) :-
% the full output/trace
check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
retractall(trace(_)),
translate_ctl_for_nusmv(Query, NusmvQuery),
normalize_query(Query, NQuery),
translate_ctl_for_nusmv(NQuery, NusmvQuery),
% FIXME better template, in $TMP, check if not existing, etc.
export_nusmv_file(nusmv, BoolSem),
open('nusmv.cmd', write, Stream),
......@@ -523,19 +526,7 @@ 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(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).
atomic_list_concat(['(', AA, ' -> ', BB, ')'], Atom).
translate_ctl_for_nusmv(A \/ B, Atom) :-
!,
......
......@@ -5,6 +5,8 @@
]
).
:- use_module(ctl).
% Only for separate compilation/linting
:- use_module(nusmv).
:- use_module(util).
......@@ -17,8 +19,9 @@ revise_model(Query) :-
'Use theory-revision on the current model to satisfy the query given as
argument. cf. \\texttt{CCFS05tcsb}.'
),
categorize_query(Query, ECTL, UCTL, ACTL),
retractall(need_recheck),
normalize_query(Query, NQuery),
categorize_query(NQuery, ECTL, UCTL, ACTL),
nb_setval(need_recheck, false),
revise_model(ECTL, UCTL, ACTL, [], [], []).
......@@ -27,6 +30,7 @@ revise_model(Query) :-
revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
item([kind: option, item: option(nusmv_initial_states: Init)]),
item([kind: option, item: option(boolean_semantics: Bool)]),
write(checking(E)),nl,
(
check_ctl_impl(E, Init, no, Bool, true)
->
......@@ -43,6 +47,7 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
item([kind: option, item: option(nusmv_initial_states: Init)]),
item([kind: option, item: option(boolean_semantics: Bool)]),
write(checking(U)),nl,
(
check_ctl_impl(U, Init, no, Bool, true)
->
......@@ -66,6 +71,7 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
revise_model([], [], [A | ACTL], Et, Ut, At) :-
item([kind: option, item: option(nusmv_initial_states: Init)]),
item([kind: option, item: option(boolean_semantics: Bool)]),
write(checking(A)),nl,
check_ctl_impl(A, Init, silent, Bool, Result),
(
Result = true
......@@ -74,7 +80,10 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
% we only consider adding U' and E' when A is fully satisfied, thus moving
% a step from the A' step of the algorithm to the A step
% FIXME check At too since self-loops can be added by removing a reaction
write(split(Et, Ut)),nl,
check_and_split(Et, Ut, [], Ett, Utt, [], Eprime, Uprime, [], Init, Bool),
write(true(Ett, Utt)),nl,
write(false(Eprime, Uprime)),nl,
revise_model(Eprime, Uprime, ACTL, Ett, Utt, [A | At])
;
print_message(informational, step('A''')),
......@@ -88,6 +97,7 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
% recursion
check_ctl_impl(A, Init, no, Bool, true)
),
nb_setval(need_recheck, true),
revise_model([], [], [A | ACTL], Et, Ut, At)
).
......@@ -106,13 +116,11 @@ recheck_spec(Specs, Init, Bool) :-
check_ctl_impl(Spec, Init, no, Bool, true).
:- dynamic(need_recheck/0).
check_and_split(E, U, A, Et, Ut, At, Ef, Uf, Af, Init, Bool) :-
(
retract(need_recheck)
nb_getval(need_recheck, true)
->
nb_setval(need_recheck, false),
% TODO use a single NuSMV process, with a single model loading step
check_and_split(E, Et, Ef, Init, Bool),
check_and_split(U, Ut, Uf, Init, Bool),
......@@ -142,7 +150,6 @@ check_and_split([F | Formulae], Ft, Ff, Init, Bool) :-
check_and_split(Formulae, FFt, FFf, Init, Bool).
categorize_query(Q1 /\ Q2, ECTL, UCTL, ACTL) :-
!,
categorize_query(Q1, E1, U1, A1),
......
......@@ -101,4 +101,28 @@ test(
findall(Item, item([kind: reaction, item: Item]), Reactions).
test(
'3_inhibitions',
[
setup(clear_model),
true(Reactions = ['_'=>a,'_'=>b,'_'=>c,c=[a]=>'_',a=[b]=>'_',b=[c]=>'_'])
]
) :-
command('_' => a),
command('_' => b),
command('_' => c),
command(a => '_'),
command(b => '_'),
command(c => '_'),
once(
revise_model(
oscil(a) /\ oscil(b) /\ oscil(c) /\
(c -> checkpoint(a, not(c))) /\
(a -> checkpoint(b, not(a))) /\
(b -> checkpoint(c, not(b)))
)
),
findall(Item, item([kind: reaction, item: Item]), Reactions).
:- end_tests(revision).
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