From fa97e0138f16378892467f7806fbde689f1014d6 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Wed, 15 May 2019 10:08:00 +0200 Subject: [PATCH] Clean up assumption maker --- src/storm-pars/analysis/AssumptionMaker.cpp | 39 +++++++++------------ src/storm-pars/analysis/AssumptionMaker.h | 26 ++++++++------ 2 files changed, 32 insertions(+), 33 deletions(-) diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index bdac30bb2..78cebe88e 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -1,37 +1,30 @@ -// -// Created by Jip Spel on 03.09.18. -// - #include "AssumptionMaker.h" namespace storm { namespace analysis { - typedef std::shared_ptr AssumptionType; + typedef std::shared_ptr AssumptionType; template AssumptionMaker::AssumptionMaker(AssumptionChecker* assumptionChecker, uint_fast64_t numberOfStates, bool validate) { this->numberOfStates = numberOfStates; this->assumptionChecker = assumptionChecker; this->validate = validate; - this->expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + this->expressionManager = std::make_shared(expressions::ExpressionManager()); for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) { - // TODO: expressenmanager pointer maken die oorspronkelijk in monotonicity checker zit expressionManager->declareRationalVariable(std::to_string(i)); } } template - std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) { - std::map, AssumptionStatus> result; + std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) { + std::map, AssumptionStatus> result; - // TODO: alleen maar als validate true is results genereren - storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); - storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); - std::shared_ptr assumption1 - = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); + expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); + std::shared_ptr assumption1 + = std::make_shared(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::Greater)); - // TODO: dischargen gebasseerd op monotonicity + expressions::BinaryRelationExpression::RelationType::Greater)); AssumptionStatus result1; AssumptionStatus result2; AssumptionStatus result3; @@ -43,10 +36,10 @@ namespace storm { result[assumption1] = result1; - std::shared_ptr assumption2 - = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + std::shared_ptr assumption2 + = std::make_shared(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::Greater)); + expressions::BinaryRelationExpression::RelationType::Greater)); if (validate) { result2 = assumptionChecker->validateAssumption(assumption2, lattice); @@ -55,10 +48,10 @@ namespace storm { } result[assumption2] = result2; - std::shared_ptr assumption3 - = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + std::shared_ptr assumption3 + = std::make_shared(expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::Equal)); + expressions::BinaryRelationExpression::RelationType::Equal)); if (validate) { result3 = assumptionChecker->validateAssumption(assumption3, lattice); } else { @@ -69,6 +62,6 @@ namespace storm { return result; } - template class AssumptionMaker; + template class AssumptionMaker; } } diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 2f52b85de..42710fcc6 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -1,7 +1,3 @@ -// -// Created by Jip Spel on 03.09.18. -// - #ifndef STORM_ASSUMPTIONMAKER_H #define STORM_ASSUMPTIONMAKER_H @@ -17,23 +13,33 @@ namespace storm { template class AssumptionMaker { - typedef std::shared_ptr AssumptionType; + typedef std::shared_ptr AssumptionType; public: /*! - * Constructs AssumptionMaker based on the lattice extender, the assumption checker and number of states of the model. - * TODO + * Constructs AssumptionMaker based on the lattice extender, the assumption checker and number of states of the mode + * * @param latticeExtender The LatticeExtender which needs the assumptions made by the AssumptionMaker. * @param checker The AssumptionChecker which checks the assumptions at sample points. * @param numberOfStates The number of states of the model. */ - AssumptionMaker( AssumptionChecker* checker, uint_fast64_t numberOfStates, bool validate); + AssumptionMaker(AssumptionChecker* checker, uint_fast64_t numberOfStates, bool validate); - std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice); + /*! + * Creates assumptions, and checks them if validate in constructor is true. + * Possible results: AssumptionStatus::VALID, AssumptionStatus::INVALID, AssumptionStatus::UNKNOWN + * If validate is false result is always AssumptionStatus::UNKNOWN + * + * @param val1 First state number + * @param val2 Second state number + * @param lattice The lattice on which the assumptions are checked + * @return Map with three assumptions, and the validation + */ + std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice); private: AssumptionChecker* assumptionChecker; - std::shared_ptr expressionManager; + std::shared_ptr expressionManager; uint_fast64_t numberOfStates;