Remove need for bisimulation

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>>());

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);
 
                                 }
                             }