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

Add simple validation for assumptions

tempestpy_adaptions
Jip Spel 6 years ago
parent
f2c2da64fa
commit
e23a222605
10 changed files with 121 additions and 48 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/storm-pars-cli/storm-pars.cpp
  2. 60
      src/storm-pars/analysis/AssumptionChecker.cpp
  3. 12
      src/storm-pars/analysis/AssumptionChecker.h
  4. 33
      src/storm-pars/analysis/AssumptionMaker.cpp
  5. 6
      src/storm-pars/analysis/AssumptionMaker.h
  6. 2
      src/storm-pars/analysis/Lattice.cpp
  7. 31
      src/storm-pars/analysis/LatticeExtender.cpp
  8. 9
      src/storm-pars/analysis/LatticeExtender.h
  9. 11
      src/storm-pars/analysis/MonotonicityChecker.cpp
  10. 2
      src/storm-pars/analysis/MonotonicityChecker.h

3
src/storm-pars-cli/storm-pars.cpp
View File

@ -549,10 +549,9 @@ namespace storm {
auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmcModel, 3); auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmcModel, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates()); auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates());
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result = assumptionMaker.makeAssumptions(
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> result = assumptionMaker.makeAssumptions(
std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair)); std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));
latticeWatch.stop(); latticeWatch.stop();
STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);

60
src/storm-pars/analysis/AssumptionChecker.cpp
View File

@ -13,20 +13,23 @@
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/storage/expressions/SimpleValuation.h" #include "storm/storage/expressions/SimpleValuation.h"
#include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/VariableExpression.h"
namespace storm { namespace storm {
namespace analysis { namespace analysis {
template <typename ValueType> template <typename ValueType>
AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) { AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
this->formula = formula; this->formula = formula;
this->matrix = model->getTransitionMatrix();
// Create sample points // Create sample points
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model.get());
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model);
auto matrix = model->getTransitionMatrix(); auto matrix = model->getTransitionMatrix();
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model); std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model);
for (auto i = 0; i < numberOfSamples; ++i) { for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = storm::utility::parametric::Valuation<ValueType>(); auto valuation = storm::utility::parametric::Valuation<ValueType>();
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
// TODO: Type
auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 1))))); auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 1)))));
valuation.insert(val); valuation.insert(val);
} }
@ -73,6 +76,61 @@ namespace storm {
return result; return result;
} }
template <typename ValueType>
bool AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice) {
bool result = false;
std::set<storm::expressions::Variable> vars = std::set<storm::expressions::Variable>({});
assumption->gatherVariables(vars);
STORM_LOG_THROW(assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, storm::exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported");
auto val1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName());
auto val2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName());
auto row1 = matrix.getRow(val1);
auto row2 = matrix.getRow(val2);
if (row1.getNumberOfEntries() != 2 && row2.getNumberOfEntries() != 2) {
assert (false);
}
auto succ11 = row1.begin();
auto succ12 = (++row1.begin());
auto succ21 = row2.begin();
auto succ22 = (++row2.begin());
if (succ12->getColumn() == succ21->getColumn() && succ11->getColumn() == succ22->getColumn()) {
auto temp = succ12;
succ12 = succ11;
succ11 = temp;
}
if (succ11->getColumn() == succ21->getColumn() && succ12->getColumn() == succ22->getColumn()) {
ValueType prob;
auto comp = lattice->compare(succ11->getColumn(), succ12->getColumn());
if (comp == storm::analysis::Lattice::ABOVE) {
prob = succ11->getValue() - succ21->getValue();
} else if (comp == storm::analysis::Lattice::BELOW) {
prob = succ12->getValue() - succ22->getValue();
}
auto vars = prob.gatherVariables();
// TODO: Type
std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> substitutions;
for (auto var:vars) {
auto derivative = prob.derivative(var);
assert(derivative.isConstant());
if (derivative.constantPart() >=0) {
substitutions[var] = 0;
} else if(derivative.constantPart() <= 0) {
substitutions[var] = 1;
}
}
result = prob.evaluate(substitutions) >= 0;
}
if (!result) {
STORM_PRINT("Could not validate: " << *assumption << std::endl);
}
return result;
}
template class AssumptionChecker<storm::RationalFunction>; template class AssumptionChecker<storm::RationalFunction>;
} }
} }

12
src/storm-pars/analysis/AssumptionChecker.h
View File

