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

Make sampling in monotonicity-analysis optional

tempestpy_adaptions
Jip Spel 6 years ago
parent
77a70179d3
commit
0d1ddb6232
6 changed files with 134 additions and 63 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. 3
      src/storm-pars-cli/storm-pars.cpp
  2. 92
      src/storm-pars/analysis/MonotonicityChecker.cpp
  3. 28
      src/storm-pars/analysis/MonotonicityChecker.h
  4. 14
      src/storm-pars/settings/modules/ParametricSettings.cpp
  5. 19
      src/storm-pars/settings/modules/ParametricSettings.h
  6. 41
      src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp

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

@ -727,7 +727,8 @@ namespace storm {
std::ofstream outfile;
outfile.open("results.txt", std::ios_base::app);
storm::utility::Stopwatch monotonicityWatch(true);
auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet());
auto numberOfSamples = parSettings.getNumberOfSamples();
auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet(), numberOfSamples);
monotonicityChecker.checkMonotonicity();
monotonicityWatch.stop();
STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl

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

@ -28,24 +28,28 @@ 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, uint_fast64_t numberOfSamples) {
outfile.open(filename, std::ios_base::app);
assert (model != nullptr);
this->model = model;
this->formulas = formulas;
this->validate = validate;
// sampling
if ( model->isOfType(storm::models::ModelType::Dtmc)) {
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>(checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples));
} else if (model->isOfType(storm::models::ModelType::Mdp)){
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>(checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples));
if (numberOfSamples > 0) {
// sampling
if (model->isOfType(storm::models::ModelType::Dtmc)) {
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples));
} else if (model->isOfType(storm::models::ModelType::Mdp)) {
this->resultCheckOnSamples = std::map<carl::Variable, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples));
}
checkSamples= true;
} else {
checkSamples= false;
}
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
this->extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
outfile << model->getNumberOfStates() << ", " << model->getNumberOfTransitions() << ", ";
outfile.close();
}
template <typename ValueType>
@ -96,10 +100,6 @@ namespace storm {
matrix);
auto assumptions = itr->second;
bool validSomewhere = false;
for (auto itr2 = varsMonotone.begin(); !validSomewhere && itr2 != varsMonotone.end(); ++itr2) {
validSomewhere = itr2->second.first || itr2->second.second;
}
if (assumptions.size() > 0) {
bool first = true;
for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) {
@ -115,12 +115,13 @@ namespace storm {
outfile << "No assumptions - ";
}
if (validSomewhere && varsMonotone.size() == 0) {
if (varsMonotone.size() == 0) {
outfile << "No params";
} else if (validSomewhere) {
} else {
auto itr2 = varsMonotone.begin();
while (itr2 != varsMonotone.end()) {
if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() &&
if (checkSamples &&
resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() &&
(!resultCheckOnSamples[itr2->first].first &&
!resultCheckOnSamples[itr2->first].second)) {
outfile << "X " << itr2->first;
@ -143,11 +144,6 @@ namespace storm {
result.insert(
std::pair<storm::analysis::Lattice *, std::map<carl::Variable, std::pair<bool, bool>>>(
lattice, varsMonotone));
} else {
result.insert(
std::pair<storm::analysis::Lattice *, std::map<carl::Variable, std::pair<bool, bool>>>(
lattice, varsMonotone));
outfile << "no monotonicity found";
}
++i;
outfile << ";";
@ -156,7 +152,6 @@ namespace storm {
outfile << ", ";
monotonicityCheckWatch.stop();
outfile << monotonicityCheckWatch << ", ";
outfile.close();
return result;
}
@ -195,9 +190,6 @@ namespace storm {
assert(false);
}
latticeWatch.stop();
outfile.open(filename, std::ios_base::app);
outfile << latticeWatch << ", ";
outfile.close();
return result;
}
@ -313,17 +305,28 @@ namespace storm {
}
// Copy info from checkOnSamples
for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
assert (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end());
if (varsMonotone.find(*itr) == varsMonotone.end()) {
varsMonotone[*itr].first = resultCheckOnSamples[*itr].first;
varsMonotone[*itr].second = resultCheckOnSamples[*itr].second;
} else {
varsMonotone[*itr].first &= resultCheckOnSamples[*itr].first;
varsMonotone[*itr].second &= resultCheckOnSamples[*itr].second;
if (checkSamples) {
for (auto var : vars) {
assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end());
if (varsMonotone.find(var) == varsMonotone.end()) {
varsMonotone[var].first = resultCheckOnSamples[var].first;
varsMonotone[var].second = resultCheckOnSamples[var].second;
} else {
varsMonotone[var].first &= resultCheckOnSamples[var].first;
varsMonotone[var].second &= resultCheckOnSamples[var].second;
}
}
} else {
for (auto var : vars) {
if (varsMonotone.find(var) == varsMonotone.end()) {
varsMonotone[var].first = true;
varsMonotone[var].second = true;
}
}
}
// Sort the states based on the lattice
auto sortedStates = lattice->sortStates(states);
if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) {
@ -426,14 +429,23 @@ namespace storm {
auto val = first.getValue();
auto vars = val.gatherVariables();
// Copy info from checkOnSamples
for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
assert (resultCheckOnSamples.find(*itr) != resultCheckOnSamples.end());
if (varsMonotone.find(*itr) == varsMonotone.end()) {
varsMonotone[*itr].first = resultCheckOnSamples[*itr].first;
varsMonotone[*itr].second = resultCheckOnSamples[*itr].second;
} else {
varsMonotone[*itr].first &= resultCheckOnSamples[*itr].first;
varsMonotone[*itr].second &= resultCheckOnSamples[*itr].second;
if (checkSamples) {
for (auto var : vars) {
assert (resultCheckOnSamples.find(var) != resultCheckOnSamples.end());
if (varsMonotone.find(var) == varsMonotone.end()) {
varsMonotone[var].first = resultCheckOnSamples[var].first;
varsMonotone[var].second = resultCheckOnSamples[var].second;
} else {
varsMonotone[var].first &= resultCheckOnSamples[var].first;
varsMonotone[var].second &= resultCheckOnSamples[var].second;
}
}
} else {
for (auto var : vars) {
if (varsMonotone.find(var) == varsMonotone.end()) {
varsMonotone[var].first = true;
varsMonotone[var].second = true;
}
}
}

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

@ -31,27 +31,23 @@ 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, uint_fast64_t numberOfSamples = 100);
/*!
* 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
* Constructor of MonotonicityChecker
* @param model the model considered
* @param formula the formula considered
* @param validate whether or not assumptions are to be validated
* @param numberOfSamples number of samples taken for monotonicity checking, default 0,
* if 0then no check on samples is executed
*/
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);
MonotonicityChecker(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, bool validate, uint_fast64_t numberOfSamples=0);
/*!
* TODO
* @return
* 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();
/*!
* TODO
* @param lattice
* @param matrix
* @return
* Checks if monotonicity can be found in this lattice. Unordered states are not checked
*/
bool somewhereMonotonicity(storm::analysis::Lattice* lattice) ;
@ -118,6 +114,8 @@ namespace storm {
}
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);
//TODO: variabele type
std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;
@ -139,13 +137,15 @@ namespace storm {
bool validate;
bool checkSamples;
std::map<carl::Variable, std::pair<bool, bool>> resultCheckOnSamples;
LatticeExtender<ValueType> *extender;
std::ofstream outfile;
std::string filename = "results.txt";
std::string filename = "monotonicity.txt";
};
}
}

14
src/storm-pars/settings/modules/ParametricSettings.cpp
View File

@ -22,8 +22,9 @@ namespace storm {
const std::string ParametricSettings::samplesGraphPreservingOptionName = "samples-graph-preserving";
const std::string ParametricSettings::sampleExactOptionName = "sample-exact";
const std::string ParametricSettings::monotonicityAnalysis = "monotonicity-analysis";
const std::string ParametricSettings::sccElimination = "elim-scc";
const std::string ParametricSettings::validateAssumptions = "validate-assumptions";
const std::string ParametricSettings::sccElimination = "mon-elim-scc";
const std::string ParametricSettings::validateAssumptions = "mon-validate-assumptions";
const std::string ParametricSettings::samplesMonotonicityAnalysis = "mon-samples";
ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.")
@ -36,8 +37,11 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, samplesGraphPreservingOptionName, false, "Sets whether it can be assumed that the samples are graph-preserving.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, sampleExactOptionName, false, "Sets whether to sample using exact arithmetic.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, monotonicityAnalysis, false, "Sets whether monotonicity analysis is done").build());
this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated").build());
this->addOption(storm::settings::OptionBuilder(moduleName, sccElimination, false, "Sets whether SCCs should be eliminated in the monotonicity analysis").build());
this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").build());
this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples")
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build());
}
bool ParametricSettings::exportResultToFile() const {
@ -83,6 +87,10 @@ namespace storm {
bool ParametricSettings::isValidateAssumptionsSet() const {
return this->getOption(validateAssumptions).getHasOptionBeenSet();
}
uint_fast64_t ParametricSettings::getNumberOfSamples() const {
return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger();
}
} // namespace modules
} // namespace settings
} // namespace storm

