Commit f1f10a97 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

added the big example from Miguel, lead to a few bugfixes

parent a4e26a9e
...@@ -70,17 +70,19 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :- ...@@ -70,17 +70,19 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
( (
Result = true Result = true
-> ->
print_message(informational, step('A')) print_message(informational, step('A')),
revise_model([], [], ACTL, Et, Ut, [A | At])
; ;
print_message(informational, step('A''')), print_message(informational, step('A''')),
list_reactions,
find_and_delete_rules, find_and_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([A | Ut], Et, AllSpec), append(Ut, Et, AllSpec),
% FIXME the published algorithm actually allows to not re-check, but % FIXME the published algorithm actually allows to not re-check, but
% simply split and add again to the formulae to be verified % simply split and add again to the formulae to be verified
recheck_spec(AllSpec, Init, Bool) recheck_spec(AllSpec, Init, Bool),
), revise_model([], [], [A | ACTL], Et, Ut, At)
revise_model([], [], ACTL, Et, Ut, [A | At]). ).
revise_model([], [], [], _, _, _) :- revise_model([], [], [], _, _, _) :-
...@@ -88,6 +90,9 @@ revise_model([], [], [], _, _, _) :- ...@@ -88,6 +90,9 @@ revise_model([], [], [], _, _, _) :-
print_message(informational, success(Reactions)). print_message(informational, success(Reactions)).
recheck_spec([], _, _) :-
!.
recheck_spec(Specs, Init, Bool) :- recheck_spec(Specs, Init, Bool) :-
join_op('/\\', Specs, Spec), join_op('/\\', Specs, Spec),
print_message(informational, checking(Spec)), print_message(informational, checking(Spec)),
...@@ -237,6 +242,7 @@ delete_rules_from_trace :- ...@@ -237,6 +242,7 @@ delete_rules_from_trace :-
rules_from_trace(States, Molecules, Rules), rules_from_trace(States, Molecules, Rules),
% We cut a single state-transition, if necessary by removing several rules % We cut a single state-transition, if necessary by removing several rules
member(ToBeDeleted, Rules), member(ToBeDeleted, Rules),
ToBeDeleted \= [],
maplist(del_reaction_backtracking, ToBeDeleted). maplist(del_reaction_backtracking, ToBeDeleted).
...@@ -293,8 +299,9 @@ compatible(SInc, SDec, SPres, Reaction) :- ...@@ -293,8 +299,9 @@ compatible(SInc, SDec, SPres, Reaction) :-
item([kind: reaction, item: Reaction]), item([kind: reaction, item: Reaction]),
reaction(Reaction, _, Reactants, Products, false), reaction(Reaction, _, Reactants, Products, false),
remove_stoichiometry_and_sort(Reactants, Products, UReac, UProd, UCata), remove_stoichiometry_and_sort(Reactants, Products, UReac, UProd, UCata),
% true products are precisely what increases % products are true at the end
SInc = UProd, ord_union(SInc, SPres, SAfter),
ord_subset(UProd, SAfter),
% only reactants can decrease % only reactants can decrease
ord_subset(SDec, UReac), ord_subset(SDec, UReac),
% all reactants and catalyst had to be present % all reactants and catalyst had to be present
......
...@@ -61,7 +61,8 @@ test( ...@@ -61,7 +61,8 @@ 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(Reactions = [[], [b => c]])
all(Reactions = [[b => c]])
] ]
) :- ) :-
command(present(a)), command(present(a)),
...@@ -72,4 +73,32 @@ test( ...@@ -72,4 +73,32 @@ test(
findall(Item, item([kind: reaction, item: Item]), Reactions). findall(Item, item([kind: reaction, item: Item]), Reactions).
test(
'revise_model rule deletion for ACTL, Miguel bigger example',
[
setup(clear_model),
all(Reactions =
[['_'=>b,'_'=>a+b,'_'=[a]=>b,'_'=[b]=>'_','_'=[b]=>a,'_'=[a+b]=>'_']])
]
) :-
command(add_reaction('_' => '_')),
command(add_reaction('_' => a)),
command(add_reaction('_' => b)),
command(add_reaction('_' => a+b)),
command(add_reaction(a => '_')),
command(add_reaction(a => a)),
command(add_reaction(a => b)),
command(add_reaction(a => a+b)),
command(add_reaction(b => '_')),
command(add_reaction(b => a)),
command(add_reaction(b => b)),
command(add_reaction(b => a+b)),
command(add_reaction(a+b => '_')),
command(add_reaction(a+b => a)),
command(add_reaction(a+b => b)),
command(add_reaction(a+b => a+b)),
revise_model(not(a) \/ 'AX'(a /\ b)),
findall(Item, item([kind: reaction, item: Item]), Reactions).
:- 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