diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index e7aedd2f7..f40d27f2f 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -547,7 +547,7 @@ namespace storm { auto dtmcModel = model->as>(); // TODO check formula type auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmcModel, 3); - auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates()); + auto assumptionMaker = storm::analysis::AssumptionMaker(extender, &assumptionChecker, sparseModel->getNumberOfStates(), parSettings.isValidateAssumptionsSet()); std::map>> result = assumptionMaker.makeAssumptions( std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair)); diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index c6804ef59..bc918b48c 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -7,10 +7,11 @@ namespace storm { namespace analysis { template - AssumptionMaker::AssumptionMaker(storm::analysis::LatticeExtender* latticeExtender, storm::analysis::AssumptionChecker* assumptionChecker, uint_fast64_t numberOfStates) { + AssumptionMaker::AssumptionMaker(storm::analysis::LatticeExtender* latticeExtender, storm::analysis::AssumptionChecker* 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()); 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 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(assumption)); result = (runRecursive(lattice, assumptions)); } else { diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 73e6c5bdd..1381d4ad0 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/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* latticeExtender, storm::analysis::AssumptionChecker* checker, uint_fast64_t numberOfStates); + AssumptionMaker(storm::analysis::LatticeExtender* latticeExtender, storm::analysis::AssumptionChecker* 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* latticeExtender; + storm::analysis::AssumptionChecker* assumptionChecker; + std::shared_ptr expressionManager; uint_fast64_t numberOfStates; - storm::analysis::AssumptionChecker* assumptionChecker; + bool validate; + + }; } } diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index ef64acb94..97c8bb16b 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/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 diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 0fa167409..dd84e9975 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/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: