From 6ac0782a186305fbc78594f384a663a0c8b5e5b2 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Mon, 20 Aug 2018 11:43:56 +0200
Subject: [PATCH] Remove need for bisimulation

---
 src/storm-pars-cli/storm-pars.cpp | 2 +-
 src/storm-pars/analysis/Lattice.h | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index a13f245bf..13767907a 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -461,7 +461,7 @@ namespace storm {
 
             if (parSettings.isMonotonicityAnalysisSet()) {
                 std::cout << "Hello, Jip1" << std::endl;
-                STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet(), storm::exceptions::InvalidSettingsException, "Monotonicity analysis requires bisimulation");
+//                STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet(), storm::exceptions::InvalidSettingsException, "Monotonicity analysis requires bisimulation");
                 storm::utility::Stopwatch simplifyingWatch(true);
                 if (model->isOfType(storm::models::ModelType::Dtmc)) {
                     auto consideredModel = (model->as<storm::models::sparse::Dtmc<ValueType>>());
diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h
index f6617871e..69f8fd4aa 100644
--- a/src/storm-pars/analysis/Lattice.h
+++ b/src/storm-pars/analysis/Lattice.h
@@ -143,22 +143,20 @@ namespace storm {
                                         lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1),
                                                             lattice->getNode(successor2));
                                         // Add stateNumber to the set with seen states.
-                                        seenStates.set(currentState->stateNumber);
                                     } else if (compareResult == 2) {
                                         // successor 2 is closer to top than successor 1
                                         lattice->addBetween(currentState->stateNumber, lattice->getNode(successor2),
                                                             lattice->getNode(successor1));
                                         // Add stateNumber to the set with seen states.
-                                        seenStates.set(currentState->stateNumber);
                                     } else if (compareResult == 0) {
                                         // the successors are at the same level
                                         lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1));
                                         // Add stateNumber to the set with seen states.
-                                        seenStates.set(currentState->stateNumber);
                                     } else {
                                         // TODO: is this what we want?
                                         lattice->add(currentState->stateNumber);
                                     }
+                                    seenStates.set(currentState->stateNumber);
 
                                 }
                             }