diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp
index deb3913cd..ceb05ea72 100644
--- a/src/storm-pars/analysis/AssumptionMaker.cpp
+++ b/src/storm-pars/analysis/AssumptionMaker.cpp
@@ -7,8 +7,7 @@
namespace storm {
namespace analysis {
template<typename ValueType>
- AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) {
- this->latticeExtender = latticeExtender;
+ AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::AssumptionChecker<ValueType>* assumptionChecker, uint_fast64_t numberOfStates, bool validate) {
this->numberOfStates = numberOfStates;
this->assumptionChecker = assumptionChecker;
this->validate = validate;
@@ -18,100 +17,40 @@ namespace storm {
}
}
- template<typename ValueType>
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>
- AssumptionMaker<ValueType>::makeAssumptions(storm::analysis::Lattice *lattice, uint_fast64_t critical1,
- uint_fast64_t critical2) {
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
-
- std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> emptySet;
- if (critical1 == numberOfStates || critical2 == numberOfStates) {
- result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, emptySet));
- } else {
- storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1));
- storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2));
-
- std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
- auto myMap = createAssumptions(var1, var2, new Lattice(lattice), assumptions);
- result.insert(myMap.begin(), myMap.end());
-
- std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions2;
- myMap = createAssumptions(var2, var1, new Lattice(lattice), assumptions2);
- result.insert(myMap.begin(), myMap.end());
- if (result.size() == 0) {
- // No assumptions could be made, all not valid based on sampling, therefore returning original lattice
- result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, emptySet));
- } else {
- delete lattice;
- }
- }
- return result;
- }
-
- template<typename ValueType>
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::runRecursive(storm::analysis::Lattice* lattice, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
- // 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 (validate && assumptionChecker->validated(assumptions.back())) {
- assert (assumptionChecker->valid(assumptions.back()));
- assumptions.pop_back();
- }
-
- if (std::get<1>(criticalTriple) == numberOfStates) {
- result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
- } else {
- auto val1 = std::get<1>(criticalTriple);
- auto val2 = std::get<2>(criticalTriple);
- storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1));
- storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2));
- // TODO: check of in lattice de relatie niet al andersom bestaat
-
- assert(lattice->compare(val1, val2) == storm::analysis::Lattice::UNKNOWN);
- auto latticeCopy = new Lattice(lattice);
- std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
- assumptions);
- auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
- result.insert(myMap.begin(), myMap.end());
+ template <typename ValueType>
+ std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice) {
+ std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool> result;
+
+ 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(),
+ var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
+ storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
+ bool result1 = (validate && assumptionChecker->validateAssumption(assumption1, lattice) && assumptionChecker->valid(assumption1));
+ result[assumption1] = result1;
+
+ std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption2
+ = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
+ var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
+ storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
+ bool result2 = (validate && assumptionChecker->validateAssumption(assumption2, lattice) && assumptionChecker->valid(assumption2));
+ result[assumption2] = result2;
- myMap = createAssumptions(var2, var1, lattice, assumptions);
- result.insert(myMap.begin(), myMap.end());
- }
return result;
}
template <typename ValueType>
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
-
- std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption
- = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
- var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
- storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
- if (assumptionChecker->checkOnSamples(assumption)) {
- if (validate) {
- assumptionChecker->validateAssumption(assumption, lattice);
- if (!assumptionChecker->validated(assumption) || assumptionChecker->valid(assumption)) {
- assumptions.push_back(
- std::shared_ptr<storm::expressions::BinaryRelationExpression>(assumption));
- result = (runRecursive(lattice, assumptions));
- } else if (assumptionChecker->validated(assumption) && !assumptionChecker->valid(assumption)) {
- delete lattice;
- }
- } else {
- assumptions.push_back(std::shared_ptr<storm::expressions::BinaryRelationExpression>(assumption));
- result = (runRecursive(lattice, assumptions));
- }
-
-
- } else {
- delete lattice;
- }
-
- return result;
+ std::shared_ptr<storm::expressions::BinaryRelationExpression> AssumptionMaker<ValueType>::createEqualAssumption(uint_fast64_t val1, uint_fast64_t val2) {
+ storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1));
+ storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2));
+ return std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
+ var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
+ storm::expressions::BinaryRelationExpression::RelationType::Equal));
}
+
template class AssumptionMaker<storm::RationalFunction>;
}
}
diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h
index 1381d4ad0..190559a72 100644
--- a/src/storm-pars/analysis/AssumptionMaker.h
+++ b/src/storm-pars/analysis/AssumptionMaker.h
@@ -20,31 +20,18 @@ namespace storm {
public:
/*!
* Constructs AssumptionMaker based on the lattice extender, the assumption checker and number of states of the model.
- *
+ * TODO
* @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(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates, bool validate);
+ AssumptionMaker( 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.
- *
- * @param lattice The lattice on which assumptions are needed to allow further extension.
- * @param critical1 State number
- * @param critical2 State number
- * @return A mapping from pointers to different lattices and assumptions made to create the specific lattice.
- */
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> makeAssumptions(
- storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2);
-
- private:
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> runRecursive(storm::analysis::Lattice* lattice, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
+ std::map<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, storm::analysis::Lattice* lattice);
- std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
-
- storm::analysis::LatticeExtender<ValueType>* latticeExtender;
+ std::shared_ptr<storm::expressions::BinaryRelationExpression> createEqualAssumption(uint_fast64_t val1, uint_fast64_t val2);
+ private:
storm::analysis::AssumptionChecker<ValueType>* assumptionChecker;
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
@@ -58,3 +45,4 @@ namespace storm {
}
}
#endif //STORM_ASSUMPTIONMAKER_H
+
diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp
index dbf2c0964..e015358cb 100644
--- a/src/storm-pars/analysis/Lattice.cpp
+++ b/src/storm-pars/analysis/Lattice.cpp
@@ -114,6 +114,10 @@ namespace storm {
below->above.insert(above);
}
+ void Lattice::mergeNodes(storm::analysis::Lattice::Node *n1, storm::analysis::Lattice::Node * n2) {
+ // TODO
+ }
+
int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) {
return compare(getNode(state1), getNode(state2));
}
diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h
index 37a86ea5e..b92570e65 100644
--- a/src/storm-pars/analysis/Lattice.h
+++ b/src/storm-pars/analysis/Lattice.h
@@ -61,6 +61,8 @@ namespace storm {
*/
void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below);
+ void mergeNodes(storm::analysis::Lattice::Node *n1, storm::analysis::Lattice::Node * n2);
+
/*!
* Compares the level of the nodes of the states.
* Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice.
diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp
index acb2a8952..004418d57 100644
--- a/src/storm-pars/analysis/LatticeExtender.cpp
+++ b/src/storm-pars/analysis/LatticeExtender.cpp
@@ -111,9 +111,34 @@ namespace storm {
if (assumption != nullptr) {
storm::expressions::BinaryRelationExpression expr = *assumption;
STORM_LOG_THROW(expr.getRelationType() ==
- storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual,
- storm::exceptions::NotImplementedException, "Only GreaterOrEqual assumptions allowed");
- if (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()) {
+ storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual
+ || expr.getRelationType() ==
+ storm::expressions::BinaryRelationExpression::RelationType::Equal,
+ storm::exceptions::NotImplementedException, "Only GreaterOrEqual or Equal assumptions allowed");
+ if (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) {
+ assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable());
+ storm::expressions::Variable var1 = expr.getFirstOperand()->asVariableExpression().getVariable();
+ storm::expressions::Variable var2 = expr.getSecondOperand()->asVariableExpression().getVariable();
+ auto val1 = std::stoul(var1.getName(), nullptr, 0);
+ auto val2 = std::stoul(var2.getName(), nullptr, 0);
+ auto comp = lattice->compare(val1, val2);
+ assert (comp == storm::analysis::Lattice::UNKNOWN || comp == storm::analysis::Lattice::SAME);
+ storm::analysis::Lattice::Node *n1 = lattice->getNode(val1);
+ storm::analysis::Lattice::Node *n2 = lattice->getNode(val2);
+
+ if (n1 != nullptr && n2 != nullptr) {
+ lattice->mergeNodes(n1, n2);
+ } else if (n1 != nullptr) {
+ lattice->addToNode(val2, n1);
+ } else if (n2 != nullptr) {
+ lattice->addToNode(val1, n2);
+ } else {
+ lattice->add(val1);
+ lattice->addToNode(val2, lattice->getNode(val1));
+
+ }
+ } else {
+ assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable());
storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable();
storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable();
if (lattice->compare(std::stoul(largest.getName(), nullptr, 0),
@@ -127,7 +152,8 @@ namespace storm {
if (n1 != nullptr && n2 != nullptr) {
lattice->addRelationNodes(n1, n2);
} else if (n1 != nullptr) {
- lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), n1, lattice->getBottom());
+ lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), n1,
+ lattice->getBottom());
} else if (n2 != nullptr) {
lattice->addBetween(std::stoul(largest.getName(), nullptr, 0), lattice->getTop(), n2);
} else {
diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index b6178dfa5..56daab152 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/src/storm-pars/analysis/MonotonicityChecker.cpp
@@ -27,6 +27,10 @@ namespace storm {
this->formulas = formulas;
this->validate = validate;
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>();
+ if (model != nullptr) {
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
+ this->extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
+ }
}
template <typename ValueType>
@@ -124,7 +128,7 @@ namespace storm {
}
finalCheckWatch.stop();
- STORM_PRINT(std::endl << "Time for monotonicitycheck on lattice: " << finalCheckWatch << "." << std::endl << std::endl);
+ STORM_PRINT(std::endl << "Time for monotonicity check on lattice: " << finalCheckWatch << "." << std::endl << std::endl);
return result;
}
@@ -132,29 +136,114 @@ namespace storm {
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::createLattice() {
// Transform to Lattices
storm::utility::Stopwatch latticeWatch(true);
- std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
- storm::analysis::LatticeExtender<ValueType> *extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toLattice(formulas);
+
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
- if (model->isOfType(storm::models::ModelType::Dtmc)) {
- auto dtmc = model->as<storm::models::sparse::Dtmc<ValueType>>();
- auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmc, 3);
- auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates(), validate);
- result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple));
- } else if (model->isOfType(storm::models::ModelType::Dtmc)) {
- auto mdp = model->as<storm::models::sparse::Mdp<ValueType>>();
- auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], mdp, 3);
- auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates(), validate);
- result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple));
+
+ auto val1 = std::get<1>(criticalTuple);
+ auto val2 = std::get<2>(criticalTuple);
+ auto numberOfStates = model->getNumberOfStates();
+ std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
+
+ if (val1 == numberOfStates && val2 == numberOfStates) {
+ result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(std::get<0>(criticalTuple), assumptions));
+ } else if (val1 != numberOfStates && val2 != numberOfStates) {
+
+ storm::analysis::AssumptionChecker<ValueType> *assumptionChecker;
+ if (model->isOfType(storm::models::ModelType::Dtmc)) {
+ auto dtmc = model->as<storm::models::sparse::Dtmc<ValueType>>();
+ assumptionChecker = new storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmc, 3);
+ } else if (model->isOfType(storm::models::ModelType::Mdp)) {
+ auto mdp = model->as<storm::models::sparse::Mdp<ValueType>>();
+ assumptionChecker = new storm::analysis::AssumptionChecker<ValueType>(formulas[0], mdp, 3);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException,
+ "Unable to perform monotonicity analysis on the provided model type.");
+ }
+ auto assumptionMaker = new storm::analysis::AssumptionMaker<ValueType>(assumptionChecker, numberOfStates, validate);
+ result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, val1, val2, assumptions);
} else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
+ assert(false);
}
-
latticeWatch.stop();
STORM_PRINT(std::endl << "Total time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
return result;
}
+ template <typename ValueType>
+ std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
+ std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
+
+ auto numberOfStates = model->getNumberOfStates();
+ if (val1 == numberOfStates || val2 == numberOfStates) {
+ assert (val1 == val2);
+ result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
+ } else {
+ auto assumptionPair = assumptionMaker->createAndCheckAssumption(val1, val2, lattice);
+ assert (assumptionPair.size() == 2);
+ auto itr = assumptionPair.begin();
+ auto assumption1 = *itr;
+ ++itr;
+ auto assumption2 = *itr;
+
+ if (!assumption1.second && !assumption2.second) {
+ // TODO check op lattice of er nog monotonicity is
+ auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
+ auto latticeCopy = new storm::analysis::Lattice(lattice);
+ assumptions.push_back(assumption1.first);
+ assumptionsCopy.push_back(assumption2.first);
+
+ auto criticalTuple = extender->extendLattice(lattice, assumption1.first);
+ if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
+ auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions);
+ result.insert(map.begin(), map.end());
+ }
+
+
+ criticalTuple = extender->extendLattice(latticeCopy, assumption2.first);
+ if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
+ auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
+ std::get<1>(criticalTuple), std::get<2>(criticalTuple),
+ assumptionsCopy);
+ result.insert(map.begin(), map.end());
+ }
+ } else if (assumption1.second && assumption2.second) {
+ auto assumption = assumptionMaker->createEqualAssumption(val1, val2);
+ if (!validate) {
+ assumptions.push_back(assumption);
+ }
+ // if validate is true and both hold, then they must be valid, so no need to add to assumptions
+ auto criticalTuple = extender->extendLattice(lattice, assumption);
+ if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
+ result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions);
+ }
+ } else if (assumption1.second) {
+ if (!validate) {
+ assumptions.push_back(assumption1.first);
+ }
+ // if validate is true and both hold, then they must be valid, so no need to add to assumptions
+
+ auto criticalTuple = extender->extendLattice(lattice, assumption1.first);
+
+ if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
+ result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions);
+ }
+
+ } else {
+ assert (assumption2.second);
+ if (!validate) {
+ assumptions.push_back(assumption2.first);
+ }
+ // if validate is true and both hold, then they must be valid, so no need to add to assumptions
+ auto criticalTuple = extender->extendLattice(lattice, assumption2.first);
+ if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
+ result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions);
+ }
+ }
+ }
+ return result;
+ }
+
template <typename ValueType>
std::map<carl::Variable, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) {
storm::utility::Stopwatch analyseWatch(true);
@@ -220,6 +309,7 @@ namespace storm {
value->first &= derivative3.constantPart() >= 0;
value->second &= derivative3.constantPart() <= 0;
} else if (compare == storm::analysis::Lattice::SAME) {
+ // TODO: klopt dit
// Behaviour doesn't matter, as the states are at the same level.
} else {
// As the relation between the states is unknown, we can't claim anything about the monotonicity.
@@ -269,6 +359,73 @@ namespace storm {
return varsMonotone;
}
+ template <typename ValueType>
+ bool MonotonicityChecker<ValueType>::somewhereMonotonicity(storm::analysis::Lattice* lattice) {
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
+ auto matrix = sparseModel->getTransitionMatrix();
+
+ // TODO: tussenresultaten hergebruiken
+ std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
+
+ for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
+ // go over all rows
+ auto row = matrix.getRow(i);
+ auto first = (*row.begin());
+ if (first.getValue() != ValueType(1)) {
+ std::map<uint_fast64_t, ValueType> transitions;
+
+ for (auto itr = row.begin(); itr != row.end(); ++itr) {
+ transitions.insert(std::pair<uint_fast64_t, ValueType>((*itr).getColumn(), (*itr).getValue()));
+ }
+
+ auto val = first.getValue();
+ auto vars = val.gatherVariables();
+ for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
+ if (varsMonotone.find(*itr) == varsMonotone.end()) {
+ varsMonotone[*itr].first = true;
+ varsMonotone[*itr].second = true;
+ }
+ std::pair<bool, bool> *value = &varsMonotone.find(*itr)->second;
+ std::pair<bool, bool> old = *value;
+
+ for (auto itr2 = transitions.begin(); itr2 != transitions.end(); ++itr2) {
+ for (auto itr3 = transitions.begin(); itr3 != transitions.end(); ++itr3) {
+ auto derivative2 = (*itr2).second.derivative(*itr);
+ auto derivative3 = (*itr3).second.derivative(*itr);
+ STORM_LOG_THROW(derivative2.isConstant() && derivative3.isConstant(),
+ storm::exceptions::NotSupportedException,
+ "Expecting derivative to be constant");
+
+ auto compare = lattice->compare((*itr2).first, (*itr3).first);
+
+ if (compare == storm::analysis::Lattice::ABOVE) {
+ // As the first state (itr2) is above the second state (itr3) it is sufficient to look at the derivative of itr2.
+ value->first &= derivative2.constantPart() >= 0;
+ value->second &= derivative2.constantPart() <= 0;
+ } else if (compare == storm::analysis::Lattice::BELOW) {
+ // As the second state (itr3) is above the first state (itr2) it is sufficient to look at the derivative of itr3.
+ value->first &= derivative3.constantPart() >= 0;
+ value->second &= derivative3.constantPart() <= 0;
+ } else if (compare == storm::analysis::Lattice::SAME) {
+ // Behaviour doesn't matter, as the states are at the same level.
+ } else {
+ // As the relation between the states is unknown, we don't do anything
+ }
+ }
+ }
+ }
+ }
+ }
+
+ bool result = false;
+
+ for (auto itr = varsMonotone.begin(); !result && itr != varsMonotone.end(); ++itr) {
+ result = itr->second.first || itr->second.second;
+ }
+ return result;
+ }
+
+
template <typename ValueType>
std::map<carl::Variable, std::pair<bool, bool>> MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
storm::utility::Stopwatch samplesWatch(true);
diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h
index 44676aa2c..c1590dd09 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.h
+++ b/src/storm-pars/analysis/MonotonicityChecker.h
@@ -7,6 +7,8 @@
#include <map>
#include "Lattice.h"
+#include "LatticeExtender.h"
+#include "AssumptionMaker.h"
#include "storm/storage/expressions/BinaryRelationExpression.h"
#include "carl/core/Variable.h"
@@ -42,6 +44,14 @@ namespace storm {
*/
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> checkMonotonicity();
+ /*!
+ * TODO
+ * @param lattice
+ * @param matrix
+ * @return
+ */
+ bool somewhereMonotonicity(storm::analysis::Lattice* lattice) ;
+
private:
//TODO: variabele type
std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;
@@ -52,6 +62,8 @@ namespace storm {
std::map<carl::Variable, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples);
+ std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
+
std::shared_ptr<storm::models::ModelBase> model;
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
@@ -59,6 +71,8 @@ namespace storm {
bool validate;
std::map<carl::Variable, std::pair<bool, bool>> resultCheckOnSamples;
+
+ storm::analysis::LatticeExtender<ValueType> *extender;
};
}
}
diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp
index 722ca69bf..f233d2563 100644
--- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp
+++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp
@@ -53,12 +53,29 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) {
ASSERT_EQ(186, std::get<2>(criticalTuple));
auto assumptionChecker = storm::analysis::AssumptionChecker<storm::RationalFunction>(formulas[0], dtmc, 3);
- auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(extender, &assumptionChecker, dtmc->getNumberOfStates(), true);
- auto result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple));
- EXPECT_EQ(1, result.size());
- auto lattice = result.begin()->first;
- EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice->compare(186, 183));
- for (auto i = 0; i < dtmc->getNumberOfStates(); ++i) {
- EXPECT_TRUE(lattice->getAddedStates()[i]);
- }
+ auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true);
+ auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple));
+
+ auto itr = result.begin();
+
+ auto var1 = itr->first->getManager().getVariable("183");
+ auto var2 = itr->first->getManager().getVariable("186");
+
+ EXPECT_EQ(2, result.size());
+
+ EXPECT_EQ(false, itr->second);
+ EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
+ EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
+ EXPECT_EQ(var1, itr->first->getFirstOperand()->asVariableExpression().getVariable());
+ EXPECT_EQ(var2, itr->first->getSecondOperand()->asVariableExpression().getVariable());
+ EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, itr->first->getRelationType());
+
+ ++itr;
+ EXPECT_EQ(false, itr->second);
+ EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
+ EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
+ EXPECT_EQ(var2, itr->first->getFirstOperand()->asVariableExpression().getVariable());
+ EXPECT_EQ(var1, itr->first->getSecondOperand()->asVariableExpression().getVariable());
+ EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, itr->first->getRelationType());
+ // TODO: createEqualsAssumption checken
}
diff --git a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
index 7912bf7b0..af9f6628f 100644
--- a/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
+++ b/src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
@@ -140,8 +140,8 @@ TEST(MonotonicityCheckerTest, Brp_with_bisimulation) {
storm::analysis::MonotonicityChecker<storm::RationalFunction> monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(dtmc, formulas, true);
auto result = monotonicityChecker.checkMonotonicity();
- EXPECT_EQ(result.size(), 1);
- EXPECT_EQ(result.begin()->second.size(), 2);
+ EXPECT_EQ(1, result.size());
+ EXPECT_EQ(2, result.begin()->second.size());
auto monotone = result.begin()->second.begin();
EXPECT_EQ(monotone->second.first, true);
EXPECT_EQ(monotone->second.second, false);