diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index e3164fd39..5bb379962 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -64,7 +64,7 @@ void analyzeDFT(std::vector const& properties, bool symred, bool al for (size_t i = 1; i < properties.size(); ++i) { propString += ";" + properties[i]; } - std::vector> props = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(propString)); + std::vector> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString)); STORM_LOG_ASSERT(props.size() > 0, "No properties found."); // Check model diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 79ed0ef95..8721efd7c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -202,7 +202,7 @@ namespace storm { // Apply bisimulation to new CTMC bisimulationTimer.start(); - ctmc = storm::performDeterministicSparseBisimulationMinimization>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as>(); + ctmc = storm::api::performDeterministicSparseBisimulationMinimization>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as>(); bisimulationTimer.stop(); if (firstTime) { @@ -214,7 +214,7 @@ namespace storm { // Apply bisimulation to parallel composition bisimulationTimer.start(); - composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); + composedModel = storm::api::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); bisimulationTimer.stop(); STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates()); @@ -382,7 +382,7 @@ namespace storm { if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { bisimulationTimer.start(); STORM_LOG_INFO("Bisimulation..."); - model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); + model = storm::api::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); bisimulationTimer.stop(); @@ -399,7 +399,7 @@ namespace storm { singleModelCheckingTimer.reset(); singleModelCheckingTimer.start(); STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); - std::unique_ptr result(storm::verifySparseModel(model, property, true)); + std::unique_ptr result(storm::api::verifyWithSparseEngine(model, storm::api::createTask(property, true))); STORM_LOG_ASSERT(result, "Result does not exist."); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); ValueType resultValue = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index f67fe125e..597feb3cb 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -2,7 +2,7 @@ #include "storm/logic/Formula.h" #include "storm/modelchecker/results/CheckResult.h" -#include "storm/utility/storm.h" // TODO this should not be included here. +#include "storm/api/storm.h" #include "storm/utility/Stopwatch.h" #include "storm-dft/storage/dft/DFT.h" diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 6e0f03dca..423afb087 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -2,7 +2,6 @@ #include "logic/Formula.h" #include "utility/initialize.h" -#include "utility/storm.h" #include "storm/cli/cli.h" #include "storm/exceptions/BaseException.h" #include "storm/utility/macros.h" @@ -13,6 +12,7 @@ #include "storm/exceptions/FileIoException.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/PGCLSettings.h" @@ -20,6 +20,7 @@ #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/JaniExportSettings.h" +#include "storm/utility/file.h" /*! * Initialize the settings manager. diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp index f45b7076c..b27dc9524 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp @@ -41,6 +41,7 @@ namespace storm { markovModel = transformer.translate(*markovModel->template as>(), timeRewardModelName); } } + return markovModel; } template diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp deleted file mode 100644 index 07bb39118..000000000 --- a/src/storm/utility/storm.cpp +++ /dev/null @@ -1,101 +0,0 @@ -#include "storm.h" - -// Headers related to parsing. -#include "storm/parser/JaniParser.h" - -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" -#include "storm/utility/macros.h" -#include "storm/storage/jani/Property.h" - -namespace storm{ - - std::vector> extractFormulasFromProperties(std::vector const& properties) { - std::vector> formulas; - for (auto const& prop : properties) { - formulas.push_back(prop.getRawFormula()); - } - return formulas; - } - - storm::prism::Program parseProgram(std::string const& path) { - storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify(); - program.checkValidity(); - return program; - } - - std::pair> parseJaniModel(std::string const& path) { - std::pair> modelAndFormulae = storm::parser::JaniParser::parse(path); - modelAndFormulae.first.checkValid(); - return modelAndFormulae; - } - - std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter) { - // 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::vector properties; - if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) { - properties = formulaParser.parseFromFile(inputString); - } else { - properties = formulaParser.parseFromString(inputString); - } - - return filterProperties(properties, propertyFilter); - } - - std::vector parsePropertiesForExplicit(std::string const& inputString, boost::optional> const& propertyFilter) { - auto exprManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(exprManager); - return parseProperties(formulaParser, inputString, propertyFilter); - } - - std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution) { - std::vector preprocessedProperties; - for (auto const& property : properties) { - preprocessedProperties.emplace_back(property.substitute(substitution)); - } - return preprocessedProperties; - } - - std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter) { - storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer()); - auto formulas = parseProperties(formulaParser, inputString, propertyFilter); - return substituteConstantsInProperties(formulas, model.getConstantsSubstitution()); - } - - std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter) { - storm::parser::FormulaParser formulaParser(program); - auto formulas = parseProperties(formulaParser, inputString, propertyFilter); - return substituteConstantsInProperties(formulas, program.getConstantsSubstitution()); - } - - boost::optional> parsePropertyFilter(boost::optional const& propertyFilter) { - std::vector propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter.get()); - std::set propertyNameSet(propertyNames.begin(), propertyNames.end()); - return propertyNameSet; - } - - std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter) { - if (propertyFilter) { - std::set const& propertyNameSet = propertyFilter.get(); - std::vector result; - std::set reducedPropertyNames; - for (auto const& property : properties) { - if (propertyNameSet.find(property.getName()) != propertyNameSet.end()) { - result.push_back(property); - reducedPropertyNames.insert(property.getName()); - } - } - - if (reducedPropertyNames.size() < propertyNameSet.size()) { - std::set missingProperties; - std::set_difference(propertyNameSet.begin(), propertyNameSet.end(), reducedPropertyNames.begin(), reducedPropertyNames.end(), std::inserter(missingProperties, missingProperties.begin())); - STORM_LOG_WARN("Filtering unknown properties " << boost::join(missingProperties, ", ") << "."); - } - - return result; - } else { - return properties; - } - } -} diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h deleted file mode 100644 index 2d5b4e90f..000000000 --- a/src/storm/utility/storm.h +++ /dev/null @@ -1,694 +0,0 @@ -#ifndef STORM_H -#define STORM_H - -#include -#include -#include -#include -#include -#include -#include "storm/storage/ModelFormulasPair.h" - -#include "initialize.h" - -#include "storm-config.h" - -// Headers that provide auxiliary functionality. -#include "storm/settings/SettingsManager.h" - -#include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/BisimulationSettings.h" -#include "storm/settings/modules/ParametricSettings.h" -#include "storm/settings/modules/EliminationSettings.h" -#include "storm/settings/modules/JitBuilderSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" - -// Formula headers. -#include "storm/logic/Formulas.h" -#include "storm/logic/FragmentSpecification.h" - -// Model headers. -#include "storm/models/ModelBase.h" -#include "storm/models/sparse/Model.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/symbolic/Model.h" -#include "storm/models/symbolic/StandardRewardModel.h" - -#include "storm/storage/dd/Add.h" -#include "storm/storage/dd/Bdd.h" - -#include "storm/parser/AutoParser.h" -#include "storm/parser/DirectEncodingParser.h" - -#include "storm/storage/jani/Model.h" -#include "storm/storage/jani/Property.h" - -// Headers of builders. -#include "storm/builder/ExplicitModelBuilder.h" -#include "storm/builder/jit/ExplicitJitJaniModelBuilder.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/builder/DdJaniModelBuilder.h" - -// Headers for model processing. -#include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" -#include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" -#include "storm/transformer/SymbolicToSparseTransformer.h" -#include "storm/storage/ModelFormulasPair.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/storage/jani/JSONExporter.h" - -// Headers for model checking. -#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" -#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" -#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" -#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" -#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" -#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" -#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" -#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h" -#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h" -#include "storm/utility/parameterlifting.h" - -#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" -#include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h" -#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" -#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" -#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" - -#include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h" - -// Headers for counterexample generation. -#include "storm/counterexamples/MILPMinimalCommandSetGenerator.h" -#include "storm/counterexamples/SMTMinimalCommandSetGenerator.h" - -// Headers related to model building. -#include "storm/generator/PrismNextStateGenerator.h" -#include "storm/generator/JaniNextStateGenerator.h" - -#include "storm/analysis/GraphConditions.h" - -// Headers related to exception handling. -#include "storm/exceptions/InvalidStateException.h" -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/InvalidTypeException.h" -#include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/NotSupportedException.h" - -#include "storm/utility/Stopwatch.h" -#include "storm/utility/file.h" - -#include - -namespace storm { - - namespace parser { - class FormulaParser; - } - - std::vector> extractFormulasFromProperties(std::vector const& properties); - std::pair> parseJaniModel(std::string const& path); - storm::prism::Program parseProgram(std::string const& path); - std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution); - std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter = boost::none); - std::vector parsePropertiesForExplicit(std::string const& inputString, boost::optional> const& propertyFilter = boost::none); - std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter = boost::none); - std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter = boost::none); - boost::optional> parsePropertyFilter(boost::optional const& propertyFilter); - std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter); - - template - std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { - STORM_LOG_INFO("Performing bisimulation minimization... "); - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; - if (!formulas.empty()) { - options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, formulas); - } - options.setType(type); - - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); - bisimulationDecomposition.computeBisimulationDecomposition(); - model = bisimulationDecomposition.getQuotient(); - STORM_LOG_INFO("Bisimulation done, quotient model has " << model->getNumberOfStates() << " states and " << model->getNumberOfTransitions() << " transitions."); - return model; - } - - template - std::shared_ptr performNondeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { - STORM_LOG_INFO("Performing bisimulation minimization... "); - typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; - if (!formulas.empty()) { - options = typename storm::storage::NondeterministicModelBisimulationDecomposition::Options(*model, formulas); - } - options.setType(type); - - storm::storage::NondeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); - bisimulationDecomposition.computeBisimulationDecomposition(); - model = bisimulationDecomposition.getQuotient(); - STORM_LOG_INFO("Bisimulation done, quotient model has " << model->getNumberOfStates() << " states and " << model->getNumberOfTransitions() << " transitions."); - return model; - } - - template - std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::vector> const& formulas, storm::storage::BisimulationType type) { - using ValueType = typename ModelType::ValueType; - - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); - model->reduceToStateBasedRewards(); - - if (model->isOfType(storm::models::ModelType::Dtmc)) { - return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); - } else if (model->isOfType(storm::models::ModelType::Ctmc)) { - return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); - } else { - return performNondeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); - } - } - - template - std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::shared_ptr const& formula, storm::storage::BisimulationType type) { - std::vector> formulas = { formula }; - return performBisimulationMinimization(model, formulas , type); - } - - - template - std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { - storm::utility::Stopwatch preprocessingWatch(true); - - bool operationPerformed = false; - if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) { - operationPerformed = true; - std::shared_ptr> ma = model->template as>(); - ma->close(); - if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC. - STORM_PRINT_AND_LOG(std::endl << "Converting deterministic MA to a CTMC..." << std::endl); - model = ma->convertToCTMC(); - } - } - - if (model->isSparseModel() && storm::settings::getModule().isBisimulationSet()) { - operationPerformed = true; - storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; - if (storm::settings::getModule().isWeakBisimulationSet()) { - bisimType = storm::storage::BisimulationType::Weak; - } - - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); - model = performBisimulationMinimization(model->template as>(), formulas, bisimType); - - STORM_LOG_INFO("Quotient model has " << model->getNumberOfStates() << " states and " << model->getNumberOfTransitions() << " transitions."); - } - - preprocessingWatch.stop(); - if (operationPerformed) { - STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); - } - - return model; - } - - template - void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr const& formula) { - if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { - STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for PRISM models."); - STORM_LOG_THROW(markovModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); - storm::prism::Program const& program = model.asPrismProgram(); - - std::shared_ptr> mdp = markovModel->template as>(); - - // Determine whether we are required to use the MILP-version or the SAT-version. - bool useMILP = storm::settings::getModule().isUseMilpBasedMinimalCommandSetGenerationSet(); - - if (useMILP) { - storm::counterexamples::MILPMinimalCommandSetGenerator::computeCounterexample(program, *mdp, formula); - } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, *mdp, formula); - } - - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected."); - } - } - -#ifdef STORM_HAVE_CARL - template<> - inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for exact arithmetic model."); - } - - template<> - inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); - } -#endif - - template - void generateCounterexamples(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::vector> const& formulas) { - for (auto const& formula : formulas) { - generateCounterexample(model, markovModel, formula); - } - } - - template - inline void performParameterLifting(std::shared_ptr>, std::shared_ptr const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting for non-parametric model."); - } - -#ifdef STORM_HAVE_CARL - template<> - inline void performParameterLifting(std::shared_ptr> markovModel, std::shared_ptr const& formula) { - storm::utility::Stopwatch parameterLiftingStopWatch(true); - std::shared_ptr consideredFormula = formula; - - STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(markovModel, formula), "Could not validate whether parameter lifting is sound on the input model and the formula " << *formula); - - if (markovModel->isOfType(storm::models::ModelType::Ctmc) || markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { - STORM_PRINT_AND_LOG("Transforming continuous model to discrete model..."); - storm::transformer::transformContinuousToDiscreteModelInPlace(markovModel, consideredFormula); - STORM_PRINT_AND_LOG(" done!" << std::endl); - markovModel->printModelInformationToStream(std::cout); - } - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel); - auto rewParameters = storm::models::sparse::getRewardParameters(*markovModel); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - STORM_LOG_THROW(storm::settings::getModule().isParameterSpaceSet(), storm::exceptions::InvalidSettingsException, "Invoked Parameter lifting but no parameter space was defined."); - auto parameterSpaceAsString = storm::settings::getModule().getParameterSpace(); - auto parameterSpace = storm::storage::ParameterRegion::parseRegion(parameterSpaceAsString, modelParameters); - auto refinementThreshold = storm::utility::convertNumber::CoefficientType>(storm::settings::getModule().getRefinementThreshold()); - std::vector, storm::modelchecker::parametric::RegionCheckResult>> result; - - STORM_PRINT_AND_LOG("Performing parameter lifting for property " << *consideredFormula << " with parameter space " << parameterSpace.toString(true) << " and refinement threshold " << storm::utility::convertNumber(refinementThreshold) << " ..." << std::endl); - - storm::modelchecker::CheckTask task(*consideredFormula, true); - std::string resultVisualization; - - if (markovModel->isOfType(storm::models::ModelType::Dtmc)) { - if (storm::settings::getModule().isExactSet()) { - storm::modelchecker::parametric::SparseDtmcRegionChecker , storm::RationalNumber> regionChecker(*markovModel->template as>()); - regionChecker.specifyFormula(task); - result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); - parameterLiftingStopWatch.stop(); - if (modelParameters.size() == 2) { - resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); - } - } else { - storm::modelchecker::parametric::SparseDtmcRegionChecker , double, storm::RationalNumber> regionChecker(*markovModel->template as>()); - regionChecker.specifyFormula(task); - result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); - parameterLiftingStopWatch.stop(); - if (modelParameters.size() == 2) { - resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); - } - } - } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) { - if (storm::settings::getModule().isExactSet()) { - storm::modelchecker::parametric::SparseMdpRegionChecker, storm::RationalNumber> regionChecker(*markovModel->template as>()); - regionChecker.specifyFormula(task); - result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); - parameterLiftingStopWatch.stop(); - if (modelParameters.size() == 2) { - resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); - } - } else { - storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*markovModel->template as>()); - regionChecker.specifyFormula(task); - result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); - parameterLiftingStopWatch.stop(); - if (modelParameters.size() == 2) { - resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); - } - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type."); - } - - - auto satArea = storm::utility::zero::CoefficientType>(); - auto unsatArea = storm::utility::zero::CoefficientType>(); - uint_fast64_t numOfSatRegions = 0; - uint_fast64_t numOfUnsatRegions = 0; - for (auto const& res : result) { - switch (res.second) { - case storm::modelchecker::parametric::RegionCheckResult::AllSat: - satArea += res.first.area(); - ++numOfSatRegions; - break; - case storm::modelchecker::parametric::RegionCheckResult::AllViolated: - unsatArea += res.first.area(); - ++numOfUnsatRegions; - break; - default: - STORM_LOG_ERROR("Unexpected result for region " << res.first.toString(true) << " : " << res.second << "."); - break; - } - } - typename storm::storage::ParameterRegion::CoefficientType satAreaFraction = satArea / parameterSpace.area(); - typename storm::storage::ParameterRegion::CoefficientType unsatAreaFraction = unsatArea / parameterSpace.area(); - STORM_PRINT_AND_LOG("Done! Found " << numOfSatRegions << " safe regions and " - << numOfUnsatRegions << " unsafe regions." << std::endl); - STORM_PRINT_AND_LOG(storm::utility::convertNumber(satAreaFraction) * 100 << "% of the parameter space is safe, and " - << storm::utility::convertNumber(unsatAreaFraction) * 100 << "% of the parameter space is unsafe." << std::endl); - STORM_PRINT_AND_LOG("Model checking with parameter lifting took " << parameterLiftingStopWatch << " seconds." << std::endl); - STORM_PRINT_AND_LOG(resultVisualization); - - if (storm::settings::getModule().exportResultToFile()) { - std::string path = storm::settings::getModule().exportResultPath(); - STORM_PRINT_AND_LOG("Exporting result to path " << path << "." << std::endl); - std::ofstream filestream; - storm::utility::openFile(path, filestream); - - for (auto const& res : result) { - switch (res.second) { - case storm::modelchecker::parametric::RegionCheckResult::AllSat: - filestream << "safe: " << res.first.toString(true) << std::endl; - break; - case storm::modelchecker::parametric::RegionCheckResult::AllViolated: - filestream << "unsafe: " << res.first.toString(true) << std::endl; - break; - default: - break; - } - } - } - } -#endif - - template - inline void performParameterLifting(std::shared_ptr> markovModel, std::vector> const& formulas) { - for (auto const& formula : formulas) { - performParameterLifting(markovModel, formula); - } - } - - template - std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - switch(storm::settings::getModule().getEngine()) { - case storm::settings::modules::CoreSettings::Engine::Sparse: { - std::shared_ptr> sparseModel = model->template as>(); - STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model."); - return (sparseModel, formula, onlyInitialStatesRelevant); - } - case storm::settings::modules::CoreSettings::Engine::Hybrid: { - std::shared_ptr> ddModel = model->template as>(); - STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a DD-based input model."); - return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant); - } - case storm::settings::modules::CoreSettings::Engine::Dd: { - std::shared_ptr> ddModel = model->template as>(); - STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a DD-based input model."); - return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant); - } - default: { - STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built."); - } - } - } - - template - std::unique_ptr verifySparseDtmc(std::shared_ptr> dtmc, storm::modelchecker::CheckTask const& task) { - std::unique_ptr result; - if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported by the dedicated elimination model checker."); - } - } else { - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } - } - return result; - } - - template - std::unique_ptr verifySparseCtmc(std::shared_ptr> ctmc, storm::modelchecker::CheckTask const& task) { - std::unique_ptr result; - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } - return result; - } - - template - std::unique_ptr verifySparseMdp(std::shared_ptr> mdp, storm::modelchecker::CheckTask const& task) { - std::unique_ptr result; - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } - return result; - } - - template - std::unique_ptr verifySparseMarkovAutomaton(std::shared_ptr> ma, storm::modelchecker::CheckTask const& task) { - std::unique_ptr result; - // Close the MA, if it is not already closed. - if (!ma->isClosed()) { - ma->close(); - } - storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << task.getFormula() << " is not supported."); - } - return result; - } - - template - std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - result = verifySparseDtmc(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::Mdp) { - result = verifySparseMdp(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::Ctmc) { - result = verifySparseCtmc(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { - result = verifySparseMarkovAutomaton(model->template as>(), task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported."); - } - return result; - } - -#ifdef STORM_HAVE_CARL - template<> - inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - result = verifySparseDtmc(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::Ctmc) { - result = verifySparseCtmc(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::Mdp) { - result = verifySparseMdp(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { - result = verifySparseMarkovAutomaton(model->template as>(), task); - } else { - STORM_LOG_ASSERT(false, "Illegal model type."); - } - return result; - } - - inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { - std::ofstream filestream; - storm::utility::openFile(path, filestream); - 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::vector stringConstraints; - std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); - std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); - filestream << "!Graph-preserving Constraints: " << std::endl; - stringConstraints.clear(); - std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); - std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); - storm::utility::closeFile(filestream); - } - - template<> - inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - result = verifySparseDtmc(model->template as>(), task); - } else if (model->getType() == storm::models::ModelType::Mdp) { - //std::shared_ptr> mdp = model->template as>(); - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support MDPs."); - } else if (model->getType() == storm::models::ModelType::Ctmc) { - result = verifySparseCtmc(model->template as>(), task); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support " << model->getType()); - } - return result; - } -#endif - - template - std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - std::unique_ptr result; - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::HybridMdpPrctlModelChecker> modelchecker(*mdp); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); - } - return result; - } - - template - std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - std::unique_ptr result; - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - - STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::NotSupportedException, "Only DTMCs are supported by this engine (in parametric mode)."); - std::shared_ptr> dtmc = model->template as>(); - - if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { - storm::transformer::SymbolicDtmcToSparseDtmcTransformer transformer; - std::shared_ptr> sparseDtmc = transformer.translate(*dtmc); - - // Optimally, we could preprocess the model here and apply, for example, bisimulation minimization. However, - // with the current structure of functions in storm.h and entrypoints.h this is not possible, because later - // the filters will be applied wrt. to states of the original model, which is problematic. - // sparseDtmc = preprocessModel>(sparseDtmc, {formula})->template as>(); - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*sparseDtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - - // Now translate the sparse result to hybrid one, so it can be filtered with the symbolic initial states of the model later. - if (result->isQualitative()) { - storm::modelchecker::ExplicitQualitativeCheckResult const& explicitResult = result->asExplicitQualitativeCheckResult(); - - if (explicitResult.isResultForAllStates()) { - result = std::make_unique>(model->getReachableStates(), storm::dd::Bdd::fromVector(model->getManager(), explicitResult.getTruthValuesVector(), transformer.getOdd(), model->getRowVariables())); - } else { - storm::dd::Odd oldOdd = transformer.getOdd(); - storm::dd::Odd newOdd = model->getInitialStates().createOdd(); - storm::storage::BitVector tmp(oldOdd.getTotalOffset()); - for (auto const& entry : explicitResult.getTruthValuesMap()) { - tmp.set(entry.first, entry.second); - } - result = std::make_unique>(model->getReachableStates(), storm::dd::Bdd::fromVector(model->getManager(), tmp, oldOdd, model->getRowVariables())); - } - } else if (result->isQuantitative()) { - storm::modelchecker::ExplicitQuantitativeCheckResult const& explicitResult = result->asExplicitQuantitativeCheckResult(); - - if (explicitResult.isResultForAllStates()) { - result = std::make_unique>(model->getReachableStates(), model->getManager().getBddZero(), model->getManager().template getAddZero(), model->getReachableStates(), transformer.getOdd(), explicitResult.getValueVector()); - } else { - storm::dd::Odd oldOdd = transformer.getOdd(); - storm::dd::Odd newOdd = model->getInitialStates().createOdd(); - std::vector tmp(oldOdd.getTotalOffset(), storm::utility::zero()); - for (auto const& entry : explicitResult.getValueMap()) { - tmp[entry.first] = entry.second; - } - std::vector newValues = model->getInitialStates().filterExplicitVector(oldOdd, tmp); - result = std::make_unique>(model->getReachableStates(), model->getManager().getBddZero(), model->getManager().template getAddZero(), model->getInitialStates(), newOdd, newValues); - } - } - } - } else { - storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } - } - - return result; - } - - template - std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - std::unique_ptr result; - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> modelchecker(*mdp); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); - } - return result; - } - - template - std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - std::unique_ptr result; - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - - STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::NotSupportedException, "Only DTMCs are supported by this engine (in parametric mode)."); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } - return result; - } - - template - void exportMatrixToFile(std::shared_ptr> model, std::string const& filepath) { - STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); - std::ofstream stream; - storm::utility::openFile(filepath, stream); - model->getTransitionMatrix().printAsMatlabMatrix(stream); - storm::utility::closeFile(stream); - } - -} - -#endif /* STORM_H */ diff --git a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp index c087a8a93..0c932d0c8 100644 --- a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp +++ b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp @@ -11,10 +11,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" - -#include "storm/utility/storm.h" +#include "storm/api/storm.h" #if defined STORM_HAVE_MSAT TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) { @@ -23,7 +20,7 @@ TEST(GameBasedMdpModelCheckerTest, DISABLED_Dice_Cudd) { #endif std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"; - storm::prism::Program program = storm::parseProgram(programFile); + storm::prism::Program program = storm::api::parseProgram(programFile); // Build the die model typename storm::builder::DdPrismModelBuilder::Options options; @@ -94,7 +91,7 @@ TEST(GameBasedMdpModelCheckerTest, DISABLED_Dice_Sylvan) { #endif std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"; - storm::prism::Program program = storm::parseProgram(programFile); + storm::prism::Program program = storm::api::parseProgram(programFile); // Build the die model typename storm::builder::DdPrismModelBuilder::Options options; diff --git a/src/test/utility/ModelInstantiatorTest.cpp b/src/test/utility/ModelInstantiatorTest.cpp index 2f317a16d..07859c600 100644 --- a/src/test/utility/ModelInstantiatorTest.cpp +++ b/src/test/utility/ModelInstantiatorTest.cpp @@ -11,7 +11,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" -#include "utility/storm.h" +#include "storm/api/storm.h" #include "utility/ModelInstantiator.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" @@ -24,9 +24,9 @@ TEST(ModelInstantiatorTest, BrpProb) { std::string formulaAsString = "P=? [F s=5 ]"; // Program and formula - storm::prism::Program program = storm::parseProgram(programFile); + storm::prism::Program program = storm::api::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front()); @@ -142,9 +142,9 @@ TEST(ModelInstantiatorTest, Brp_Rew) { std::string formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]"; // Program and formula - storm::prism::Program program = storm::parseProgram(programFile); + storm::prism::Program program = storm::api::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front()); @@ -212,9 +212,9 @@ TEST(ModelInstantiatorTest, Consensus) { std::string formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]"; // Program and formula - storm::prism::Program program = storm::parseProgram(programFile); + storm::prism::Program program = storm::api::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); ASSERT_TRUE(formulas.size()==1); // Parametric model storm::generator::NextStateGeneratorOptions options(*formulas.front());