fixing stuff again

revision.pl

@@ -42,9 +42,8 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
 revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
   item([kind: option, item: option(nusmv_initial_states: Init)]),
   item([kind: option, item: option(boolean_semantics: Bool)]),
-  check_ctl_impl(U, Init, silent, Bool, Result),
   (
-    Result = true
+    check_ctl_impl(U, Init, no, Bool, true)
   ->
     print_message(informational, step('U'))
   ;
@@ -55,7 +54,7 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
       append([U | Ut], At, AllSpec)
     ;
       print_message(informational, step('U''''')),
-      find_and_delete_rules,
+      delete_rules,
       % FIXME check At too since self-loops can be added by removing a reaction
       append([U | Ut], Et, AllSpec)
     ),
@@ -74,10 +73,17 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
     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(Ut, Et, AllSpec),
+    (
+      nusmv:trace(_)
+    ->
+      delete_rules_from_trace,
+      % FIXME check At too since self-loops can be added by removing a reaction
+      append(Ut, Et, AllSpec)
+    ;
+      delete_rules,
+      % we delete blindly, so we need to check A now
+      append([A | 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),
@@ -216,7 +222,6 @@ find_rule(R) :-
 add_reaction_backtracking(R) :-
   (
     add_item([kind: reaction, item: R]),
-    % list_reactions,nl,
     print_message(informational, added(R))
   ;
     delete_item([kind: reaction, item: R]),
@@ -226,16 +231,6 @@ add_reaction_backtracking(R) :-
   ).
 
 
-find_and_delete_rules :-
-  (
-    nusmv:trace(_)
-  ->
-    delete_rules_from_trace
-  ;
-    delete_rules
-  ).
-
-
 delete_rules_from_trace :-
   enumerate_all_molecules(Molecules),
   findall(State, nusmv:trace(State), States),