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

Merge branch 'master' of https://sselab.de/lab9/private/git/storm 

Former-commit-id: cfcfbd77f8
main
dehnert 10 years ago
parent
b2d8cae9ce 1250b842b1
commit
7ac6dd94ab
5 changed files with 348 additions and 314 deletions
Unified View
  1. 19
      src/cli/cli.cpp
  2. 6
      src/parser/FormulaParser.cpp
  3. 6
      src/parser/FormulaParser.h
  4. 41
      src/utility/storm.cpp
  5. 556
      src/utility/storm.h

19
src/cli/cli.cpp
View File

@ -214,27 +214,20 @@ namespace storm {
boost::optional<storm::prism::Program> program; boost::optional<storm::prism::Program> program;
if (settings.isSymbolicSet()) { if (settings.isSymbolicSet()) {
std::string const& programFile = settings.getSymbolicModelFilename(); std::string const& programFile = settings.getSymbolicModelFilename();
program = storm::parser::PrismParser::parse(programFile).simplify().simplify(); program = storm::parseProgram(programFile);
program->checkValidity();
} }
// Then proceed to parsing the property (if given), since the model we are building may depend on the property. // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
std::vector<std::shared_ptr<storm::logic::Formula>> formulas; std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
if (settings.isPropertySet()) { if (settings.isPropertySet()) {
storm::parser::FormulaParser formulaParser; std::string properties = settings.getProperty();
if (program) {
formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer());
}
// If the given property looks like a file (containing a dot and there exists a file with that name), if(program) {
// we try to parse it as a file, otherwise we assume it's a property. formulas = storm::parseFormulasForProgram(properties, program.get());
std::string property = settings.getProperty();
if (property.find(".") != std::string::npos && std::ifstream(property).good()) {
formulas = formulaParser.parseFromFile(settings.getProperty());
} else { } else {
formulas = formulaParser.parseFromString(settings.getProperty()); formulas = storm::parseFormulasForExplicit(properties);
} }
} }
if (settings.isSymbolicSet()) { if (settings.isSymbolicSet()) {

6
src/parser/FormulaParser.cpp
View File

@ -184,13 +184,13 @@ namespace storm {
return *this; return *this;
} }
std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) { std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const {
std::vector<std::shared_ptr<storm::logic::Formula>> formulas = parseFromString(formulaString); std::vector<std::shared_ptr<storm::logic::Formula>> formulas = parseFromString(formulaString);
STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead."); STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead.");
return formulas.front(); return formulas.front();
} }
std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) { std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) const {
// Open file and initialize result. // Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in); std::ifstream inputFileStream(filename, std::ios::in);
STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
@ -212,7 +212,7 @@ namespace storm {
return formulas; return formulas;
} }
std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) { std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) const {
PositionIteratorType first(formulaString.begin()); PositionIteratorType first(formulaString.begin());
PositionIteratorType iter = first; PositionIteratorType iter = first;
PositionIteratorType last(formulaString.end()); PositionIteratorType last(formulaString.end());

6
src/parser/FormulaParser.h
View File

@ -28,7 +28,7 @@ namespace storm {
* @param formulaString The formula as a string. * @param formulaString The formula as a string.
* @return The resulting formula. * @return The resulting formula.
*/ */
std::shared_ptr<storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString); std::shared_ptr<storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString) const;
/*! /*!
* Parses the formula given by the provided string. * Parses the formula given by the provided string.
@ -36,7 +36,7 @@ namespace storm {
* @param formulaString The formula as a string. * @param formulaString The formula as a string.
* @return The contained formulas. * @return The contained formulas.
*/ */
std::vector<std::shared_ptr<storm::logic::Formula>> parseFromString(std::string const& formulaString); std::vector<std::shared_ptr<storm::logic::Formula>> parseFromString(std::string const& formulaString) const;
/*! /*!
* Parses the formulas in the given file. * Parses the formulas in the given file.
@ -44,7 +44,7 @@ namespace storm {
* @param filename The name of the file to parse. * @param filename The name of the file to parse.
* @return The contained formulas. * @return The contained formulas.
*/ */
std::vector<std::shared_ptr<storm::logic::Formula>> parseFromFile(std::string const& filename); std::vector<std::shared_ptr<storm::logic::Formula>> parseFromFile(std::string const& filename) const;
/*! /*!
* Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used

41
src/utility/storm.cpp
View File

@ -0,0 +1,41 @@
#include "storm.h"
// Headers related to parsing.
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
namespace storm {
storm::prism::Program parseProgram(std::string const& path) {
storm::prism::Program program= storm::parser::PrismParser::parse(path).simplify().simplify();
program.checkValidity();
return program;
}
/**
* Helper
* @param FormulaParser
* @return The formulas.
*/
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) {
// If the given property looks like a file (containing a dot and there exists a file with that name),
// we try to parse it as a file, otherwise we assume it's a property.
if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) {
return formulaParser.parseFromFile(inputString);
} else {
return formulaParser.parseFromString(inputString);
}
}
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString) {
storm::parser::FormulaParser formulaParser;
return parseFormulas(formulaParser, inputString);
}
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) {
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
return parseFormulas(formulaParser, inputString);
}
}