@ -9,6 +9,7 @@
#include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Dtmc.h"
#include "storm/environment/Environment.h" #include "storm/environment/Environment.h"
#include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm/storage/expressions/BinaryRelationExpression.h"
#include "Lattice.h"
namespace storm { namespace storm {
namespace analysis { namespace analysis {
@ -32,9 +33,20 @@ namespace storm {
*/ */
bool checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption); bool checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
/*!
* Checks if an assumption can be validated based on the lattice and underlying transition matrix.
*
* @param assumption The assumption to validate.
* @param lattice The lattice.
* @return true if the assumption is validated and holds, false otherwise
*/
bool validateAssumption(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption, storm::analysis::Lattice* lattice);
private: private:
std::shared_ptr<storm::logic::Formula const> formula; std::shared_ptr<storm::logic::Formula const> formula;
storm::storage::SparseMatrix<ValueType> matrix;
std::vector<std::vector<double>> results; std::vector<std::vector<double>> results;
}; };

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

@ -18,24 +18,24 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>>
AssumptionMaker<ValueType>::makeAssumptions(storm::analysis::Lattice *lattice, uint_fast64_t critical1, AssumptionMaker<ValueType>::makeAssumptions(storm::analysis::Lattice *lattice, uint_fast64_t critical1,
uint_fast64_t critical2) { uint_fast64_t critical2) {
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> result;
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> emptySet;
std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>> emptySet;
if (critical1 == numberOfStates || critical2 == numberOfStates) { if (critical1 == numberOfStates || critical2 == numberOfStates) {
result.insert(std::pair<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, emptySet));
result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>>(lattice, emptySet));
} else { } else {
storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1)); storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1));
storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2));
auto latticeCopy = new Lattice(lattice); auto latticeCopy = new Lattice(lattice);
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>> assumptions;
auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions); auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions);
result.insert(myMap.begin(), myMap.end()); result.insert(myMap.begin(), myMap.end());
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions2;
std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>> assumptions2;
myMap = createAssumptions(var2, var1, lattice, assumptions2); myMap = createAssumptions(var2, var1, lattice, assumptions2);
result.insert(myMap.begin(), myMap.end()); result.insert(myMap.begin(), myMap.end());
} }
@ -43,12 +43,17 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::runRecursive(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions);
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> AssumptionMaker<ValueType>::runRecursive(storm::analysis::Lattice* lattice, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>,bool>> assumptions) {
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>,bool>>> 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().first);
if (assumptions.back().second) {
assumptions.pop_back();
}
if (std::get<1>(criticalTriple) == numberOfStates) { if (std::get<1>(criticalTriple) == numberOfStates) {
result.insert(std::pair<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>,bool>>>(lattice, assumptions));
} else { } else {
auto val1 = std::get<1>(criticalTriple); auto val1 = std::get<1>(criticalTriple);
auto val2 = std::get<2>(criticalTriple); auto val2 = std::get<2>(criticalTriple);
@ -56,7 +61,7 @@ namespace storm {
storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2));
auto latticeCopy = new Lattice(lattice); auto latticeCopy = new Lattice(lattice);
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptionsCopy = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(
std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>> assumptionsCopy = std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>(
assumptions); assumptions);
auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy); auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy);
result.insert(myMap.begin(), myMap.end()); result.insert(myMap.begin(), myMap.end());
@ -68,15 +73,15 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> AssumptionMaker<ValueType>::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>> assumptions) {
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> result;
std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption
= std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
if (assumptionChecker->checkOnSamples(assumption)) { if (assumptionChecker->checkOnSamples(assumption)) {
assumptions.insert(assumption);
assumptions.push_back(std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>(assumption, assumptionChecker->validateAssumption(assumption, lattice)));
result = (runRecursive(lattice, assumptions)); result = (runRecursive(lattice, assumptions));
} else { } else {
delete lattice; delete lattice;

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

@ -35,13 +35,13 @@ namespace storm {
* @param critical2 State number * @param critical2 State number
* @return A mapping from pointers to different lattices and assumptions made to create the specific lattice. * @return A mapping from pointers to different lattices and assumptions made to create the specific lattice.
*/ */
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> makeAssumptions(
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> makeAssumptions(
storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2); storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2);
private: private:
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> runRecursive(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> runRecursive(storm::analysis::Lattice* lattice, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>> assumptions);
std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>> assumptions);
storm::analysis::LatticeExtender<ValueType>* latticeExtender; storm::analysis::LatticeExtender<ValueType>* latticeExtender;

2
src/storm-pars/analysis/Lattice.cpp
View File

@ -121,7 +121,7 @@ namespace storm {
if (node1 == node2) { if (node1 == node2) {
return SAME; return SAME;
} }
// TODO: Uberhaupt niet mogelijk?
bool isAbove = above(node1, node2, new std::set<Node*>({})); bool isAbove = above(node1, node2, new std::set<Node*>({}));
bool isBelow = above(node2, node1, new std::set<Node*>({})); bool isBelow = above(node2, node1, new std::set<Node*>({}));
if (isAbove && isBelow) { if (isAbove && isBelow) {

31
src/storm-pars/analysis/LatticeExtender.cpp
View File

@ -75,24 +75,24 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice) {
std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
return this->extendLattice(lattice, assumptions);
}
template <typename ValueType>
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
auto numberOfStates = this->model->getNumberOfStates(); auto numberOfStates = this->model->getNumberOfStates();
// First handle assumptions
for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
storm::expressions::BinaryRelationExpression expr = *(*itr);
STORM_LOG_THROW(expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, storm::exceptions::NotImplementedException, "Only greater assumptions allowed");
// First handle assumption
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()) { if (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()) {
storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable(); storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable();
storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable();
if (lattice->compare(std::stoul(largest.getName(), nullptr, 0), std::stoul(smallest.getName(), nullptr, 0)) != storm::analysis::Lattice::ABOVE) {
storm::analysis::Lattice::Node* n1 = lattice->getNode(std::stoul(largest.getName(), nullptr, 0));
storm::analysis::Lattice::Node* n2 = lattice->getNode(std::stoul(smallest.getName(), nullptr, 0));
if (lattice->compare(std::stoul(largest.getName(), nullptr, 0),
std::stoul(smallest.getName(), nullptr, 0)) !=
storm::analysis::Lattice::ABOVE) {
storm::analysis::Lattice::Node *n1 = lattice->getNode(
std::stoul(largest.getName(), nullptr, 0));
storm::analysis::Lattice::Node *n2 = lattice->getNode(
std::stoul(smallest.getName(), nullptr, 0));
if (n1 != nullptr && n2 != nullptr) { if (n1 != nullptr && n2 != nullptr) {
lattice->addRelationNodes(n1, n2); lattice->addRelationNodes(n1, n2);
@ -102,7 +102,8 @@ namespace storm {
lattice->addBetween(std::stoul(largest.getName(), nullptr, 0), lattice->getTop(), n2); lattice->addBetween(std::stoul(largest.getName(), nullptr, 0), lattice->getTop(), n2);
} else { } else {
lattice->add(std::stoul(largest.getName(), nullptr, 0)); lattice->add(std::stoul(largest.getName(), nullptr, 0));
lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), lattice->getNode(std::stoul(largest.getName(), nullptr, 0)),
lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0),
lattice->getNode(std::stoul(largest.getName(), nullptr, 0)),
lattice->getBottom()); lattice->getBottom());
} }
} }

9
src/storm-pars/analysis/LatticeExtender.h
View File

@ -39,23 +39,20 @@ namespace storm {
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas); std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
/*! /*!
* Extends the lattice based on the given assumptions.
* Extends the lattice based on the given assumption.
* *
* @param lattice The lattice. * @param lattice The lattice.
* @param assumptions The assumptions on states.
* @param assumption The assumption on states.
* @return A triple with a pointer to the lattice and two states of which the current place in the lattice * @return A triple with a pointer to the lattice and two states of which the current place in the lattice
* is unknown but needed. When the states have as number the number of states, no states are * is unknown but needed. When the states have as number the number of states, no states are
* unplaced but needed. * unplaced but needed.
*/ */
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption = nullptr);
private: private:
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::map<uint_fast64_t, storm::storage::BitVector> stateMap; std::map<uint_fast64_t, storm::storage::BitVector> stateMap;
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice);
}; };
} }
} }

