Commit 264da436 authored by Sylvain Soliman's avatar Sylvain Soliman

sorting heuristics for rule deletion FTW

parent 7dbe8a80
......@@ -544,7 +544,7 @@ check_ctl :-
doc('Checks the current CTL specification (i.e., the conjunction of all
formulae of the current specification).'),
findall(Formula, item([kind: ctl_spec, item: Formula]), Specs),
join_op('/\\', Specs, Spec),
join_with_op(Specs, '/\\', Spec),
check_ctl(Spec).
......
......@@ -30,7 +30,7 @@ revise_model :-
doc('Use theory-revision as above, using the currently defined CTL
specification.'),
findall(Formula, item([kind: ctl_spec, item: Formula]), Specs),
join_op('/\\', Specs, Spec),
join_with_op(Specs, '/\\', Spec),
revise_model(Spec).
......@@ -115,7 +115,7 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
->
% might not be enough to make A true, thus we do not add A to the
% treated formulae
delete_rules_from_trace
delete_rules_from_trace(A, Et, Ut, Init, Bool)
;
delete_rules,
% we delete blindly, so we need to check A now to avoid useless
......@@ -136,7 +136,7 @@ recheck_spec([], _, _) :-
!.
recheck_spec(Specs, Init, Bool) :-
join_op('/\\', Specs, Spec),
join_with_op(Specs, '/\\', Spec),
debug(revision, 'Checking consolidated query ~w', [Spec]),
check_ctl_impl(Spec, Init, no, Bool, true).
......@@ -306,14 +306,53 @@ add_reaction_backtracking(R) :-
).
delete_rules_from_trace :-
:- dynamic(ruleset_score/2).
delete_rules_from_trace(A, Et, Ut, Init, Bool) :-
retractall(ruleset_score(_, _)),
enumerate_all_molecules(Molecules),
findall(State, nusmv:trace(State), States),
rules_from_trace(States, Molecules, Rules),
% We cut a single state-transition, if necessary by removing several rules
member(ToBeDeleted, Rules),
ToBeDeleted \= [],
maplist(del_reaction_backtracking, ToBeDeleted).
% we score the cutsets by checking what they broke
debugging(revision, Debug),
nodebug(revision),
nb_getval(need_recheck, NeedRecheck),
(
(
member(ToBeDeleted, Rules),
% Avoid the no-state, or single-state traces
% FIXME what do we do then?
ToBeDeleted \= []
),
(
maplist(del_reaction_backtracking, ToBeDeleted),
nb_setval(need_recheck, true),
check_and_split(Et, Ut, [A], _, _, _, Etf, Utf, Atf, Init, Bool),
length(Etf, Etl),
length(Utf, Utl),
length(Atf, Atl),
TrueFormulae is Etl + Atl + Utl,
assertz(ruleset_score(ToBeDeleted, TrueFormulae))
),
fail
;
true
),
(
Debug = true
->
debug(revision)
;
true
),
nb_setval(need_recheck, NeedRecheck),
findall(Score-RuleSet, ruleset_score(RuleSet, Score), Choices),
keysort(Choices, SortedChoices),
% now iterate on the cutsets in order
member(_-ChoiceToBeDeleted, SortedChoices),
maplist(del_reaction_backtracking, ChoiceToBeDeleted).
rules_from_trace([_], _, []).
......@@ -347,10 +386,11 @@ rules_from_states(["FALSE" | S1], ["FALSE" | S2], [_ | Molecules], I, D, P, R) :
delete_rules :-
% FIXME Biocham v3 never deletes blindly
fail,
findall(Item, item([kind: reaction, item: Item]), Reactions),
% FIXME make the upper bound parameterizable, currently using 6 Chabrier
% style
extract_sublist(Reactions, ToBeDeleted, 1, 6),
extract_sublist(Reactions, ToBeDeleted),
ToBeDeleted \= [],
maplist(del_reaction_backtracking, ToBeDeleted).
......
......@@ -138,7 +138,6 @@ test(
test(
'Qu2',
[
blocked(tooslow),
setup(clear_model)
]
) :-
......@@ -162,7 +161,7 @@ test(
command(add_ctl('AG'(not('CycB-CDK~{p1}')->checkpoint('C25~{p1,p2}','CycB-CDK~{p1}')))),
findall(Formula, item([kind: ctl_spec, item: Formula]), Specs),
join_op('/\\', Specs, Spec),
join_with_op(Specs, '/\\', Spec),
once(
revision:revise_model(
Spec,
......
......@@ -28,8 +28,8 @@
with_clean/2,
clean/1,
check_cleaned/1,
join_op/3,
extract_sublist/4,
join_with_op/3,
extract_sublist/2,
alphabetic_char/1,
alphanumeric_char/1,
numeric_char/1,
......@@ -421,25 +421,20 @@ check_cleaned(M : F / N) :-
).
join_op(_Op, [Item], Item).
join_with_op([Item], _Op, Item) :-
% indexing not enough to efficiently remove choice point
!.
join_op(Op, [I1, I2 | Items], Term) :-
join_with_op([I1, I2 | Items], Op, Term) :-
Term =..[Op, I1, T],
join_op(Op, [I2 | Items], T).
join_with_op([I2 | Items], Op, T).
extract_sublist([H | T], [H | TT], Min, Max) :-
Max > 0,
MMin is Min - 1,
MMax is Max - 1,
extract_sublist(T, TT, MMin, MMax).
extract_sublist([H | T], [H | TT]) :-
extract_sublist(T, TT).
extract_sublist([_ | T], TT, Min, Max) :-
extract_sublist(T, TT, Min, Max).
extract_sublist([], [], Min, Max) :-
Min =< 0,
Max >= 0.
extract_sublist([_ | T], TT) :-
extract_sublist(T, TT).
uppercase_char(Char) :-
......
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