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

First check on samples for monotonicity

tempestpy_adaptions
Jip Spel 6 years ago
parent
8c7808b0df
commit
cca2ad474e
4 changed files with 210 additions and 42 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. 40
      src/storm-pars-cli/storm-pars.cpp
  2. 120
      src/storm-pars/analysis/MonotonicityChecker.cpp
  3. 28
      src/storm-pars/analysis/MonotonicityChecker.h
  4. 64
      src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp

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

@ -1,9 +1,5 @@
#include "storm-pars/analysis/AssumptionMaker.h"
#include "storm-pars/analysis/Lattice.h"
#include "storm-pars/analysis/LatticeExtender.h"
#include "storm-pars/analysis/MonotonicityChecker.h"
#include "storm-cli-utilities/cli.h"
@ -529,40 +525,12 @@ namespace storm {
std::cout << "Hello, Jip2" << std::endl;
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
// Transform to Lattices
storm::utility::Stopwatch latticeWatch(true);
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 dtmcModel = model->as<storm::models::sparse::Dtmc<ValueType>>();
auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmcModel, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates(), parSettings.isValidateAssumptionsSet());
result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple));
} else if (model->isOfType(storm::models::ModelType::Dtmc)) {
auto mdpModel = model->as<storm::models::sparse::Mdp<ValueType>>();
auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], mdpModel, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates(), parSettings.isValidateAssumptionsSet());
result = assumptionMaker.makeAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
}
latticeWatch.stop();
STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
// Monotonicity?
// Monotonicity
storm::utility::Stopwatch monotonicityWatch(true);
if (result.size() > 0) {
auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>();
monotonicityChecker.checkMonotonicity(result, sparseModel->getTransitionMatrix());
monotonicityWatch.stop();
} else {
STORM_PRINT(std::endl << "Could not find monotonicity, no lattices created" << std::endl);
}
auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet());
monotonicityChecker.checkMonotonicity();
monotonicityWatch.stop();
STORM_PRINT(std::endl << "Time for monotonicity: " << monotonicityWatch << "." << std::endl
<< std::endl);

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

@ -3,11 +3,50 @@
//
#include "MonotonicityChecker.h"
#include "storm-pars/analysis/AssumptionMaker.h"
#include "storm-pars/analysis/AssumptionChecker.h"
#include "storm-pars/analysis/Lattice.h"
#include "storm-pars/analysis/LatticeExtender.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/utility/Stopwatch.h"
#include "storm/models/ModelType.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
namespace storm {
namespace analysis {
template <typename ValueType>
MonotonicityChecker<ValueType>::MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate) {
this->model = model;
this->formulas = formulas;
this->validate = validate;
}
template <typename ValueType>
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() {
bool maybeMonotone = true;
if (model->isOfType(storm::models::ModelType::Dtmc)) {
auto dtmcModel = model->as<storm::models::sparse::Dtmc<ValueType>>();
maybeMonotone = checkOnSamples(dtmcModel,3);
} //TODO mdp
if (maybeMonotone) {
auto map = createLattice();
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
auto matrix = sparseModel->getTransitionMatrix();
return checkMonotonicity(map, matrix);
} else {
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> result;
std::cout << "Not monotone" << std::endl;
return result;
}
}
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) {
auto i = 0;
@ -65,6 +104,33 @@ namespace storm {
return result;
}
template <typename ValueType>
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 dtmcModel = model->as<storm::models::sparse::Dtmc<ValueType>>();
auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmcModel, 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 mdpModel = model->as<storm::models::sparse::Mdp<ValueType>>();
auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], mdpModel, 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 {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
}
latticeWatch.stop();
STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
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) {
std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
@ -163,6 +229,58 @@ namespace storm {
return varsMonotone;
}
template <typename ValueType>
bool MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
bool monDecr = true;
bool monIncr = true;
auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model);
auto matrix = model->getTransitionMatrix();
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*model);
double previous = -1;
for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = storm::utility::parametric::Valuation<ValueType>();
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)))));
valuation.insert(val);
}
storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);
auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>(sampleModel);
std::unique_ptr<storm::modelchecker::CheckResult> checkResult;
auto formula = formulas[0];
if (formula->isProbabilityOperatorFormula() &&
formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
const storm::modelchecker::CheckTask<storm::logic::UntilFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::UntilFormula, double>(
(*formula).asProbabilityOperatorFormula().getSubformula().asUntilFormula());
checkResult = checker.computeUntilProbabilities(Environment(), checkTask);
} else if (formula->isProbabilityOperatorFormula() &&
formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()) {
const storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double> checkTask = storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, double>(
(*formula).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula());
checkResult = checker.computeReachabilityProbabilities(Environment(), checkTask);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
"Expecting until or eventually formula");
}
auto quantitativeResult = checkResult->asExplicitQuantitativeCheckResult<double>();
std::vector<double> values = quantitativeResult.getValueVector();
auto initialStates = model->getInitialStates();
double initial = 0;
for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) {
initial += values[i];
}
if (previous != -1) {
monDecr &= previous >= initial;
monIncr &= previous <= initial;
}
previous = initial;
}
bool result = monDecr || monIncr;
return result;
}
template class MonotonicityChecker<storm::RationalFunction>;
}
}

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

