Commit 73b1bc15 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

messages informational->debug, get added/removed reactions, add Qu to tosts

parent 6d9b65c7
...@@ -19,23 +19,41 @@ revise_model(Query) :- ...@@ -19,23 +19,41 @@ revise_model(Query) :-
'Use theory-revision on the current model to satisfy the query given as 'Use theory-revision on the current model to satisfy the query given as
argument. cf. \\texttt{CCFS05tcsb}.' argument. cf. \\texttt{CCFS05tcsb}.'
), ),
revise_model(Query, Added, Removed),
print_message(informational, added(Added)),
print_message(informational, removed(Removed)).
revise_model(Query, Added, Removed) :-
findall(Item, item([kind: reaction, item: Item]), Reactions),
nb_setval(need_recheck, false),
normalize_query(Query, NQuery, _), normalize_query(Query, NQuery, _),
categorize_query(NQuery, ECTL, UCTL, ACTL), categorize_query(NQuery, ECTL, UCTL, ACTL),
nb_setval(need_recheck, false), revise_model(ECTL, UCTL, ACTL, [], [], []),
revise_model(ECTL, UCTL, ACTL, [], [], []). findall(Item, item([kind: reaction, item: Item]), NewReactions),
subtract(NewReactions, Reactions, Added),
subtract(Reactions, NewReactions, Removed).
% Everything copied as much as possible from CCFS05tcsb % Everything copied as much as possible from CCFS05tcsb
revise_model(ECTL, UCTL, ACTL, Et, Ut, At) :-
debug(
revision,
'calling revise_model(~w, ~w, ~w, ~w, ~w, ~w)',
[ECTL, UCTL, ACTL, Et, Ut, At]
),
fail.
revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :- revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
item([kind: option, item: option(nusmv_initial_states: Init)]), item([kind: option, item: option(nusmv_initial_states: Init)]),
item([kind: option, item: option(boolean_semantics: Bool)]), item([kind: option, item: option(boolean_semantics: Bool)]),
( (
check_ctl_impl(E, Init, no, Bool, true) check_ctl_impl(E, Init, no, Bool, true)
-> ->
print_message(informational, step('E')) debug(revision, 'Entering step w', ['E'])
; ;
print_message(informational, step('E''')), debug(revision, 'Entering step w', ['E''']),
find_and_add_rule, find_and_add_rule,
% FIXME check Et too since self-loops can be broken by adding a reaction % FIXME check Et too since self-loops can be broken by adding a reaction
append([E | Ut], At, AllSpec), append([E | Ut], At, AllSpec),
...@@ -49,15 +67,15 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :- ...@@ -49,15 +67,15 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
( (
check_ctl_impl(U, Init, no, Bool, true) check_ctl_impl(U, Init, no, Bool, true)
-> ->
print_message(informational, step('U')) debug(revision, 'Entering step w', ['U'])
; ;
( (
print_message(informational, step('U''')), debug(revision, 'Entering step w', ['U''']),
find_and_add_rule, find_and_add_rule,
% FIXME check Et too since self-loops can be broken by adding a reaction % FIXME check Et too since self-loops can be broken by adding a reaction
append([U | Ut], At, AllSpec) append([U | Ut], At, AllSpec)
; ;
print_message(informational, step('U''''')), debug(revision, 'Entering step w', ['U''''']),
delete_rules, delete_rules,
% FIXME check At too since self-loops can be added by removing a reaction % FIXME check At too since self-loops can be added by removing a reaction
append([U | Ut], Et, AllSpec) append([U | Ut], Et, AllSpec)
...@@ -73,14 +91,14 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :- ...@@ -73,14 +91,14 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
( (
Result = true Result = true
-> ->
print_message(informational, step('A')), debug(revision, 'Entering step w', ['A']),
% we only consider adding U' and E' when A is fully satisfied, thus moving % 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 % 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 % FIXME check At too since self-loops can be added by removing a reaction
check_and_split(Et, Ut, [], Ett, Utt, [], Eprime, Uprime, [], Init, Bool), check_and_split(Et, Ut, [], Ett, Utt, [], Eprime, Uprime, [], Init, Bool),
revise_model(Eprime, Uprime, ACTL, Ett, Utt, [A | At]) revise_model(Eprime, Uprime, ACTL, Ett, Utt, [A | At])
; ;
print_message(informational, step('A''')), debug(revision, 'Entering step w', ['A''']),
( (
nusmv:trace(_) nusmv:trace(_)
-> ->
...@@ -218,7 +236,7 @@ is_ectl(Q) :- ...@@ -218,7 +236,7 @@ is_ectl(Q) :-
find_and_add_rule :- find_and_add_rule :-
find_rule(R), find_rule(R),
print_message(informational, trying(R)), debug(revision, 'Considering adding reaction ~w', [R]),
add_reaction_backtracking(R). add_reaction_backtracking(R).
find_rule(R) :- find_rule(R) :-
...@@ -270,8 +288,7 @@ add_reaction_backtracking(R) :- ...@@ -270,8 +288,7 @@ add_reaction_backtracking(R) :-
debug(revision, 'Adding reaction ~w', [R]) debug(revision, 'Adding reaction ~w', [R])
; ;
delete_item([kind: reaction, item: R]), delete_item([kind: reaction, item: R]),
print_message(informational, failure), debug(revision, 'Failure, removing added reaction ~w', [R]),
debug(revision, 'Removing reaction ~w', [R]),
fail fail
). ).
...@@ -329,8 +346,7 @@ del_reaction_backtracking(R) :- ...@@ -329,8 +346,7 @@ del_reaction_backtracking(R) :-
debug(revision, 'Removing reaction ~w', [R]) debug(revision, 'Removing reaction ~w', [R])
; ;
add_item([kind: reaction, item: R]), add_item([kind: reaction, item: R]),
print_message(informational, failure), debug(revision, 'Failure, adding back reaction ~w', [R]),
debug(revision, 'Adding reaction ~w', [R]),
fail fail
). ).
...@@ -367,11 +383,12 @@ remove_stoichiometry_and_sort(Reactants, Products, UReac, UProd, []) :- ...@@ -367,11 +383,12 @@ remove_stoichiometry_and_sort(Reactants, Products, UReac, UProd, []) :-
remove_stoich(_*X, X). remove_stoich(_*X, X).
prolog:message(step(Step)) --> prolog:message(added(Added)) -->
['Entering step ~w'-[Step]]. { maplist(term_to_atom, Added, AddedAtoms),
atomic_list_concat(AddedAtoms, ', ', AddedAtom) },
prolog:message(trying(Reaction)) --> ['Added reactions: ~w'-[AddedAtom]].
['Considering adding reaction ~w'-[Reaction]].
prolog:message(failure) --> prolog:message(removed(Removed)) -->
['Failed']. { maplist(term_to_atom, Removed, RemovedAtoms),
atomic_list_concat(RemovedAtoms, ', ', RemovedAtom) },
['Removed reactions: ~w'-[RemovedAtom]].
...@@ -27,9 +27,7 @@ test( ...@@ -27,9 +27,7 @@ test(
) :- ) :-
command(present(a)), command(present(a)),
command(absent(b)), command(absent(b)),
revise_model('EU'(a, b)), revision:revise_model('EU'(a, b), Reactions, []).
findall(Item, item([kind: reaction, item: Item]), Reactions).
test( test(
'revise_model rule addition for UCTL', 'revise_model rule addition for UCTL',
...@@ -40,45 +38,40 @@ test( ...@@ -40,45 +38,40 @@ test(
) :- ) :-
command(present(a)), command(present(a)),
command(absent(b)), command(absent(b)),
revise_model('EF'(b /\ 'AG'(not(a)))), revision:revise_model('EF'(b /\ 'AG'(not(a))), Reactions, []).
findall(Item, item([kind: reaction, item: Item]), Reactions).
test( test(
'revise_model rule deletion for ACTL, Miguel example', 'revise_model rule deletion for ACTL, Miguel example',
[ [
setup(clear_model), setup(clear_model),
all(Reactions = [['_' =[a]=> b]]) all((Added, Removed) = [([], [a =[b]=> '_'])])
] ]
) :- ) :-
command(add_reaction(a => a + b)), command(add_reaction(a => a + b)),
command(add_reaction(a + b => b)), command(add_reaction(a + b => b)),
revise_model(not(a) \/ 'AX'(a /\ b)), revision:revise_model(not(a) \/ 'AX'(a /\ b), Added, Removed).
findall(Item, item([kind: reaction, item: Item]), Reactions).
test( test(
'revise_model rule deletion (from counter-example) for ACTL', 'revise_model rule deletion (from counter-example) for ACTL',
[ [
setup(clear_model), setup(clear_model),
% all(Reactions = [[], [b => c]]) all((Added, Removed) = [([], [a => b])])
all(Reactions = [[b => c]])
] ]
) :- ) :-
command(present(a)), command(present(a)),
command(absent(b)), command(absent(b)),
command(add_reaction(a => b)), command(add_reaction(a => b)),
command(add_reaction(b => c)), command(add_reaction(b => c)),
revise_model('AG'(a)), revision:revise_model('AG'(a), Added, Removed).
findall(Item, item([kind: reaction, item: Item]), Reactions).
test( test(
'revise_model rule deletion for ACTL, Miguel bigger example', 'revise_model rule deletion for ACTL, Miguel bigger example',
[ [
setup(clear_model), setup(clear_model),
all(Reactions = all((Added, Removed) =
[['_'=>b,'_'=>a+b,'_'=[a]=>b,'_'=[b]=>'_','_'=[b]=>a,'_'=[a+b]=>'_']]) [([], [
'_'=>'_', '_'=>a, a=>'_', '_'=[a]=>'_', a=>b, b=>'_', b=>a, a+b=>'_',
b=[a]=>'_', a=[b]=>'_'])])
] ]
) :- ) :-
command(add_reaction('_' => '_')), command(add_reaction('_' => '_')),
...@@ -97,15 +90,12 @@ test( ...@@ -97,15 +90,12 @@ test(
command(add_reaction(a+b => a)), command(add_reaction(a+b => a)),
command(add_reaction(a+b => b)), command(add_reaction(a+b => b)),
command(add_reaction(a+b => a+b)), command(add_reaction(a+b => a+b)),
revise_model(not(a) \/ 'AX'(a /\ b)), revision:revise_model(not(a) \/ 'AX'(a /\ b), Added, Removed).
findall(Item, item([kind: reaction, item: Item]), Reactions).
test( test(
'3_inhibitions', '3_inhibitions',
[ [
setup(clear_model), setup(clear_model)
true(Reactions = ['_'=>a,'_'=>b,'_'=>c,c=[a]=>'_',a=[b]=>'_',b=[c]=>'_'])
] ]
) :- ) :-
command('_' => a), command('_' => a),
...@@ -115,14 +105,34 @@ test( ...@@ -115,14 +105,34 @@ test(
command(b => '_'), command(b => '_'),
command(c => '_'), command(c => '_'),
once( once(
revise_model( revision:revise_model(
oscil(a) /\ oscil(b) /\ oscil(c) /\ oscil(a) /\ oscil(b) /\ oscil(c) /\
(c -> checkpoint(a, not(c))) /\ (c -> checkpoint(a, not(c))) /\
(a -> checkpoint(b, not(a))) /\ (a -> checkpoint(b, not(a))) /\
(b -> checkpoint(c, not(b))) (b -> checkpoint(c, not(b))),
Added,
Removed
)
),
assertion(Added = [c=[a]=>'_', a=[b]=>'_', b=[c]=>'_']),
assertion(Removed = [a=>'_', b=>'_', c=>'_']).
test(
'Qu',
[
setup(clear_model)
]
) :-
command(load('library:examples/cell_cycle/Qu_et_al_2003.bc')),
once(
revision:revise_model(
'AG'(not('CycB-CDK~{p1}') -> checkpoint('C25~{p1,p2}','CycB-CDK~{p1}')),
Added,
Removed
) )
), ),
findall(Item, item([kind: reaction, item: Item]), Reactions). assertion(Added == []),
assertion(Removed = [k1 for '_' => 'CycB']).
:- end_tests(revision). :- 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