From 28b06f5eda73f5ac68890d012c1bf1c095f58ec5 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Tue, 2 Oct 2018 16:47:53 +0200
Subject: [PATCH] Add another way to extend the lattice

---
 src/storm-pars/analysis/LatticeExtender.cpp | 36 +++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp
index 7765dc8ed..24058fd8a 100644
--- a/src/storm-pars/analysis/LatticeExtender.cpp
+++ b/src/storm-pars/analysis/LatticeExtender.cpp
@@ -54,6 +54,10 @@ namespace storm {
                             added = true;
                         }
                     }
+                    if (!added) {
+                        // Add one of the states of the scc
+                        initialMiddleStates.set(*(states.begin()));
+                    }
                 }
             }
         }
@@ -111,6 +115,7 @@ namespace storm {
 
         template <typename ValueType>
         std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
+            // TODO: split up
             auto numberOfStates = this->model->getNumberOfStates();
             // First handle assumption
             if (assumption != nullptr) {
@@ -207,6 +212,37 @@ namespace storm {
                         }
                         lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest));
                     }
+
+                    bool checkOneSuccLeft = seenStates[stateNumber] && successors.getNumberOfSetBits() <= 2;
+                    bool helper = true;
+                    for (auto succIndex = successors.getNextSetIndex(0); (check || checkOneSuccLeft) && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) {
+                        checkOneSuccLeft &= !(!helper && !seenStates[succIndex]);
+                        helper &= seenStates[succIndex];
+                    }
+
+                    checkOneSuccLeft &= !helper;
+
+
+                    if (checkOneSuccLeft) {
+                        // at most 2 successors
+                        auto succ1 = successors.getNextSetIndex(0);
+                        auto succ2 = successors.getNextSetIndex(succ1+1);
+                        // Otherwise there is just one transition, this is already handled above
+                        if (succ2 != numberOfStates) {
+                            auto nodeCurr = lattice->getNode(stateNumber);
+                            if (!seenStates[succ1]) {
+                                std::swap(succ1, succ2);
+                            }
+                            assert (seenStates[succ1]);
+                            auto nodeSucc = lattice->getNode(succ1);
+                            auto compare = lattice->compare(stateNumber, succ1);
+                            if (compare == storm::analysis::Lattice::ABOVE) {
+                                lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber));
+                            } else if (compare == storm::analysis::Lattice::BELOW) {
+                                lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom());
+                            }
+                        }
+                    }
                 }
             }
             return std::make_tuple(lattice, numberOfStates, numberOfStates);