From 91bbe85a0768731e5befe958cd7ecd5ac5c06d57 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 16 May 2018 22:55:34 +0200 Subject: [PATCH 01/13] builder options for labeling overlapping guards --- src/storm/builder/BuilderOptions.cpp | 11 ++++++++++- src/storm/builder/BuilderOptions.h | 12 +++++++++++- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 33152ca36..d4d729d21 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -36,7 +36,7 @@ namespace storm { return boost::get(labelOrExpression); } - BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) { + BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) { // Intentionally left empty. } @@ -164,6 +164,10 @@ namespace storm { return addOutOfBoundsState; } + bool BuilderOptions::isAddOverlappingGuardLabelSet() const { + return addOverlappingGuardsLabel; + } + BuilderOptions& BuilderOptions::setBuildAllRewardModels(bool newValue) { buildAllRewardModels = newValue; return *this; @@ -238,5 +242,10 @@ namespace storm { return *this; } + BuilderOptions& BuilderOptions::setAddOverlappingGuardsLabel(bool newValue) { + addOverlappingGuardsLabel = newValue; + return *this; + } + } } diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index c6106172b..904d45de6 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -108,6 +108,7 @@ namespace storm { bool isExplorationChecksSet() const; bool isShowProgressSet() const; bool isAddOutOfBoundsStateSet() const; + bool isAddOverlappingGuardLabelSet() const; uint64_t getShowProgressDelay() const; /** @@ -164,6 +165,12 @@ namespace storm { */ BuilderOptions& setAddOutOfBoundsState(bool newValue = true); + /** + * Should a state be labelled for overlapping guards + * @param newValue the new value (default true) + */ + BuilderOptions& setAddOverlappingGuardsLabel(bool newValue = true); + private: /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are @@ -194,10 +201,13 @@ namespace storm { // A flag that indicates whether or not to generate the information from which parts of the model specification // each choice originates. bool buildChoiceOrigins; - + /// A flag that stores whether exploration checks are to be performed. bool explorationChecks; + /// A flag for states with overlapping guards + bool addOverlappingGuardsLabel; + /// A flag indicating that the an additional state for out of bounds should be created. bool addOutOfBoundsState; From f52aab00120087a670d76ca6619f31d29f572a13 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 16 May 2018 22:58:36 +0200 Subject: [PATCH 02/13] fixed out-of-bounds-labelling, added overlapping guards building, and some improved error messages if something goes wrong with highlevel counterex generation --- src/storm/builder/ExplicitModelBuilder.cpp | 3 ++ .../SMTMinimalLabelSetGenerator.h | 31 ++++++++++++++----- src/storm/generator/CompressedState.cpp | 7 +++++ src/storm/generator/CompressedState.h | 2 ++ .../generator/JaniNextStateGenerator.cpp | 4 +++ src/storm/generator/NextStateGenerator.cpp | 30 ++++++++++++++++-- src/storm/generator/NextStateGenerator.h | 10 ++++++ .../generator/PrismNextStateGenerator.cpp | 4 +++ src/storm/generator/VariableInformation.cpp | 23 +++++++++++--- src/storm/generator/VariableInformation.h | 7 +++-- 10 files changed, 106 insertions(+), 15 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 986e04ae7..70e548ae4 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -275,6 +275,7 @@ namespace storm { // (a) the transition matrix // (b) the initial states // (c) the hash map storing the mapping states -> ids + // (d) fix remapping for state-generation labels // Fix (a). transitionMatrixBuilder.replaceColumns(remapping, 0); @@ -287,6 +288,8 @@ namespace storm { // Fix (c). this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } ); + + this->generator->remapStateIds([&remapping] (StateType const& state) { return remapping[state]; }); } } diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index f66205fbf..6b4c440c1 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -458,6 +458,12 @@ namespace storm { // Now check for possible backward cuts. for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabels) { + bool backwardImplicationAdded = false; +// std::cout << "labelSetAndPrecedingLabelSetsPair.first "; +// for (auto const& e : labelSetAndPrecedingLabelSetsPair.first) { +// std::cout << e << ", "; +// } +// std::cout << std::endl; // Find out the commands for the currently considered label set. storm::expressions::Expression guardConjunction; @@ -510,15 +516,18 @@ namespace storm { // If the solver reports unsat, then we know that the current selection is not enabled in the initial state. if (checkResult == storm::solver::SmtSolver::CheckResult::Unsat) { STORM_LOG_DEBUG("Selection not enabled in initial state."); - + + //std::cout << "not gc: " << !guardConjunction << std::endl; localSolver->add(!guardConjunction); STORM_LOG_DEBUG("Asserted disjunction of negated guards."); // Now check the possible preceding label sets for the essential ones. for (auto const& precedingLabelSet : labelSetAndPrecedingLabelSetsPair.second) { + if (labelSetAndPrecedingLabelSetsPair.first == precedingLabelSet) continue; - + + //std::cout << "push" << std::endl; // Create a restore point so we can easily pop-off all weakest precondition expressions. localSolver->push(); @@ -576,7 +585,9 @@ namespace storm { } } } - + + //std::cout << "pgc: " << preceedingGuardConjunction << std::endl; + // Assert all the guards of the preceding command set. localSolver->add(preceedingGuardConjunction); @@ -624,11 +635,15 @@ namespace storm { assertDisjunction(*localSolver, formulae, symbolicModel.isPrismProgram() ? symbolicModel.asPrismProgram().getManager() : symbolicModel.asJaniModel().getManager()); STORM_LOG_DEBUG("Asserted disjunction of all weakest preconditions."); - - if (localSolver->check() == storm::solver::SmtSolver::CheckResult::Sat) { + storm::solver::SmtSolver::CheckResult result = localSolver->check(); + + if (result == storm::solver::SmtSolver::CheckResult::Sat) { backwardImplications[labelSetAndPrecedingLabelSetsPair.first].insert(precedingLabelSet); + backwardImplicationAdded = true; + } else if (result == storm::solver::SmtSolver::CheckResult::Unknown) { + STORM_LOG_ERROR("The SMT solver does not come to a conclusive answer. Does your model contain integer division?"); } - + localSolver->pop(); } @@ -637,6 +652,7 @@ namespace storm { } else { STORM_LOG_DEBUG("Selection is enabled in initial state."); } + STORM_LOG_ERROR_COND(backwardImplicationAdded, "Error in adding cuts for counterexample generation (backward implication misses a label set)."); } } else if (symbolicModel.isJaniModel()) { STORM_LOG_WARN("Model uses assignment levels, did not assert backward implications."); @@ -1697,6 +1713,7 @@ namespace storm { labelSets[choice] = choiceOrigins.getEdgeIndexSet(choice); } } + assert(labelSets.size() == model.getNumberOfChoices()); // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; @@ -1764,7 +1781,7 @@ namespace storm { solverClock = std::chrono::high_resolution_clock::now(); commandSet = findSmallestCommandSet(*solver, variableInformation, currentBound); totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock; - STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << "."); + STORM_LOG_DEBUG("Computed minimal command set of size " << commandSet.size() + relevancyInformation.knownLabels.size() << " (" << commandSet.size() << " + " << relevancyInformation.knownLabels.size() << ") "); // Restrict the given model to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); diff --git a/src/storm/generator/CompressedState.cpp b/src/storm/generator/CompressedState.cpp index a785f1c79..175a753fa 100644 --- a/src/storm/generator/CompressedState.cpp +++ b/src/storm/generator/CompressedState.cpp @@ -46,6 +46,13 @@ namespace storm { template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); + CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit) { + CompressedState result(varInfo.getTotalBitOffset(roundTo64Bit)); + assert(varInfo.hasOutOfBoundsBit()); + result.set(varInfo.getOutOfBoundsBit()); + return result; + } + #ifdef STORM_HAVE_CARL template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); diff --git a/src/storm/generator/CompressedState.h b/src/storm/generator/CompressedState.h index 1a785dbaa..6965022f2 100644 --- a/src/storm/generator/CompressedState.h +++ b/src/storm/generator/CompressedState.h @@ -36,6 +36,8 @@ namespace storm { * @return A valuation that corresponds to the compressed state. */ storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); + + CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit = true); } } diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index a1a683b5b..2df1784a1 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -320,6 +320,10 @@ namespace storm { // If the model is a deterministic model, we need to fuse the choices into one. if (this->isDeterministicModel() && totalNumberOfChoices > 1) { Choice globalChoice; + + if (this->options.isAddOverlappingGuardLabelSet()) { + this->overlappingGuardStates->push_back(stateToIdCallback(*this->state)); + } // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs // this is equal to the number of choices, which is why we initialize it like this here. diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index e02d2ee13..3b3186b68 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -1,4 +1,5 @@ #include +#include #include "storm/generator/NextStateGenerator.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -18,12 +19,22 @@ namespace storm { template NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(nullptr), state(nullptr) { - // Intentionally left empty. + if(variableInformation.hasOutOfBoundsBit()) { + outOfBoundsState = createOutOfBoundsState(variableInformation); + } + if (options.isAddOverlappingGuardLabelSet()) { + overlappingGuardStates = std::vector(); + } } template NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(nullptr), state(nullptr) { - // Intentionally left empty. + if(variableInformation.hasOutOfBoundsBit()) { + outOfBoundsState = createOutOfBoundsState(variableInformation); + } + if (options.isAddOverlappingGuardLabelSet()) { + overlappingGuardStates = std::vector(); + } } template @@ -101,6 +112,14 @@ namespace storm { } } + if (this->options.isAddOverlappingGuardLabelSet()) { + STORM_LOG_THROW(!result.containsLabel("overlap_guards"), storm::exceptions::WrongFormatException, "Label 'overlap_guards' is reserved when adding overlapping guard labels"); + result.addLabel("overlap_guards"); + for (auto index : overlappingGuardStates.get()) { + result.addLabelToState("overlap_guards", index); + } + } + if (this->options.isAddOutOfBoundsStateSet() && stateStorage.stateToId.contains(outOfBoundsState)) { STORM_LOG_THROW(!result.containsLabel("out_of_bounds"),storm::exceptions::WrongFormatException, "Label 'out_of_bounds' is reserved when adding out of bounds states."); result.addLabel("out_of_bounds"); @@ -163,6 +182,13 @@ namespace storm { return nullptr; } + template + void NextStateGenerator::remapStateIds(std::function const& remapping) { + if (overlappingGuardStates != boost::none) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Remapping of Ids during model building is not supported for overlapping guard statements."); + } + } + template class NextStateGenerator; #ifdef STORM_HAVE_CARL diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index ce1dd1f7b..7229ca802 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -66,6 +66,13 @@ namespace storm { NextStateGeneratorOptions const& getOptions() const; virtual std::shared_ptr generateChoiceOrigins(std::vector& dataForChoiceOrigins) const; + + /*! + * Performs a remapping of all values stored by applying the given remapping. + * + * @param remapping The remapping to apply. + */ + void remapStateIds(std::function const& remapping); protected: /*! @@ -98,6 +105,9 @@ namespace storm { /// A state that encodes the outOfBoundsState CompressedState outOfBoundsState; + + /// A map that stores the indices of states with overlapping guards. + boost::optional> overlappingGuardStates; }; } } diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 1de65ce30..61fe1e80f 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -229,6 +229,10 @@ namespace storm { // If the model is a deterministic model, we need to fuse the choices into one. if (this->isDeterministicModel() && totalNumberOfChoices > 1) { Choice globalChoice; + + if (this->options.isAddOverlappingGuardLabelSet()) { + this->overlappingGuardStates->push_back(stateToIdCallback(*this->state)); + } // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs // this is equal to the number of choices, which is why we initialize it like this here. diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 7f7ce0708..e4befba41 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -31,11 +31,14 @@ namespace storm { VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) { if(outOfBoundsState) { - deadlockBit = 0; + outOfBoundsBit = 0; ++totalBitOffset; } else { - deadlockBit = boost::none; + outOfBoundsBit = boost::none; } + + + for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true); ++totalBitOffset; @@ -75,11 +78,13 @@ namespace storm { STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'."); } if(outOfBoundsState) { - deadlockBit = 0; + outOfBoundsBit = 0; ++totalBitOffset; } else { - deadlockBit = boost::none; + outOfBoundsBit = boost::none; } + + for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { if (!variable.isTransient()) { @@ -133,6 +138,16 @@ namespace storm { } return result; } + + bool VariableInformation::hasOutOfBoundsBit() const { + return outOfBoundsBit != boost::none; + } + + uint64_t VariableInformation::getOutOfBoundsBit() const { + assert(hasOutOfBoundsBit()); + return outOfBoundsBit.get(); + } + void VariableInformation::sortVariables() { // Sort the variables so we can make some assumptions when iterating over them (in the next-state generators). diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index 2e51f7db7..fac200d1a 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -93,9 +93,12 @@ namespace storm { /// The integer variables. std::vector integerVariables; - + bool hasOutOfBoundsBit() const; + + uint64_t getOutOfBoundsBit() const; + private: - boost::optional deadlockBit; + boost::optional outOfBoundsBit; /*! * Sorts the variables to establish a known ordering. From 6b914853829233d24ddf4506618dc7248f096297 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 11:35:16 +0200 Subject: [PATCH 03/13] Removed redundant file --- src/storm/builder/DdPrismModelBuilder.cp | 1429 ---------------------- 1 file changed, 1429 deletions(-) delete mode 100644 src/storm/builder/DdPrismModelBuilder.cp diff --git a/src/storm/builder/DdPrismModelBuilder.cp b/src/storm/builder/DdPrismModelBuilder.cp deleted file mode 100644 index 26308f45b..000000000 --- a/src/storm/builder/DdPrismModelBuilder.cp +++ /dev/null @@ -1,1429 +0,0 @@ -#include "storm/builder/DdPrismModelBuilder.h" - -#include - -#include "storm/models/symbolic/Dtmc.h" -#include "storm/models/symbolic/Ctmc.h" -#include "storm/models/symbolic/Mdp.h" -#include "storm/models/symbolic/StandardRewardModel.h" - -#include "storm/settings/SettingsManager.h" - -#include "storm/exceptions/InvalidStateException.h" -#include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/InvalidArgumentException.h" - -#include "storm/utility/prism.h" -#include "storm/utility/math.h" -#include "storm/utility/dd.h" - -#include "storm/storage/dd/DdManager.h" -#include "storm/storage/prism/Program.h" -#include "storm/storage/prism/Compositions.h" -#include "storm/storage/dd/Add.h" -#include "storm/storage/dd/cudd/CuddAddIterator.h" -#include "storm/storage/dd/Bdd.h" - -#include "storm/settings/modules/CoreSettings.h" - -namespace storm { - namespace builder { - - template - class DdPrismModelBuilder::GenerationInformation { - public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { - // Initializes variables and identity DDs. - createMetaVariablesAndIdentities(); - } - - // The program that is currently translated. - storm::prism::Program const& program; - - // The manager used to build the decision diagrams. - std::shared_ptr> manager; - - // The meta variables for the row encoding. - std::set rowMetaVariables; - std::shared_ptr> variableToRowMetaVariableMap; - std::shared_ptr> rowExpressionAdapter; - - // The meta variables for the column encoding. - std::set columnMetaVariables; - std::shared_ptr> variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; - - // All pairs of row/column meta variables. - std::vector> rowColumnMetaVariablePairs; - - // The meta variables used to encode the nondeterminism. - std::vector nondeterminismMetaVariables; - - // The meta variables used to encode the synchronization. - std::vector synchronizationMetaVariables; - - // A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization - // variables). This is handy to abstract from this variable set. - std::set allNondeterminismVariables; - - // As set of all variables used for encoding the synchronization. - std::set allSynchronizationMetaVariables; - - // DDs representing the identity for each variable. - std::map> variableToIdentityMap; - - // A set of all meta variables that correspond to global variables. - std::set allGlobalVariables; - - // DDs representing the identity for each module. - std::map> moduleToIdentityMap; - - // DDs representing the valid ranges of the variables of each module. - std::map> moduleToRangeMap; - - private: - /*! - * Creates the required meta variables and variable/module identities. - */ - void createMetaVariablesAndIdentities() { - // Add synchronization variables. - for (auto const& actionIndex : program.getSynchronizingActionIndices()) { - std::pair variablePair = manager->addMetaVariable(program.getActionName(actionIndex)); - synchronizationMetaVariables.push_back(variablePair.first); - allSynchronizationMetaVariables.insert(variablePair.first); - allNondeterminismVariables.insert(variablePair.first); - } - - // Add nondeterminism variables (number of modules + number of commands). - uint_fast64_t numberOfNondeterminismVariables = program.getModules().size(); - for (auto const& module : program.getModules()) { - numberOfNondeterminismVariables += module.getNumberOfCommands(); - } - for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { - std::pair variablePair = manager->addMetaVariable("nondet" + std::to_string(i)); - nondeterminismMetaVariables.push_back(variablePair.first); - allNondeterminismVariables.insert(variablePair.first); - } - - // Create meta variables for global program variables. - for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) { - int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); - std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); - - STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); - rowColumnMetaVariablePairs.push_back(variablePair); - - allGlobalVariables.insert(integerVariable.getExpressionVariable()); - } - for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { - std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - - STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd(); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); - - rowColumnMetaVariablePairs.push_back(variablePair); - allGlobalVariables.insert(booleanVariable.getExpressionVariable()); - } - - // Create meta variables for each of the modules' variables. - for (storm::prism::Module const& module : program.getModules()) { - storm::dd::Bdd moduleIdentity = manager->getBddOne(); - storm::dd::Bdd moduleRange = manager->getBddOne(); - - for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { - int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); - std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); - STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd()); - moduleIdentity &= variableIdentity; - moduleRange &= manager->getRange(variablePair.first); - - rowColumnMetaVariablePairs.push_back(variablePair); - } - for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { - std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd()); - moduleIdentity &= variableIdentity; - moduleRange &= manager->getRange(variablePair.first); - - rowColumnMetaVariablePairs.push_back(variablePair); - } - moduleToIdentityMap[module.getName()] = moduleIdentity.template toAdd(); - moduleToRangeMap[module.getName()] = moduleRange.template toAdd(); - } - } - }; - - template - class ModuleComposer : public storm::prism::CompositionVisitor { - public: - ModuleComposer(typename DdPrismModelBuilder::GenerationInformation& generationInfo) : generationInfo(generationInfo) { - // Intentionally left empty. - } - - typename DdPrismModelBuilder::ModuleDecisionDiagram compose(storm::prism::Composition const& composition) { - return boost::any_cast::ModuleDecisionDiagram>(composition.accept(*this, newSynchronizingActionToOffsetMap())); - } - - std::map newSynchronizingActionToOffsetMap() const { - std::map result; - for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { - result[actionIndex] = 0; - } - return result; - } - - std::map updateSynchronizingActionToOffsetMap(typename DdPrismModelBuilder::ModuleDecisionDiagram const& sub, std::map const& oldMapping) const { - std::map result = oldMapping; - for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) { - result[action.first] = action.second.numberOfUsedNondeterminismVariables; - } - return result; - } - - virtual boost::any visit(storm::prism::ModuleComposition const& composition, boost::any const& data) override { - STORM_LOG_TRACE("Translating module '" << composition.getModuleName() << "'."); - std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); - - typename DdPrismModelBuilder::ModuleDecisionDiagram result = DdPrismModelBuilder::createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(composition.getModuleName()), synchronizingActionToOffsetMap); - - return result; - } - - virtual boost::any visit(storm::prism::RenamingComposition const& composition, boost::any const& data) override { - // Create the mapping from action indices to action indices. - std::map renaming; - for (auto const& namePair : composition.getActionRenaming()) { - STORM_LOG_THROW(generationInfo.program.hasAction(namePair.first), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.first << "'."); - STORM_LOG_THROW(generationInfo.program.hasAction(namePair.second), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.second << "'."); - renaming.emplace(generationInfo.program.getActionIndex(namePair.first), generationInfo.program.getActionIndex(namePair.second)); - } - - // Prepare the new offset mapping. - std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); - std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; - for (auto const& indexPair : renaming) { - auto it = synchronizingActionToOffsetMap.find(indexPair.second); - STORM_LOG_THROW(it != synchronizingActionToOffsetMap.end(), storm::exceptions::InvalidArgumentException, "Invalid action index " << indexPair.second << "."); - newSynchronizingActionToOffsetMap[indexPair.first] = it->second; - } - - // Then, we translate the subcomposition. - typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); - - // Perform the renaming and return result. - return rename(sub, renaming); - } - - virtual boost::any visit(storm::prism::HidingComposition const& composition, boost::any const& data) override { - // Create the mapping from action indices to action indices. - std::set actionIndicesToHide; - for (auto const& action : composition.getActionsToHide()) { - STORM_LOG_THROW(generationInfo.program.hasAction(action), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << action << "'."); - actionIndicesToHide.insert(generationInfo.program.getActionIndex(action)); - } - - // Prepare the new offset mapping. - std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); - std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; - for (auto const& index : actionIndicesToHide) { - newSynchronizingActionToOffsetMap[index] = 0; - } - - // Then, we translate the subcomposition. - typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); - - // Perform the hiding and return result. - hide(sub, actionIndicesToHide); - return sub; - } - - virtual boost::any visit(storm::prism::SynchronizingParallelComposition const& composition, boost::any const& data) override { - // First, we translate the subcompositions. - typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); - - // Prepare the new offset mapping. - std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); - std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; - for (auto const& action : left.synchronizingActionToDecisionDiagramMap) { - newSynchronizingActionToOffsetMap[action.first] = action.second.numberOfUsedNondeterminismVariables; - } - - typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); - - // Then, determine the action indices on which we need to synchronize. - std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); - std::set rightSynchronizationActionIndices = right.getSynchronizingActionIndices(); - std::set synchronizationActionIndices; - std::set_intersection(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), std::inserter(synchronizationActionIndices, synchronizationActionIndices.begin())); - - // Finally, we compose the subcompositions to create the result. - composeInParallel(left, right, synchronizationActionIndices); - return left; - } - - virtual boost::any visit(storm::prism::InterleavingParallelComposition const& composition, boost::any const& data) override { - // First, we translate the subcompositions. - typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); - - typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, data)); - - // Finally, we compose the subcompositions to create the result. - composeInParallel(left, right, std::set()); - return left; - } - - virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition, boost::any const& data) override { - // Construct the synchronizing action indices from the synchronizing action names. - std::set synchronizingActionIndices; - for (auto const& action : composition.getSynchronizingActions()) { - synchronizingActionIndices.insert(generationInfo.program.getActionIndex(action)); - } - - // Then, we translate the subcompositions. - typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); - - // Prepare the new offset mapping. - std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); - std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; - for (auto const& actionIndex : synchronizingActionIndices) { - auto it = left.synchronizingActionToDecisionDiagramMap.find(actionIndex); - if (it != left.synchronizingActionToDecisionDiagramMap.end()) { - newSynchronizingActionToOffsetMap[actionIndex] = it->second.numberOfUsedNondeterminismVariables; - } - } - - typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); - - std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); - bool isContainedInLeft = std::includes(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end()); - STORM_LOG_WARN_COND(isContainedInLeft, "Left subcomposition of composition '" << composition << "' does not include all actions over which to synchronize."); - - std::set rightSynchronizationActionIndices = right.getSynchronizingActionIndices(); - bool isContainedInRight = std::includes(rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end()); - STORM_LOG_WARN_COND(isContainedInRight, "Right subcomposition of composition '" << composition << "' does not include all actions over which to synchronize."); - - // Finally, we compose the subcompositions to create the result. - composeInParallel(left, right, synchronizingActionIndices); - return left; - } - - private: - /*! - * Hides the actions of the given module according to the given set. As a result, the module is modified in - * place. - */ - void hide(typename DdPrismModelBuilder::ModuleDecisionDiagram& sub, std::set const& actionIndicesToHide) const { - STORM_LOG_TRACE("Hiding actions."); - - for (auto const& actionIndex : actionIndicesToHide) { - auto it = sub.synchronizingActionToDecisionDiagramMap.find(actionIndex); - if (it != sub.synchronizingActionToDecisionDiagramMap.end()) { - sub.independentAction = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, sub.independentAction, it->second); - sub.numberOfUsedNondeterminismVariables = std::max(sub.numberOfUsedNondeterminismVariables, sub.independentAction.numberOfUsedNondeterminismVariables); - sub.synchronizingActionToDecisionDiagramMap.erase(it); - } - } - } - - /*! - * Renames the actions of the given module according to the given renaming. - */ - typename DdPrismModelBuilder::ModuleDecisionDiagram rename(typename DdPrismModelBuilder::ModuleDecisionDiagram& sub, std::map const& renaming) const { - STORM_LOG_TRACE("Renaming actions."); - std::map::ActionDecisionDiagram> actionIndexToDdMap; - - // Go through all action DDs with a synchronizing label and rename them if they appear in the renaming. - for (auto& action : sub.synchronizingActionToDecisionDiagramMap) { - auto renamingIt = renaming.find(action.first); - if (renamingIt != renaming.end()) { - // If the action is to be renamed and an action with the target index already exists, we need - // to combine the action DDs. - auto itNewActions = actionIndexToDdMap.find(renamingIt->second); - if (itNewActions != actionIndexToDdMap.end()) { - actionIndexToDdMap[renamingIt->second] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second); - - } else { - // In this case, we can simply copy the action over. - actionIndexToDdMap[renamingIt->second] = action.second; - } - } else { - // If the action is not to be renamed, we need to copy it over. However, if some other action - // was renamed to the very same action name before, we need to combine the transitions. - auto itNewActions = actionIndexToDdMap.find(action.first); - if (itNewActions != actionIndexToDdMap.end()) { - actionIndexToDdMap[action.first] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second); - } else { - // In this case, we can simply copy the action over. - actionIndexToDdMap[action.first] = action.second; - } - } - } - - return typename DdPrismModelBuilder::ModuleDecisionDiagram(sub.independentAction, actionIndexToDdMap, sub.identity, sub.numberOfUsedNondeterminismVariables); - } - - /*! - * Composes the given modules while synchronizing over the provided action indices. As a result, the first - * module is modified in place and will contain the composition after a call to this method. - */ - void composeInParallel(typename DdPrismModelBuilder::ModuleDecisionDiagram& left, typename DdPrismModelBuilder::ModuleDecisionDiagram& right, std::set const& synchronizationActionIndices) const { - STORM_LOG_TRACE("Composing two modules."); - - // Combine the tau action. - uint_fast64_t numberOfUsedNondeterminismVariables = right.independentAction.numberOfUsedNondeterminismVariables; - left.independentAction = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, left.independentAction, right.independentAction, left.identity, right.identity); - numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.independentAction.numberOfUsedNondeterminismVariables); - - // Create an empty action for the case where one of the modules does not have a certain action. - typename DdPrismModelBuilder::ActionDecisionDiagram emptyAction(*generationInfo.manager); - - // Treat all non-tau actions of the left module. - for (auto& action : left.synchronizingActionToDecisionDiagramMap) { - // If we need to synchronize over this action index, we try to do so now. - if (synchronizationActionIndices.find(action.first) != synchronizationActionIndices.end()) { - // If we are to synchronize over an action that does not exist in the second module, the result - // is that the synchronization is the empty action. - if (!right.hasSynchronizingAction(action.first)) { - action.second = emptyAction; - } else { - // Otherwise, the actions of the modules are synchronized. - action.second = DdPrismModelBuilder::combineSynchronizingActions(action.second, right.synchronizingActionToDecisionDiagramMap[action.first]); - } - } else { - // If we don't synchronize over this action, we need to construct the interleaving. - - // If both modules contain the action, we need to mutually multiply the other identity. - if (right.hasSynchronizingAction(action.first)) { - action.second = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first], left.identity, right.identity); - } else { - // If only the first module has this action, we need to use a dummy action decision diagram - // for the second module. - action.second = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, emptyAction, left.identity, right.identity); - } - } - numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, action.second.numberOfUsedNondeterminismVariables); - } - - // Treat all non-tau actions of the right module. - for (auto const& actionIndex : right.getSynchronizingActionIndices()) { - // Here, we only need to treat actions that the first module does not have, because we have handled - // this case earlier. - if (!left.hasSynchronizingAction(actionIndex)) { - if (synchronizationActionIndices.find(actionIndex) != synchronizationActionIndices.end()) { - // If we are to synchronize over this action that does not exist in the first module, the - // result is that the synchronization is the empty action. - left.synchronizingActionToDecisionDiagramMap[actionIndex] = emptyAction; - } else { - // If only the second module has this action, we need to use a dummy action decision diagram - // for the first module. - left.synchronizingActionToDecisionDiagramMap[actionIndex] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, emptyAction, right.synchronizingActionToDecisionDiagramMap[actionIndex], left.identity, right.identity); - } - } - numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables); - } - - // Combine identity matrices. - left.identity = left.identity * right.identity; - - // Keep track of the number of nondeterminism variables used. - left.numberOfUsedNondeterminismVariables = std::max(left.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables); - } - - typename DdPrismModelBuilder::GenerationInformation& generationInfo; - }; - - template - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { - // Intentionally left empty. - } - - template - DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set()), terminalStates(), negatedTerminalStates() { - this->preserveFormula(formula); - this->setTerminalStatesFromFormula(formula); - } - - template - DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { - if (formulas.empty()) { - this->buildAllRewardModels = true; - this->buildAllLabels = true; - } else { - for (auto const& formula : formulas) { - this->preserveFormula(*formula); - } - if (formulas.size() == 1) { - this->setTerminalStatesFromFormula(*formulas.front()); - } - } - } - - template - void DdPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { - // If we already had terminal states, we need to erase them. - if (terminalStates) { - terminalStates.reset(); - } - if (negatedTerminalStates) { - negatedTerminalStates.reset(); - } - - // If we are not required to build all reward models, we determine the reward models we need to build. - if (!buildAllRewardModels) { - std::set referencedRewardModels = formula.getReferencedRewardModels(); - rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); - } - - // Extract all the labels used in the formula. - std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); - for (auto const& formula : atomicLabelFormulas) { - if (!labelsToBuild) { - labelsToBuild = std::set(); - } - labelsToBuild.get().insert(formula.get()->getLabel()); - } - } - - template - void DdPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - terminalStates = formula.asAtomicExpressionFormula().getExpression(); - } else if (formula.isAtomicLabelFormula()) { - terminalStates = formula.asAtomicLabelFormula().getLabel(); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - negatedTerminalStates = left.asAtomicExpressionFormula().getExpression(); - } else if (left.isAtomicLabelFormula()) { - negatedTerminalStates = left.asAtomicLabelFormula().getLabel(); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } - } - - template - struct DdPrismModelBuilder::SystemResult { - SystemResult(storm::dd::Add const& allTransitionsDd, DdPrismModelBuilder::ModuleDecisionDiagram const& globalModule, storm::dd::Add const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) { - // Intentionally left empty. - } - - storm::dd::Add allTransitionsDd; - typename DdPrismModelBuilder::ModuleDecisionDiagram globalModule; - storm::dd::Add stateActionDd; - }; - - template - typename DdPrismModelBuilder::UpdateDecisionDiagram DdPrismModelBuilder::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Add const& guard, storm::prism::Update const& update) { - storm::dd::Add updateDd = generationInfo.manager->template getAddOne(); - - STORM_LOG_TRACE("Translating update " << update); - - // Iterate over all assignments (boolean and integer) and build the DD for it. - std::vector assignments = update.getAssignments(); - std::set assignedVariables; - for (auto const& assignment : assignments) { - // Record the variable as being written. - STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap->at(assignment.getVariable()).getName()); - assignedVariables.insert(assignment.getVariable()); - - // Translate the written variable. - auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap->at(assignment.getVariable()); - storm::dd::Add writtenVariable = generationInfo.manager->template getIdentity(primedMetaVariable); - - // Translate the expression that is being assigned. - storm::dd::Add updateExpression = generationInfo.rowExpressionAdapter->translateExpression(assignment.getExpression()); - - // Combine the update expression with the guard. - storm::dd::Add result = updateExpression * guard; - - // Combine the variable and the assigned expression. - storm::dd::Add tmp = result; - result = result.equals(writtenVariable).template toAdd(); - result *= guard; - - // Restrict the transitions to the range of the written variable. - result = result * generationInfo.manager->getRange(primedMetaVariable).template toAdd(); - - updateDd *= result; - } - - // Compute the set of assigned global variables. - std::set assignedGlobalVariables; - std::set_intersection(assignedVariables.begin(), assignedVariables.end(), generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); - - // All unassigned boolean variables need to keep their value. - for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { - if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) { - STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName()); - updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable()); - } - } - - // All unassigned integer variables need to keep their value. - for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { - if (assignedVariables.find(integerVariable.getExpressionVariable()) == assignedVariables.end()) { - STORM_LOG_TRACE("Multiplying identity of variable " << integerVariable.getName()); - updateDd *= generationInfo.variableToIdentityMap.at(integerVariable.getExpressionVariable()); - } - } - - return UpdateDecisionDiagram(updateDd, assignedGlobalVariables); - } - - template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) { - STORM_LOG_TRACE("Translating guard " << command.getGuardExpression()); - storm::dd::Add guard = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; - STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); - - if (!guard.isZero()) { - // Create the DDs representing the individual updates. - std::vector updateResults; - for (storm::prism::Update const& update : command.getUpdates()) { - updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guard, update)); - - STORM_LOG_WARN_COND(!updateResults.back().updateDd.isZero(), "Update '" << update << "' does not have any effect."); - } - - // Start by gathering all variables that were written in at least one update. - std::set globalVariablesInSomeUpdate; - - // If the command is labeled, we have to analyze which portion of the global variables was written by - // any of the updates and make all update results equal w.r.t. this set. If the command is not labeled, - // we can already multiply the identities of all global variables. - if (command.isLabeled()) { - std::for_each(updateResults.begin(), updateResults.end(), [&globalVariablesInSomeUpdate] (UpdateDecisionDiagram const& update) { globalVariablesInSomeUpdate.insert(update.assignedGlobalVariables.begin(), update.assignedGlobalVariables.end()); } ); - } else { - globalVariablesInSomeUpdate = generationInfo.allGlobalVariables; - } - - // Then, multiply the missing identities. - for (auto& updateResult : updateResults) { - std::set missingIdentities; - std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), updateResult.assignedGlobalVariables.begin(), updateResult.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << "[" << variable.getIndex() << "] to update."); - updateResult.updateDd *= generationInfo.variableToIdentityMap.at(variable); - } - } - - // Now combine the update DDs to the command DD. - storm::dd::Add commandDd = generationInfo.manager->template getAddZero(); - auto updateResultsIt = updateResults.begin(); - for (auto updateIt = command.getUpdates().begin(), updateIte = command.getUpdates().end(); updateIt != updateIte; ++updateIt, ++updateResultsIt) { - storm::dd::Add probabilityDd = generationInfo.rowExpressionAdapter->translateExpression(updateIt->getLikelihoodExpression()); - commandDd += updateResultsIt->updateDd * probabilityDd; - } - - return ActionDecisionDiagram(guard, guard * commandDd, globalVariablesInSomeUpdate); - } else { - return ActionDecisionDiagram(*generationInfo.manager); - } - } - - template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) { - std::vector commandDds; - for (storm::prism::Command const& command : module.getCommands()) { - - // Determine whether the command is relevant for the selected action. - bool relevant = (synchronizationActionIndex == 0 && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex); - - if (!relevant) { - continue; - } - - STORM_LOG_TRACE("Translating command " << command); - - // At this point, the command is known to be relevant for the action. - commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command)); - } - - ActionDecisionDiagram result(*generationInfo.manager); - if (!commandDds.empty()) { - switch (generationInfo.program.getModelType()){ - case storm::prism::Program::ModelType::DTMC: - case storm::prism::Program::ModelType::CTMC: - result = combineCommandsToActionMarkovChain(generationInfo, commandDds); - break; - case storm::prism::Program::ModelType::MDP: - result = combineCommandsToActionMDP(generationInfo, commandDds, nondeterminismVariableOffset); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type."); - } - } - - return result; - } - - template - std::set DdPrismModelBuilder::equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2) { - // Start by gathering all variables that were written in at least one action DD. - std::set globalVariablesInActionDd; - std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(globalVariablesInActionDd, globalVariablesInActionDd.begin())); - - std::set missingIdentitiesInAction1; - std::set_difference(globalVariablesInActionDd.begin(), globalVariablesInActionDd.end(), action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), std::inserter(missingIdentitiesInAction1, missingIdentitiesInAction1.begin())); - for (auto const& variable : missingIdentitiesInAction1) { - action1.transitionsDd *= generationInfo.variableToIdentityMap.at(variable); - } - - std::set missingIdentitiesInAction2; - std::set_difference(globalVariablesInActionDd.begin(), globalVariablesInActionDd.end(), action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), std::inserter(missingIdentitiesInAction2, missingIdentitiesInAction2.begin())); - for (auto const& variable : missingIdentitiesInAction2) { - action2.transitionsDd *= generationInfo.variableToIdentityMap.at(variable); - } - - return globalVariablesInActionDd; - } - - template - std::set DdPrismModelBuilder::equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, std::vector& actionDds) { - // Start by gathering all variables that were written in at least one action DD. - std::set globalVariablesInActionDd; - for (auto const& commandDd : actionDds) { - globalVariablesInActionDd.insert(commandDd.assignedGlobalVariables.begin(), commandDd.assignedGlobalVariables.end()); - } - - STORM_LOG_TRACE("Equalizing assigned global variables."); - - // Then multiply the transitions of each action with the missing identities. - for (auto& actionDd : actionDds) { - STORM_LOG_TRACE("Equalizing next action."); - std::set missingIdentities; - std::set_difference(globalVariablesInActionDd.begin(), globalVariablesInActionDd.end(), actionDd.assignedGlobalVariables.begin(), actionDd.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName() << "."); - actionDd.transitionsDd *= generationInfo.variableToIdentityMap.at(variable); - } - } - return globalVariablesInActionDd; - } - - template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMarkovChain(GenerationInformation& generationInfo, std::vector& commandDds) { - storm::dd::Add allGuards = generationInfo.manager->template getAddZero(); - storm::dd::Add allCommands = generationInfo.manager->template getAddZero(); - storm::dd::Add temporary; - - // Make all command DDs assign to the same global variables. - std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, commandDds); - - // Then combine the commands to the full action DD and multiply missing identities along the way. - for (auto& commandDd : commandDds) { - // Check for overlapping guards. - temporary = commandDd.guardDd * allGuards; - - // Issue a warning if there are overlapping guards in a non-CTMC model. - STORM_LOG_WARN_COND(temporary.isZero() || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC, "Guard of a command overlaps with previous guards."); - - allGuards += commandDd.guardDd; - allCommands += commandDd.transitionsDd; - } - - return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables); - } - - template - storm::dd::Add DdPrismModelBuilder::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) { - storm::dd::Add result = generationInfo.manager->template getAddZero(); - - STORM_LOG_TRACE("Encoding " << value << " with " << numberOfBinaryVariables << " binary variable(s) starting from offset " << nondeterminismVariableOffset << "."); - - std::map metaVariableNameToValueMap; - for (uint_fast64_t i = nondeterminismVariableOffset; i < nondeterminismVariableOffset + numberOfBinaryVariables; ++i) { - if (value & (1ull << (numberOfBinaryVariables - i - 1))) { - metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 1); - } else { - metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 0); - } - } - - result.setValue(metaVariableNameToValueMap, ValueType(1)); - return result; - } - - template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector& commandDds, uint_fast64_t nondeterminismVariableOffset) { - storm::dd::Bdd allGuards = generationInfo.manager->getBddZero(); - storm::dd::Add allCommands = generationInfo.manager->template getAddZero(); - - // Make all command DDs assign to the same global variables. - std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, commandDds); - - // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. - storm::dd::Add sumOfGuards = generationInfo.manager->template getAddZero(); - for (auto const& commandDd : commandDds) { - sumOfGuards += commandDd.guardDd; - allGuards |= commandDd.guardDd.toBdd(); - } - uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); - - STORM_LOG_TRACE("Found " << maxChoices << " local choices."); - - // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. - if (maxChoices == 0) { - return ActionDecisionDiagram(*generationInfo.manager); - } else if (maxChoices == 1) { - // Sum up all commands. - for (auto const& commandDd : commandDds) { - allCommands += commandDd.transitionsDd; - } - return ActionDecisionDiagram(sumOfGuards, allCommands, assignedGlobalVariables); - } else { - // Calculate number of required variables to encode the nondeterminism. - uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - - storm::dd::Bdd equalsNumberOfChoicesDd; - std::vector> choiceDds(maxChoices, generationInfo.manager->template getAddZero()); - std::vector> remainingDds(maxChoices, generationInfo.manager->getBddZero()); - - for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { - // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(ValueType(currentChoices))); - - // If there is no such state, continue with the next possible number of choices. - if (equalsNumberOfChoicesDd.isZero()) { - continue; - } - - // Reset the previously used intermediate storage. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - choiceDds[j] = generationInfo.manager->template getAddZero(); - remainingDds[j] = equalsNumberOfChoicesDd; - } - - for (std::size_t j = 0; j < commandDds.size(); ++j) { - // Check if command guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices - // choices such that one outgoing choice is given by the j-th command. - storm::dd::Bdd guardChoicesIntersection = commandDds[j].guardDd.toBdd() && equalsNumberOfChoicesDd; - - // If there is no such state, continue with the next command. - if (guardChoicesIntersection.isZero()) { - continue; - } - - // Split the nondeterministic choices. - for (uint_fast64_t k = 0; k < currentChoices; ++k) { - // Calculate the overlapping part of command guard and the remaining DD. - storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; - - // Check if we can add some overlapping parts to the current index. - if (!remainingGuardChoicesIntersection.isZero()) { - // Remove overlapping parts from the remaining DD. - remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; - - // Combine the overlapping part of the guard with command updates and add it to the resulting DD. - choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * commandDds[j].transitionsDd; - } - - // Remove overlapping parts from the command guard DD - guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; - - // If the guard DD has become equivalent to false, we can stop here. - if (guardChoicesIntersection.isZero()) { - break; - } - } - } - - // Add the meta variables that encode the nondeterminisim to the different choices. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - allCommands += encodeChoice(generationInfo, nondeterminismVariableOffset, numberOfBinaryVariables, j) * choiceDds[j]; - } - - // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); - } - - return ActionDecisionDiagram(allGuards.template toAdd(), allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); - } - } - - template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { - std::set assignedGlobalVariables; - std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); - return ActionDecisionDiagram(action1.guardDd * action2.guardDd, action1.transitionsDd * action2.transitionsDd, assignedGlobalVariables, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables)); - } - - template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2) { - - // First extend the action DDs by the other identities. - STORM_LOG_TRACE("Multiplying identities to combine unsynchronized actions."); - action1.transitionsDd = action1.transitionsDd * identityDd2; - action2.transitionsDd = action2.transitionsDd * identityDd1; - - // Then combine the extended action DDs. - return combineUnsynchronizedActions(generationInfo, action1, action2); - } - - template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2) { - STORM_LOG_TRACE("Combining unsynchronized actions."); - - // Make both action DDs write to the same global variables. - std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, action1, action2); - - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1.transitionsDd + action2.transitionsDd, assignedGlobalVariables, 0); - } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - if (action1.transitionsDd.isZero()) { - return ActionDecisionDiagram(action2.guardDd, action2.transitionsDd, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables); - } else if (action2.transitionsDd.isZero()) { - return ActionDecisionDiagram(action1.guardDd, action1.transitionsDd, assignedGlobalVariables, action1.numberOfUsedNondeterminismVariables); - } - - // Bring both choices to the same number of variables that encode the nondeterminism. - uint_fast64_t numberOfUsedNondeterminismVariables = std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables); - if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) { - storm::dd::Add nondeterminismEncoding = generationInfo.manager->template getAddOne(); - - for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); - } - action2.transitionsDd *= nondeterminismEncoding; - } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) { - storm::dd::Add nondeterminismEncoding = generationInfo.manager->template getAddOne(); - - for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); - } - action1.transitionsDd *= nondeterminismEncoding; - } - - // Add a new variable that resolves the nondeterminism between the two choices. - storm::dd::Add combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2.transitionsDd, action1.transitionsDd); - - return ActionDecisionDiagram((action1.guardDd.toBdd() || action2.guardDd.toBdd()).template toAdd(), combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); - } - } - - template - typename DdPrismModelBuilder::ModuleDecisionDiagram DdPrismModelBuilder::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap) { - // Start by creating the action DD for the independent action. - ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, 0, 0); - uint_fast64_t numberOfUsedNondeterminismVariables = independentActionDd.numberOfUsedNondeterminismVariables; - - // Create module DD for all synchronizing actions of the module. - std::map actionIndexToDdMap; - for (auto const& actionIndex : module.getSynchronizingActionIndices()) { - STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'."); - ActionDecisionDiagram tmp = createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex)); - numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, tmp.numberOfUsedNondeterminismVariables); - actionIndexToDdMap.emplace(actionIndex, tmp); - } - - return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()), numberOfUsedNondeterminismVariables); - } - - template - storm::dd::Add DdPrismModelBuilder::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex) { - storm::dd::Add synchronization = generationInfo.manager->template getAddOne(); - if (actionIndex != 0) { - for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { - if ((actionIndex - 1) == i) { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1).template toAdd(); - } else { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).template toAdd(); - } - } - } else { - for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).template toAdd(); - } - } - return synchronization; - } - - template - storm::dd::Add DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) { - // If the model is an MDP, we need to encode the nondeterminism using additional variables. - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - storm::dd::Add result = generationInfo.manager->template getAddZero(); - - // First, determine the highest number of nondeterminism variables that is used in any action and make - // all actions use the same amout of nondeterminism variables. - uint_fast64_t numberOfUsedNondeterminismVariables = module.numberOfUsedNondeterminismVariables; - - // Compute missing global variable identities in independent action. - std::set missingIdentities; - std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), module.independentAction.assignedGlobalVariables.begin(), module.independentAction.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - storm::dd::Add identityEncoding = generationInfo.manager->template getAddOne(); - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to independent action."); - identityEncoding *= generationInfo.variableToIdentityMap.at(variable); - } - - // Add variables to independent action DD. - storm::dd::Add nondeterminismEncoding = generationInfo.manager->template getAddOne(); - for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); - } - result = identityEncoding * module.independentAction.transitionsDd * nondeterminismEncoding; - - // Add variables to synchronized action DDs. - std::map> synchronizingActionToDdMap; - for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { - // Compute missing global variable identities in synchronizing actions. - missingIdentities = std::set(); - std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), synchronizingAction.second.assignedGlobalVariables.begin(), synchronizingAction.second.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - identityEncoding = generationInfo.manager->template getAddOne(); - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to synchronizing action '" << synchronizingAction.first << "'."); - identityEncoding *= generationInfo.variableToIdentityMap.at(variable); - } - - nondeterminismEncoding = generationInfo.manager->template getAddOne(); - for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); - } - synchronizingActionToDdMap.emplace(synchronizingAction.first, identityEncoding * synchronizingAction.second.transitionsDd * nondeterminismEncoding); - } - - // Add variables for synchronization. - result *= getSynchronizationDecisionDiagram(generationInfo); - - for (auto& synchronizingAction : synchronizingActionToDdMap) { - synchronizingAction.second *= getSynchronizationDecisionDiagram(generationInfo, synchronizingAction.first); - } - - // Now, we can simply add all synchronizing actions to the result. - for (auto const& synchronizingAction : synchronizingActionToDdMap) { - result += synchronizingAction.second; - } - - return result; - } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - // Simply add all actions, but make sure to include the missing global variable identities. - - // Compute missing global variable identities in independent action. - std::set missingIdentities; - std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), module.independentAction.assignedGlobalVariables.begin(), module.independentAction.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - storm::dd::Add identityEncoding = generationInfo.manager->template getAddOne(); - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to independent action."); - identityEncoding *= generationInfo.variableToIdentityMap.at(variable); - } - - storm::dd::Add result = identityEncoding * module.independentAction.transitionsDd; - - for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { - // Compute missing global variable identities in synchronizing actions. - missingIdentities = std::set(); - std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), synchronizingAction.second.assignedGlobalVariables.begin(), synchronizingAction.second.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - identityEncoding = generationInfo.manager->template getAddOne(); - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to synchronizing action '" << synchronizingAction.first << "'."); - identityEncoding *= generationInfo.variableToIdentityMap.at(variable); - } - - result += identityEncoding * synchronizingAction.second.transitionsDd; - } - return result; - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); - } - } - - template - typename DdPrismModelBuilder::SystemResult DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { - ModuleComposer composer(generationInfo); - ModuleDecisionDiagram system = composer.compose(generationInfo.program.specifiesSystemComposition() ? generationInfo.program.getSystemCompositionConstruct().getSystemComposition() : *generationInfo.program.getDefaultSystemComposition()); - - storm::dd::Add result = createSystemFromModule(generationInfo, system); - - // Create an auxiliary DD that is used later during the construction of reward models. - STORM_LOG_TRACE("Counting: " << result.getNonZeroCount() << " // " << result.getNodeCount()); - storm::dd::Add stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables); - - // For DTMCs, we normalize each row to 1 (to account for non-determinism). - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - result = result / stateActionDd; - } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - // For MDPs, we need to throw away the nondeterminism variables from the generation information that - // were never used. - for (uint_fast64_t index = system.numberOfUsedNondeterminismVariables; index < generationInfo.nondeterminismMetaVariables.size(); ++index) { - generationInfo.allNondeterminismVariables.erase(generationInfo.nondeterminismMetaVariables[index]); - } - generationInfo.nondeterminismMetaVariables.resize(system.numberOfUsedNondeterminismVariables); - } - - return SystemResult(result, system, stateActionDd); - } - - template - storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { - - // Start by creating the state reward vector. - boost::optional> stateRewards; - if (rewardModel.hasStateRewards()) { - stateRewards = generationInfo.manager->template getAddZero(); - - for (auto const& stateReward : rewardModel.getStateRewards()) { - storm::dd::Add states = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getStatePredicateExpression()); - storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getRewardValueExpression()); - - // Restrict the rewards to those states that satisfy the condition. - rewards = reachableStatesAdd * states * rewards; - - // Perform some sanity checks. - STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states."); - STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); - - // Add the rewards to the global state reward vector. - stateRewards.get() += rewards; - } - } - - // Next, build the state-action reward vector. - boost::optional> stateActionRewards; - if (rewardModel.hasStateActionRewards()) { - stateActionRewards = generationInfo.manager->template getAddZero(); - - for (auto const& stateActionReward : rewardModel.getStateActionRewards()) { - storm::dd::Add states = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getStatePredicateExpression()); - storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getRewardValueExpression()); - storm::dd::Add synchronization = generationInfo.manager->template getAddOne(); - - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - synchronization = getSynchronizationDecisionDiagram(generationInfo, stateActionReward.getActionIndex()); - } - ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction; - states *= actionDd.guardDd * reachableStatesAdd; - storm::dd::Add stateActionRewardDd = synchronization * states * rewards; - - // If we are building the state-action rewards for an MDP, we need to make sure that the encoding - // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the - // legal state-actions. - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - stateActionRewardDd *= stateActionDd; - } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action. - stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables); - } - - // Perform some sanity checks. - STORM_LOG_WARN_COND(stateActionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states."); - STORM_LOG_WARN_COND(!stateActionRewardDd.isZero(), "The reward model does not assign any non-zero rewards."); - - // Add the rewards to the global transition reward matrix. - stateActionRewards.get() += stateActionRewardDd; - } - - // Scale state-action rewards for DTMCs and CTMCs. - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - stateActionRewards.get() /= stateActionDd; - } - } - - // Then build the transition reward matrix. - boost::optional> transitionRewards; - if (rewardModel.hasTransitionRewards()) { - transitionRewards = generationInfo.manager->template getAddZero(); - - for (auto const& transitionReward : rewardModel.getTransitionRewards()) { - storm::dd::Add sourceStates = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getSourceStatePredicateExpression()); - storm::dd::Add targetStates = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getTargetStatePredicateExpression()); - storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getRewardValueExpression()); - - storm::dd::Add synchronization = generationInfo.manager->template getAddOne(); - - storm::dd::Add transitions; - if (transitionReward.isLabeled()) { - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - synchronization = getSynchronizationDecisionDiagram(generationInfo, transitionReward.getActionIndex()); - } - transitions = globalModule.synchronizingActionToDecisionDiagramMap.at(transitionReward.getActionIndex()).transitionsDd; - } else { - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - synchronization = getSynchronizationDecisionDiagram(generationInfo); - } - transitions = globalModule.independentAction.transitionsDd; - } - - storm::dd::Add transitionRewardDd = synchronization * sourceStates * targetStates * rewards; - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - // For DTMCs we need to keep the weighting for the scaling that follows. - transitionRewardDd = transitions * transitionRewardDd; - } else { - // For all other model types, we do not scale the rewards. - transitionRewardDd = transitions.notZero().template toAdd() * transitionRewardDd; - } - - // Perform some sanity checks. - STORM_LOG_WARN_COND(transitionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states."); - STORM_LOG_WARN_COND(!transitionRewardDd.isZero(), "The reward model does not assign any non-zero rewards."); - - // Add the rewards to the global transition reward matrix. - transitionRewards.get() += transitionRewardDd; - } - - // Scale transition rewards for DTMCs. - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - transitionRewards.get() /= stateActionDd; - } - } - - return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); - } - - template - std::shared_ptr> DdPrismModelBuilder::build(storm::prism::Program const& program, Options const& options) { - if (program.hasUndefinedConstants()) { - std::vector> undefinedConstants = program.getUndefinedConstants(); - std::stringstream stream; - bool printComma = false; - for (auto const& constant : undefinedConstants) { - if (printComma) { - stream << ", "; - } else { - printComma = true; - } - stream << constant.get().getName() << " (" << constant.get().getType() << ")"; - } - stream << "."; - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); - } - - STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl); - - // Start by initializing the structure used for storing all information needed during the model generation. - // In particular, this creates the meta variables used to encode the model. - GenerationInformation generationInfo(program); - - SystemResult system = createSystemDecisionDiagram(generationInfo); - storm::dd::Add transitionMatrix = system.allTransitionsDd; - - ModuleDecisionDiagram const& globalModule = system.globalModule; - storm::dd::Add stateActionDd = system.stateActionDd; - - // If we were asked to treat some states as terminal states, we cut away their transitions now. - storm::dd::Bdd terminalStatesBdd = generationInfo.manager->getBddZero(); - if (options.terminalStates || options.negatedTerminalStates) { - std::map constantsSubstitution = program.getConstantsSubstitution(); - - if (options.terminalStates) { - storm::expressions::Expression terminalExpression; - if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { - terminalExpression = boost::get(options.terminalStates.get()); - } else { - std::string const& labelName = boost::get(options.terminalStates.get()); - if (program.hasLabel(labelName)) { - terminalExpression = program.getLabelExpression(labelName); - } else { - STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); - } - } - - if (terminalExpression.isInitialized()) { - // If the expression refers to constants of the model, we need to substitute them. - terminalExpression = terminalExpression.substitute(constantsSubstitution); - - STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); - terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); - } - } - if (options.negatedTerminalStates) { - storm::expressions::Expression negatedTerminalExpression; - if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) { - negatedTerminalExpression = boost::get(options.negatedTerminalStates.get()); - } else { - std::string const& labelName = boost::get(options.negatedTerminalStates.get()); - if (program.hasLabel(labelName)) { - negatedTerminalExpression = program.getLabelExpression(labelName); - } else { - STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); - } - } - - if (negatedTerminalExpression.isInitialized()) { - // If the expression refers to constants of the model, we need to substitute them. - negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution); - - STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); - terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); - } - } - - transitionMatrix *= (!terminalStatesBdd).template toAdd(); - } - - std::cout << "trans matrix has size " << transitionMatrix.getNodeCount() << std::endl; - - // Cut the transitions and rewards to the reachable fragment of the state space. - storm::dd::Bdd initialStates = createInitialStatesDecisionDiagram(generationInfo); - - storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); - if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); - } - - storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionMatrixBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); - storm::dd::Add reachableStatesAdd = reachableStates.template toAdd(); - transitionMatrix *= reachableStatesAdd; - stateActionDd *= reachableStatesAdd; - - // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. - storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); - storm::dd::Bdd deadlockStates = reachableStates && !statesWithTransition; - - // If there are deadlocks, either fix them or raise an error. - if (!deadlockStates.isZero()) { - // If we need to fix deadlocks, we do so now. - if (!storm::settings::getModule().isDontFixDeadlocksSet()) { - STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); - - storm::dd::Add deadlockStatesAdd = deadlockStates.template toAdd(); - uint_fast64_t count = 0; - for (auto it = deadlockStatesAdd.begin(), ite = deadlockStatesAdd.end(); it != ite && count < 3; ++it, ++count) { - STORM_LOG_INFO((*it).first.toPrettyString(generationInfo.rowMetaVariables) << std::endl); - } - - if (program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC) { - storm::dd::Add identity = globalModule.identity; - - // Make sure that global variables do not change along the introduced self-loops. - for (auto const& var : generationInfo.allGlobalVariables) { - identity *= generationInfo.variableToIdentityMap.at(var); - } - - // For DTMCs, we can simply add the identity of the global module for all deadlock states. - transitionMatrix += deadlockStatesAdd * identity; - } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - // For MDPs, however, we need to select an action associated with the self-loop, if we do not - // want to attach a lot of self-loops to the deadlock states. - storm::dd::Add action = generationInfo.manager->template getAddOne(); - for (auto const& metaVariable : generationInfo.allNondeterminismVariables) { - action *= generationInfo.manager->template getIdentity(metaVariable); - } - // Make sure that global variables do not change along the introduced self-loops. - for (auto const& var : generationInfo.allGlobalVariables) { - action *= generationInfo.variableToIdentityMap.at(var); - } - transitionMatrix += deadlockStatesAdd * globalModule.identity * action; - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); - } - } - - // Reduce the deadlock states by the states that we did simply not explore. - deadlockStates = deadlockStates && !terminalStatesBdd; - - // Now build the reward models. - std::vector> selectedRewardModels; - - // First, we make sure that all selected reward models actually exist. - for (auto const& rewardModelName : options.rewardModelsToBuild) { - STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); - } - - for (auto const& rewardModel : program.getRewardModels()) { - if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) { - std::cout << "build all? " << buildAllRewardModels << std::endl; - selectedRewardModels.push_back(rewardModel); - } - } - // If no reward model was selected until now and a referenced reward model appears to be unique, we build - // the only existing reward model (given that no explicit name was given for the referenced reward model). - if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { - selectedRewardModels.push_back(program.getRewardModel(0)); - } - - std::unordered_map> rewardModels; - for (auto const& rewardModel : selectedRewardModels) { - rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, stateActionDd)); - } - - // Build the labels that can be accessed as a shortcut. - std::map labelToExpressionMapping; - for (auto const& label : program.getLabels()) { - labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression()); - } - - if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); - } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); - } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); - } - } - - template - storm::dd::Bdd DdPrismModelBuilder::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) { - storm::dd::Bdd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialStatesExpression()).toBdd(); - - for (auto const& metaVariable : generationInfo.rowMetaVariables) { - initialStates &= generationInfo.manager->getRange(metaVariable); - } - - return initialStates; - } - - // Explicitly instantiate the symbolic model builder. - template class DdPrismModelBuilder; - template class DdPrismModelBuilder; - - } // namespace adapters -} // namespace storm - - From 2ba70e964c24e91f3b7834344f8b299eaf1f4c8b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 13:45:25 +0200 Subject: [PATCH 04/13] Added hasParameters() and supportsParameters() for symbolic models --- src/storm/models/sparse/Model.cpp | 4 ---- src/storm/models/symbolic/Model.cpp | 21 +++++++++++++++++++++ src/storm/models/symbolic/Model.h | 10 ++++++++++ 3 files changed, 31 insertions(+), 4 deletions(-) diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 4bece4dcf..9ee91b5dd 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -423,11 +423,7 @@ namespace storm { template bool Model::supportsParameters() const { -#ifdef STORM_HAVE_CARL return std::is_same::value; -#else - return false; -#endif } template diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index ee90118cb..f7a9f367f 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -15,6 +15,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/dd.h" @@ -362,6 +363,26 @@ namespace storm { bool Model::isSymbolicModel() const { return true; } + + template + bool Model::supportsParameters() const { + return std::is_same::value; + } + + template + bool Model::hasParameters() const { + if (!this->supportsParameters()) { + return false; + } + // Check for parameters + for (auto it = this->getTransitionMatrix().begin(false); it != this->getTransitionMatrix().end(); ++it) { + if (!storm::utility::isConstant((*it).second)) { + return true; + } + } + // Only constant values present + return false; + } template void Model::addParameters(std::set const& parameters) { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 1dca3dc6d..7b3500bd1 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -321,6 +321,16 @@ namespace storm { virtual bool isSymbolicModel() const override; + virtual bool supportsParameters() const override; + + /*! + * Checks whether the model has parameters. + * Performance warning: the worst-case complexity is linear in the number of transitions. + * + * @return True iff the model has parameters. + */ + virtual bool hasParameters() const override; + std::vector getLabels() const; void addParameters(std::set const& parameters); From 94a5a3da7c3638735fc3c334147ae852c0099919 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 May 2018 21:00:00 +0200 Subject: [PATCH 05/13] remove ffast-math --- CMakeLists.txt | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d5c8aa732..d4c789dd7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -179,7 +179,7 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") set(STORM_COMPILER_APPLECLANG ON) set(CLANG ON) set(STORM_COMPILER_ID "AppleClang") - set(CMAKE_MACOSX_RPATH ON) + set(CMAKE_MACOSX_RPATH ON) elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU") set(GCC ON) # using GCC @@ -223,16 +223,16 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG) if(FORCE_COLOR) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics") endif() - + if (LINUX) set(CLANG_STDLIB libstdc++) else() set(CLANG_STDLIB libc++) endif() - + set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -ftemplate-depth=1024") - set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -ffast-math -fno-finite-math-only") - + set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE}") + if(LINUX) set (CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic") set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -rdynamic") @@ -242,20 +242,20 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG) endif() elseif (STORM_COMPILER_GCC) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14") - set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fprefetch-loop-arrays -ffast-math -fno-finite-math-only") + set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fprefetch-loop-arrays") set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic") set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -rdynamic") endif () if (STORM_USE_LTO) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto") - + # Fix for problems that occurred when using LTO on gcc. This should be removed when it # is not needed anymore as it makes the the already long link-step potentially longer. if (STORM_COMPILER_GCC) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto-partition=none") endif() - + message(STATUS "Storm - Enabling link-time optimizations.") else() message(STATUS "Storm - Disabling link-time optimizations.") From 03707f0234f1d6b3f77ca080fbe0149afecccf83 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 May 2018 21:49:39 +0200 Subject: [PATCH 06/13] first step for fixing MEC decomposition: making SCC decomposition accept a bit vector of subsystem choices --- ...tronglyConnectedComponentDecomposition.cpp | 121 ++++++++++++------ .../StronglyConnectedComponentDecomposition.h | 24 +++- 2 files changed, 103 insertions(+), 42 deletions(-) diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp index f6567985c..9eae9d05a 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp @@ -23,30 +23,35 @@ namespace storm { template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end()); - performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(model.getTransitionMatrix(), &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); } template template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(model.getTransitionMatrix(), &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { storm::storage::BitVector subsystem(transitionMatrix.getRowGroupCount(), block.begin(), block.end()); - performSccDecomposition(transitionMatrix, subsystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(transitionMatrix, &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(transitionMatrix, nullptr, nullptr, dropNaiveSccs, onlyBottomSccs); } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, subsystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(transitionMatrix, &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); + } + + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices, bool dropNaiveSccs, bool onlyBottomSccs) { + performSccDecomposition(transitionMatrix, &subsystem, &choices, dropNaiveSccs, onlyBottomSccs); } template @@ -72,7 +77,10 @@ namespace storm { } template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, bool dropNaiveSccs, bool onlyBottomSccs) { + + STORM_LOG_ASSERT(!choices || subsystem, "Expecting subsystem if choices are given."); + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // Set up the environment of the algorithm. @@ -94,16 +102,30 @@ namespace storm { // Start the search for SCCs from every state in the block. uint_fast64_t currentIndex = 0; - for (auto state : subsystem) { - if (!hasPreorderNumber.get(state)) { - performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); + if (subsystem) { + for (auto state : *subsystem) { + if (!hasPreorderNumber.get(state)) { + performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, choices, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); + } + } + } else { + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + if (!hasPreorderNumber.get(state)) { + performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, choices, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); + } } } // After we obtained the state-to-SCC mapping, we build the actual blocks. this->blocks.resize(sccCount); - for (auto state : subsystem) { - this->blocks[stateToSccMapping[state]].insert(state); + if (subsystem) { + for (auto state : *subsystem) { + this->blocks[stateToSccMapping[state]].insert(state); + } + } else { + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + this->blocks[stateToSccMapping[state]].insert(state); + } } // Now flag all trivial SCCs as such. @@ -132,13 +154,34 @@ namespace storm { // If requested, we need to drop all non-bottom SCCs. if (onlyBottomSccs) { - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - // If the block of the state is already known to be dropped, we don't need to check the transitions. - if (!blocksToDrop.get(stateToSccMapping[state])) { - for (typename storm::storage::SparseMatrix::const_iterator successorIt = transitionMatrix.getRowGroup(state).begin(), successorIte = transitionMatrix.getRowGroup(state).end(); successorIt != successorIte; ++successorIt) { - if (subsystem.get(successorIt->getColumn()) && stateToSccMapping[state] != stateToSccMapping[successorIt->getColumn()]) { - blocksToDrop.set(stateToSccMapping[state]); - break; + if (subsystem) { + for (uint64_t state : *subsystem) { + // If the block of the state is already known to be dropped, we don't need to check the transitions. + if (!blocksToDrop.get(stateToSccMapping[state])) { + for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row != endRow; ++row) { + if (choices && !choices->get(row)) { + continue; + } + for (auto const& entry : transitionMatrix.getRow(row)) { + if (subsystem->get(entry.getColumn()) && stateToSccMapping[state] != stateToSccMapping[entry.getColumn()]) { + blocksToDrop.set(stateToSccMapping[state]); + break; + } + } + } + } + } + } else { + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + // If the block of the state is already known to be dropped, we don't need to check the transitions. + if (!blocksToDrop.get(stateToSccMapping[state])) { + for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row != endRow; ++row) { + for (auto const& entry : transitionMatrix.getRow(row)) { + if (stateToSccMapping[state] != stateToSccMapping[entry.getColumn()]) { + blocksToDrop.set(stateToSccMapping[state]); + break; + } + } } } } @@ -163,15 +206,11 @@ namespace storm { template template void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) { - // Prepare a block that contains all states for a call to the other overload of this function. - storm::storage::BitVector fullSystem(model.getNumberOfStates(), true); - - // Call the overloaded function. - performSccDecomposition(model.getTransitionMatrix(), fullSystem, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(model.getTransitionMatrix(), nullptr, nullptr, dropNaiveSccs, onlyBottomSccs); } template - void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount) { + void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount) { // Prepare the stack used for turning the recursive procedure into an iterative one. std::vector recursionStateStack; @@ -190,20 +229,26 @@ namespace storm { s.push_back(currentState); p.push_back(currentState); - for (auto const& successor : transitionMatrix.getRowGroup(currentState)) { - if (subsystem.get(successor.getColumn()) && successor.getValue() != storm::utility::zero()) { - if (currentState == successor.getColumn()) { - statesWithSelfLoop.set(currentState); - } - - if (!hasPreorderNumber.get(successor.getColumn())) { - // In this case, we must recursively visit the successor. We therefore push the state - // onto the recursion stack. - recursionStateStack.push_back(successor.getColumn()); - } else { - if (!stateHasScc.get(successor.getColumn())) { - while (preorderNumbers[p.back()] > preorderNumbers[successor.getColumn()]) { - p.pop_back(); + for (uint64_t row = transitionMatrix.getRowGroupIndices()[currentState], rowEnd = transitionMatrix.getRowGroupIndices()[currentState + 1]; row != rowEnd; ++row) { + if (choices && !choices->get(row)) { + continue; + } + + for (auto const& successor : transitionMatrix.getRow(row)) { + if ((!subsystem || subsystem->get(successor.getColumn())) && successor.getValue() != storm::utility::zero()) { + if (currentState == successor.getColumn()) { + statesWithSelfLoop.set(currentState); + } + + if (!hasPreorderNumber.get(successor.getColumn())) { + // In this case, we must recursively visit the successor. We therefore push the state + // onto the recursion stack. + recursionStateStack.push_back(successor.getColumn()); + } else { + if (!stateHasScc.get(successor.getColumn())) { + while (preorderNumbers[p.back()] > preorderNumbers[successor.getColumn()]) { + p.pop_back(); + } } } } diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.h b/src/storm/storage/StronglyConnectedComponentDecomposition.h index 04cebff92..5a9fa2cf4 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.h @@ -103,6 +103,20 @@ namespace storm { */ StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + /* + * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is + * given by a sparse matrix). + * + * @param transitionMatrix The transition matrix of the system to decompose. + * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. + * @param choices A bit vector indicating which choices of the states are contained in the subsystem. + * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state + * without a self-loop) are to be kept in the decomposition. + * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of + * leaving the SCC), are kept. + */ + StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + /*! * Creates an SCC decomposition by copying the given SCC decomposition. * @@ -158,13 +172,14 @@ namespace storm { * the vector of blocks of the decomposition. * * @param transitionMatrix The transition matrix of the system to decompose. - * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. + * @param subsystem An optional bit vector indicating which subsystem to consider. + * @param choices An optional bit vector indicating which choices belong to the subsystem. * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state * without a self-loop) are to be kept in the decomposition. * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of * leaving the SCC), are kept. */ - void performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); + void performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, bool dropNaiveSccs, bool onlyBottomSccs); /*! * Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to @@ -175,7 +190,8 @@ namespace storm { * @param startState The starting state for the search of Tarjan's algorithm. * @param statesWithSelfLoop A bit vector that is to be filled with all states that have a self-loop. This * is later needed for identification of the naive SCCs. - * @param subsystem The subsystem to search. + * @param subsystem An optional bit vector indicating which subsystem to consider. + * @param choices An optional bit vector indicating which choices belong to the subsystem. * @param currentIndex The next free index that can be assigned to states. * @param hasPreorderNumber A bit that is used to keep track of the states that already have a preorder number. * @param preorderNumbers A vector storing the preorder number for each state. @@ -187,7 +203,7 @@ namespace storm { * @param sccCount The number of SCCs that have been computed. As a side effect of this function, this count * is increased. */ - void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount); + void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount); }; } } From ca651ec61cc91cc1ebcacc8812879f01b8940009 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 May 2018 13:03:14 +0200 Subject: [PATCH 07/13] fixes github issue #24 related to MEC decomposition --- .../testfiles/mdp/prism-mec-example1.nm | 12 ++++++ .../testfiles/mdp/prism-mec-example2.nm | 13 ++++++ .../MaximalEndComponentDecomposition.cpp | 35 +++++++++------ ...tronglyConnectedComponentDecomposition.cpp | 5 +++ .../StronglyConnectedComponentDecomposition.h | 16 ++++++- .../MaximalEndComponentDecompositionTest.cpp | 43 +++++++++++++++++++ 6 files changed, 111 insertions(+), 13 deletions(-) create mode 100644 resources/examples/testfiles/mdp/prism-mec-example1.nm create mode 100644 resources/examples/testfiles/mdp/prism-mec-example2.nm diff --git a/resources/examples/testfiles/mdp/prism-mec-example1.nm b/resources/examples/testfiles/mdp/prism-mec-example1.nm new file mode 100644 index 000000000..bb8ec7d17 --- /dev/null +++ b/resources/examples/testfiles/mdp/prism-mec-example1.nm @@ -0,0 +1,12 @@ +mdp + +module test + + x : [0..2]; + + [] x=0 -> true; + [] x=0 -> 0.5 : (x'=1) + 0.5: (x'=2); + [] x=1 -> (x'=0); + [] x=2 -> true; + +endmodule diff --git a/resources/examples/testfiles/mdp/prism-mec-example2.nm b/resources/examples/testfiles/mdp/prism-mec-example2.nm new file mode 100644 index 000000000..7ef54d4b2 --- /dev/null +++ b/resources/examples/testfiles/mdp/prism-mec-example2.nm @@ -0,0 +1,13 @@ +mdp + +module test + + x : [0..2]; + + [] x=0 -> true; + [] x=0 -> 0.5 : (x'=1) + 0.5: (x'=1); + [] x=0 -> (x'=2); + [] x=1 -> (x'=0); + [] x=2 -> true; + +endmodule diff --git a/src/storm/storage/MaximalEndComponentDecomposition.cpp b/src/storm/storage/MaximalEndComponentDecomposition.cpp index cd8b637e3..7cbf36fd7 100644 --- a/src/storm/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storm/storage/MaximalEndComponentDecomposition.cpp @@ -80,7 +80,20 @@ namespace storm { endComponentStateSets.emplace_back(states.begin(), states.end(), true); } storm::storage::BitVector statesToCheck(numberOfStates); - + storm::storage::BitVector includedChoices; + if (choices) { + includedChoices = *choices; + } else if (states) { + includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount()); + for (auto state : *states) { + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + includedChoices.set(choice, true); + } + } + } else { + includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount(), true); + } + for (std::list::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { StateBlock const& mec = *mecIterator; @@ -88,7 +101,7 @@ namespace storm { bool mecChanged = false; // Get an SCC decomposition of the current MEC candidate. - StronglyConnectedComponentDecomposition sccs(transitionMatrix, mec, true); + StronglyConnectedComponentDecomposition sccs(transitionMatrix, mec, includedChoices, true); // We need to do another iteration in case we have either more than once SCC or the SCC is smaller than // the MEC canditate itself. @@ -105,10 +118,16 @@ namespace storm { bool keepStateInMEC = false; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + // If the choice is not part of our subsystem, skip it. if (choices && !choices->get(choice)) { continue; } + + // If the choice is not included any more, skip it. + if (!includedChoices.get(choice)) { + continue; + } bool choiceContainedInMEC = true; for (auto const& entry : transitionMatrix.getRow(choice)) { @@ -117,6 +136,7 @@ namespace storm { } if (!scc.containsState(entry.getColumn())) { + includedChoices.set(choice, false); choiceContainedInMEC = false; break; } @@ -125,7 +145,6 @@ namespace storm { // If there is at least one choice whose successor states are fully contained in the MEC, we can leave the state in the MEC. if (choiceContainedInMEC) { keepStateInMEC = true; - break; } } @@ -185,15 +204,7 @@ namespace storm { continue; } - bool choiceContained = true; - for (auto const& entry : transitionMatrix.getRow(choice)) { - if (!mecStateSet.containsState(entry.getColumn())) { - choiceContained = false; - break; - } - } - - if (choiceContained) { + if (includedChoices.get(choice)) { containedChoices.insert(choice); } } diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp index 9eae9d05a..6ab3e31f6 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp @@ -38,6 +38,11 @@ namespace storm { performSccDecomposition(transitionMatrix, &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); } + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs, bool onlyBottomSccs) { + storm::storage::BitVector subsystem(transitionMatrix.getRowGroupCount(), block.begin(), block.end()); + performSccDecomposition(transitionMatrix, &subsystem, &choices, dropNaiveSccs, onlyBottomSccs); + } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs, bool onlyBottomSccs) { diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.h b/src/storm/storage/StronglyConnectedComponentDecomposition.h index 5a9fa2cf4..7d244b914 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.h @@ -78,7 +78,21 @@ namespace storm { * leaving the SCC), are kept. */ StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - + + /* + * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is + * given by a sparse matrix). + * + * @param transitionMatrix The transition matrix of the system to decompose. + * @param block The block to decompose into SCCs. + * @param choices A bit vector indicating which choices of the states are contained in the subsystem. + * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state + * without a self-loop) are to be kept in the decomposition. + * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of + * leaving the SCC), are kept. + */ + StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + /* * Creates an SCC decomposition of the given system (whose transition relation is given by a sparse matrix). * diff --git a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp index a7c23edf3..6e9718e6b 100644 --- a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp +++ b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp @@ -3,7 +3,11 @@ #include "storm/parser/AutoParser.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/parser/PrismParser.h" TEST(MaximalEndComponentDecomposition, FullSystem1) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", ""); @@ -133,3 +137,42 @@ TEST(MaximalEndComponentDecomposition, Subsystem) { ASSERT_TRUE(false); } } + +TEST(MaximalEndComponentDecomposition, Example1) { + std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm"; + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + std::shared_ptr> mdp = model->as>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); + + EXPECT_EQ(mecDecomposition.size(), 2); + + ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); + EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{3}); + + ASSERT_TRUE(mecDecomposition[1].getStateSet() == storm::storage::MaximalEndComponent::set_type{0}); + EXPECT_TRUE(mecDecomposition[1].getChoicesForState(0) == storm::storage::MaximalEndComponent::set_type{0}); +} + +TEST(MaximalEndComponentDecomposition, Example2) { + std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example2.nm"; + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); + std::shared_ptr> mdp = model->as>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); + + EXPECT_EQ(mecDecomposition.size(), 2); + + ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); + EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{4}); + + ASSERT_TRUE((mecDecomposition[1].getStateSet() == storm::storage::MaximalEndComponent::set_type{0, 1})); + EXPECT_TRUE((mecDecomposition[1].getChoicesForState(0) == storm::storage::MaximalEndComponent::set_type{0, 1})); + EXPECT_TRUE((mecDecomposition[1].getChoicesForState(1) == storm::storage::MaximalEndComponent::set_type{3})); +} From 62e493d978dca21c17b14117b8609e7150e6b98e Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 May 2018 15:27:26 +0200 Subject: [PATCH 08/13] fix computation of generator matrix, pointed out by jklein --- src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 7e50785d0..a64cf4781 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -722,7 +722,7 @@ namespace storm { for (uint_fast64_t row = 0; row < generatorMatrix.getRowCount(); ++row) { for (auto& entry : generatorMatrix.getRow(row)) { if (entry.getColumn() == row) { - entry.setValue(-exitRates[row]); + entry.setValue(exitRates[row] - entry.getValue()); } } } From e1bb35ca0fe56139e372b7ae47d7e84a42ad7e10 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 May 2018 15:29:37 +0200 Subject: [PATCH 09/13] fix for the generator matrix fix --- src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index a64cf4781..99bad8ce1 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -722,7 +722,7 @@ namespace storm { for (uint_fast64_t row = 0; row < generatorMatrix.getRowCount(); ++row) { for (auto& entry : generatorMatrix.getRow(row)) { if (entry.getColumn() == row) { - entry.setValue(exitRates[row] - entry.getValue()); + entry.setValue(-exitRates[row] + entry.getValue()); } } } From 5c38a4ef896684ddfa9a5b27629958076234f7f5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 28 May 2018 15:42:59 +0200 Subject: [PATCH 10/13] implemented environment for multiobjective settings --- src/storm/environment/Environment.cpp | 23 +++- src/storm/environment/Environment.h | 13 ++- src/storm/environment/SubEnvironment.cpp | 12 ++- .../modelchecker/ModelCheckerEnvironment.cpp | 31 ++++++ .../modelchecker/ModelCheckerEnvironment.h | 28 +++++ .../MultiObjectiveModelCheckerEnvironment.cpp | 100 ++++++++++++++++++ .../MultiObjectiveModelCheckerEnvironment.h | 48 +++++++++ .../multiObjectiveModelChecking.cpp | 6 +- .../pcaa/SparsePcaaAchievabilityQuery.cpp | 7 +- .../pcaa/SparsePcaaParetoQuery.cpp | 24 ++--- .../pcaa/SparsePcaaQuantitativeQuery.cpp | 18 ++-- .../pcaa/SparsePcaaQuantitativeQuery.h | 2 +- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 57 +++++----- .../multiobjective/pcaa/SparsePcaaQuery.h | 4 +- 14 files changed, 305 insertions(+), 68 deletions(-) create mode 100644 src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp create mode 100644 src/storm/environment/modelchecker/ModelCheckerEnvironment.h create mode 100644 src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp create mode 100644 src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h diff --git a/src/storm/environment/Environment.cpp b/src/storm/environment/Environment.cpp index 0836de3f7..6d5d3ca2b 100644 --- a/src/storm/environment/Environment.cpp +++ b/src/storm/environment/Environment.cpp @@ -1,6 +1,8 @@ #include "storm/environment/Environment.h" #include "storm/environment/SubEnvironment.h" #include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" + namespace storm { @@ -12,11 +14,28 @@ namespace storm { // Intentionally left empty. } + Environment::Environment(Environment const& other) : internalEnv(other.internalEnv) { + // Intentionally left empty. + } + + Environment& Environment::operator=(Environment const& other) { + internalEnv = other.internalEnv; + return *this; + } + SolverEnvironment& Environment::solver() { - return solverEnvironment.get(); + return internalEnv.get().solverEnvironment.get(); } SolverEnvironment const& Environment::solver() const { - return solverEnvironment.get(); + return internalEnv.get().solverEnvironment.get(); + } + + ModelCheckerEnvironment& Environment::modelchecker() { + return internalEnv.get().modelcheckerEnvironment.get(); + } + + ModelCheckerEnvironment const& Environment::modelchecker() const { + return internalEnv.get().modelcheckerEnvironment.get(); } } \ No newline at end of file diff --git a/src/storm/environment/Environment.h b/src/storm/environment/Environment.h index 988ca34c6..30ac31803 100644 --- a/src/storm/environment/Environment.h +++ b/src/storm/environment/Environment.h @@ -6,19 +6,30 @@ namespace storm { // Forward declare sub-environments class SolverEnvironment; + class ModelCheckerEnvironment; + + // Avoid implementing ugly copy constructors for environment by using an internal environment. + struct InternalEnvironment { + SubEnvironment solverEnvironment; + SubEnvironment modelcheckerEnvironment; + }; class Environment { public: Environment(); virtual ~Environment(); + Environment(Environment const& other); + Environment& operator=(Environment const& other); SolverEnvironment& solver(); SolverEnvironment const& solver() const; + ModelCheckerEnvironment& modelchecker(); + ModelCheckerEnvironment const& modelchecker() const; private: - SubEnvironment solverEnvironment; + SubEnvironment internalEnv; }; } diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index f11b2b1bf..920a06049 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -1,4 +1,9 @@ -#include +#include + +#include "storm/environment/Environment.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" + #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" @@ -36,6 +41,11 @@ namespace storm { return *subEnv; } + template class SubEnvironment; + + template class SubEnvironment; + template class SubEnvironment; + template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp new file mode 100644 index 000000000..f0d917a28 --- /dev/null +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp @@ -0,0 +1,31 @@ +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" + +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidEnvironmentException.h" +#include "storm/exceptions/UnexpectedException.h" + + +namespace storm { + + ModelCheckerEnvironment::ModelCheckerEnvironment() { + // Intentionally left empty + } + + ModelCheckerEnvironment::~ModelCheckerEnvironment() { + // Intentionally left empty + } + + MultiObjectiveModelCheckerEnvironment& ModelCheckerEnvironment::multi() { + return multiObjectiveModelCheckerEnvironment.get(); + } + + MultiObjectiveModelCheckerEnvironment const& ModelCheckerEnvironment::multi() const { + return multiObjectiveModelCheckerEnvironment.get(); + } +} + + diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.h b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h new file mode 100644 index 000000000..2ec1eebd8 --- /dev/null +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h @@ -0,0 +1,28 @@ +#pragma once + +#include +#include + +#include "storm/environment/Environment.h" +#include "storm/environment/SubEnvironment.h" + +namespace storm { + + // Forward declare subenvironments + class MultiObjectiveModelCheckerEnvironment; + + class ModelCheckerEnvironment { + public: + + ModelCheckerEnvironment(); + ~ModelCheckerEnvironment(); + + MultiObjectiveModelCheckerEnvironment& multi(); + MultiObjectiveModelCheckerEnvironment const& multi() const; + + + private: + SubEnvironment multiObjectiveModelCheckerEnvironment; + }; +} + diff --git a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp new file mode 100644 index 000000000..92b51fde8 --- /dev/null +++ b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp @@ -0,0 +1,100 @@ +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +namespace storm { + + MultiObjectiveModelCheckerEnvironment::MultiObjectiveModelCheckerEnvironment() { + auto const& multiobjectiveSettings = storm::settings::getModule(); + method = multiobjectiveSettings.getMultiObjectiveMethod(); + if (multiobjectiveSettings.isExportPlotSet()) { + plotPathUnderApprox = multiobjectiveSettings.getExportPlotDirectory() + "underapproximation.csv"; + plotPathOverApprox = multiobjectiveSettings.getExportPlotDirectory() + "overapproximation.csv"; + plotPathParetoPoints = multiobjectiveSettings.getExportPlotDirectory() + "paretopoints.csv"; + } + + precision = storm::utility::convertNumber(multiobjectiveSettings.getPrecision()); + if (multiobjectiveSettings.isMaxStepsSet()) { + maxSteps = multiobjectiveSettings.getMaxSteps(); + } + } + + MultiObjectiveModelCheckerEnvironment::~MultiObjectiveModelCheckerEnvironment() { + // Intentionally left empty + } + + storm::modelchecker::multiobjective::MultiObjectiveMethod const& MultiObjectiveModelCheckerEnvironment::getMethod() const { + return this->method; + } + + void MultiObjectiveModelCheckerEnvironment::setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod value) { + this->method = value; + } + + bool MultiObjectiveModelCheckerEnvironment::isExportPlotSet() const { + return this->plotPathUnderApprox.is_initialized() || this->plotPathOverApprox.is_initialized() || this->plotPathParetoPoints.is_initialized(); + } + + boost::optional MultiObjectiveModelCheckerEnvironment::getPlotPathUnderApproximation() const { + return plotPathUnderApprox; + } + + void MultiObjectiveModelCheckerEnvironment::setPlotPathUnderApproximation(std::string const& path) { + plotPathUnderApprox = path; + } + + void MultiObjectiveModelCheckerEnvironment::unsetPlotPathUnderApproximation() { + plotPathUnderApprox = boost::none; + } + + boost::optional MultiObjectiveModelCheckerEnvironment::getPlotPathOverApproximation() const { + return plotPathOverApprox; + } + + void MultiObjectiveModelCheckerEnvironment::setPlotPathOverApproximation(std::string const& path) { + plotPathOverApprox = path; + } + + void MultiObjectiveModelCheckerEnvironment::unsetPlotPathOverApproximation() { + plotPathOverApprox = boost::none; + } + + boost::optional MultiObjectiveModelCheckerEnvironment::getPlotPathParetoPoints() const { + return plotPathParetoPoints; + } + + void MultiObjectiveModelCheckerEnvironment::setPlotPathParetoPoints(std::string const& path) { + plotPathParetoPoints = path; + } + + void MultiObjectiveModelCheckerEnvironment::unsetPlotPathParetoPoints() { + plotPathParetoPoints = boost::none; + } + + storm::RationalNumber const& MultiObjectiveModelCheckerEnvironment::getPrecision() const { + return precision; + } + + void MultiObjectiveModelCheckerEnvironment::setPrecision(storm::RationalNumber const& value) { + precision = value; + } + + bool MultiObjectiveModelCheckerEnvironment::isMaxStepsSet() const { + return maxSteps.is_initialized(); + } + + uint64_t const& MultiObjectiveModelCheckerEnvironment::getMaxSteps() const { + return maxSteps.get(); + } + + void MultiObjectiveModelCheckerEnvironment::setMaxSteps(uint64_t const& value) { + maxSteps = value; + } + + void MultiObjectiveModelCheckerEnvironment::unsetMaxSteps() { + maxSteps = boost::none; + } +} \ No newline at end of file diff --git a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h new file mode 100644 index 000000000..f1d4f0203 --- /dev/null +++ b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h @@ -0,0 +1,48 @@ +#pragma once + +#include + +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" +#include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h" +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + + class MultiObjectiveModelCheckerEnvironment { + public: + + MultiObjectiveModelCheckerEnvironment(); + ~MultiObjectiveModelCheckerEnvironment(); + + storm::modelchecker::multiobjective::MultiObjectiveMethod const& getMethod() const; + void setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod value); + + bool isExportPlotSet() const; + boost::optional getPlotPathUnderApproximation() const; + void setPlotPathUnderApproximation(std::string const& path); + void unsetPlotPathUnderApproximation(); + boost::optional getPlotPathOverApproximation() const; + void setPlotPathOverApproximation(std::string const& path); + void unsetPlotPathOverApproximation(); + boost::optional getPlotPathParetoPoints() const; + void setPlotPathParetoPoints(std::string const& path); + void unsetPlotPathParetoPoints(); + + storm::RationalNumber const& getPrecision() const; + void setPrecision(storm::RationalNumber const& value); + + uint64_t const& getMaxSteps() const; + bool isMaxStepsSet() const; + void setMaxSteps(uint64_t const& value); + void unsetMaxSteps(); + + + private: + storm::modelchecker::multiobjective::MultiObjectiveMethod method; + boost::optional plotPathUnderApprox, plotPathOverApprox, plotPathParetoPoints; + storm::RationalNumber precision; + boost::optional maxSteps; + + }; +} + diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index 10276ffa6..bb18e9385 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -1,7 +1,7 @@ #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/utility/macros.h" - +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -74,8 +74,8 @@ namespace storm { result = query->check(env); - if(storm::settings::getModule().isExportPlotSet()) { - query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); + if (env.modelchecker().multi().isExportPlotSet()) { + query->exportPlotOfCurrentApproximation(env); } break; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index 409bd9ba9..b8ac5fe2d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -7,9 +7,8 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" + #include "storm/exceptions/InvalidOperationException.h" @@ -57,7 +56,7 @@ namespace storm { template bool SparsePcaaAchievabilityQuery::checkAchievability(Environment const& env) { // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx. - while(!this->maxStepsPerformed()){ + while(!this->maxStepsPerformed(env)){ WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecision(separatingVector); this->performRefinementStep(env, std::move(separatingVector)); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index fe7a7b367..93c04e527 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -7,10 +7,7 @@ #include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" -#include "storm/settings/modules/GeneralSettings.h" - +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" namespace storm { namespace modelchecker { @@ -19,20 +16,19 @@ namespace storm { template SparsePcaaParetoQuery::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult::QueryType::Pareto, "Invalid query Type"); + } + + template + std::unique_ptr SparsePcaaParetoQuery::check(Environment const& env) { // Set the precision of the weight vector checker - typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); + typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); weightedPrecision /= storm::utility::sqrt(storm::utility::convertNumber(this->objectives.size())); // multiobjPrecision / sqrt(numObjectives) is the largest possible value for which termination is guaranteed. // Lets be a little bit more precise to reduce the number of required iterations. weightedPrecision *= storm::utility::convertNumber(0.9); this->weightVectorChecker->setWeightedPrecision(weightedPrecision); - - } - - template - std::unique_ptr SparsePcaaParetoQuery::check(Environment const& env) { - + // refine the approximation exploreSetOfAchievablePoints(env); @@ -55,13 +51,13 @@ namespace storm { void SparsePcaaParetoQuery::exploreSetOfAchievablePoints(Environment const& env) { //First consider the objectives individually - for(uint_fast64_t objIndex = 0; objIndexobjectives.size() && !this->maxStepsPerformed(); ++objIndex) { + for(uint_fast64_t objIndex = 0; objIndexobjectives.size() && !this->maxStepsPerformed(env); ++objIndex) { WeightVector direction(this->objectives.size(), storm::utility::zero()); direction[objIndex] = storm::utility::one(); this->performRefinementStep(env, std::move(direction)); } - while(!this->maxStepsPerformed()) { + while(!this->maxStepsPerformed(env)) { // Get the halfspace of the underApproximation with maximal distance to a vertex of the overApproximation std::vector> underApproxHalfspaces = this->underApproximation->getHalfspaces(); std::vector overApproxVertices = this->overApproximation->getVertices(); @@ -76,7 +72,7 @@ namespace storm { } } } - if(farestDistance < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { + if(farestDistance < storm::utility::convertNumber(env.modelchecker().multi().getPrecision())) { // Goal precision reached! return; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 538752ab2..4df353cdd 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -8,9 +8,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" -#include "storm/settings/modules/GeneralSettings.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/exceptions/InvalidOperationException.h" @@ -99,7 +97,7 @@ namespace storm { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); - while(!this->maxStepsPerformed()){ + while(!this->maxStepsPerformed(env)){ WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecisionInAchievabilityPhase(separatingVector); this->performRefinementStep(env, std::move(separatingVector)); @@ -150,10 +148,10 @@ namespace storm { // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds. GeometryValueType result = storm::utility::zero(); - while(!this->maxStepsPerformed()) { + while(!this->maxStepsPerformed(env)) { if (this->refinementSteps.empty()) { // We did not make any refinement steps during the checkAchievability phase (e.g., because there is only one objective). - this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(storm::settings::getModule().getPrecision())); + this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(env.modelchecker().multi().getPrecision())); WeightVector separatingVector = directionOfOptimizingObjective; this->performRefinementStep(env, std::move(separatingVector)); } @@ -165,7 +163,7 @@ namespace storm { optimizationRes = this->overApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); if (optimizationRes.second) { GeometryValueType precisionOfResult = optimizationRes.first[indexOfOptimizingObjective] - result; - if (precisionOfResult < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { + if (precisionOfResult < storm::utility::convertNumber(env.modelchecker().multi().getPrecision())) { // Goal precision reached! return result; } else { @@ -176,7 +174,7 @@ namespace storm { thresholds[indexOfOptimizingObjective] = result + storm::utility::one(); } WeightVector separatingVector = this->findSeparatingVector(thresholds); - this->updateWeightedPrecisionInImprovingPhase(separatingVector); + this->updateWeightedPrecisionInImprovingPhase(env, separatingVector); this->performRefinementStep(env, std::move(separatingVector)); } STORM_LOG_ERROR("Could not reach the desired precision: Exceeded maximum number of refinement steps"); @@ -185,11 +183,11 @@ namespace storm { template - void SparsePcaaQuantitativeQuery::updateWeightedPrecisionInImprovingPhase(WeightVector const& weights) { + void SparsePcaaQuantitativeQuery::updateWeightedPrecisionInImprovingPhase(Environment const& env, WeightVector const& weights) { STORM_LOG_THROW(!storm::utility::isZero(weights[this->indexOfOptimizingObjective]), exceptions::UnexpectedException, "The chosen weight-vector gives zero weight for the objective that is to be optimized."); // If weighs[indexOfOptimizingObjective] is low, the computation of the weightVectorChecker needs to be more precise. // Our heuristic ensures that if p is the new vertex of the under-approximation, then max{ eps | p' = p + (0..0 eps 0..0) is in the over-approximation } <= multiobjective_precision/0.9 - GeometryValueType weightedPrecision = weights[this->indexOfOptimizingObjective] * storm::utility::convertNumber(storm::settings::getModule().getPrecision()); + GeometryValueType weightedPrecision = weights[this->indexOfOptimizingObjective] * storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); // Normalize by division with the Euclidean Norm of the weight-vector weightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weights, weights)); weightedPrecision *= storm::utility::convertNumber(0.9); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h index 164a87f21..234e6f291 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h @@ -45,7 +45,7 @@ namespace storm { * Updates the precision of the weightVectorChecker w.r.t. the provided weights */ void updateWeightedPrecisionInAchievabilityPhase(WeightVector const& weights); - void updateWeightedPrecisionInImprovingPhase(WeightVector const& weights); + void updateWeightedPrecisionInImprovingPhase(Environment const& env, WeightVector const& weights); /* * Given that the thresholds are achievable, this function further refines the approximations and returns the optimized value diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 2164665e0..ef7e50d80 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -5,8 +5,7 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/multiobjective/Objective.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/storage/geometry/Hyperrectangle.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" @@ -126,9 +125,9 @@ namespace storm { } template - bool SparsePcaaQuery::maxStepsPerformed() const { - return storm::settings::getModule().isMaxStepsSet() && - this->refinementSteps.size() >= storm::settings::getModule().getMaxSteps(); + bool SparsePcaaQuery::maxStepsPerformed(Environment const& env) const { + return env.modelchecker().multi().isMaxStepsSet() && + this->refinementSteps.size() >= env.modelchecker().multi().getMaxSteps(); } @@ -191,7 +190,7 @@ namespace storm { } template - void SparsePcaaQuery::exportPlotOfCurrentApproximation(std::string const& destinationDir) const { + void SparsePcaaQuery::exportPlotOfCurrentApproximation(Environment const& env) const { STORM_LOG_ERROR_COND(objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case."); @@ -223,35 +222,33 @@ namespace storm { std::vector columnHeaders = {"x", "y"}; std::vector> pointsForPlotting; - underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(underApproxVertices.size()); - for(auto const& v : underApproxVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); - } - storm::utility::exportDataToCSVFile(destinationDir + "underapproximation.csv", pointsForPlotting, columnHeaders); - - pointsForPlotting.clear(); - overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(overApproxVertices.size()); - for(auto const& v : overApproxVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + if (env.modelchecker().multi().getPlotPathUnderApproximation()) { + underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(underApproxVertices.size()); + for(auto const& v : underApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathUnderApproximation().get(), pointsForPlotting, columnHeaders); } - storm::utility::exportDataToCSVFile(destinationDir + "overapproximation.csv", pointsForPlotting, columnHeaders); - pointsForPlotting.clear(); - pointsForPlotting.reserve(paretoPoints.size()); - for(auto const& v : paretoPoints) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + if (env.modelchecker().multi().getPlotPathOverApproximation()) { + pointsForPlotting.clear(); + overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(overApproxVertices.size()); + for(auto const& v : overApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathOverApproximation().get(), pointsForPlotting, columnHeaders); } - storm::utility::exportDataToCSVFile(destinationDir + "paretopoints.csv", pointsForPlotting, columnHeaders); - pointsForPlotting.clear(); - auto boundVertices = boundariesAsPolytope->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(4); - for(auto const& v : boundVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + if (env.modelchecker().multi().getPlotPathParetoPoints()) { + pointsForPlotting.clear(); + pointsForPlotting.reserve(paretoPoints.size()); + for(auto const& v : paretoPoints) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathParetoPoints().get(), pointsForPlotting, columnHeaders); } - storm::utility::exportDataToCSVFile(destinationDir + "boundaries.csv", pointsForPlotting, columnHeaders); } #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index d92f0ccee..630503a08 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -38,7 +38,7 @@ namespace storm { * Note that the approximations will be intersected with a (sufficiently large) hyperrectangle in order to ensure that the polytopes are bounded * This only works for 2 dimensional queries. */ - void exportPlotOfCurrentApproximation(std::string const& destinationDir) const; + void exportPlotOfCurrentApproximation(Environment const& env) const; protected: @@ -87,7 +87,7 @@ namespace storm { /* * Returns true iff the maximum number of refinement steps (as possibly specified in the settings) has been reached */ - bool maxStepsPerformed() const; + bool maxStepsPerformed(Environment const& env) const; /* * Transforms the given point (or polytope) to values w.r.t. the original model/formula (e.g. negates values for minimizing objectives). From 1e4b81812cc40aedd022a2ce5a37afbb3af8dc07 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 29 May 2018 16:47:39 +0200 Subject: [PATCH 11/13] Environment does no longer require that unused setting modules still have to be registered. --- src/storm/environment/SubEnvironment.cpp | 19 ++++++++++++++++--- src/storm/environment/SubEnvironment.h | 4 ++-- 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index 920a06049..5226fdca4 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -16,31 +16,44 @@ namespace storm { template - SubEnvironment::SubEnvironment() : subEnv(std::make_unique()) { + SubEnvironment::SubEnvironment() : subEnv(nullptr) { // Intentionally left empty } template - SubEnvironment::SubEnvironment(SubEnvironment const& other) : subEnv(new EnvironmentType(*other.subEnv)) { + SubEnvironment::SubEnvironment(SubEnvironment const& other) : subEnv(other.subEnv ? new EnvironmentType(*other.subEnv) : nullptr) { // Intentionally left empty } template SubEnvironment& SubEnvironment::operator=(SubEnvironment const& other) { - subEnv = std::make_unique(*other.subEnv); + if (other.subEnv) { + subEnv = std::make_unique(*other.subEnv); + } else { + subEnv.reset(); + } return *this; } template EnvironmentType const& SubEnvironment::get() const { + assertInitialized(); return *subEnv; } template EnvironmentType& SubEnvironment::get() { + assertInitialized(); return *subEnv; } + template + void SubEnvironment::assertInitialized() const { + if (!subEnv) { + subEnv = std::make_unique(); + } + } + template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/SubEnvironment.h b/src/storm/environment/SubEnvironment.h index 2b6ecbf87..b1858936d 100644 --- a/src/storm/environment/SubEnvironment.h +++ b/src/storm/environment/SubEnvironment.h @@ -16,8 +16,8 @@ namespace storm { EnvironmentType& get(); private: - std::unique_ptr subEnv; + void assertInitialized() const; + mutable std::unique_ptr subEnv; }; } - From 99e561995208116cfa7c7f65216b8b14932a68dd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 28 May 2018 17:33:05 +0200 Subject: [PATCH 12/13] Export storm targets --- CMakeLists.txt | 2 ++ src/storm-cli-utilities/CMakeLists.txt | 2 +- src/storm-dft-cli/CMakeLists.txt | 2 +- src/storm-dft/CMakeLists.txt | 2 +- src/storm-gspn-cli/CMakeLists.txt | 2 +- src/storm-gspn/CMakeLists.txt | 2 +- src/storm-pars-cli/CMakeLists.txt | 2 +- src/storm-pars/CMakeLists.txt | 2 +- src/storm-pgcl-cli/CMakeLists.txt | 2 +- src/storm-pgcl/CMakeLists.txt | 2 +- src/storm/CMakeLists.txt | 4 ++-- 11 files changed, 13 insertions(+), 11 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d4c789dd7..43ddbd8e9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -500,4 +500,6 @@ add_subdirectory(src) include(export) +install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${CMAKE_INSTALL_DIR}) + include(StormCPackConfig.cmake) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt index 64c2848c7..84819b72b 100644 --- a/src/storm-cli-utilities/CMakeLists.txt +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -36,5 +36,5 @@ add_custom_target(copy_storm_cli_util_headers DEPENDS ${STORM_CLI_UTIL_OUTPUT_HE add_dependencies(storm-cli-utilities copy_storm_pars_headers) # installation -install(TARGETS storm-cli-utilities RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-cli-utilities EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index 4780eef4d..5886ac0a0 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -6,4 +6,4 @@ set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") add_dependencies(binaries storm-dft-cli) # installation -install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-dft-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 9ec70aed2..f191e537f 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -36,5 +36,5 @@ add_custom_target(copy_storm_dft_headers DEPENDS ${STORM_DFT_OUTPUT_HEADERS} ${S add_dependencies(storm-dft copy_storm_dft_headers) # installation -install(TARGETS storm-dft RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-dft EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt index 39d656a4c..f06ff4a53 100644 --- a/src/storm-gspn-cli/CMakeLists.txt +++ b/src/storm-gspn-cli/CMakeLists.txt @@ -5,4 +5,4 @@ set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn") add_dependencies(binaries storm-gspn-cli) # installation -install(TARGETS storm-gspn-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-gspn-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt index cf80ff6aa..9312af543 100644 --- a/src/storm-gspn/CMakeLists.txt +++ b/src/storm-gspn/CMakeLists.txt @@ -15,4 +15,4 @@ set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES}) # installation -install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-gspn EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt index 9e2f6f315..955ee93c8 100644 --- a/src/storm-pars-cli/CMakeLists.txt +++ b/src/storm-pars-cli/CMakeLists.txt @@ -6,4 +6,4 @@ set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars") add_dependencies(binaries storm-pars-cli) # installation -install(TARGETS storm-pars-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-pars-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pars/CMakeLists.txt b/src/storm-pars/CMakeLists.txt index 4e2ec1e0f..b91292be4 100644 --- a/src/storm-pars/CMakeLists.txt +++ b/src/storm-pars/CMakeLists.txt @@ -36,5 +36,5 @@ add_custom_target(copy_storm_pars_headers DEPENDS ${STORM_PARS_OUTPUT_HEADERS} $ add_dependencies(storm-pars copy_storm_pars_headers) # installation -install(TARGETS storm-pars RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-pars EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pgcl-cli/CMakeLists.txt b/src/storm-pgcl-cli/CMakeLists.txt index 4f2799d4d..506772fd9 100644 --- a/src/storm-pgcl-cli/CMakeLists.txt +++ b/src/storm-pgcl-cli/CMakeLists.txt @@ -5,4 +5,4 @@ set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl") add_dependencies(binaries storm-pgcl-cli) # installation -install(TARGETS storm-pgcl-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-pgcl-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pgcl/CMakeLists.txt b/src/storm-pgcl/CMakeLists.txt index e20a99483..059bff395 100644 --- a/src/storm-pgcl/CMakeLists.txt +++ b/src/storm-pgcl/CMakeLists.txt @@ -13,4 +13,4 @@ add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS}) target_link_libraries(storm-pgcl storm) # installation -install(TARGETS storm-pgcl RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-pgcl EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 0cf8d3183..6a8cda64e 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -72,7 +72,7 @@ add_dependencies(storm copy_resources_headers) add_dependencies(binaries storm-main) # installation -install(TARGETS storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib) -install(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib) +install(TARGETS storm-main EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) install(DIRECTORY ${CMAKE_BINARY_DIR}/include/ DESTINATION include/storm FILES_MATCHING PATTERN "*.h") From c5e356bc40956c22c2e2c3b41d2bd1a0e1a055d9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 May 2018 16:50:30 +0200 Subject: [PATCH 13/13] Proper installation of Storm --- CMakeLists.txt | 10 ++++++++++ resources/cmake/macros/export.cmake | 20 ++++++++++++++++++-- resources/cmake/stormConfigVersion.cmake.in | 11 +++++++++++ 3 files changed, 39 insertions(+), 2 deletions(-) create mode 100644 resources/cmake/stormConfigVersion.cmake.in diff --git a/CMakeLists.txt b/CMakeLists.txt index 43ddbd8e9..8ca3b9b7e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -78,6 +78,14 @@ set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables") set(DEF_INSTALL_CMAKE_DIR "lib/CMake/storm") set(CMAKE_INSTALL_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH "Installation directory for CMake files") +# Add CMake install prefix +foreach(p LIB BIN INCLUDE CMAKE) + set(var ${p}_INSTALL_DIR) + if(NOT IS_ABSOLUTE "${${var}}") + set(${var} "${CMAKE_INSTALL_PREFIX}/${${var}}") + endif() +endforeach() + message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}") # If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version. @@ -500,6 +508,8 @@ add_subdirectory(src) include(export) +install(FILES ${CMAKE_BINARY_DIR}/stormConfig.install.cmake DESTINATION ${CMAKE_INSTALL_DIR} RENAME stormConfig.cmake) +install(FILES ${CMAKE_BINARY_DIR}/stormConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_DIR}) install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${CMAKE_INSTALL_DIR}) include(StormCPackConfig.cmake) diff --git a/resources/cmake/macros/export.cmake b/resources/cmake/macros/export.cmake index eb2e8fa84..606bde62f 100644 --- a/resources/cmake/macros/export.cmake +++ b/resources/cmake/macros/export.cmake @@ -8,7 +8,7 @@ message(STATUS "Registered with cmake") export(PACKAGE storm) set(DEP_TARGETS "") -foreach(dt ${STORM_DEP_TARGETS}) +foreach(dt ${STORM_DEP_TARGETS}) export_target(DEP_TARGETS ${dt}) endforeach() @@ -19,10 +19,26 @@ endforeach() include(CMakePackageConfigHelpers) +write_basic_package_version_file(${CMAKE_CURRENT_BINARY_DIR}/stormConfigVersion.cmake + VERSION 0.1.0 + COMPATIBILITY SameMajorVersion ) + +# For the build tree set(CONF_INCLUDE_DIRS "${CMAKE_BINARY_DIR}/include/") configure_package_config_file( resources/cmake/stormConfig.cmake.in ${PROJECT_BINARY_DIR}/stormConfig.cmake INSTALL_DESTINATION ${CMAKE_INSTALL_DIR} - PATH_VARS INCLUDE_INSTALL_DIR #SYSCONFIG_INSTALL_DIR + PATH_VARS INCLUDE_INSTALL_DIR +) + + # For the install tree +file(RELATIVE_PATH REL_INCLUDE_DIR "${CMAKE_INSTALL_DIR}" "${INCLUDE_INSTALL_DIR}") +set(CONF_INCLUDE_DIRS "\${storm_CMAKE_DIR}/${REL_INCLUDE_DIR}/storm") + +configure_package_config_file( + resources/cmake/stormConfig.cmake.in + ${PROJECT_BINARY_DIR}/stormConfig.install.cmake + INSTALL_DESTINATION ${CMAKE_INSTALL_DIR} + PATH_VARS INCLUDE_INSTALL_DIR ) diff --git a/resources/cmake/stormConfigVersion.cmake.in b/resources/cmake/stormConfigVersion.cmake.in new file mode 100644 index 000000000..d248393ad --- /dev/null +++ b/resources/cmake/stormConfigVersion.cmake.in @@ -0,0 +1,11 @@ +set(PACKAGE_VERSION "@storm_VERSION@") + +# Check whether the requested PACKAGE_FIND_VERSION is compatible +if("${PACKAGE_VERSION}" VERSION_LESS "${PACKAGE_FIND_VERSION}") + set(PACKAGE_VERSION_COMPATIBLE FALSE) +else() + set(PACKAGE_VERSION_COMPATIBLE TRUE) + if ("${PACKAGE_VERSION}" VERSION_EQUAL "${PACKAGE_FIND_VERSION}") + set(PACKAGE_VERSION_EXACT TRUE) + endif() +endif()