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().isBisimulationSet(), storm::exceptions::InvalidSettingsException, "Monotonicity analysis requires bisimulation"); +// STORM_LOG_THROW(storm::settings::getModule().isBisimulationSet(), storm::exceptions::InvalidSettingsException, "Monotonicity analysis requires bisimulation"); storm::utility::Stopwatch simplifyingWatch(true); if (model->isOfType(storm::models::ModelType::Dtmc)) { auto consideredModel = (model->as>()); 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); } }