19
src/storm-pars/settings/modules/ParametricSettings.h
View File

@ -42,7 +42,7 @@ namespace storm {
*/
bool transformContinuousModel() const;
/*
/*!
* Retrieves whether instead of model checking, only the wellformedness constraints should be obtained.
*/
bool onlyObtainConstraints() const;
@ -64,12 +64,26 @@ namespace storm {
*/
bool isSampleExactSet() const;
/*!
* Retrieves whether monotonicity analysis should be applied.
*/
bool isMonotonicityAnalysisSet() const;
// TODO: maybe move to other place
/*!
* Retrieves whether SCCs in the monotonicity analysis should be eliminated.
*/
bool isSccEliminationSet() const;
/*!
* Retrieves whether assumptions in monotonicity analysis should be validated
*/
bool isValidateAssumptionsSet() const;
/*!
* Retrieves the number of samples used for sampling in the monotonicity analysis
*/
uint_fast64_t getNumberOfSamples() const;
const static std::string moduleName;
private:
@ -84,6 +98,7 @@ namespace storm {
const static std::string monotonicityAnalysis;
const static std::string sccElimination;
const static std::string validateAssumptions;
const static std::string samplesMonotonicityAnalysis;
};
} // namespace modules

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

@ -80,7 +80,7 @@ TEST(MonotonicityCheckerTest, Derivative_checker) {
EXPECT_FALSE(functionRes.second);
}
TEST(MonotonicityCheckerTest, Brp_with_bisimulation) {
TEST(MonotonicityCheckerTest, Brp_with_bisimulation_no_samples) {
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
@ -111,6 +111,41 @@ TEST(MonotonicityCheckerTest, Brp_with_bisimulation) {
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);
EXPECT_EQ(true, monotone->second.first);
EXPECT_EQ(false, monotone->second.second);
}
TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) {
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, 50);
auto result = monotonicityChecker.checkMonotonicity();
EXPECT_EQ(1, result.size());
EXPECT_EQ(2, result.begin()->second.size());
auto monotone = result.begin()->second.begin();
EXPECT_EQ(true, monotone->second.first);
EXPECT_EQ(false, monotone->second.second);
}
Write Preview
Loading…
Cancel
Save