From f9049ff25aecc08552636bce18b58bb7966eba9e Mon Sep 17 00:00:00 2001
From: Morten Konggaard Schou <mschou15@student.aau.dk>
Date: Mon, 11 May 2020 11:59:41 +0200
Subject: [PATCH] Make reduction R4 as R1 + R3 (i.e. without R2).

---
 src/pdaaal/Reducer.h | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/pdaaal/Reducer.h b/src/pdaaal/Reducer.h
index f0fbd11..5fbf517 100644
--- a/src/pdaaal/Reducer.h
+++ b/src/pdaaal/Reducer.h
@@ -71,7 +71,7 @@ namespace pdaaal {
             Reducer::forwards_prune(pda, initial_id);
             Reducer::backwards_prune(pda, terminal_id);
             std::queue<size_t> waiting;
-            auto ds = (aggresivity >= 2);
+            auto ds = (aggresivity >= 2 && aggresivity <= 3);
             std::vector<tos_t> approximation(pda.states().size());
             // initialize
             for (const auto& [r,labels] : pda.states()[initial_id]._rules) {
@@ -89,7 +89,7 @@ namespace pdaaal {
                     ss._tos.insert(lb, r._op_label);
             }
 
-            if (aggresivity == 3) {
+            if (aggresivity >= 3) {
                 Reducer::target_tos_prune(pda, terminal_id);
             }
             // saturate
@@ -158,7 +158,7 @@ namespace pdaaal {
             }
 
             Reducer::backwards_prune(pda, terminal_id);
-            if (aggresivity == 3) {
+            if (aggresivity >= 3) {
                 // it could potentially work as fixpoint; not sure if it has any effect.
                 Reducer::target_tos_prune(pda, terminal_id);
             }