From e0b2869bd53626b76df4b00b6920320fe4536b74 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Thu, 25 Jul 2019 18:26:36 +0200
Subject: [PATCH] Fix region check

---
 src/storm-pars-cli/storm-pars.cpp               | 6 +++---
 src/storm-pars/analysis/MonotonicityChecker.cpp | 1 +
 src/storm-pars/analysis/OrderExtender.cpp       | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

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<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
+
             if (monSettings.isMonotonicityAnalysisSet()) {
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
                 // Monotonicity
                 storm::utility::Stopwatch monotonicityWatch(true);
-                std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(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<ValueType> monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, regions, monSettings.isValidateAssumptionsSet(), monSettings.getNumberOfSamples(), monSettings.getMonotonicityAnalysisPrecision());
                 monotonicityChecker.checkMonotonicity();
                 monotonicityWatch.stop();
@@ -731,7 +732,6 @@ namespace storm {
                 return;
             }
 
-            std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
             std::string samplesAsString = parSettings.getSamples();
             SampleInformation<ValueType> 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<double> maxValues = maxRes.getValueVector();
             // Create initial order
             std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas, minValues, maxValues);
+//            std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> 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);