Fix region check

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

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

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