diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index bba77fb37..5cc5e6ea9 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -1,26 +1,26 @@ // // Created by Jip Spel on 12.09.18. // +#include "AssumptionChecker.h" #include "storm-pars/utility/ModelInstantiator.h" -#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" + +#include "storm/environment/Environment.h" #include "storm/exceptions/NotSupportedException.h" -#include "AssumptionChecker.h" #include "storm/modelchecker/CheckTask.h" -#include "storm/environment/Environment.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/storage/expressions/SimpleValuation.h" #include "storm/storage/expressions/ExpressionManager.h" - - namespace storm { namespace analysis { template AssumptionChecker::AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples) { this->formula = formula; + // Create sample points auto instantiator = storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>(*model.get()); auto matrix = model->getTransitionMatrix(); std::set variables = storm::models::sparse::getProbabilityParameters(*model); @@ -51,19 +51,6 @@ namespace storm { std::vector values = quantitativeResult.getValueVector(); results.push_back(values); } -// this->numberOfStates = model->getNumberOfStates(); -// this->initialStates = model->getInitialStates(); - } - - template - bool AssumptionChecker::checkOnSamples(uint_fast64_t val1, uint_fast64_t val2) { - bool result = true; - for (auto itr = results.begin(); result && itr != results.end(); ++itr) { - // TODO: als expressie - auto values = (*itr); - result &= (values[val1] >= values[val2]); - } - return result; } template @@ -80,6 +67,7 @@ namespace storm { auto index = std::stoi(par.getName()); valuation.setRationalValue(par, values[index]); } + assert(assumption->hasBooleanType()); result &= assumption->evaluateAsBool(&valuation); } return result; @@ -87,4 +75,4 @@ namespace storm { template class AssumptionChecker; } -} \ No newline at end of file +} diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index 78e209ab2..2f0f8313a 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -10,29 +10,35 @@ #include "storm/environment/Environment.h" #include "storm/storage/expressions/BinaryRelationExpression.h" - namespace storm { namespace analysis { template class AssumptionChecker { public: + /*! + * Constructs an AssumptionChecker based on the number of samples, for the given formula and model. + * + * @param formula The formula to check. + * @param model The model to check the formula on. + * @param numberOfSamples Number of sample points. + */ AssumptionChecker(std::shared_ptr formula, std::shared_ptr> model, uint_fast64_t numberOfSamples); - bool checkOnSamples(uint_fast64_t val1, uint_fast64_t val2); + /*! + * Checks if the assumption holds at the sample points of the AssumptionChecker. + * + * @param assumption The assumption to check. + * @return true if the assumption holds at the sample points + */ bool checkOnSamples(std::shared_ptr assumption); + private: std::shared_ptr formula; -// std::vector> sampleModels; - std::vector> results; -// uint_fast64_t numberOfStates; -// -// storm::storage::BitVector initialStates; }; } } - #endif //STORM_ASSUMPTIONCHECKER_H