From e6fc962e5ea45749440e38c4cff94b8a5edc3b8d Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 23 Oct 2018 17:07:47 +0200 Subject: [PATCH 01/17] In exact mode, use LP as LRA Method for nondeterministic models. --- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 8 +++++++- .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 8 +++++++- src/storm/settings/modules/CoreSettings.cpp | 4 ++++ src/storm/settings/modules/CoreSettings.h | 7 +++++++ .../settings/modules/MinMaxEquationSolverSettings.cpp | 4 ++++ src/storm/settings/modules/MinMaxEquationSolverSettings.h | 5 +++++ src/storm/utility/solver.cpp | 6 +++++- 7 files changed, 39 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 6e6a39acf..1975ebf45 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -16,6 +16,7 @@ #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/utility/graph.h" +#include "storm/utility/NumberTraits.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" @@ -824,7 +825,12 @@ namespace storm { } // Solve MEC with the method specified in the settings - storm::solver::LraMethod method = storm::settings::getModule().getLraMethod(); + auto minMaxSettings = storm::settings::getModule(); + storm::solver::LraMethod method = minMaxSettings.getLraMethod(); + if (storm::NumberTraits::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) { + STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); + method = storm::solver::LraMethod::LinearProgramming; + } if (method == storm::solver::LraMethod::LinearProgramming) { return computeLraForMaximalEndComponentLP(env, dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec); } else if (method == storm::solver::LraMethod::ValueIteration) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 81c53dfd9..8c7b93738 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -34,6 +34,7 @@ #include "storm/utility/Stopwatch.h" #include "storm/utility/ProgressMeasurement.h" #include "storm/utility/export.h" +#include "storm/utility/NumberTraits.h" #include "storm/transformer/EndComponentEliminator.h" @@ -1478,7 +1479,12 @@ namespace storm { } // Solve MEC with the method specified in the settings - storm::solver::LraMethod method = storm::settings::getModule().getLraMethod(); + auto minMaxSettings = storm::settings::getModule(); + storm::solver::LraMethod method = minMaxSettings.getLraMethod(); + if (storm::NumberTraits::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) { + STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); + method = storm::solver::LraMethod::LinearProgramming; + } if (method == storm::solver::LraMethod::LinearProgramming) { return computeLraForMaximalEndComponentLP(env, dir, transitionMatrix, rewardModel, mec); } else if (method == storm::solver::LraMethod::ValueIteration) { diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 343d3c3d1..3925012e3 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -112,6 +112,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); } + bool CoreSettings::isLpSolverSetFromDefaultValue() const { + return !this->getOption(lpSolverOptionName).getHasOptionBeenSet() || this->getOption(lpSolverOptionName).getArgumentByName("name").wasSetFromDefaultValue(); + } + storm::solver::SmtSolverType CoreSettings::getSmtSolver() const { std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString(); if (smtSolverName == "z3") { diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index 8a07a48d0..483e61df3 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -94,6 +94,13 @@ namespace storm { * @return The selected LP solver. */ storm::solver::LpSolverType getLpSolver() const; + + /*! + * Retrieves whether the lp solver has been set from its default value. + * + * @return True iff it has been set from its default value. + */ + bool isLpSolverSetFromDefaultValue() const; /*! * Retrieves the selected SMT solver. diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index d0e891b56..0a2943efd 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -111,6 +111,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown lra solving technique '" << lraMethodString << "'."); } + bool MinMaxEquationSolverSettings::isLraMethodSetFromDefaultValue() const { + return !this->getOption(lraMethodOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(lraMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue(); + } + MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod MinMaxEquationSolverSettings::getMarkovAutomatonBoundedReachabilityMethod() const { std::string techniqueAsString = this->getOption(markovAutomatonBoundedReachabilityMethodOptionName).getArgumentByName("name").getValueAsString(); if (techniqueAsString == "imca") { diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index 43d3d1b00..2b958d374 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -93,6 +93,11 @@ namespace storm { */ storm::solver::LraMethod getLraMethod() const; + /*! + * Retrieves whether the LraMethod was set from a default value. + */ + bool isLraMethodSetFromDefaultValue() const; + /*! * Retrieves the method to be used for bounded reachability on MAs. * diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 6955f5eed..34982374e 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -15,6 +15,7 @@ #include "storm/solver/MathsatSmtSolver.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/NumberTraits.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -25,8 +26,11 @@ namespace storm { template std::unique_ptr> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; - if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { + if (solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { t = storm::settings::getModule().getLpSolver(); + if (storm::NumberTraits::IsExact && t != storm::solver::LpSolverType::Z3 && storm::settings::getModule().isLpSolverSetFromDefaultValue()) { + t = storm::solver::LpSolverType::Z3; + } } else { t = convert(solvT); } From 7038858379722642218abbe121aab8bdf88bf10c Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 24 Oct 2018 18:08:08 +0200 Subject: [PATCH 02/17] storm-conv: Added ability to make global variables of a jani model local (or vice versa) --- src/storm-conv/api/storm-conv.cpp | 20 +++ .../options/JaniConversionOptions.cpp | 4 +- .../converter/options/JaniConversionOptions.h | 6 + .../settings/modules/JaniExportSettings.cpp | 6 + .../settings/modules/JaniExportSettings.h | 3 + .../storage/jani/JaniLocationExpander.cpp | 2 - src/storm/storage/jani/JaniScopeChanger.cpp | 164 ++++++++++++++++++ src/storm/storage/jani/JaniScopeChanger.h | 57 ++++++ src/storm/storage/jani/LValue.cpp | 15 +- src/storm/storage/jani/Property.cpp | 20 +++ src/storm/storage/jani/Property.h | 3 + src/storm/storage/jani/VariableSet.cpp | 45 +++++ src/storm/storage/jani/VariableSet.h | 5 + 13 files changed, 343 insertions(+), 7 deletions(-) create mode 100644 src/storm/storage/jani/JaniScopeChanger.cpp create mode 100644 src/storm/storage/jani/JaniScopeChanger.h diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index ddbe8abb2..9b747fe2c 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -4,6 +4,7 @@ #include "storm/storage/jani/Property.h" #include "storm/storage/jani/Constant.h" #include "storm/storage/jani/JaniLocationExpander.h" +#include "storm/storage/jani/JaniScopeChanger.h" #include "storm/storage/jani/JSONExporter.h" #include "storm/settings/SettingsManager.h" @@ -18,7 +19,26 @@ namespace storm { janiModel = janiModel.substituteConstants(); } + if (options.localVars) { + STORM_LOG_WARN_COND(!options.globalVars, "Ignoring 'globalvars' option, since 'localvars' is also set."); + storm::jani::JaniScopeChanger().makeVariablesLocal(janiModel, properties); + } else if (options.globalVars) { + storm::jani::JaniScopeChanger().makeVariablesGlobal(janiModel); + } + if (!options.locationVariables.empty()) { + // Make variables local if necessary/possible + for (auto const& pair : options.locationVariables) { + if (janiModel.hasGlobalVariable(pair.second)) { + auto var = janiModel.getGlobalVariable(pair.second).getExpressionVariable(); + if (storm::jani::JaniScopeChanger().canMakeVariableLocal(var, janiModel, properties, janiModel.getAutomatonIndex(pair.first)).first) { + storm::jani::JaniScopeChanger().makeVariableLocal(var, janiModel, janiModel.getAutomatonIndex(pair.first)); + } else { + STORM_LOG_ERROR("Can not transform variable " << pair.second << " into locations since it can not be made local to automaton " << pair.first << "."); + } + } + } + for (auto const& pair : options.locationVariables) { storm::jani::JaniLocationExpander expander(janiModel); expander.transform(pair.first, pair.second); diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index df6eed905..e4df3bf5b 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.cpp +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -3,11 +3,11 @@ namespace storm { namespace converter { - JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { + JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { // Intentionally left empty } - JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { + JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { if (settings.isEliminateFunctionsSet()) { allowedModelFeatures.remove(storm::jani::ModelFeature::Functions); } diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h index f0fc6e62c..8ecf1ca56 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.h +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -27,6 +27,12 @@ namespace storm { /// If set, constants in expressions are substituted with their definition bool substituteConstants; + /// If set, variables will be made local wherever possible + bool localVars; + + /// If set, variables will be made global wherever possible + bool globalVars; + /// If given, the model will get this name boost::optional modelName; diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp index 207de8edb..11fb061cf 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.cpp +++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string JaniExportSettings::exportFlattenOptionName = "flatten"; const std::string JaniExportSettings::locationVariablesOptionName = "location-variables"; const std::string JaniExportSettings::globalVariablesOptionName = "globalvars"; + const std::string JaniExportSettings::localVariablesOptionName = "localvars"; const std::string JaniExportSettings::compactJsonOptionName = "compactjson"; const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays"; const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions"; @@ -27,6 +28,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, edgeAssignmentsOptionName, false, "If set, the output model can have transient edge assignments. This can simplify the jani model but is not compliant to the jani standard.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build()); this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, localVariablesOptionName, false, "If set, variables will preferably be made local.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, eliminateArraysOptionName, false, "If set, transforms the model such that array variables/expressions are eliminated.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build()); @@ -64,6 +66,10 @@ namespace storm { return this->getOption(globalVariablesOptionName).getHasOptionBeenSet(); } + bool JaniExportSettings::isLocalVarsSet() const { + return this->getOption(localVariablesOptionName).getHasOptionBeenSet(); + } + bool JaniExportSettings::isCompactJsonSet() const { return this->getOption(compactJsonOptionName).getHasOptionBeenSet(); } diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h index 04952e9fd..469ef6b71 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.h +++ b/src/storm-conv/settings/modules/JaniExportSettings.h @@ -22,6 +22,8 @@ namespace storm { bool isGlobalVarsSet() const; + bool isLocalVarsSet() const; + bool isCompactJsonSet() const; bool isEliminateArraysSet() const; @@ -40,6 +42,7 @@ namespace storm { static const std::string exportFlattenOptionName; static const std::string locationVariablesOptionName; static const std::string globalVariablesOptionName; + static const std::string localVariablesOptionName; static const std::string compactJsonOptionName; static const std::string eliminateArraysOptionName; static const std::string eliminateFunctionsOptionName; diff --git a/src/storm/storage/jani/JaniLocationExpander.cpp b/src/storm/storage/jani/JaniLocationExpander.cpp index 8c06fb3c1..bb94a5de4 100644 --- a/src/storm/storage/jani/JaniLocationExpander.cpp +++ b/src/storm/storage/jani/JaniLocationExpander.cpp @@ -67,10 +67,8 @@ namespace storm { for (int64_t i = variableLowerBound; i <= variableUpperBound; i++) { std::string newLocationName = loc.getName() + "_" + variableName + "_" + std::to_string(i); substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(i); - std::cout << "eliminate " << eliminatedExpressionVariable.getName() << " with " << i << std::endl; OrderedAssignments newAssignments = loc.getAssignments().clone(); newAssignments.substitute(substitutionMap); - std::cout << newAssignments << std::endl; uint64_t newLocationIndex = newAutomaton.addLocation(Location(newLocationName, newAssignments)); locationVariableValueMap[origIndex][i] = newLocationIndex; diff --git a/src/storm/storage/jani/JaniScopeChanger.cpp b/src/storm/storage/jani/JaniScopeChanger.cpp new file mode 100644 index 000000000..752dc033e --- /dev/null +++ b/src/storm/storage/jani/JaniScopeChanger.cpp @@ -0,0 +1,164 @@ +#include "storm/storage/jani/JaniScopeChanger.h" + +#include +#include +#include + +#include "storm/storage/expressions/Variable.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" +#include "storm/storage/jani/traverser/JaniTraverser.h" + +namespace storm { + namespace jani { + + namespace detail { + class VariableAccessedTraverser : public ConstJaniTraverser { + public: + VariableAccessedTraverser(std::set const& varSet) : varSet(varSet) { + // Intentionally left empty + } + using ConstJaniTraverser::traverse; + + virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) override { + bool* result = boost::any_cast(data); + if (*result) { return; } + *result = expression.containsVariable(varSet); + } + + private: + std::set const& varSet; + }; + + std::set getAutomataAccessingVariable(storm::expressions::Variable const& variable, Model const& model) { + std::set res; + for (uint64_t i = 0; i < model.getNumberOfAutomata(); ++i) { + if (model.getAutomaton(i).getVariables().hasVariable(variable)) { + res.insert(i); + } else { + VariableAccessedTraverser vat({variable}); + bool varAccessed = false; + vat.traverse(model.getAutomaton(i), &varAccessed); + if (varAccessed) { + res.insert(i); + } + } + } + return res; + } + } + + void JaniScopeChanger::makeVariableGlobal(storm::expressions::Variable const& variable, Model& model) const { + uint64_t automatonIndex = 0; + for (; automatonIndex < model.getNumberOfAutomata(); ++automatonIndex) { + if (model.getAutomaton(automatonIndex).getVariables().hasVariable(variable)) { + break; + } + } + std::map> remapping; + auto oldJaniVar = model.getAutomaton(automatonIndex).getVariables().eraseVariable(variable); + remapping.emplace(oldJaniVar.get(), model.addVariable(*oldJaniVar)); + + // Only one automaton accesses this variable + model.getAutomaton(automatonIndex).changeAssignmentVariables(remapping); + } + + void JaniScopeChanger::makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const { + std::map> remapping; + auto oldJaniVar = model.getGlobalVariables().eraseVariable(variable); + remapping.emplace(oldJaniVar.get(), model.getAutomaton(automatonIndex).addVariable(*oldJaniVar)); + // Only one automaton accesses this variable (otherwise this call would be illegal) + model.getAutomaton(automatonIndex).changeAssignmentVariables(remapping); + } + + bool JaniScopeChanger::canMakeVariableGlobal(storm::expressions::Variable const& variable, Model const& model) const { + if (model.hasGlobalVariable(variable.getName())) { + return false; + } + // Check whether there are multiple local variables with this name + bool foundVar = false; + for (auto const& aut : model.getAutomata()) { + if (aut.hasVariable(variable.getName())) { + if (foundVar) { + return false; + } + foundVar = true; + } + } + return foundVar; + } + + std::pair JaniScopeChanger::canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model, std::vector const& properties, boost::optional automatonIndex) const { + uint64_t index = model.getNumberOfAutomata(); + + if (!model.getGlobalVariables().hasVariable(variable)) { + return {false, index}; + } + + auto accessingAutomata = detail::getAutomataAccessingVariable(variable, model); + if (accessingAutomata.size() > 1 || (automatonIndex.is_initialized() && accessingAutomata.count(automatonIndex.get()) == 0)) { + return {false, index}; + } + if (model.getInitialStatesRestriction().containsVariable({variable})) { + return {false, index}; + } + for (auto const& rewExp : model.getNonTrivialRewardExpressions()) { + if (rewExp.second.containsVariable({variable})) { + return {false, index}; + } + } + for (auto const& funDef : model.getGlobalFunctionDefinitions()) { + if (funDef.second.getFunctionBody().containsVariable({variable})) { + return {false, index}; + } + } + for (auto const& p : properties) { + if (p.getUsedVariablesAndConstants().count(variable) > 0) { + return {false, index}; + } + if (p.getUsedLabels().count(variable.getName()) > 0) { + return {false, index}; + } + } + + if (accessingAutomata.empty()) { + index = automatonIndex.is_initialized() ? automatonIndex.get() : 0; + } else { + index = *accessingAutomata.begin(); + assert(!automatonIndex.is_initialized() || index == automatonIndex.get()); + } + return {true, index}; + } + + void JaniScopeChanger::makeVariablesGlobal(Model& model) const { + for (uint64_t i = 0; i < model.getNumberOfAutomata(); ++i) { + // Make sure to not erase from a set while iterating over it... + std::set varsToMakeGlobal; + for (auto const& v : model.getAutomaton(i).getVariables()) { + if (canMakeVariableGlobal(v.getExpressionVariable(), model)) { + varsToMakeGlobal.insert(v.getExpressionVariable()); + } + } + for (auto const& v : varsToMakeGlobal) { + makeVariableGlobal(v, model); + } + } + } + + void JaniScopeChanger::makeVariablesLocal(Model& model, std::vector const& properties) const { + // Make sure to not erase from a set while iterating over it... + std::map varsToMakeLocal; + for (auto const& v : model.getGlobalVariables()) { + auto makeLocal = canMakeVariableLocal(v.getExpressionVariable(), model, properties); + if (makeLocal.first) { + varsToMakeLocal[v.getExpressionVariable()] = makeLocal.second; + } + } + for (auto const& v : varsToMakeLocal) { + makeVariableLocal(v.first, model, v.second); + } + } + + } + +} diff --git a/src/storm/storage/jani/JaniScopeChanger.h b/src/storm/storage/jani/JaniScopeChanger.h new file mode 100644 index 000000000..b948506af --- /dev/null +++ b/src/storm/storage/jani/JaniScopeChanger.h @@ -0,0 +1,57 @@ +#pragma once + +#include +#include + +namespace storm { + + namespace expressions { + class Variable; + } + + namespace jani { + + class Model; + class Property; + + class JaniScopeChanger { + public: + JaniScopeChanger() = default; + + /*! + * Moves the given variable to the global scope. + * It is *not* checked whether this introduces name clashes + */ + void makeVariableGlobal(storm::expressions::Variable const& variable, Model& model) const; + + /*! + * Moves the given variable into the local scope of the automaton with the given index. + * It is *not* checked whether this introduces out-of-scope accesses. + */ + void makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const; + + /*! + * Checks whether this variable can be made global without introducing name clashes. + */ + bool canMakeVariableGlobal(storm::expressions::Variable const& variable, Model const& model) const; + + /*! + * Checks whether this variable can be made local without introducing out-of-scope accesses. + * Returns true if this is a case as well as an automaton index where to pout the variable + */ + std::pair canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model, std::vector const& properties = {}, boost::optional automatonIndex = boost::none) const; + + /*! + * Moves as many variables to the global scope as possible + */ + void makeVariablesGlobal(Model& model) const; + + /*! + * Moves as many variables to a local scope as possible + */ + void makeVariablesLocal(Model& model, std::vector const& properties = {}) const; + + }; + } + +} diff --git a/src/storm/storage/jani/LValue.cpp b/src/storm/storage/jani/LValue.cpp index 57d80bfdd..a8aefe037 100644 --- a/src/storm/storage/jani/LValue.cpp +++ b/src/storm/storage/jani/LValue.cpp @@ -50,14 +50,23 @@ namespace storm { LValue LValue::changeAssignmentVariables(std::map> const& remapping) const { if (isVariable()) { - return LValue(remapping.at(variable)); + auto it = remapping.find(variable); + if (it == remapping.end()) { + return *this; + } else { + return LValue(it->second); + } } else { STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue."); - return LValue(LValue(remapping.at(variable)), arrayIndex); + auto it = remapping.find(variable); + if (it == remapping.end()) { + return *this; + } else { + return LValue(LValue(it->second), arrayIndex); + } } } - bool LValue::operator<(LValue const& other) const { if (isVariable()) { return !other.isVariable() || variable->getExpressionVariable() < other.getVariable().getExpressionVariable(); diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index 5a1c50023..999968e12 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -70,6 +70,26 @@ namespace storm { bool Property::containsUndefinedConstants() const { return !undefinedConstants.empty(); } + + std::set Property::getUsedVariablesAndConstants() const { + auto res = getUndefinedConstants(); + getFilter().getFormula()->gatherUsedVariables(res); + getFilter().getStatesFormula()->gatherUsedVariables(res); + return res; + } + + std::set Property::getUsedLabels() const { + std::set res; + auto labFormSet = getFilter().getFormula()->getAtomicLabelFormulas(); + for (auto const& f : labFormSet) { + res.insert(f->getLabel()); + } + labFormSet = getFilter().getStatesFormula()->getAtomicLabelFormulas(); + for (auto const& f : labFormSet) { + res.insert(f->getLabel()); + } + return res; + } std::ostream& operator<<(std::ostream& os, Property const& p) { return os << "(" << p.getName() << "): " << p.getFilter(); diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 2d1d88d70..249920f36 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -129,8 +129,11 @@ namespace storm { std::set const& getUndefinedConstants() const; bool containsUndefinedConstants() const; + std::set getUsedVariablesAndConstants() const; + std::set getUsedLabels() const; std::shared_ptr getRawFormula() const; + private: std::string name; std::string comment; diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index 83ef34bdb..65725888c 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -196,6 +196,51 @@ namespace storm { return getVariable(it->second); } + template + void eraseFromVariableVector(std::vector>& varVec, storm::expressions::Variable const& variable) { + for (auto vIt = varVec.begin(); vIt != varVec.end(); ++vIt) { + if ((*vIt)->getExpressionVariable() == variable) { + varVec.erase(vIt); + break; + } + } + } + + std::shared_ptr VariableSet::eraseVariable(storm::expressions::Variable const& variable) { + auto vToVIt = variableToVariable.find(variable); + STORM_LOG_THROW(vToVIt != variableToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to erase unknown variable '" << variable.getName() << "'."); + std::shared_ptr janiVar = std::move(vToVIt->second); + variableToVariable.erase(vToVIt); + + nameToVariable.erase(variable.getName()); + eraseFromVariableVector(variables, variable); + if (janiVar->isBooleanVariable()) { + eraseFromVariableVector(booleanVariables, variable); + } + if (janiVar->isBooleanVariable()) { + eraseFromVariableVector(booleanVariables, variable); + } + if (janiVar->isBoundedIntegerVariable()) { + eraseFromVariableVector(boundedIntegerVariables, variable); + } + if (janiVar->isUnboundedIntegerVariable()) { + eraseFromVariableVector(unboundedIntegerVariables, variable); + } + if (janiVar->isRealVariable()) { + eraseFromVariableVector(realVariables, variable); + } + if (janiVar->isArrayVariable()) { + eraseFromVariableVector(arrayVariables, variable); + } + if (janiVar->isClockVariable()) { + eraseFromVariableVector(clockVariables, variable); + } + if (janiVar->isTransient()) { + eraseFromVariableVector(transientVariables, variable); + } + return janiVar; + } + typename detail::Variables::iterator VariableSet::begin() { return detail::Variables::make_iterator(variables.begin()); } diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h index af63c949d..7a428ba16 100644 --- a/src/storm/storage/jani/VariableSet.h +++ b/src/storm/storage/jani/VariableSet.h @@ -153,6 +153,11 @@ namespace storm { * Retrieves the variable object associated with the given expression variable (if any). */ Variable const& getVariable(storm::expressions::Variable const& variable) const; + + /*! + * Erases the given variable from this set. + */ + std::shared_ptr eraseVariable(storm::expressions::Variable const& variable); /*! * Retrieves whether this variable set contains a transient variable. From c27b8af90f1a5c94faf9d2ba409c96cef4ea1722 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 25 Oct 2018 13:47:24 +0200 Subject: [PATCH 03/17] Display the time required for parsing the prism/jani input --- src/storm-cli-utilities/model-handling.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 815f80128..beba289d1 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -61,6 +61,7 @@ namespace storm { void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, storm::builder::BuilderType const& builderType) { if (ioSettings.isPrismOrJaniInputSet()) { + storm::utility::Stopwatch modelParsingWatch(true); if (ioSettings.isPrismInputSet()) { input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule().isPrismCompatibilityEnabled()); } else { @@ -81,6 +82,8 @@ namespace storm { input.properties = std::move(janiInput.second); } } + modelParsingWatch.stop(); + STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl); } } From 003922a9e4c9ca6162d43e48cd9e245f0adaa1af Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 25 Oct 2018 14:25:33 +0200 Subject: [PATCH 04/17] Fixed optimization direction when exporting standard petri net properties to jani --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index a8669b1b8..21dfc6264 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -296,7 +296,7 @@ namespace storm { auto expTimeDeadlock = std::make_shared( std::make_shared(deadlock, storm::logic::FormulaContext::Time), - storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); + storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Minimize)); standardProperties.emplace_back("MinExpTimeDeadlock", expTimeDeadlock, emptyVariableSet, "The minimal expected time to reach a deadlock."); } From 9be488b9698e11fdf3f654f7a4d19e6960d08c9c Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 25 Oct 2018 14:48:21 +0200 Subject: [PATCH 05/17] Enabling expected time queries for ctmcs in the hybrid engine. --- .../csl/HybridCtmcCslModelChecker.cpp | 17 ++++++++++++++--- .../csl/HybridCtmcCslModelChecker.h | 1 + .../csl/SparseCtmcCslModelChecker.cpp | 2 +- 3 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index b7b71dfaa..6e41f2782 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -7,6 +7,7 @@ #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" @@ -30,14 +31,14 @@ namespace storm { template::SupportsExponential, int>::type> bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true)); } template template::SupportsExponential, int>::type> bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); } template @@ -60,7 +61,6 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeNextProbabilities(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); } - template std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); @@ -70,6 +70,17 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } + template + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); + SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); + + storm::models::symbolic::StandardRewardModel timeRewardModel(this->getModel().getManager().getConstant(storm::utility::one()), boost::none, boost::none); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), timeRewardModel, subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + } + + template std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h index f66f3c10e..eaa55d42e 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -32,6 +32,7 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: template::SupportsExponential, int>::type = 0> diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 08fc02cad..cf2aa5bcb 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -44,7 +44,7 @@ namespace storm { template::SupportsExponential, int>::type> bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false)); } template From f601405d55cc1b6a5a146aa46b51df70ce5f18e9 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 11 Oct 2018 10:20:49 +0200 Subject: [PATCH 06/17] set edge color default to zero --- src/storm/storage/jani/Edge.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index 5af6ec38d..35864b85b 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -163,7 +163,7 @@ namespace storm { std::vector destinations; /// The color of the edge, used to persistently mark and identify specific edges (by the user) - uint64_t color; + uint64_t color = 0; }; std::ostream& operator<<(std::ostream& stream, Edge const& edge); From 9a0794fca1b2a63d79e2bb34109c674886166c0b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 25 Oct 2018 19:11:27 +0200 Subject: [PATCH 07/17] refined error message wrt unexpected type of scheduler --- .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 8c7b93738..eb90df88d 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1277,7 +1277,11 @@ namespace storm { } // Sanity check for created scheduler. - STORM_LOG_ASSERT((!produceScheduler && !scheduler) || (!scheduler->isPartialScheduler() && scheduler->isDeterministicScheduler() && scheduler->isMemorylessScheduler()), "Unexpected format of obtained scheduler."); + STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained."); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); + return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } From 07588df1376364c76ab300cae4abc907fe4ff52c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 25 Oct 2018 19:12:17 +0200 Subject: [PATCH 08/17] operators to remove bounds / optimality types from a formula --- src/storm/logic/OperatorFormula.cpp | 12 ++++++++++++ src/storm/logic/OperatorFormula.h | 9 +++++++-- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/src/storm/logic/OperatorFormula.cpp b/src/storm/logic/OperatorFormula.cpp index a86e5a47a..890d5476c 100644 --- a/src/storm/logic/OperatorFormula.cpp +++ b/src/storm/logic/OperatorFormula.cpp @@ -60,6 +60,10 @@ namespace storm { void OperatorFormula::setBound(Bound const& newBound) { operatorInformation.bound = newBound; } + + void OperatorFormula::removeBound() { + operatorInformation.bound = boost::none; + } bool OperatorFormula::hasOptimalityType() const { return static_cast(operatorInformation.optimalityType); @@ -68,6 +72,14 @@ namespace storm { OptimizationDirection const& OperatorFormula::getOptimalityType() const { return operatorInformation.optimalityType.get(); } + + void OperatorFormula::setOptimalityType(storm::solver::OptimizationDirection newOptimalityType) { + operatorInformation.optimalityType = newOptimalityType; + } + + void OperatorFormula::removeOptimalityType() { + operatorInformation.optimalityType = boost::none; + } bool OperatorFormula::isOperatorFormula() const { return true; diff --git a/src/storm/logic/OperatorFormula.h b/src/storm/logic/OperatorFormula.h index a396f21ac..c4d3067fb 100644 --- a/src/storm/logic/OperatorFormula.h +++ b/src/storm/logic/OperatorFormula.h @@ -30,18 +30,23 @@ namespace storm { // Bound-related accessors. bool hasBound() const; + Bound const& getBound() const; + void setBound(Bound const& newBound); + void removeBound(); + ComparisonType getComparisonType() const; void setComparisonType(ComparisonType newComparisonType); storm::expressions::Expression const& getThreshold() const; template ValueType getThresholdAs() const; void setThreshold(storm::expressions::Expression const& newThreshold); - Bound const& getBound() const; - void setBound(Bound const& newBound); + // Optimality-type-related accessors. bool hasOptimalityType() const; storm::solver::OptimizationDirection const& getOptimalityType() const; + void setOptimalityType(storm::solver::OptimizationDirection newOptimalityType); + void removeOptimalityType(); virtual bool isOperatorFormula() const override; OperatorInformation const& getOperatorInformation() const; From 5d0ec15ad426d4d8ee302abe7e5c8a0590a99610 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 25 Oct 2018 20:16:40 +0200 Subject: [PATCH 09/17] clarified error message, as the reward models are present (according to output) but simply empty --- src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 2 +- src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index eb90df88d..4821d9ea3 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -919,7 +919,7 @@ namespace storm { template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) { // Only compute the result if the model has at least one reward this->getModel(). - STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Reward model for formula is empty. Skipping formula."); return computeReachabilityRewardsHelper(env, std::move(goal), transitionMatrix, backwardTransitions, [&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 5080d90a8..f52d7eb17 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -202,7 +202,7 @@ namespace storm { template std::unique_ptr SymbolicMdpPrctlHelper::computeCumulativeRewards(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound) { // Only compute the result if the model has at least one reward this->getModel(). - STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Reward model for formula is empty. Skipping formula."); // Compute the reward vector to add in each step based on the available reward models. storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables()); From 16d7dccb4ee6ef8373376bb39263419084683436 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 26 Oct 2018 10:50:22 +0200 Subject: [PATCH 10/17] I am utterly stupid. Fixed an assertion that I changed yesterday --- src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 4821d9ea3..3b1d9954b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1279,8 +1279,8 @@ namespace storm { // Sanity check for created scheduler. STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained."); STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler"); - STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler"); - STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); From 602d18d8446d0e7f77048ccf792a6257e1048a53 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 Oct 2018 12:11:19 +0200 Subject: [PATCH 11/17] Fixed parsing of edge assignments. --- src/storm-parsers/parser/JaniParser.cpp | 26 ++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 1459a9259..4065d89c6 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -1416,7 +1416,7 @@ namespace storm { STORM_LOG_THROW(automatonStructure.count("edges") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' must have a list of edges"); - for(auto const& edgeEntry : automatonStructure.at("edges")) { + for (auto const& edgeEntry : automatonStructure.at("edges")) { // source location STORM_LOG_THROW(edgeEntry.count("location") == 1, storm::exceptions::InvalidJaniException, "Each edge in automaton '" << name << "' must have a source"); std::string sourceLoc = getString(edgeEntry.at("location"), "source location for edge in automaton '" + name + "'"); @@ -1441,15 +1441,35 @@ namespace storm { // guard STORM_LOG_THROW(edgeEntry.count("guard") <= 1, storm::exceptions::InvalidJaniException, "Guard can be given at most once in edge from '" << sourceLoc << "' in automaton '" << name << "'"); storm::expressions::Expression guardExpr = expressionManager->boolean(true); - if(edgeEntry.count("guard") == 1) { + if (edgeEntry.count("guard") == 1) { STORM_LOG_THROW(edgeEntry.at("guard").count("exp") == 1, storm::exceptions::InvalidJaniException, "Guard in edge from '" + sourceLoc + "' in automaton '" + name + "' must have one expression"); guardExpr = parseExpression(edgeEntry.at("guard").at("exp"), scope.refine("guard expression in edge from '" + sourceLoc)); STORM_LOG_THROW(guardExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Guard " << guardExpr << " does not have Boolean type."); } assert(guardExpr.isInitialized()); - std::shared_ptr templateEdge = std::make_shared(guardExpr); + + // edge assignments + if (edgeEntry.count("assignments") > 0) { + STORM_LOG_THROW(edgeEntry.count("assignments") == 1, storm::exceptions::InvalidJaniException, "Multiple edge assignments in edge from '" + sourceLoc + "' in automaton '" + name + "'."); + for (auto const& assignmentEntry : edgeEntry.at("assignments")) { + // ref + STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "' must have one ref field"); + storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), scope.refine("Assignment variable in edge from '" + sourceLoc + "' in automaton '" + name + "'")); + // value + STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "' must have one value field"); + storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), scope.refine("assignment in edge from '" + sourceLoc + "' in automaton '" + name + "'")); + // TODO check types + // index + int64_t assignmentIndex = 0; // default. + if(assignmentEntry.count("index") > 0) { + assignmentIndex = getSignedInt(assignmentEntry.at("index"), "assignment index in edge from '" + sourceLoc + "' in automaton '" + name + "'"); + } + templateEdge->getAssignments().add(storm::jani::Assignment(lValue, assignmentExpr, assignmentIndex)); + } + } + // destinations STORM_LOG_THROW(edgeEntry.count("destinations") == 1, storm::exceptions::InvalidJaniException, "A single list of destinations must be given in edge from '" << sourceLoc << "' in automaton '" << name << "'"); std::vector> destinationLocationsAndProbabilities; for(auto const& destEntry : edgeEntry.at("destinations")) { From ca828729ff7a2fe9748816555f2e0a1833c7db71 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 Oct 2018 12:50:10 +0200 Subject: [PATCH 12/17] Fixed a few warnings --- src/storm/generator/TransientVariableInformation.cpp | 6 +++--- src/storm/storage/jani/ArrayEliminator.cpp | 1 - 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/storm/generator/TransientVariableInformation.cpp b/src/storm/generator/TransientVariableInformation.cpp index 461b43eb0..391f290cd 100644 --- a/src/storm/generator/TransientVariableInformation.cpp +++ b/src/storm/generator/TransientVariableInformation.cpp @@ -175,9 +175,9 @@ namespace storm { } } - template class TransientVariableInformation; - template class TransientVariableInformation; - template class TransientVariableInformation; + template struct TransientVariableInformation; + template struct TransientVariableInformation; + template struct TransientVariableInformation; } } diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp index 4e5c975b0..148a7cac2 100644 --- a/src/storm/storage/jani/ArrayEliminator.cpp +++ b/src/storm/storage/jani/ArrayEliminator.cpp @@ -614,7 +614,6 @@ namespace storm { } void insertLValueArrayAccessReplacements(std::vector const& arrayAccesses, std::vector const& arrayVariableReplacements, int64_t level, std::vector& newAssignments) const { - storm::expressions::Variable const& arrayVariable = arrayAccesses.front()->getLValue().getArray().getExpressionVariable(); bool onlyConstantIndices = true; for (auto const& aa : arrayAccesses) { if (aa->getLValue().getArrayIndex().containsVariables()) { From b3987b178cf757083a6601375b055d062804bdc2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 Oct 2018 16:09:27 +0200 Subject: [PATCH 13/17] Explicit model builder: Give an error if no initial state is found. --- src/storm/builder/ExplicitModelBuilder.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 6711c79f2..71a2681de 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -130,7 +130,8 @@ namespace storm { // Let the generator create all initial states. this->stateStorage.initialStateIndices = generator->getInitialStates(stateToIdCallback); - + STORM_LOG_THROW(!this->stateStorage.initialStateIndices.empty(), storm::exceptions::WrongFormatException, "The model does not have a single initial state."); + // Now explore the current state until there is no more reachable state. uint_fast64_t currentRowGroup = 0; uint_fast64_t currentRow = 0; From 6b094111227a1adac1bea62b4cb6181f219e7029 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 Oct 2018 16:11:17 +0200 Subject: [PATCH 14/17] Fixed an error in the jani location expander. --- src/storm/storage/jani/JaniLocationExpander.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/jani/JaniLocationExpander.cpp b/src/storm/storage/jani/JaniLocationExpander.cpp index bb94a5de4..15d8b1d7d 100644 --- a/src/storm/storage/jani/JaniLocationExpander.cpp +++ b/src/storm/storage/jani/JaniLocationExpander.cpp @@ -98,8 +98,8 @@ namespace storm { int64_t value; for (auto const& assignment : oa) { if (assignment.getVariable() == *variable) { - oa.remove(assignment); value = assignment.getAssignedExpression().evaluateAsInt(); + oa.remove(assignment); break; } } From 93ca559c83a430ab1e63fb502fba1695cc46c1c8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 28 Oct 2018 17:45:39 +0100 Subject: [PATCH 15/17] additional sanity checks for scheduler extraction --- .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 7 +++++-- src/storm/utility/graph.cpp | 4 ++++ 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 3b1d9954b..e455e2308 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -779,8 +779,11 @@ namespace storm { } // Sanity check for created scheduler. - STORM_LOG_ASSERT((!produceScheduler && !scheduler) || (!scheduler->isPartialScheduler() && scheduler->isDeterministicScheduler() && scheduler->isMemorylessScheduler()), "Unexpected format of obtained scheduler."); - + STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained."); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler"); + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler"); + // Return result. return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 193f6a5a5..6cd7ca91f 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -402,6 +402,8 @@ namespace storm { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& state : states) { + bool setValue = false; + STORM_LOG_ASSERT(nondeterministicChoiceIndices[state+1] - nondeterministicChoiceIndices[state] > 0, "Expected at least one action enabled in state " << state); for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool allSuccessorsInStates = true; for (auto const& element : transitionMatrix.getRow(choice)) { @@ -414,9 +416,11 @@ namespace storm { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState); } + setValue = true; break; } } + STORM_LOG_ASSERT(setValue, "Expected that at least one action for state " << state << " stays within the selected state"); } } From 43688d09ea3afd643c2ac74e2f16f9ecbedff295 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 29 Oct 2018 11:32:48 +0100 Subject: [PATCH 16/17] reward infinity scheduler extraction is now correct --- .../prctl/helper/SparseMdpPrctlHelper.cpp | 2 +- src/storm/utility/graph.cpp | 17 +++++++++++++++-- src/storm/utility/graph.h | 10 ++++++++++ 3 files changed, 26 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index e455e2308..7e1d6e45c 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1053,7 +1053,7 @@ namespace storm { scheduler.setChoice(0, state); } } else { - storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.infinityStates, transitionMatrix, scheduler); + storm::utility::graph::computeSchedulerRewInf(qualitativeStateSets.infinityStates, transitionMatrix, scheduler); for (auto const& state : qualitativeStateSets.rewardZeroStates) { scheduler.setChoice(0, state); } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 6cd7ca91f..d17d95edc 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -429,6 +429,7 @@ namespace storm { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& state : states) { + bool setValue = false; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool oneSuccessorInStates = false; for (auto const& element : transitionMatrix.getRow(choice)) { @@ -441,9 +442,11 @@ namespace storm { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState); } + setValue = true; break; } } + STORM_LOG_ASSERT(setValue, "Expected that at least one action for state " << state << " leads with positive probability to the selected state"); } } @@ -494,6 +497,11 @@ namespace storm { void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { computeSchedulerStayingInStates(prob0EStates, transitionMatrix, scheduler); } + + template + void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { + computeSchedulerWithOneSuccessorInStates(rewInfStates, transitionMatrix, scheduler); + } template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter) { @@ -1665,7 +1673,10 @@ namespace storm { template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter); template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); - + + template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); + + template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; @@ -1734,7 +1745,9 @@ namespace storm { template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter); template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); - + + template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); + template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index d42a6be2f..152cf10b9 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -284,6 +284,16 @@ namespace storm { template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); + /*! + * Computes a scheduler for the given states that have a scheduler that has a reward infinity. + * + * @param rewInfStates The states that have a scheduler achieving reward infinity. + * @param transitionMatrix The transition matrix of the system. + * @param scheduler The resulting scheduler for the rewInf States. The scheduler is not set at other states. + */ + template + void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); + /*! * Computes a scheduler for the given states that have a scheduler that has a probability 0. * From ca3b8786542d421951aaf43fd2c3ba390818cac5 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 29 Oct 2018 12:38:59 +0100 Subject: [PATCH 17/17] do not add rate 0 edges to jani (but print a warning) --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 21dfc6264..940f38374 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -141,6 +141,10 @@ namespace storm { } for (auto const& trans : gspn.getTimedTransitions()) { + if(storm::utility::isZero(trans.getRate())) { + STORM_LOG_WARN("Transitions with rate zero are not allowed in JANI. Skipping this transition"); + continue; + } storm::expressions::Expression guard = expressionManager->boolean(true); std::vector assignments;