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

Make variabletype depend on value type

tempestpy_adaptions
Jip Spel 6 years ago
parent
7f5416adb8
commit
8732a7f40d
2 changed files with 37 additions and 46 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. 60
      src/storm-pars/analysis/MonotonicityChecker.cpp
  2. 23
      src/storm-pars/analysis/MonotonicityChecker.h

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

@ -1,7 +1,3 @@
//
// Created by Jip Spel on 05.09.18.
//
#include "MonotonicityChecker.h" #include "MonotonicityChecker.h"
#include "storm-pars/analysis/AssumptionMaker.h" #include "storm-pars/analysis/AssumptionMaker.h"
#include "storm-pars/analysis/AssumptionChecker.h" #include "storm-pars/analysis/AssumptionChecker.h"
@ -36,10 +32,10 @@ namespace storm {
if (numberOfSamples > 0) { if (numberOfSamples > 0) {
// sampling // sampling
if (model->isOfType(storm::models::ModelType::Dtmc)) { if (model->isOfType(storm::models::ModelType::Dtmc)) {
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>(
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples)); checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples));
} else if (model->isOfType(storm::models::ModelType::Mdp)) { } else if (model->isOfType(storm::models::ModelType::Mdp)) {
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>(
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples)); checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples));
} }
@ -53,7 +49,7 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() {
std::map<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() {
auto map = createLattice(); auto map = createLattice();
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>(); std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
auto matrix = sparseModel->getTransitionMatrix(); auto matrix = sparseModel->getTransitionMatrix();
@ -61,9 +57,9 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
std::map<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
storm::utility::Stopwatch monotonicityCheckWatch(true); storm::utility::Stopwatch monotonicityCheckWatch(true);
std::map<storm::analysis::Lattice *, std::map<carl::Variable, std::pair<bool, bool>>> result;
std::map<storm::analysis::Lattice *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> result;
outfile.open(filename, std::ios_base::app); outfile.open(filename, std::ios_base::app);
@ -96,7 +92,7 @@ namespace storm {
auto addedStates = lattice->getAddedStates()->getNumberOfSetBits(); auto addedStates = lattice->getAddedStates()->getNumberOfSetBits();
assert (addedStates == lattice->getAddedStates()->size()); assert (addedStates == lattice->getAddedStates()->size());
std::map<carl::Variable, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, lattice,
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, lattice,
matrix); matrix);
auto assumptions = itr->second; auto assumptions = itr->second;
@ -142,7 +138,7 @@ namespace storm {
} }
} }
result.insert( result.insert(
std::pair<storm::analysis::Lattice *, std::map<carl::Variable, std::pair<bool, bool>>>(
std::pair<storm::analysis::Lattice *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>>(
lattice, varsMonotone)); lattice, varsMonotone));
} }
++i; ++i;
@ -267,7 +263,7 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
ValueType MonotonicityChecker<ValueType>::getDerivative(ValueType function, carl::Variable var) {
ValueType MonotonicityChecker<ValueType>::getDerivative(ValueType function, typename utility::parametric::VariableType<ValueType>::type var) {
if (function.isConstant()) { if (function.isConstant()) {
return storm::utility::zero<ValueType>(); return storm::utility::zero<ValueType>();
} }
@ -279,8 +275,8 @@ namespace storm {
} }
template <typename ValueType> 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) {
std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) {
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone;
// go over all rows, check for each row local monotonicity // go over all rows, check for each row local monotonicity
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
@ -292,7 +288,7 @@ namespace storm {
// Gather all states which are reached with a non constant probability // Gather all states which are reached with a non constant probability
auto states = new storm::storage::BitVector(matrix.getColumnCount()); auto states = new storm::storage::BitVector(matrix.getColumnCount());
std::set<carl::Variable> vars;
std::set<typename utility::parametric::VariableType<ValueType>::type> vars;
for (auto const& entry : row) { for (auto const& entry : row) {
if (!entry.getValue().isConstant()) { if (!entry.getValue().isConstant()) {
// only analyse take non constant transitions // only analyse take non constant transitions
@ -413,7 +409,7 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>(); std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
auto matrix = sparseModel->getTransitionMatrix(); auto matrix = sparseModel->getTransitionMatrix();
std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone;
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
// go over all rows // go over all rows
@ -502,14 +498,14 @@ namespace storm {
template <typename ValueType> 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) {
std::map<typename utility::parametric::VariableType<ValueType>::type, 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); storm::utility::Stopwatch samplesWatch(true);
std::map<carl::Variable, std::pair<bool, bool>> result;
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> result;
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model); 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<carl::Variable> variables = storm::models::sparse::getProbabilityParameters(*model);
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = storm::models::sparse::getProbabilityParameters(*model);
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
double previous = -1; double previous = -1;
@ -521,13 +517,13 @@ namespace storm {
for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) {
// Only change value for current variable // Only change value for current variable
if ((*itr) == (*itr2)) { if ((*itr) == (*itr2)) {
auto val = std::pair<carl::Variable, storm::RationalFunctionCoefficient>(
(*itr2), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1))))); boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1)))));
valuation.insert(val); valuation.insert(val);
} else { } else {
auto val = std::pair<carl::Variable, storm::RationalFunctionCoefficient>(
(*itr2), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1))))); boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1)))));
valuation.insert(val); valuation.insert(val);
} }
@ -565,7 +561,7 @@ namespace storm {
} }
previous = initial; previous = initial;
} }
result.insert(std::pair<carl::Variable, std::pair<bool, bool>>(*itr, std::pair<bool,bool>(monIncr, monDecr)));
result.insert(std::pair<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(*itr, std::pair<bool,bool>(monIncr, monDecr)));
} }
samplesWatch.stop(); samplesWatch.stop();
@ -574,14 +570,14 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
std::map<carl::Variable, std::pair<bool, bool>> MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples) {
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples) {
storm::utility::Stopwatch samplesWatch(true); storm::utility::Stopwatch samplesWatch(true);
std::map<carl::Variable, std::pair<bool, bool>> result;
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> result;
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Mdp<double>>(*model); auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Mdp<double>>(*model);
auto matrix = model->getTransitionMatrix(); auto matrix = model->getTransitionMatrix();
std::set<carl::Variable> variables = storm::models::sparse::getProbabilityParameters(*model);
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = storm::models::sparse::getProbabilityParameters(*model);
for (auto itr = variables.begin(); itr != variables.end(); ++itr) { for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
double previous = -1; double previous = -1;
@ -593,13 +589,13 @@ namespace storm {
for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) {
// Only change value for current variable // Only change value for current variable
if ((*itr) == (*itr2)) { if ((*itr) == (*itr2)) {
auto val = std::pair<carl::Variable, storm::RationalFunctionCoefficient>(
(*itr2), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1))))); boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1)))));
valuation.insert(val); valuation.insert(val);
} else { } else {
auto val = std::pair<carl::Variable, storm::RationalFunctionCoefficient>(
(*itr2), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1))))); boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1)))));
valuation.insert(val); valuation.insert(val);
} }
@ -635,7 +631,7 @@ namespace storm {
} }
previous = initial; previous = initial;
} }
result.insert(std::pair<carl::Variable, std::pair<bool, bool>>(*itr, std::pair<bool,bool>(monIncr, monDecr)));
result.insert(std::pair<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(*itr, std::pair<bool,bool>(monIncr, monDecr)));
} }
samplesWatch.stop(); samplesWatch.stop();

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

