From 5794bbea56633939717852d3ae1dac56b005751f Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 12 Feb 2015 18:52:37 +0100 Subject: [PATCH] Made some adaptions to make parametric model checking work in the main executable. Former-commit-id: 0f56bec3e25a42e62d90ed5293afea701695ae9e --- src/adapters/CarlAdapter.h | 48 ++-- .../SparsePropositionalModelChecker.cpp | 5 +- .../SparseDtmcEliminationModelChecker.cpp | 8 +- src/modelchecker/results/CheckResult.cpp | 4 +- .../ExplicitQuantitativeCheckResult.cpp | 7 +- .../results/QuantitativeCheckResult.cpp | 4 +- src/settings/modules/GeneralSettings.cpp | 14 +- src/settings/modules/GeneralSettings.h | 8 + ...ministicModelBisimulationDecomposition.cpp | 4 +- src/storage/SparseMatrix.cpp | 4 +- ...tronglyConnectedComponentDecomposition.cpp | 12 +- src/storage/expressions/ExpressionEvaluator.h | 2 +- .../expressions/ExpressionEvaluatorBase.cpp | 4 +- .../expressions/ExprtkExpressionEvaluator.cpp | 2 +- .../expressions/ToRationalFunctionVisitor.h | 2 +- src/utility/ConstantsComparator.cpp | 4 +- src/utility/ConstantsComparator.h | 9 +- src/utility/PrismUtility.h | 2 +- src/utility/cli.h | 216 +++++++++++------- 19 files changed, 203 insertions(+), 156 deletions(-) diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index 1fb6ca9c0..abfedf126 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -1,12 +1,10 @@ -/** - * @file: extendedCarl.h - * @author: Sebastian Junges - * - * @since March 18, 2014 - */ +#ifndef STORM_ADAPTERS_CARLADAPTER_H_ +#define STORM_ADAPTERS_CARLADAPTER_H_ -#ifndef STORM_ADAPTERS_EXTENDEDCARL_H_ -#define STORM_ADAPTERS_EXTENDEDCARL_H_ +// Include config to know whether CARL is available or not. +#include "storm-config.h" + +#ifdef STORM_HAVE_CARL #include #include @@ -15,29 +13,35 @@ #include #include -namespace carl -{ +namespace carl { + // Define hash values for all polynomials and rational function. template - inline size_t hash_value(carl::MultivariatePolynomial const& p) - { + inline size_t hash_value(carl::MultivariatePolynomial const& p) { std::hash> h; return h(p); } template - inline size_t hash_value(carl::RationalFunction const& f) - { - std::hash h; - return h(f.nominator()) ^ h(f.denominator()); - } - - template - inline size_t hash_value(carl::FactorizedPolynomial const& p) - { + inline size_t hash_value(carl::FactorizedPolynomial const& p) { std::hash> h; return h(p); } + + template + inline size_t hash_value(carl::RationalFunction const& f) { + std::hash h; + return h(f.nominator()) ^ h(f.denominator()); + } +} + +namespace storm { + typedef carl::Variable Variable; + typedef carl::MultivariatePolynomial RawPolynomial; + typedef carl::FactorizedPolynomial Polynomial; + typedef carl::CompareRelation CompareRelation; + typedef carl::RationalFunction RationalFunction; } +#endif -#endif \ No newline at end of file +#endif /* STORM_ADAPTERS_CARLADAPTER_H_ */ \ No newline at end of file diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 1d3056426..57eefb270 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -1,7 +1,6 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm-config.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/models/Dtmc.h" #include "src/models/Mdp.h" @@ -54,7 +53,7 @@ namespace storm { template storm::models::Mdp const& SparsePropositionalModelChecker::getModelAs() const; template class SparsePropositionalModelChecker; -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template storm::models::Dtmc const& SparsePropositionalModelChecker::getModelAs() const; template storm::models::Mdp const& SparsePropositionalModelChecker::getModelAs() const; template class SparsePropositionalModelChecker; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 4769ba873..8e9564ad6 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -3,9 +3,7 @@ #include #include -#ifdef PARAMETRIC_SYSTEMS -#include "src/storage/parameters.h" -#endif +#include "src/adapters/CarlAdapter.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" @@ -1021,8 +1019,8 @@ namespace storm { template class SparseDtmcEliminationModelChecker; -#ifdef PARAMETRIC_SYSTEMS - template class SparseDtmcEliminationModelChecker; +#ifdef STORM_HAVE_CARL + template class SparseDtmcEliminationModelChecker; #endif } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp index 735e6c021..22bb96ee9 100644 --- a/src/modelchecker/results/CheckResult.cpp +++ b/src/modelchecker/results/CheckResult.cpp @@ -1,7 +1,7 @@ #include "src/modelchecker/results/CheckResult.h" #include "storm-config.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -90,7 +90,7 @@ namespace storm { template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index d1c5aebae..90d7b09ef 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -4,10 +4,7 @@ #include "src/storage/BitVector.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" - -// Include the configuration to check whether rational functions are available. -#include "storm-config.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" namespace storm { namespace modelchecker { @@ -231,7 +228,7 @@ namespace storm { template class ExplicitQuantitativeCheckResult; -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template class ExplicitQuantitativeCheckResult; #endif } diff --git a/src/modelchecker/results/QuantitativeCheckResult.cpp b/src/modelchecker/results/QuantitativeCheckResult.cpp index 0b6e2c9d2..40d97d99e 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.cpp +++ b/src/modelchecker/results/QuantitativeCheckResult.cpp @@ -1,7 +1,7 @@ #include "src/modelchecker/results/QuantitativeCheckResult.h" #include "storm-config.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" @@ -15,7 +15,7 @@ namespace storm { template class QuantitativeCheckResult; -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template class QuantitativeCheckResult; #endif } diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index d361c4de5..d38cf4305 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -41,6 +41,7 @@ namespace storm { const std::string GeneralSettings::statisticsOptionShortName = "stats"; const std::string GeneralSettings::bisimulationOptionName = "bisimulation"; const std::string GeneralSettings::bisimulationOptionShortName = "bisim"; + const std::string GeneralSettings::parametricOptionName = "parametric"; GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) @@ -84,6 +85,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build()); } bool GeneralSettings::isHelpSet() const { @@ -239,6 +241,14 @@ namespace storm { return this->getOption(statisticsOptionName).getHasOptionBeenSet(); } + bool GeneralSettings::isBisimulationSet() const { + return this->getOption(bisimulationOptionName).getHasOptionBeenSet(); + } + + bool GeneralSettings::isParametricSet() const { + return this->getOption(parametricOptionName).getHasOptionBeenSet(); + } + bool GeneralSettings::check() const { // Ensure that the model was given either symbolically or explicitly. STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both."); @@ -250,10 +260,6 @@ namespace storm { return true; } - bool GeneralSettings::isBisimulationSet() const { - return this->getOption(bisimulationOptionName).getHasOptionBeenSet(); - } - } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 583bf7e3b..e0d84e894 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -286,6 +286,13 @@ namespace storm { */ bool isBisimulationSet() const; + /*! + * Retrieves whether the option enabling parametric model checking is set. + * + * @return True iff the option was set. + */ + bool isParametricSet() const; + bool check() const override; // The name of the module. @@ -325,6 +332,7 @@ namespace storm { static const std::string statisticsOptionShortName; static const std::string bisimulationOptionName; static const std::string bisimulationOptionShortName; + static const std::string parametricOptionName; }; } // namespace modules diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 33d2589da..ba1e52efa 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -6,7 +6,7 @@ #include #include -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -1488,7 +1488,7 @@ namespace storm { template class DeterministicModelBisimulationDecomposition; -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template class DeterministicModelBisimulationDecomposition; #endif } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index c191ba9e0..9fcdb856e 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -8,7 +8,7 @@ #endif #include "src/storage/SparseMatrix.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/exceptions/InvalidStateException.h" #include "src/utility/macros.h" @@ -986,7 +986,7 @@ namespace storm { template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template class MatrixEntry::index_type, RationalFunction>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index f510f478c..692fdd9d7 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -1,6 +1,6 @@ #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/models/AbstractModel.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" namespace storm { namespace storage { @@ -211,11 +211,9 @@ namespace storm { // Explicitly instantiate the SCC decomposition. template class StronglyConnectedComponentDecomposition; - #ifdef PARAMETRIC_SYSTEMS - template class StronglyConnectedComponentDecomposition; - template class StronglyConnectedComponentDecomposition; - #endif - - +#ifdef STORM_HAVE_CARL + template class StronglyConnectedComponentDecomposition; + template class StronglyConnectedComponentDecomposition; +#endif } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExpressionEvaluator.h index 5229807f0..d9fa1653b 100644 --- a/src/storage/expressions/ExpressionEvaluator.h +++ b/src/storage/expressions/ExpressionEvaluator.h @@ -3,7 +3,7 @@ #include -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExprtkExpressionEvaluator.h" diff --git a/src/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storage/expressions/ExpressionEvaluatorBase.cpp index a750946e3..e707a48ca 100644 --- a/src/storage/expressions/ExpressionEvaluatorBase.cpp +++ b/src/storage/expressions/ExpressionEvaluatorBase.cpp @@ -1,7 +1,7 @@ #include "src/storage/expressions/ExpressionEvaluatorBase.h" #include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" namespace storm { namespace expressions { @@ -17,7 +17,7 @@ namespace storm { template class ExpressionEvaluatorBase; #ifdef STORM_HAVE_CARL - template class ExpressionEvaluatorBase; + template class ExpressionEvaluatorBase; #endif } } \ No newline at end of file diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp index 11799faa5..b621b64a6 100644 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -1,7 +1,7 @@ #include "src/storage/expressions/ExprtkExpressionEvaluator.h" #include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/utility/macros.h" namespace storm { diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h index 51cc96761..4ad74acc9 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storage/expressions/ToRationalFunctionVisitor.h @@ -1,7 +1,7 @@ #ifndef STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ #define STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ -#include "src/storage/parameters.h" +#include "src/adapters/CarlAdapter.h" #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expressions.h" #include "src/storage/expressions/ExpressionVisitor.h" diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index 0c189adaf..ac05599a0 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -79,7 +79,7 @@ namespace storm { return true; } -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template<> RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { return carl::pow(value, exponent); @@ -182,7 +182,7 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template class ConstantsComparator; template class ConstantsComparator; diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index 5d77504e0..2c45c9f8f 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -13,12 +13,7 @@ #include #include "src/settings/SettingsManager.h" - -#include "storm-config.h" - -#ifdef PARAMETRIC_SYSTEMS -#include "src/storage/parameters.h" -#endif +#include "src/adapters/CarlAdapter.h" namespace storm { @@ -81,7 +76,7 @@ namespace storm { double precision; }; -#ifdef PARAMETRIC_SYSTEMS +#ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h index 5f5e716d3..7d76dd5f4 100644 --- a/src/utility/PrismUtility.h +++ b/src/utility/PrismUtility.h @@ -225,7 +225,7 @@ namespace storm { constantDefinitions[variable] = program.getManager().rational(doubleValue); } } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant " << constantName << "."); } } } diff --git a/src/utility/cli.h b/src/utility/cli.h index 1961fc738..f82da0994 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -274,58 +274,59 @@ namespace storm { } // Customize model-building. - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitPrismModelBuilder::Options options; if (formula) { - options = storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); } options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); // Then, build the model from the symbolic description. - result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); return result; } template std::shared_ptr> preprocessModel(std::shared_ptr> model, boost::optional> const& formula) { if (storm::settings::generalSettings().isBisimulationSet()) { - STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs."); - std::shared_ptr> dtmc = model->template as>(); + STORM_LOG_THROW(model->getType() == storm::models::DTMC || model->getType() == storm::models::CTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs."); + std::shared_ptr> dtmc = model->template as>(); if (dtmc->hasTransitionRewards()) { dtmc->convertTransitionRewardsToStateRewards(); } std::cout << "Performing bisimulation minimization... "; - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; if (formula) { - options = storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, *formula.get()); + options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, *formula.get()); } if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { options.weak = true; options.bounded = false; } - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); model = bisimulationDecomposition.getQuotient(); std::cout << "done." << std::endl << std::endl; } return model; } - void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { + template + void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr formula) { if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { STORM_LOG_THROW(model->getType() == storm::models::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."); - std::shared_ptr> mdp = model->as>(); + std::shared_ptr> mdp = model->template as>(); // Determine whether we are required to use the MILP-version or the SAT-version. bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet(); if (useMILP) { - storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); + storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula); + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula); } } else { @@ -333,12 +334,119 @@ namespace storm { } } + template<> + void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr formula) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); + } + + template + void verifyModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); + + // If we were requested to generate a counterexample, we now do so. + if (settings.isCounterexampleSet()) { + STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model."); + generateCounterexample(program.get(), model, formula); + } else { + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + if (model->getType() == storm::models::DTMC) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula.get())) { + result = modelchecker.check(*formula.get()); + } else { + storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker2(*dtmc); + if (modelchecker2.canHandle(*formula.get())) { + modelchecker2.check(*formula.get()); + } + } + } else if (model->getType() == storm::models::MDP) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(*mdp); + result = modelchecker.check(*formula.get()); + } + + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->writeToStream(std::cout, model->getInitialStates()); + std::cout << std::endl << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } + } + } + + template<> + void verifyModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); + + STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); + std::shared_ptr> dtmc = model->template as>(); + + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula.get())) { + result = modelchecker.check(*formula.get()); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); + } + + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->writeToStream(std::cout, model->getInitialStates()); + std::cout << std::endl << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } + } + + template + void buildAndCheckSymbolicModel(boost::optional const& program, boost::optional> formula) { + // Now we are ready to actually build the model. + STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed."); + std::shared_ptr> model = buildSymbolicModel(program.get(), formula); + + // Preprocess the model if needed. + model = preprocessModel(model, formula); + + // Print some information about the model. + model->printModelInformationToStream(std::cout); + + // Verify the model, if a formula was given. + if (formula) { + verifyModel(program, model, formula.get()); + } + } + + template + void buildAndCheckExplicitModel(boost::optional> formula) { + 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> model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional()); + + // Preprocess the model if needed. + model = preprocessModel(model, formula); + + // Print some information about the model. + model->printModelInformationToStream(std::cout); + + // Verify the model, if a formula was given. + if (formula) { + verifyModel(boost::optional(), model, formula.get()); + } + } + void processOptions() { if (storm::settings::debugSettings().isLogfileSet()) { initializeFileLogging(); } - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); // If we have to build the model from a symbolic representation, we need to parse the representation first. @@ -360,82 +468,16 @@ namespace storm { } } - // Now we are ready to actually build the model. - std::chrono::high_resolution_clock::time_point buildingTimeStart = std::chrono::high_resolution_clock::now(); - std::shared_ptr> model; - if (settings.isExplicitSet()) { - model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional()); - } else if (settings.isSymbolicSet()) { - STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed."); - model = buildSymbolicModel(program.get(), formula); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); - } - std::chrono::high_resolution_clock::time_point buildingTimeEnd = std::chrono::high_resolution_clock::now(); - - // Now, we can do the preprocessing on the model, if it was requested. - std::chrono::high_resolution_clock::time_point preprocessingTimeStart = std::chrono::high_resolution_clock::now(); - model = preprocessModel(model, formula); - std::chrono::high_resolution_clock::time_point preprocessingTimeEnd = std::chrono::high_resolution_clock::now(); - - // Print some information about the model. - model->printModelInformationToStream(std::cout); - - std::chrono::high_resolution_clock::time_point checkingTimeStart = std::chrono::high_resolution_clock::now(); - // If we were requested to generate a counterexample, we now do so. - if (settings.isCounterexampleSet()) { - STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property."); - STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model."); - generateCounterexample(program.get(), model, formula.get()); - } else if (formula) { - std::cout << std::endl << "Model checking property: " << *formula.get() << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::DTMC) { - std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula.get())) { - result = modelchecker.check(*formula.get()); - } else { - storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker2(*dtmc); - if (modelchecker2.canHandle(*formula.get())) { - modelchecker2.check(*formula.get()); - } - } - } else if (model->getType() == storm::models::MDP) { - std::shared_ptr> mdp = model->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(*mdp); - result = modelchecker.check(*formula.get()); - } - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->writeToStream(std::cout, model->getInitialStates()); - std::cout << std::endl << std::endl; + if (settings.isSymbolicSet()) { + if (settings.isParametricSet()) { + buildAndCheckSymbolicModel(program.get(), formula); } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + buildAndCheckSymbolicModel(program.get(), formula); } - } - std::chrono::high_resolution_clock::time_point checkingTimeEnd = std::chrono::high_resolution_clock::now(); - std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); - - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; - std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); - std::chrono::high_resolution_clock::duration buildingTime = buildingTimeEnd - buildingTimeStart; - std::chrono::milliseconds buildingTimeInMilliseconds = std::chrono::duration_cast(buildingTime); - std::chrono::high_resolution_clock::duration preprocessingTime = preprocessingTimeEnd - preprocessingTimeStart; - std::chrono::milliseconds preprocessingTimeInMilliseconds = std::chrono::duration_cast(preprocessingTime); - std::chrono::high_resolution_clock::duration checkingTime = checkingTimeEnd - checkingTimeStart; - std::chrono::milliseconds checkingTimeInMilliseconds = std::chrono::duration_cast(checkingTime); - - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); - STORM_PRINT_AND_LOG(" * time for building: " << buildingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(" * time for preprocessing: " << preprocessingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(" * time for checking: " << checkingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); - STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(std::endl); + } else if (settings.isExplicitSet()) { + buildAndCheckExplicitModel(formula); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } } }