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

changed cli to create tasks that only compute the value for the initial state (if the model checker supports that) 

Former-commit-id: 3745aa138f
tempestpy_adaptions
dehnert 9 years ago
parent
1308b91fda
commit
e5f9ddfbcc
4 changed files with 56 additions and 53 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. 6
      src/cli/cli.cpp
  2. 39
      src/cli/entrypoints.h
  3. 4
      src/modelchecker/CheckTask.h
  4. 60
      src/utility/storm.h

6
src/cli/cli.cpp
View File

@ -236,15 +236,15 @@ namespace storm {
if (settings.isSymbolicSet()) {
#ifdef STORM_HAVE_CARL
if (settings.isParametricSet()) {
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas);
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas, true);
} else {
#endif
buildAndCheckSymbolicModel<double>(program.get(), formulas);
buildAndCheckSymbolicModel<double>(program.get(), formulas, true);
#ifdef STORM_HAVE_CARL
}
#endif
} else if (settings.isExplicitSet()) {
buildAndCheckExplicitModel<double>(formulas);
buildAndCheckExplicitModel<double>(formulas, true);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}

39
src/cli/entrypoints.h
View File

@ -9,10 +9,10 @@ namespace storm {
namespace cli {
template<typename ValueType>
void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula));
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant));
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
@ -26,12 +26,12 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<>
inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant) {
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::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula));
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant));
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
@ -50,15 +50,15 @@ namespace storm {
#endif
template<storm::dd::DdType DdType>
void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
}
template<storm::dd::DdType DdType>
void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, formula));
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant));
if (result) {
std::cout << " done." << std::endl;
@ -72,10 +72,10 @@ namespace storm {
}
template<storm::dd::DdType DdType>
void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula));
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant));
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
@ -114,12 +114,12 @@ namespace storm {
}
template<typename ValueType, storm::dd::DdType LibraryType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas);
verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas, onlyInitialStatesRelevant);
} else {
storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException,
@ -133,7 +133,6 @@ namespace storm {
// Verify the model, if a formula was given.
if (!formulas.empty()) {
if (modelFormulasPair.model->isSparseModel()) {
if (storm::settings::generalSettings().isCounterexampleSet()) {
// If we were requested to generate a counterexample, we now do so for each formula.
@ -141,15 +140,15 @@ namespace storm {
generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas);
verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas, onlyInitialStatesRelevant);
}
} else if (modelFormulasPair.model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
modelFormulasPair.formulas);
modelFormulasPair.formulas, onlyInitialStatesRelevant);
} else {
verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
modelFormulasPair.formulas);
modelFormulasPair.formulas, onlyInitialStatesRelevant);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
@ -159,16 +158,16 @@ namespace storm {
}
template<typename ValueType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) {
buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::CUDD>(program, formulas);
buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant);
} else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) {
buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::Sylvan>(program, formulas);
buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant);
}
}
template<typename ValueType>
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
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.");
@ -183,7 +182,7 @@ namespace storm {
// 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);
verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas, onlyInitialStatesRelevant);
}
}
}

4
src/modelchecker/CheckTask.h
View File

@ -28,8 +28,8 @@ namespace storm {
/*!
* Creates a task object with the default options for the given formula.
*/
CheckTask(FormulaType const& formula) : formula(formula) {
this->onlyInitialStatesRelevant = false;
CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) {
this->onlyInitialStatesRelevant = onlyInitialStatesRelevant;
this->produceStrategies = true;
this->qualitative = false;

60
src/utility/storm.h
View File

@ -236,23 +236,23 @@ namespace storm {
#endif
template<typename ValueType, storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
switch(settings.getEngine()) {
case storm::settings::modules::GeneralSettings::Engine::Sparse: {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model");
return verifySparseModel(sparseModel, formula);
return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant);
}
case storm::settings::modules::GeneralSettings::Engine::Hybrid: {
std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model");
return verifySymbolicModelWithHybridEngine(ddModel, formula);
return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant);
}
case storm::settings::modules::GeneralSettings::Engine::Dd: {
std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
return verifySymbolicModelWithDdEngine(ddModel, formula);
return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant);
}
case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: {
STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built.");
@ -261,18 +261,19 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
} else {
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
if (modelchecker2.canHandle(*formula)) {
result = modelchecker2.check(*formula);
if (modelchecker2.canHandle(task)) {
result = modelchecker2.check(task);
}
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
@ -280,20 +281,20 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
if (settings.isCudaSet()) {
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
result = modelchecker.check(*formula);
result = modelchecker.check(task);
} else {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula);
result = modelchecker.check(task);
}
#else
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula);
result = modelchecker.check(task);
#endif
} 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>>();
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
result = modelchecker.check(*formula);
result = modelchecker.check(task);
}
return result;
@ -317,13 +318,14 @@ namespace storm {
}
template<>
inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
}
@ -333,25 +335,26 @@ namespace storm {
#endif
template<storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} 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);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} 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);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
@ -361,19 +364,20 @@ namespace storm {
template<storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant) {
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} 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::SymbolicMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
if (modelchecker.canHandle(task)) {
result = modelchecker.check(task);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");

Write Preview
Loading…
Cancel
Save