Make validation of assumptions optional

src/storm-pars-cli/storm-pars.cpp

@@ -547,7 +547,7 @@ namespace storm {
                 auto dtmcModel = model->as<storm::models::sparse::Dtmc<ValueType>>();
                 // TODO check formula type
                 auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmcModel, 3);
-                auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates());
+                auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates(), parSettings.isValidateAssumptionsSet());
 
                 std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result = assumptionMaker.makeAssumptions(
                         std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));

src/storm-pars/analysis/AssumptionMaker.cpp

@@ -7,10 +7,11 @@
 namespace storm {
     namespace analysis {
         template<typename ValueType>
-        AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates) {
+        AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) {
             this->latticeExtender = latticeExtender;
             this->numberOfStates = numberOfStates;
             this->assumptionChecker = assumptionChecker;
+            this->validate = validate;
             this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
             for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) {
                 expressionManager->declareRationalVariable(std::to_string(i));
@@ -48,7 +49,7 @@ namespace storm {
             // only the last assumption is new
             std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions.back());
 
-            if (assumptionChecker->validated(assumptions.back())) {
+            if (validate && assumptionChecker->validated(assumptions.back())) {
                 assumptions.pop_back();
             }
 
@@ -81,8 +82,9 @@ namespace storm {
                         var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
                         storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
             if (assumptionChecker->checkOnSamples(assumption)) {
-                // TODO: only if validation on
-                assumptionChecker->validateAssumption(assumption, lattice);
+                if (validate) {
+                    assumptionChecker->validateAssumption(assumption, lattice);
+                }
                 assumptions.push_back(std::shared_ptr<storm::expressions::BinaryRelationExpression>(assumption));
                 result = (runRecursive(lattice, assumptions));
             } else {

src/storm-pars/analysis/AssumptionMaker.h

@@ -25,7 +25,7 @@ namespace storm {
              * @param checker The AssumptionChecker which checks the assumptions at sample points.
              * @param numberOfStates The number of states of the model.
              */
-            AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates);
+            AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates, bool validate);
 
             /*!
              * Make the assumptions given a lattice and two states which could not be added to the lattice. Returns when no more assumptions can be made.
@@ -45,11 +45,15 @@ namespace storm {
 
             storm::analysis::LatticeExtender<ValueType>* latticeExtender;
 
+            storm::analysis::AssumptionChecker<ValueType>* assumptionChecker;
+
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
 
             uint_fast64_t numberOfStates;
 
-            storm::analysis::AssumptionChecker<ValueType>* assumptionChecker;
+            bool validate;
+
+
         };
     }
 }

src/storm-pars/settings/modules/ParametricSettings.cpp

@@ -70,6 +70,11 @@ namespace storm {
                 // TODO: Make this dependent on the input.
                 return true;
             }
+
+            bool ParametricSettings::isValidateAssumptionsSet() const {
+                // TODO: Make this dependent on the input.
+                return true;
+            }
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/storm-pars/settings/modules/ParametricSettings.h

@@ -65,7 +65,9 @@ namespace storm {
                 bool isSampleExactSet() const;
 
                 bool isMonotonicityAnalysisSet() const;
-                
+
+                bool isValidateAssumptionsSet() const;
+
                 const static std::string moduleName;
                 
             private: