sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Clean up assumption maker

tempestpy_adaptions
Jip Spel 6 years ago
parent
ee08139641
commit
fa97e0138f
2 changed files with 32 additions and 33 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 39
      src/storm-pars/analysis/AssumptionMaker.cpp
  2. 26
      src/storm-pars/analysis/AssumptionMaker.h

39
src/storm-pars/analysis/AssumptionMaker.cpp
View File

@ -1,37 +1,30 @@
//
// Created by Jip Spel on 03.09.18.
//
#include "AssumptionMaker.h"
namespace storm {
namespace analysis {
typedef std::shared_ptr<storm::expressions::BinaryRelationExpression> AssumptionType;
typedef std::shared_ptr<expressions::BinaryRelationExpression> AssumptionType;
template<typename ValueType>
AssumptionMaker<ValueType>::AssumptionMaker(AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) {
this->numberOfStates = numberOfStates;
this->assumptionChecker = assumptionChecker;
this->validate = validate;
this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
this->expressionManager = std::make_shared<expressions::ExpressionManager>(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 <typename ValueType>
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) {
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, AssumptionStatus> result;
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) {
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, 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<storm::expressions::BinaryRelationExpression> assumption1
= std::make_shared<storm::expressions::BinaryRelationExpression>(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<expressions::BinaryRelationExpression> assumption1
= std::make_shared<expressions::BinaryRelationExpression>(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<storm::expressions::BinaryRelationExpression> assumption2
= std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
std::shared_ptr<expressions::BinaryRelationExpression> assumption2
= std::make_shared<expressions::BinaryRelationExpression>(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<storm::expressions::BinaryRelationExpression> assumption3
= std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
std::shared_ptr<expressions::BinaryRelationExpression> assumption3
= std::make_shared<expressions::BinaryRelationExpression>(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<storm::RationalFunction>;
template class AssumptionMaker<RationalFunction>;
}
}

26
src/storm-pars/analysis/AssumptionMaker.h
View File

@ -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<typename ValueType>
class AssumptionMaker {
typedef std::shared_ptr<storm::expressions::BinaryRelationExpression> AssumptionType;
typedef std::shared_ptr<expressions::BinaryRelationExpression> 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<ValueType>* checker, uint_fast64_t numberOfStates, bool validate);
AssumptionMaker(AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates, bool validate);
std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, 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<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice);
private:
AssumptionChecker<ValueType>* assumptionChecker;
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
std::shared_ptr<expressions::ExpressionManager> expressionManager;
uint_fast64_t numberOfStates;

Write Preview
Loading…
Cancel
Save