From f1f10a97868b5d055284b31e6257fb43b45703e8 Mon Sep 17 00:00:00 2001
From: Sylvain Soliman <Sylvain.Soliman@inria.fr>
Date: Wed, 6 Jul 2016 16:20:40 +0200
Subject: [PATCH] added the big example from Miguel, lead to a few bugfixes

---
 revision.pl  | 21 ++++++++++++++-------
 revision.plt | 31 ++++++++++++++++++++++++++++++-
 2 files changed, 44 insertions(+), 8 deletions(-)

diff --git a/revision.pl b/revision.pl
index 1c0de9d5..c85cb829 100644
--- a/revision.pl
+++ b/revision.pl
@@ -70,17 +70,19 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
   (
     Result = true
   ->
-    print_message(informational, step('A'))
+    print_message(informational, step('A')),
+    revise_model([], [], ACTL, Et, Ut, [A | At])
   ;
     print_message(informational, step('A''')),
+    list_reactions,
     find_and_delete_rules,
     % 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
     % simply split and add again to the formulae to be verified
-    recheck_spec(AllSpec, Init, Bool)
-  ),
-  revise_model([], [], ACTL, Et, Ut, [A | At]).
+    recheck_spec(AllSpec, Init, Bool),
+    revise_model([], [], [A | ACTL], Et, Ut, At)
+  ).
 
 
 revise_model([], [], [], _, _, _) :-
@@ -88,6 +90,9 @@ revise_model([], [], [], _, _, _) :-
   print_message(informational, success(Reactions)).
 
 
+recheck_spec([], _, _) :-
+  !.
+
 recheck_spec(Specs, Init, Bool) :-
   join_op('/\\', Specs, Spec),
   print_message(informational, checking(Spec)),
@@ -237,6 +242,7 @@ delete_rules_from_trace :-
   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).
 
 
@@ -293,8 +299,9 @@ 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,
+  % products are true at the end
+  ord_union(SInc, SPres, SAfter),
+  ord_subset(UProd, SAfter),
   % only reactants can decrease
   ord_subset(SDec, UReac),
   % all reactants and catalyst had to be present
diff --git a/revision.plt b/revision.plt
index 5a7a2de4..261cd59e 100644
--- a/revision.plt
+++ b/revision.plt
@@ -61,7 +61,8 @@ test(
   'revise_model rule deletion (from counter-example) for ACTL',
   [
     setup(clear_model),
-    all(Reactions = [[], [b => c]])
+    % all(Reactions = [[], [b => c]])
+    all(Reactions = [[b => c]])
   ]
 ) :-
   command(present(a)),
@@ -72,4 +73,32 @@ test(
   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).
-- 
GitLab