556
src/utility/storm.h
View File

@ -22,10 +22,6 @@
#include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/BisimulationSettings.h"
#include "src/settings/modules/ParametricSettings.h" #include "src/settings/modules/ParametricSettings.h"
// Headers related to parsing.
#include "src/parser/AutoParser.h"
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
// Formula headers. // Formula headers.
#include "src/logic/Formulas.h" #include "src/logic/Formulas.h"
@ -40,6 +36,8 @@
#include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h" #include "src/storage/dd/CuddBdd.h"
#include "src/parser/AutoParser.h"
// Headers of builders. // Headers of builders.
#include "src/builder/ExplicitPrismModelBuilder.h" #include "src/builder/ExplicitPrismModelBuilder.h"
#include "src/builder/DdPrismModelBuilder.h" #include "src/builder/DdPrismModelBuilder.h"
@ -73,327 +71,329 @@
namespace storm { namespace storm {
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& choiceLabelingFile = boost::optional<std::string>()) {
return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
}
template<typename ValueType> storm::prism::Program parseProgram(std::string const& path);
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& choiceLabelingFile = boost::optional<std::string>()) { std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
}
template<typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<storm::models::ModelBase> result(nullptr);
storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
// Get the string that assigns values to the unknown currently undefined constants in the model. template<typename ValueType>
std::string constants = settings.getConstantDefinitionString(); std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<storm::models::ModelBase> result(nullptr);
// Customize and perform model-building. storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) {
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(formulas);
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
// Generate command labels if we are going to build a counterexample later. // Get the string that assigns values to the unknown currently undefined constants in the model.
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { std::string constants = settings.getConstantDefinitionString();
options.buildCommandLabels = true;
}
result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(formulas);
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
result = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options); // Customize and perform model-building.
} if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) {
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(formulas);
options.addConstantDefinitionsFromString(program, constants);
// Then, build the model from the symbolic description. // Generate command labels if we are going to build a counterexample later.
return result; if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
options.buildCommandLabels = true;
} }
template<typename ValueType> result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
if (storm::settings::generalSettings().isBisimulationSet()) { typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(formulas);
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>(); options.addConstantDefinitionsFromString(program, constants);
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs."); result = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(); }
// Then, build the model from the symbolic description.
dtmc->reduceToStateBasedRewards(); return result;
}
std::cout << "Performing bisimulation minimization... "; template<typename ValueType>
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options; std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
if (!formulas.empty()) { if (storm::settings::generalSettings().isBisimulationSet()) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*sparseModel, formulas); STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
} std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
options.weak = true; std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>();
options.bounded = false; dtmc->reduceToStateBasedRewards();
} std::cout << "Performing bisimulation minimization... ";
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options;
storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options); if (!formulas.empty()) {
model = bisimulationDecomposition.getQuotient(); options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*sparseModel, formulas);
std::cout << "done." << std::endl << std::endl; }
} if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
return model; options.weak = true;
options.bounded = false;
} }
template<typename ValueType> storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) { model = bisimulationDecomposition.getQuotient();
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { std::cout << "done." << std::endl << std::endl;
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); }
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models."); return model;
}
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>(); template<typename ValueType>
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
// Determine whether we are required to use the MILP-version or the SAT-version. std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
if (useMILP) { // Determine whether we are required to use the MILP-version or the SAT-version.
storm::counterexamples::MILPMinimalLabelSetGenerator<ValueType>::computeCounterexample(program, *mdp, formula); bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
} else {
storm::counterexamples::SMTMinimalCommandSetGenerator<ValueType>::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula);
}
} else { if (useMILP) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected."); storm::counterexamples::MILPMinimalLabelSetGenerator<ValueType>::computeCounterexample(program, *mdp, formula);
} } else {
storm::counterexamples::SMTMinimalCommandSetGenerator<ValueType>::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula);
} }
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected.");
}
}
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<> template<>
inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) { inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
} }
#endif #endif
template<typename ValueType> template<typename ValueType>
void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ...";
for (auto const& formula : formulas) { std::unique_ptr<storm::modelchecker::CheckResult> result;
// If we were requested to generate a counterexample, we now do so. if (model->getType() == storm::models::ModelType::Dtmc) {
if (settings.isCounterexampleSet()) { std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model."); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
generateCounterexample<ValueType>(program.get(), model, formula); if (modelchecker.canHandle(*formula)) {
} else { result = modelchecker.check(*formula);
std::cout << std::endl << "Model checking property: " << *formula << " ..."; } else {
std::unique_ptr<storm::modelchecker::CheckResult> result; storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
if (model->getType() == storm::models::ModelType::Dtmc) { if (modelchecker2.canHandle(*formula)) {
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>(); result = modelchecker2.check(*formula);
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc); }
if (modelchecker.canHandle(*formula)) { }
result = modelchecker.check(*formula); } else if (model->getType() == storm::models::ModelType::Mdp) {
} else { std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
if (modelchecker2.canHandle(*formula)) {
result = modelchecker2.check(*formula);
}
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
#ifdef STORM_HAVE_CUDA #ifdef STORM_HAVE_CUDA
if (settings.isCudaSet()) { if (settings.isCudaSet()) {
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp); storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
result = modelchecker.check(*formula); result = modelchecker.check(*formula);
} else { } else {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula); result = modelchecker.check(*formula);
} }
#else #else
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula); result = modelchecker.check(*formula);
#endif #endif
} else if (model->getType() == storm::models::ModelType::Ctmc) { } else if (model->getType() == storm::models::ModelType::Ctmc) {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>(); std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
result = modelchecker.check(*formula);
}
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
std::cout << *result << std::endl;
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
}
}
}
#ifdef STORM_HAVE_CARL storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) { result = modelchecker.check(*formula);
std::ofstream filestream;
filestream.open(path);
// TODO: add checks.
filestream << "!Parameters: ";
std::set<storm::Variable> vars = result.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
filestream << std::endl;
filestream << "!Result: " << result << std::endl;
filestream << "!Well-formed Constraints: " << std::endl;
std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
filestream << "!Graph-preserving Constraints: " << std::endl;
std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
filestream.close();
} }
template<> if (result) {
inline void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
for (auto const& formula : formulas) { result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); std::cout << *result << std::endl;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); } else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
std::cout << std::endl << "Model checking property: " << *formula << " ..."; }
std::unique_ptr<storm::modelchecker::CheckResult> result; }
}
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc); #ifdef STORM_HAVE_CARL
if (modelchecker.canHandle(*formula)) { inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
result = modelchecker.check(*formula); std::ofstream filestream;
} else { filestream.open(path);
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); // TODO: add checks.
} filestream << "!Parameters: ";
std::set<storm::Variable> vars = result.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
filestream << std::endl;
filestream << "!Result: " << result << std::endl;
filestream << "!Well-formed Constraints: " << std::endl;
std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
filestream << "!Graph-preserving Constraints: " << std::endl;
std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
filestream.close();
}
template<>
inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
for (auto const& formula : formulas) {
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
}
if (result) { if (result) {
std::cout << " done." << std::endl; std::cout << " done." << std::endl;
std::cout << "Result (initial states): "; std::cout << "Result (initial states): ";
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates())); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates()));
std::cout << *result << std::endl; std::cout << *result << std::endl;
} else { } else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
} }
storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings();
if (parametricSettings.exportResultToFile()) { if (parametricSettings.exportResultToFile()) {
exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector(*dtmc), parametricSettings.exportResultPath());
}
}
} }
}
}
#endif #endif
template<storm::dd::DdType DdType> template<storm::dd::DdType DdType>
void verifySymbolicModelWithHybridEngine(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
for (auto const& formula : formulas) { for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>(); std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc); storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula)) { if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula); result = modelchecker.check(*formula);
}
} else if (model->getType() == storm::models::ModelType::Ctmc) {
std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
}
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
std::cout << *result << std::endl;
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
} }
} else if (model->getType() == storm::models::ModelType::Ctmc) {
std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
} }
template<storm::dd::DdType DdType> if (result) {
void verifySymbolicModelWithSymbolicEngine(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { std::cout << " done." << std::endl;
for (auto const& formula : formulas) { std::cout << "Result (initial states): ";
std::cout << std::endl << "Model checking property: " << *formula << " ..."; result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
std::unique_ptr<storm::modelchecker::CheckResult> result; std::cout << *result << std::endl;
if (model->getType() == storm::models::ModelType::Dtmc) { } else {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>(); std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
storm::modelchecker::SymbolicDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc); }
if (modelchecker.canHandle(*formula)) { }
result = modelchecker.check(*formula); }
} template<storm::dd::DdType DdType>
} else if (model->getType() == storm::models::ModelType::Mdp) { void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>(); for (auto const& formula : formulas) {
storm::modelchecker::SymbolicMdpPrctlModelChecker<DdType, double> modelchecker(*mdp); std::cout << std::endl << "Model checking property: " << *formula << " ...";
if (modelchecker.canHandle(*formula)) { std::unique_ptr<storm::modelchecker::CheckResult> result;
result = modelchecker.check(*formula); if (model->getType() == storm::models::ModelType::Dtmc) {
} std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
} else { storm::modelchecker::SymbolicDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); if (modelchecker.canHandle(*formula)) {
} result = modelchecker.check(*formula);
}
if (result) { } else if (model->getType() == storm::models::ModelType::Mdp) {
std::cout << " done." << std::endl; std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
std::cout << "Result (initial states): "; storm::modelchecker::SymbolicMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); if (modelchecker.canHandle(*formula)) {
std::cout << *result << std::endl; result = modelchecker.check(*formula);
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
} }
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
} }
template<typename ValueType> if (result) {
void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) { std::cout << " done." << std::endl;
// Now we are ready to actually build the model. std::cout << "Result (initial states): ";
STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed."); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program.get(), formulas); std::cout << *result << std::endl;
} else {
STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
// Preprocess the model if needed.
model = preprocessModel<ValueType>(model, formulas);
// Print some information about the model.
model->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given.
if (!formulas.empty()) {
if (model->isSparseModel()) {
verifySparseModel<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formulas);
} else if (model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
} else {
verifySymbolicModelWithSymbolicEngine(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
}
}
} }
}
}
template<typename ValueType>
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); template<typename ValueType>
std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>()); void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program, formulas);
STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Preprocess the model if needed. // Preprocess the model if needed.
model = preprocessModel<ValueType>(model, formulas); model = preprocessModel<ValueType>(model, formulas);
// Print some information about the model. // Print some information about the model.
model->printModelInformationToStream(std::cout); model->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given. // Verify the model, if a formula was given.
if (!formulas.empty()) { if (!formulas.empty()) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); if (model->isSparseModel()) {
verifySparseModel<ValueType>(boost::optional<storm::prism::Program>(), model->as<storm::models::sparse::Model<ValueType>>(), formulas); if(storm::settings::generalSettings().isCounterexampleSet()) {
// If we were requested to generate a counterexample, we now do so for each formula.
for(auto const& formula : formulas) {
generateCounterexample<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
}
} else if (model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
} else {
verifySymbolicModelWithSymbolicEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
} }
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
} }
}
}
template<typename ValueType>
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>());
// Preprocess the model if needed.
model = preprocessModel<ValueType>(model, formulas);
// Print some information about the model.
model->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given.
if (!formulas.empty()) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
}
}
} }

Write Preview
|||||||
100:0
Loading…
Cancel
Save