diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 03665fe25..39218ab43 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -716,13 +716,14 @@ namespace storm { model->printModelInformationToStream(std::cout); } + std::vector> regions = parseRegions(model); + if (monSettings.isMonotonicityAnalysisSet()) { std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); // Monotonicity storm::utility::Stopwatch monotonicityWatch(true); - std::vector> regions = parseRegions(model); - STORM_LOG_THROW(regions.size() > 1, storm::exceptions::InvalidArgumentException, "Monotonicity analysis only allowed on single region"); + STORM_LOG_THROW(regions.size() <= 1, storm::exceptions::InvalidArgumentException, "Monotonicity analysis only allowed on single region"); storm::analysis::MonotonicityChecker monotonicityChecker = storm::analysis::MonotonicityChecker(model, formulas, regions, monSettings.isValidateAssumptionsSet(), monSettings.getNumberOfSamples(), monSettings.getMonotonicityAnalysisPrecision()); monotonicityChecker.checkMonotonicity(); monotonicityWatch.stop(); @@ -731,7 +732,6 @@ namespace storm { return; } - std::vector> regions = parseRegions(model); std::string samplesAsString = parSettings.getSamples(); SampleInformation samples; if (!samplesAsString.empty()) { diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 1137d8ce1..e4d18e9f6 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -197,6 +197,7 @@ namespace storm { std::vector maxValues = maxRes.getValueVector(); // Create initial order std::tuple criticalTuple = extender->toOrder(formulas, minValues, maxValues); +// std::tuple criticalTuple = extender->toOrder(formulas); // Continue based on not (yet) sorted states diff --git a/src/storm-pars/analysis/OrderExtender.cpp b/src/storm-pars/analysis/OrderExtender.cpp index 6662e2757..4b32d63eb 100644 --- a/src/storm-pars/analysis/OrderExtender.cpp +++ b/src/storm-pars/analysis/OrderExtender.cpp @@ -205,7 +205,7 @@ namespace storm { } if (!order->contains(max)) { // Because of construction min is in the order - order->addBetween(max, order->getNode(min), order->getTop()); + order->addBetween(max, order->getTop(), order->getNode(min)); } assert (order->compare(max, min) == Order::ABOVE); order->addBetween(state, max, min);