From 01a3748e872d90e447006ffd73815778b6d8d13e Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 7 Sep 2015 11:35:59 +0200 Subject: [PATCH] Refactored part of the API / more functions Former-commit-id: eb8deb537c58598f0c27a5d63519a53391864517 --- src/cli/cli.cpp | 19 +- src/parser/FormulaParser.cpp | 6 +- src/parser/FormulaParser.h | 6 +- src/utility/storm.cpp | 41 +++ src/utility/storm.h | 590 ++++++++++++++++++----------------- 5 files changed, 349 insertions(+), 313 deletions(-) create mode 100644 src/utility/storm.cpp diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index cfc88468b..c9e0aa7e6 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -214,27 +214,20 @@ namespace storm { boost::optional program; if (settings.isSymbolicSet()) { std::string const& programFile = settings.getSymbolicModelFilename(); - program = storm::parser::PrismParser::parse(programFile).simplify().simplify(); - - program->checkValidity(); + program = storm::parseProgram(programFile); } // Then proceed to parsing the property (if given), since the model we are building may depend on the property. std::vector> formulas; if (settings.isPropertySet()) { - storm::parser::FormulaParser formulaParser; - if (program) { - formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer()); - } + std::string properties = settings.getProperty(); - // 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. - std::string property = settings.getProperty(); - if (property.find(".") != std::string::npos && std::ifstream(property).good()) { - formulas = formulaParser.parseFromFile(settings.getProperty()); + if(program) { + formulas = storm::parseFormulasForProgram(properties, program.get()); } else { - formulas = formulaParser.parseFromString(settings.getProperty()); + formulas = storm::parseFormulasForExplicit(properties); } + } if (settings.isSymbolicSet()) { diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 2d3fa0198..082474187 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -184,13 +184,13 @@ namespace storm { return *this; } - std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) { + std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { std::vector> formulas = parseFromString(formulaString); STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead."); return formulas.front(); } - std::vector> FormulaParser::parseFromFile(std::string const& filename) { + std::vector> FormulaParser::parseFromFile(std::string const& filename) const { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); @@ -212,7 +212,7 @@ namespace storm { return formulas; } - std::vector> FormulaParser::parseFromString(std::string const& formulaString) { + std::vector> FormulaParser::parseFromString(std::string const& formulaString) const { PositionIteratorType first(formulaString.begin()); PositionIteratorType iter = first; PositionIteratorType last(formulaString.end()); diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index 895d84cd5..25dc6514f 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -28,7 +28,7 @@ namespace storm { * @param formulaString The formula as a string. * @return The resulting formula. */ - std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString); + std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString) const; /*! * Parses the formula given by the provided string. @@ -36,7 +36,7 @@ namespace storm { * @param formulaString The formula as a string. * @return The contained formulas. */ - std::vector> parseFromString(std::string const& formulaString); + std::vector> parseFromString(std::string const& formulaString) const; /*! * Parses the formulas in the given file. @@ -44,7 +44,7 @@ namespace storm { * @param filename The name of the file to parse. * @return The contained formulas. */ - std::vector> parseFromFile(std::string const& filename); + std::vector> 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 diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp new file mode 100644 index 000000000..49ca3e48a --- /dev/null +++ b/src/utility/storm.cpp @@ -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> 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> parseFormulasForExplicit(std::string const& inputString) { + storm::parser::FormulaParser formulaParser; + return parseFormulas(formulaParser, inputString); + } + + std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) { + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + return parseFormulas(formulaParser, inputString); + } +} \ No newline at end of file diff --git a/src/utility/storm.h b/src/utility/storm.h index b54ee42d6..4c390984a 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -22,10 +22,6 @@ #include "src/settings/modules/BisimulationSettings.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. #include "src/logic/Formulas.h" @@ -40,6 +36,8 @@ #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddBdd.h" +#include "src/parser/AutoParser.h" + // Headers of builders. #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/builder/DdPrismModelBuilder.h" @@ -74,326 +72,330 @@ namespace storm { - template - std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::optional(), boost::optional const& transitionRewardsFile = boost::optional()) { - return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : ""); - } + template + std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::optional(), boost::optional const& transitionRewardsFile = boost::optional()) { + return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : ""); + } - template - std::shared_ptr buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::shared_ptr 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. - std::string constants = settings.getConstantDefinitionString(); - - // Customize and perform model-building. - if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) { - typename storm::builder::ExplicitPrismModelBuilder::Options options; - options = typename storm::builder::ExplicitPrismModelBuilder::Options(formulas); - options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); - - // Generate command labels if we are going to build a counterexample later. - if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { - options.buildCommandLabels = true; - } - - result = storm::builder::ExplicitPrismModelBuilder::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::Options options; - options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); - - result = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - } - - // Then, build the model from the symbolic description. - return result; + storm::prism::Program parseProgram(std::string const& path); + std::vector> parseFormulasForExplicit(std::string const& inputString); + std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); + + + + template + std::shared_ptr buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + std::shared_ptr 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. + std::string constants = settings.getConstantDefinitionString(); + + // Customize and perform model-building. + if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) { + typename storm::builder::ExplicitPrismModelBuilder::Options options; + options = typename storm::builder::ExplicitPrismModelBuilder::Options(formulas); + options.addConstantDefinitionsFromString(program, constants); + + // Generate command labels if we are going to build a counterexample later. + if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { + options.buildCommandLabels = true; } + + result = storm::builder::ExplicitPrismModelBuilder::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::Options options; + options = typename storm::builder::DdPrismModelBuilder::Options(formulas); + options.addConstantDefinitionsFromString(program, constants); + + result = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + } + + // Then, build the model from the symbolic description. + return result; + } - template - std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { - if (storm::settings::generalSettings().isBisimulationSet()) { - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); - std::shared_ptr> sparseModel = model->template as>(); - 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."); - std::shared_ptr> dtmc = sparseModel->template as>(); - - dtmc->reduceToStateBasedRewards(); - - std::cout << "Performing bisimulation minimization... "; - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; - if (!formulas.empty()) { - options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*sparseModel, formulas); - } - if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { - options.weak = true; - options.bounded = false; - } - - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); - model = bisimulationDecomposition.getQuotient(); - std::cout << "done." << std::endl << std::endl; - } - return model; + template + std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { + if (storm::settings::generalSettings().isBisimulationSet()) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); + std::shared_ptr> sparseModel = model->template as>(); + 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."); + std::shared_ptr> dtmc = sparseModel->template as>(); + + dtmc->reduceToStateBasedRewards(); + + std::cout << "Performing bisimulation minimization... "; + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + if (!formulas.empty()) { + options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*sparseModel, formulas); } + if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { + options.weak = true; + options.bounded = false; + } + + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); + model = bisimulationDecomposition.getQuotient(); + std::cout << "done." << std::endl << std::endl; + } + return model; + } - template - void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr 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."); - - 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); - } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula); - } - - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected."); - } + template + void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr 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."); + + 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); + } else { + storm::counterexamples::SMTMinimalCommandSetGenerator::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 - template<> - inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); - } + template<> + inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); + } #endif - template - void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::vector> const& formulas) { - storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - - for (auto const& formula : formulas) { - // 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::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } else { - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); - if (modelchecker2.canHandle(*formula)) { - result = modelchecker2.check(*formula); - } - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); + template + void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { + for (auto const& formula : formulas) { + + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } else { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); + if (modelchecker2.canHandle(*formula)) { + result = modelchecker2.check(*formula); + } + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); #ifdef STORM_HAVE_CUDA - if (settings.isCudaSet()) { - storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); - result = modelchecker.check(*formula); - } else { - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula); - } + if (settings.isCudaSet()) { + storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); + result = modelchecker.check(*formula); + } else { + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + result = modelchecker.check(*formula); + } #else - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + result = modelchecker.check(*formula); #endif - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - - storm::modelchecker::SparseCtmcCslModelChecker> 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; - } - } - } + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); + + storm::modelchecker::SparseCtmcCslModelChecker> 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 - inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { - std::ofstream filestream; - filestream.open(path); - // TODO: add checks. - filestream << "!Parameters: "; - std::set vars = result.gatherVariables(); - std::copy(vars.begin(), vars.end(), std::ostream_iterator(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>(filestream, "\n")); - filestream << "!Graph-preserving Constraints: " << std::endl; - std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); - filestream.close(); - } + inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { + std::ofstream filestream; + filestream.open(path); + // TODO: add checks. + filestream << "!Parameters: "; + std::set vars = result.gatherVariables(); + std::copy(vars.begin(), vars.end(), std::ostream_iterator(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>(filestream, "\n")); + filestream << "!Graph-preserving Constraints: " << std::endl; + std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); + filestream.close(); + } - template<> - inline void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::vector> 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> 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)) { - result = modelchecker.check(*formula); - } 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->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } - - storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); - if (parametricSettings.exportResultToFile()) { - exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); - } - } + template<> + inline void verifySparseModel(std::shared_ptr> model, std::vector> 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> 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)) { + result = modelchecker.check(*formula); + } 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->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates())); + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } + + storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); + if (parametricSettings.exportResultToFile()) { + exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } + } + } #endif - template - void verifySymbolicModelWithHybridEngine(boost::optional const& program, std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::HybridMdpPrctlModelChecker 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(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } + template + void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { + for (auto const& formula : formulas) { + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::HybridMdpPrctlModelChecker 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(model->getReachableStates(), model->getInitialStates())); + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } + } + } - template - void verifySymbolicModelWithSymbolicEngine(boost::optional const& program, std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker 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(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } + template + void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas) { + for (auto const& formula : formulas) { + std::cout << std::endl << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::SymbolicMdpPrctlModelChecker 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(model->getReachableStates(), model->getInitialStates())); + std::cout << *result << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } + } + } - template - void buildAndCheckSymbolicModel(boost::optional const& program, std::vector> const& formulas) { - // 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(), formulas); - - STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); - - // Preprocess the model if needed. - model = preprocessModel(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(program, model->as>(), formulas); - } else if (model->isSymbolicModel()) { - if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(program, model->as>(), formulas); - } else { - verifySymbolicModelWithSymbolicEngine(program, model->as>(), formulas); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); + + template + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + std::shared_ptr model = buildSymbolicModel(program, formulas); + STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); + + // Preprocess the model if needed. + model = preprocessModel(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()) { + 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(program, model->as>(), formula); } + } else { + verifySparseModel(model->as>(), formulas); } - } - - template - void buildAndCheckExplicitModel(std::vector> 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 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, 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(boost::optional(), model->as>(), formulas); + } else if (model->isSymbolicModel()) { + if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { + verifySymbolicModelWithHybridEngine(model->as>(), formulas); + } else { + verifySymbolicModelWithSymbolicEngine(model->as>(), formulas); } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); } + } + } + + template + void buildAndCheckExplicitModel(std::vector> 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 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, 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(model->as>(), formulas); + } + } }