11
src/storm-pars/analysis/MonotonicityChecker.cpp
View File

@ -9,7 +9,7 @@
namespace storm { namespace storm {
namespace analysis { namespace analysis {
template <typename ValueType> template <typename ValueType>
void MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
void MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
auto i = 0; auto i = 0;
for (auto itr = map.begin(); itr != map.end(); ++itr) { for (auto itr = map.begin(); itr != map.end(); ++itr) {
auto lattice = itr->first; auto lattice = itr->first;
@ -23,17 +23,18 @@ namespace storm {
if (assumptions.size() > 0) { if (assumptions.size() > 0) {
STORM_PRINT("Given assumptions: " << std::endl); STORM_PRINT("Given assumptions: " << std::endl);
bool first = true; bool first = true;
for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) {
if (!first) { if (!first) {
STORM_PRINT(" ^ "); STORM_PRINT(" ^ ");
} else { } else {
STORM_PRINT(" "); STORM_PRINT(" ");
first = false;
} }
first = false;
std::shared_ptr<storm::expressions::BinaryRelationExpression> expression = *itr;
std::shared_ptr<storm::expressions::BinaryRelationExpression> expression = itr2->first;
auto var1 = expression->getFirstOperand(); auto var1 = expression->getFirstOperand();
auto var2 = expression->getSecondOperand(); auto var2 = expression->getSecondOperand();
STORM_PRINT("(" << var1->getIdentifier() << " > " << var2->getIdentifier() << ")");
STORM_PRINT(*expression);
} }
STORM_PRINT(std::endl); STORM_PRINT(std::endl);
} }

2
src/storm-pars/analysis/MonotonicityChecker.h
View File

@ -24,7 +24,7 @@ namespace storm {
* @param map The map with lattices and the assumptions made to create the lattices. * @param map The map with lattices and the assumptions made to create the lattices.
* @param matrix The transition matrix. * @param matrix The transition matrix.
*/ */
void checkMonotonicity(std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
void checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::pair<std::shared_ptr<storm::expressions::BinaryRelationExpression>, bool>>> map, storm::storage::SparseMatrix<ValueType> matrix);
private: private:
std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ; std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;

Write Preview
Loading…
Cancel
Save