Commit c99fd1ac authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

deleting rules from trace, but only sometimes

parent bcfdf1b4
......@@ -202,7 +202,6 @@ find_rule(R) :-
;
true
),
write(find_rule(M1, M2, M3, M4)),nl,
reaction_editor:simplify_reaction('=>'(M1 + M2, M3 + M4), R),
\+ item([kind: reaction, item: R]).
......@@ -224,14 +223,52 @@ find_and_delete_rules :-
(
nusmv:trace(_)
->
write('trace!'),nl,
delete_rules_from_trace
;
write('notrace :('),nl,
delete_rules
).
delete_rules_from_trace :-
fail.
enumerate_all_molecules(Molecules),
findall(State, nusmv:trace(State), States),
rules_from_trace(States, Molecules, Rules),
write(rules(Rules)),nl,
% We cut a single state-transition, if necessary by removing several rules
member(ToBeDeleted, Rules),
maplist(del_reaction_backtracking, ToBeDeleted).
rules_from_trace([_], _, []).
rules_from_trace([S1, S2 | States], Molecules, [R | Rules]) :-
rules_from_states(S1, S2, Molecules, R),
rules_from_trace([S2 | States], Molecules, Rules).
rules_from_states(S1, S2, Molecules, R) :-
rules_from_states(S1, S2, Molecules, [], [], [], R).
rules_from_states([], [], [], Inc, Dec, Pres, Reactions) :-
msort(Inc, SInc),
msort(Dec, SDec),
msort(Pres, SPres),
findall(Reaction, compatible(SInc, SDec, SPres, Reaction), Reactions).
rules_from_states(["TRUE" | S1], ["TRUE" | S2], [M | Molecules], I, D, P, R) :-
rules_from_states(S1, S2, Molecules, I, D, [M | P], R).
rules_from_states(["TRUE" | S1], ["FALSE" | S2], [M | Molecules], I, D, P, R) :-
rules_from_states(S1, S2, Molecules, I, [M | D], [M | P], R).
rules_from_states(["FALSE" | S1], ["TRUE" | S2], [M | Molecules], I, D, P, R) :-
rules_from_states(S1, S2, Molecules, [M | I], D, P, R).
rules_from_states(["FALSE" | S1], ["FALSE" | S2], [_ | Molecules], I, D, P, R) :-
rules_from_states(S1, S2, Molecules, I, D, P, R).
delete_rules :-
......@@ -253,6 +290,35 @@ del_reaction_backtracking(R) :-
).
compatible(SInc, SDec, SPres, Reaction) :-
item([kind: reaction, item: Reaction]),
reaction(Reaction, _, Reactants, Products, false),
remove_stoichiometry_and_sort(Reactants, Products, UReac, UProd, UCata),
% true products are precisely what increases
SInc = UProd,
% only reactants can decrease
ord_subset(SDec, UReac),
% all reactants and catalyst had to be present
ord_subset(UReac, SPres),
ord_subset(UCata, SPres).
% Based on reaction/5 implementation, we know catalysts come first
remove_stoichiometry_and_sort([_*M | Reac], [_*M | Prod], UReac, UProd, UUCata) :-
!,
remove_stoichiometry_and_sort(Reac, Prod, UReac, UProd, UCata),
ord_add_element(UCata, M, UUCata).
remove_stoichiometry_and_sort(Reactants, Products, UReac, UProd, []) :-
maplist(remove_stoich, Reactants, Reac),
msort(Reac, UReac),
maplist(remove_stoich, Products, Prod),
msort(Prod, UProd).
remove_stoich(_*X, X).
prolog:message(step(Step)) -->
['Entering step ~w'-[Step]].
......
......@@ -3,6 +3,7 @@
:- use_module(reaction_rules).
:- begin_tests(revision).
% condition(flag(slow_test, true, true)),
test(
'categorize_query',
......@@ -22,7 +23,6 @@ test(
[
setup(clear_model),
all(Reactions = [['_' => b], [a => b], ['_' =[a]=> b]])
% condition(flag(slow_test, true, true)),
]
) :-
command(present(a)),
......@@ -36,7 +36,6 @@ test(
[
setup(clear_model),
all(Reactions = [[a => b]])
% condition(flag(slow_test, true, true)),
]
) :-
command(present(a)),
......@@ -50,7 +49,6 @@ test(
[
setup(clear_model),
all(Reactions = [[], [b => c]])
% condition(flag(slow_test, true, true)),
]
) :-
command(present(a)),
......@@ -62,16 +60,17 @@ test(
test(
'revise_model rule deletion for ACTL, Miguel example',
'revise_model rule deletion for ACTL, deleting from NuSMV counter-example',
[
setup(clear_model),
all(Reactions = [['_' =[a]=> b]])
% condition(flag(slow_test, true, true)),
]
) :-
command(present(a)),
command(present(b)),
command(add_reaction(a => a + b)),
command(add_reaction(a + b => b)),
revise_model(not(a) \/ 'AX'(a /\ b)),
revise_model('AX'(a /\ b)),
findall(Item, item([kind: reaction, item: Item]), Reactions).
......
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