@ -1,7 +1,3 @@
//
// Created by Jip Spel on 03.09.18.
//
#ifndef STORM_MONOTONICITYCHECKER_H #ifndef STORM_MONOTONICITYCHECKER_H
#define STORM_MONOTONICITYCHECKER_H #define STORM_MONOTONICITYCHECKER_H
@ -14,7 +10,6 @@
#include "storm/storage/expressions/RationalFunctionToExpression.h" #include "storm/storage/expressions/RationalFunctionToExpression.h"
#include "storm/utility/constants.h" #include "storm/utility/constants.h"
#include "carl/core/Variable.h"
#include "storm/models/ModelBase.h" #include "storm/models/ModelBase.h"
#include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Mdp.h"
@ -44,7 +39,7 @@ namespace storm {
/*! /*!
* Checks for model and formula as provided in constructor for monotonicity * Checks for model and formula as provided in constructor for monotonicity
*/ */
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> checkMonotonicity();
std::map<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity();
/*! /*!
* Checks if monotonicity can be found in this lattice. Unordered states are not checked * Checks if monotonicity can be found in this lattice. Unordered states are not checked
@ -74,7 +69,7 @@ namespace storm {
storm::solver::Z3SmtSolver s(*manager); storm::solver::Z3SmtSolver s(*manager);
std::set<carl::Variable> variables = derivative.gatherVariables();
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = derivative.gatherVariables();
for (auto variable : variables) { for (auto variable : variables) {
@ -114,20 +109,20 @@ namespace storm {
} }
private: private:
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
std::map<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
//TODO: variabele type //TODO: variabele type
std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;
std::map<Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createLattice(); std::map<Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createLattice();
std::map<carl::Variable, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
std::map<carl::Variable, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples);
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> model, uint_fast64_t numberOfSamples);
std::unordered_map<ValueType, std::unordered_map<carl::Variable, ValueType>> derivatives;
std::unordered_map<ValueType, std::unordered_map<typename utility::parametric::VariableType<ValueType>::type, ValueType>> derivatives;
ValueType getDerivative(ValueType function, carl::Variable var);
ValueType getDerivative(ValueType function, typename utility::parametric::VariableType<ValueType>::type var);
std::map<Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendLatticeWithAssumptions(Lattice* lattice, AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions); std::map<Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendLatticeWithAssumptions(Lattice* lattice, AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
@ -139,7 +134,7 @@ namespace storm {
bool checkSamples; bool checkSamples;
std::map<carl::Variable, std::pair<bool, bool>> resultCheckOnSamples;
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> resultCheckOnSamples;
LatticeExtender<ValueType> *extender; LatticeExtender<ValueType> *extender;

Write Preview
Loading…
Cancel
Save