@ -8,8 +8,13 @@
#include <map>
#include "Lattice.h"
#include "storm/storage/expressions/BinaryRelationExpression.h"
#include "storm/storage/SparseMatrix.h"
#include "carl/core/Variable.h"
#include "storm/models/ModelBase.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/logic/Formula.h"
#include "storm/storage/SparseMatrix.h"
namespace storm {
namespace analysis {
@ -18,17 +23,38 @@ namespace storm {
class MonotonicityChecker {
public:
MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate);
/*!
* Checks for all lattices in the map if they are monotone increasing or monotone decreasing.
*
* @param map The map with lattices and the assumptions made to create the lattices.
* @param matrix The transition matrix.
* @return TODO
*/
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);
/*!
* TODO
* @param model
* @param formulas
* @param validate
* @return
*/
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> checkMonotonicity();
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) ;
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createLattice();
bool checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
std::shared_ptr<storm::models::ModelBase> model;
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
bool validate;
};
}
}

64
src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
View File

@ -10,8 +10,27 @@
#include "storm/storage/SparseMatrix.h"
#include "storm/adapters/RationalFunctionAdapter.h"
TEST(MonotonicityCheckerTest, Monotone) {
auto checker = storm::analysis::MonotonicityChecker<storm::RationalFunction>();
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm-parsers/parser/AutoParser.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/api/builder.h"
#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
#include "storm-pars/api/storm-pars.h"
#include "storm/api/storm.h"
#include "storm-parsers/api/storm-parsers.h"
TEST(MonotonicityCheckerTest, Monotone_no_model) {
std::shared_ptr<storm::models::ModelBase> model;
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
auto checker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(model, formulas, false);
// Build lattice
auto numberOfStates = 4;
auto above = storm::storage::BitVector(numberOfStates);
@ -53,8 +72,10 @@ TEST(MonotonicityCheckerTest, Monotone) {
EXPECT_TRUE(entry2->second.second);
}
TEST(MonotonicityCheckerTest, NotMonotone) {
auto checker = storm::analysis::MonotonicityChecker<storm::RationalFunction>();
TEST(MonotonicityCheckerTest, Not_monotone_no_model) {
std::shared_ptr<storm::models::ModelBase> model;
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
auto checker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(model, formulas, false);
// Build lattice
auto numberOfStates = 4;
auto above = storm::storage::BitVector(numberOfStates);
@ -89,4 +110,39 @@ TEST(MonotonicityCheckerTest, NotMonotone) {
ASSERT_EQ("p", entry1->first.name());
EXPECT_FALSE(entry1->second.first);
EXPECT_FALSE(entry1->second.second);
}
TEST(MonotonicityCheckerTest, Brp_with_bisimulation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P=? [F s=4 & i=N ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
model = simplifier.getSimplifiedModel();
// Apply bisimulation
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
bisimType = storm::storage::BisimulationType::Weak;
}
dtmc = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 99ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull);
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);
auto monotone = result.begin()->second.begin();
EXPECT_EQ(monotone->second.first, true);
EXPECT_EQ(monotone->second.second, false);
}
Write Preview
Loading…
Cancel
Save