From 99badd02c54f438e00d9437ccce96661a9dc4c41 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 13 Sep 2016 11:06:34 +0200 Subject: [PATCH] more work towards JANI reward models Former-commit-id: 4be9f840c4742c7f9d6d42e29b50aa3e424e3d34 [formerly be673543113b2335f7bb59bc6a57c7c595d60b16] Former-commit-id: b8ea6172e77b792c739a9f80badcdc261eeabfaa --- examples/dtmc/die/die.pm | 1 + src/builder/DdJaniModelBuilder.cpp | 189 ++++++++++++++---- src/builder/DdPrismModelBuilder.cpp | 2 + src/cli/cli.cpp | 3 + src/generator/JaniNextStateGenerator.cpp | 7 +- .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 2 +- src/settings/modules/IOSettings.cpp | 10 + src/settings/modules/IOSettings.h | 8 + src/storage/SymbolicModelDescription.cpp | 2 + src/storage/jani/Automaton.cpp | 10 +- src/storage/jani/Automaton.h | 7 +- src/storage/jani/Location.cpp | 6 + src/storage/jani/Location.h | 5 + src/storage/jani/Model.cpp | 6 + src/storage/jani/Model.h | 5 + 15 files changed, 222 insertions(+), 41 deletions(-) diff --git a/examples/dtmc/die/die.pm b/examples/dtmc/die/die.pm index dacde8a79..c5634bf4f 100644 --- a/examples/dtmc/die/die.pm +++ b/examples/dtmc/die/die.pm @@ -29,3 +29,4 @@ label "three" = s=7&d=3; label "four" = s=7&d=4; label "five" = s=7&d=5; label "six" = s=7&d=6; +label "end" = s=7; diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 1a61b51c0..5ab18683b 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -241,6 +241,7 @@ namespace storm { // Start by creating a meta variable for the location of the automaton. std::pair variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1); result.automatonToLocationVariableMap[automaton.getName()] = variablePair; + result.rowColumnMetaVariablePairs.push_back(variablePair); // Add the location variable to the row/column variables. result.rowMetaVariables.insert(variablePair.first); @@ -353,11 +354,13 @@ namespace storm { template struct ComposerResult { - ComposerResult(storm::dd::Add const& transitions, storm::dd::Bdd const& illegalFragment, uint64_t numberOfNondeterminismVariables = 0) : transitions(transitions), illegalFragment(illegalFragment), numberOfNondeterminismVariables(numberOfNondeterminismVariables) { + ComposerResult(storm::dd::Add const& transitions, std::map> const& transientLocationAssignments, std::map> const& transientEdgeAssignments, storm::dd::Bdd const& illegalFragment, uint64_t numberOfNondeterminismVariables = 0) : transitions(transitions), transientLocationAssignments(transientLocationAssignments), transientEdgeAssignments(transientEdgeAssignments), illegalFragment(illegalFragment), numberOfNondeterminismVariables(numberOfNondeterminismVariables) { // Intentionally left empty. } storm::dd::Add transitions; + std::map> transientLocationAssignments; + std::map> transientEdgeAssignments; storm::dd::Bdd illegalFragment; uint64_t numberOfNondeterminismVariables; }; @@ -919,7 +922,7 @@ namespace storm { public: // This structure represents an edge. struct EdgeDd { - EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::map> const& transientVariableAssignments = {}, std::set const& writtenGlobalVariables = {}) : guard(guard), transitions(transitions), transientVariableAssignments(transientVariableAssignments), writtenGlobalVariables(writtenGlobalVariables) { + EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::map> const& transientEdgeAssignments = {}, std::set const& writtenGlobalVariables = {}) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), writtenGlobalVariables(writtenGlobalVariables) { // Intentionally left empty. } @@ -930,7 +933,7 @@ namespace storm { storm::dd::Add transitions; // A mapping from transient variables to the DDs representing their value assignments. - std::map> transientVariableAssignments; + std::map> transientEdgeAssignments; // The set of global variables written by this edge. std::set writtenGlobalVariables; @@ -938,7 +941,7 @@ namespace storm { // This structure represents an edge. struct ActionDd { - ActionDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::pair localNondeterminismVariables = std::pair(0, 0), std::map> const& variableToWritingFragment = {}, storm::dd::Bdd const& illegalFragment = storm::dd::Bdd()) : guard(guard), transitions(transitions), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment) { + ActionDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::map> const& transientEdgeAssignments = {}, std::pair localNondeterminismVariables = std::pair(0, 0), std::map> const& variableToWritingFragment = {}, storm::dd::Bdd const& illegalFragment = storm::dd::Bdd()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment) { // Intentionally left empty. } @@ -960,6 +963,9 @@ namespace storm { // A DD that represents the transitions of this edge. storm::dd::Add transitions; + // A mapping from transient variables to their assignments. + std::map> transientEdgeAssignments; + // The local nondeterminism variables used by this action DD, given as the lowest std::pair localNondeterminismVariables; @@ -974,7 +980,7 @@ namespace storm { // This structure represents a subcomponent of a composition. struct AutomatonDd { - AutomatonDd(storm::dd::Add const& identity) : actionIndexToAction(), identity(identity), localNondeterminismVariables(std::make_pair(0, 0)) { + AutomatonDd(storm::dd::Add const& identity, std::map> const& transientLocationAssignments = {}) : actionIndexToAction(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair(0, 0)) { // Intentionally left empty. } @@ -1002,6 +1008,9 @@ namespace storm { // A mapping from action indices to the action DDs. std::map actionIndexToAction; + // A mapping from transient variables to their location-based transient assignment values. + std::map> transientLocationAssignments; + // The identity of the automaton's variables. storm::dd::Add identity; @@ -1094,6 +1103,7 @@ namespace storm { private: AutomatonDd composeInParallel(AutomatonDd const& automaton1, AutomatonDd const& automaton2, std::set const& synchronizingActionIndices) { AutomatonDd result(automaton1); + result.transientLocationAssignments = joinTransientAssignmentMaps(automaton1.transientLocationAssignments, automaton2.transientLocationAssignments); // Treat all actions of the first automaton. for (auto const& action1 : automaton1.actionIndexToAction) { @@ -1117,7 +1127,7 @@ namespace storm { } else { // If only the first automaton has this action, we only need to apply the identity of the // second automaton. - result.actionIndexToAction[action1.first] = ActionDd(action1.second.guard, action1.second.transitions * automaton2.identity, action1.second.localNondeterminismVariables, action1.second.variableToWritingFragment, action1.second.illegalFragment); + result.actionIndexToAction[action1.first] = ActionDd(action1.second.guard, action1.second.transitions * automaton2.identity, action1.second.transientEdgeAssignments, action1.second.localNondeterminismVariables, action1.second.variableToWritingFragment, action1.second.illegalFragment); } } } @@ -1130,7 +1140,7 @@ namespace storm { if (synchronizingActionIndices.find(action2.first) == synchronizingActionIndices.end()) { // If only the second automaton has this action, we only need to apply the identity of the // first automaton. - result.actionIndexToAction[action2.first] = ActionDd(action2.second.guard, action2.second.transitions * automaton1.identity, action2.second.localNondeterminismVariables, action2.second.variableToWritingFragment, action2.second.illegalFragment); + result.actionIndexToAction[action2.first] = ActionDd(action2.second.guard, action2.second.transitions * automaton1.identity, action2.second.transientEdgeAssignments, action2.second.localNondeterminismVariables, action2.second.variableToWritingFragment, action2.second.illegalFragment); } } } @@ -1166,7 +1176,7 @@ namespace storm { } } - return ActionDd(action1.guard * action2.guard, action1.transitions * action2.transitions, std::make_pair(std::min(action1.getLowestLocalNondeterminismVariable(), action2.getLowestLocalNondeterminismVariable()), std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable())), globalVariableToWritingFragment, illegalFragment); + return ActionDd(combinedGuard.template toAdd(), action1.transitions * action2.transitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(std::min(action1.getLowestLocalNondeterminismVariable(), action2.getLowestLocalNondeterminismVariable()), std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable())), globalVariableToWritingFragment, illegalFragment); } ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add const& identity1, storm::dd::Add const& identity2) { @@ -1183,7 +1193,7 @@ namespace storm { STORM_LOG_TRACE("Combining unsynchronized actions."); if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { - return ActionDd(action1.guard + action2.guard, action1.transitions + action2.transitions, std::make_pair(0, 0), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), this->variables.manager->getBddZero()); + return ActionDd(action1.guard + action2.guard, action1.transitions + action2.transitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(0, 0), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), this->variables.manager->getBddZero()); } else if (this->model.getModelType() == storm::jani::ModelType::MDP) { if (action1.transitions.isZero()) { return action2; @@ -1192,7 +1202,7 @@ namespace storm { } // Bring both choices to the same number of variables that encode the nondeterminism. - assert(action1.getLowestLocalNondeterminismVariable() == action2.getLowestLocalNondeterminismVariable()); + STORM_LOG_ASSERT(action1.getLowestLocalNondeterminismVariable() == action2.getLowestLocalNondeterminismVariable(), "Mismatching lowest nondeterminism variable indices."); uint_fast64_t highestLocalNondeterminismVariable = std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable()); if (action1.getHighestLocalNondeterminismVariable() > action2.getHighestLocalNondeterminismVariable()) { storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); @@ -1201,6 +1211,10 @@ namespace storm { nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); } action2.transitions *= nondeterminismEncoding; + + for (auto& transientAssignment : action2.transientEdgeAssignments) { + transientAssignment.second *= nondeterminismEncoding; + } } else if (action2.getHighestLocalNondeterminismVariable() > action1.getHighestLocalNondeterminismVariable()) { storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); @@ -1208,6 +1222,10 @@ namespace storm { nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); } action1.transitions *= nondeterminismEncoding; + + for (auto& transientAssignment : action1.transientEdgeAssignments) { + transientAssignment.second *= nondeterminismEncoding; + } } // Add a new variable that resolves the nondeterminism between the two choices. @@ -1221,14 +1239,14 @@ namespace storm { entry.second = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 1) && entry.second; } - return ActionDd((action1.guard.toBdd() || action2.guard.toBdd()).template toAdd(), combinedTransitions, std::make_pair(action1.getLowestLocalNondeterminismVariable(), highestLocalNondeterminismVariable + 1), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), action1.illegalFragment || action2.illegalFragment); + return ActionDd((action1.guard.toBdd() || action2.guard.toBdd()).template toAdd(), combinedTransitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(action1.getLowestLocalNondeterminismVariable(), highestLocalNondeterminismVariable + 1), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), action1.illegalFragment || action2.illegalFragment); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); } } AutomatonDd rename(AutomatonDd const& automaton, std::map const& indexToIndex) { - AutomatonDd result(automaton.identity); + AutomatonDd result(automaton.identity, automaton.transientLocationAssignments); for (auto const& action : automaton.actionIndexToAction) { auto renamingIt = indexToIndex.find(action.first); @@ -1258,6 +1276,23 @@ namespace storm { return result; } + void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function const& callback) { + auto transientVariableIt = this->transientVariables.begin(); + auto transientVariableIte = this->transientVariables.end(); + for (auto const& assignment : transientAssignments) { + while (transientVariableIt != transientVariableIte && *transientVariableIt < assignment.getExpressionVariable()) { + ++transientVariableIt; + } + if (transientVariableIt == transientVariableIte) { + break; + } + if (*transientVariableIt == assignment.getExpressionVariable()) { + callback(assignment); + ++transientVariableIt; + } + } + } + EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { STORM_LOG_TRACE("Translating guard " << edge.getGuard()); @@ -1324,27 +1359,12 @@ namespace storm { } // Finally treat the transient assignments. + std::map> transientEdgeAssignments; if (!this->transientVariables.empty()) { - auto transientAssignments = edge.getAssignments().getTransientAssignments(); - - auto transientVariableIt = this->transientVariables.begin(); - auto transientVariableIte = this->transientVariables.end(); - for (auto const& assignment : transientAssignments) { - while (transientVariableIt != transientVariableIte && *transientVariableIt < assignment.getExpressionVariable()) { -// callback(storm::utility::zero()); - ++transientVariableIt; - } - if (transientVariableIt == transientVariableIte) { - break; - } - if (*transientVariableIt == assignment.getExpressionVariable()) { -// callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression()))); - ++transientVariableIt; - } - } + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = guard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } ); } - return EdgeDd(guard, guard * transitions, globalVariablesInSomeDestination); + return EdgeDd(guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); } else { return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); } @@ -1373,16 +1393,52 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type."); } } else { - return ActionDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero(), std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); + return ActionDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero(), {}, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); } } + void addToTransientAssignmentMap(std::map>& transientAssignments, std::map> const& assignmentsToAdd) { + for (auto const& entry : assignmentsToAdd) { + auto it = transientAssignments.find(entry.first); + if (it != transientAssignments.end()) { + it->second += entry.second; + } else { + transientAssignments[entry.first] = entry.second; + } + } + } + + void addToTransientAssignmentMap(std::map>& transientAssignments, storm::expressions::Variable const& variable, storm::dd::Add const& assignmentToAdd) { + auto it = transientAssignments.find(variable); + if (it != transientAssignments.end()) { + it->second += assignmentToAdd; + } else { + transientAssignments[variable] = assignmentToAdd; + } + } + + std::map> joinTransientAssignmentMaps(std::map> const& transientAssignments1, std::map> const& transientAssignments2) { + std::map> result = transientAssignments1; + + for (auto const& entry : transientAssignments2) { + auto resultIt = result.find(entry.first); + if (resultIt != result.end()) { + resultIt->second += entry.second; + } else { + result[entry.first] = entry.second; + } + } + + return result; + } + ActionDd combineEdgesToActionMarkovChain(std::vector const& edgeDds) { storm::dd::Bdd allGuards = this->variables.manager->getBddZero(); storm::dd::Add allTransitions = this->variables.manager->template getAddZero(); storm::dd::Bdd temporary; std::map> globalVariableToWritingFragment; + std::map> transientEdgeAssignments; for (auto const& edgeDd : edgeDds) { // Check for overlapping guards. storm::dd::Bdd guardBdd = edgeDd.guard.toBdd(); @@ -1395,6 +1451,9 @@ namespace storm { allGuards |= guardBdd; allTransitions += edgeDd.transitions; + // Add the transient variable assignments to the resulting one. + addToTransientAssignmentMap(transientEdgeAssignments, edgeDd.transientEdgeAssignments); + // Keep track of the fragment that is writing global variables. for (auto const& variable : edgeDd.writtenGlobalVariables) { auto it = globalVariableToWritingFragment.find(variable); @@ -1406,7 +1465,7 @@ namespace storm { } } - return ActionDd(allGuards.template toAdd(), allTransitions, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); + return ActionDd(allGuards.template toAdd(), allTransitions, transientEdgeAssignments, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } void addToVariableWritingFragmentMap(std::map>& globalVariableToWritingFragment, storm::expressions::Variable const& variable, storm::dd::Bdd const& partToAdd) const { @@ -1436,13 +1495,15 @@ namespace storm { ActionDd combineEdgesBySummation(storm::dd::Add const& guard, std::vector const& edges) { storm::dd::Add transitions = this->variables.manager->template getAddZero(); std::map> globalVariableToWritingFragment; + std::map> transientEdgeAssignments; for (auto const& edge : edges) { transitions += edge.transitions; + addToTransientAssignmentMap(transientEdgeAssignments, edge.transientEdgeAssignments); for (auto const& variable : edge.writtenGlobalVariables) { addToVariableWritingFragmentMap(globalVariableToWritingFragment, variable, edge.guard.toBdd()); } } - return ActionDd(guard, transitions, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); + return ActionDd(guard, transitions, transientEdgeAssignments, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } ActionDd combineEdgesToActionMdp(std::vector const& edges, uint64_t localNondeterminismVariableOffset) { @@ -1465,6 +1526,7 @@ namespace storm { storm::dd::Add allEdges = this->variables.manager->template getAddZero(); std::map> globalVariableToWritingFragment; + std::map> transientAssignments; storm::dd::Bdd equalsNumberOfChoicesDd; std::vector> choiceDds(maxChoices, this->variables.manager->template getAddZero()); @@ -1515,6 +1577,11 @@ namespace storm { // Combine the overlapping part of the guard with command updates and add it to the resulting DD. choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * currentEdge.transitions; + // Keep track of the fragment of transient assignments. + for (auto const& transientAssignment : currentEdge.transientEdgeAssignments) { + addToTransientAssignmentMap(transientAssignments, transientAssignment.first, remainingGuardChoicesIntersection.template toAdd() * transientAssignment.second * indicesEncodedWithLocalNondeterminismVariables[k].first.template toAdd()); + } + // Keep track of the written global variables of the fragment. for (auto const& variable : currentEdge.writtenGlobalVariables) { addToVariableWritingFragmentMap(globalVariableToWritingFragment, variable, remainingGuardChoicesIntersection && indicesEncodedWithLocalNondeterminismVariables[k].first); @@ -1540,7 +1607,7 @@ namespace storm { sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); } - return ActionDd(allGuards.template toAdd(), allEdges, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero()); + return ActionDd(allGuards.template toAdd(), allEdges, transientAssignments, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } } @@ -1558,6 +1625,20 @@ namespace storm { result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable())); result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable())); } + + for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) { + auto const& location = automaton.getLocation(locationIndex); + performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) { + storm::dd::Add assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automatonName).first, locationIndex).template toAdd() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + auto it = result.transientLocationAssignments.find(assignment.getExpressionVariable()); + if (it != result.transientLocationAssignments.end()) { + it->second += assignedValues; + } else { + result.transientLocationAssignments[assignment.getExpressionVariable()] = assignedValues; + } + }); + } + return result; } @@ -1588,28 +1669,36 @@ namespace storm { uint64_t numberOfUsedNondeterminismVariables = automaton.getHighestLocalNondeterminismVariable(); // Add missing global variable identities, action and nondeterminism encodings. + std::map> transientEdgeAssignments; for (auto& action : automaton.actionIndexToAction) { illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); storm::dd::Add actionEncoding = encodeAction(action.first != this->model.getSilentActionIndex() ? boost::optional(action.first) : boost::none, this->variables); storm::dd::Add missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables); storm::dd::Add extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions; + + for (auto const& transientAssignment : action.second.transientEdgeAssignments) { + addToTransientAssignmentMap(transientEdgeAssignments, transientAssignment.first, actionEncoding * missingNondeterminismEncoding * transientAssignment.second); + } + result += extendedTransitions; } - return ComposerResult(result, illegalFragment, numberOfUsedNondeterminismVariables); + return ComposerResult(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, numberOfUsedNondeterminismVariables); } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { // Simply add all actions, but make sure to include the missing global variable identities. storm::dd::Add result = this->variables.manager->template getAddZero(); storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); + std::map> transientEdgeAssignments; for (auto& action : automaton.actionIndexToAction) { illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); + addToTransientAssignmentMap(transientEdgeAssignments, action.second.transientEdgeAssignments); result += action.second.transitions; } - return ComposerResult(result, illegalFragment, 0); + return ComposerResult(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, 0); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); } @@ -1782,6 +1871,31 @@ namespace storm { return result; } + template + std::unordered_map> buildRewardModels(ComposerResult const& system, std::vector const& rewardVariables) { + std::unordered_map> result; + + for (auto const& variable : rewardVariables) { + boost::optional> stateRewards = boost::none; + boost::optional> stateActionRewards = boost::none; + boost::optional> transitionRewards = boost::none; + + auto it = system.transientLocationAssignments.find(variable); + if (it != system.transientLocationAssignments.end()) { + stateRewards = it->second; + } + + it = system.transientEdgeAssignments.find(variable); + if (it != system.transientEdgeAssignments.end()) { + stateActionRewards = it->second; + } + + result.emplace(variable.getName(), storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards)); + } + + return result; + } + template std::shared_ptr> DdJaniModelBuilder::build(storm::jani::Model const& model, Options const& options) { if (model.hasUndefinedConstants()) { @@ -1840,6 +1954,9 @@ namespace storm { // Cut the deadlock states by removing all states that we 'converted' to deadlock states by making them terminal. modelComponents.deadlockStates = modelComponents.deadlockStates && !terminalStates; + // Build the reward models. + modelComponents.rewardModels = buildRewardModels(system, rewardVariables); + // Finally, create the model. return createModel(model.getModelType(), variables, modelComponents); } diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 859a2424e..b45269dc4 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1219,6 +1219,8 @@ namespace storm { } } + stateActionRewards.get().exportToDot("prismrew.dot"); + return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); } diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 78cbcc042..755674cd1 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -213,6 +213,9 @@ namespace storm { storm::storage::SymbolicModelDescription model; if (ioSettings.isPrismInputSet()) { model = storm::parseProgram(ioSettings.getPrismInputFilename()); + if (ioSettings.isPrismToJaniSet()) { + model = model.toJani(true); + } } else if (ioSettings.isJaniInputSet()) { model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first; } diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 23a3a7068..5b5f54151 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -550,12 +550,15 @@ namespace storm { } if (rewardVariableIt == rewardVariableIte) { break; - } - if (*rewardVariableIt == assignment.getExpressionVariable()) { + } else if (*rewardVariableIt == assignment.getExpressionVariable()) { callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression()))); ++rewardVariableIt; } } + // Add a value of zero for all variables that have no assignment. + for (; rewardVariableIt != rewardVariableIte; ++rewardVariableIt) { + callback(storm::utility::zero()); + } } template diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index b5adb7e15..6266fbb73 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -172,7 +172,7 @@ namespace storm { // for solving the equation system (i.e. compute (I-A)). submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; - + // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index ef6877089..c174f1f51 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::prismInputOptionName = "prism"; const std::string IOSettings::janiInputOptionName = "jani"; + const std::string IOSettings::prismToJaniOptionName = "prism2jani"; const std::string IOSettings::explorationOrderOptionName = "explorder"; const std::string IOSettings::explorationOrderOptionShortName = "eo"; const std::string IOSettings::transitionRewardsOptionName = "transrew"; @@ -42,6 +43,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); std::vector explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) @@ -85,6 +87,10 @@ namespace storm { return isJaniInputSet() || isPrismInputSet(); } + bool IOSettings::isPrismToJaniSet() const { + return this->getOption(prismToJaniOptionName).getHasOptionBeenSet(); + } + std::string IOSettings::getPrismInputFilename() const { return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString(); } @@ -160,6 +166,10 @@ namespace storm { // Ensure that the model was given either symbolically or explicitly. STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); + + // Make sure PRISM-to-JANI conversion is only set if the actual input is in PRISM format. + STORM_LOG_THROW(!isPrismToJaniSet() || isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the transformation from PRISM to JANI, the input model must be given in the prism format."); + return true; } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index 8585ea573..ae6ce6831 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -79,6 +79,13 @@ namespace storm { */ bool isPrismOrJaniInputSet() const; + /*! + * Retrieves whether the option to convert PRISM to JANI input was set. + * + * @return True if the option was set. + */ + bool isPrismToJaniSet() const; + /*! * Retrieves the name of the file that contains the PRISM model specification if the model was given * using the PRISM input option. @@ -198,6 +205,7 @@ namespace storm { static const std::string explicitOptionShortName; static const std::string prismInputOptionName; static const std::string janiInputOptionName; + static const std::string prismToJaniOptionName; static const std::string explorationOrderOptionName; static const std::string explorationOrderOptionShortName; static const std::string transitionRewardsOptionName; diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index 3bccf3b73..1058e464f 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -19,10 +19,12 @@ namespace storm { SymbolicModelDescription& SymbolicModelDescription::operator=(storm::jani::Model const& model) { this->modelDescription = model; + return *this; } SymbolicModelDescription& SymbolicModelDescription::operator=(storm::prism::Program const& program) { this->modelDescription = program; + return *this; } bool SymbolicModelDescription::hasModel() const { diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 9e288695f..9c618a838 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -108,7 +108,11 @@ namespace storm { std::vector const& Automaton::getLocations() const { return locations; } - + + std::vector& Automaton::getLocations() { + return locations; + } + Location const& Automaton::getLocation(uint64_t index) const { return locations[index]; } @@ -371,6 +375,10 @@ namespace storm { variable.substitute(substitution); } + for (auto& location : this->getLocations()) { + location.substitute(substitution); + } + this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution)); for (auto& edge : this->getEdges()) { diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 9ef3c57f2..c6219aa1e 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -157,7 +157,12 @@ namespace storm { * Retrieves the locations of the automaton. */ std::vector const& getLocations() const; - + + /*! + * Retrieves the locations of the automaton. + */ + std::vector& getLocations(); + /*! * Retrieves the location with the given index. */ diff --git a/src/storage/jani/Location.cpp b/src/storage/jani/Location.cpp index 4f09e4959..05a22d4e5 100644 --- a/src/storage/jani/Location.cpp +++ b/src/storage/jani/Location.cpp @@ -24,6 +24,12 @@ namespace storm { assignments.add(assignment); } + void Location::substitute(std::map const& substitution) { + for (auto& assignment : assignments) { + assignment.substitute(substitution); + } + } + void Location::checkValid() const { // Intentionally left empty. } diff --git a/src/storage/jani/Location.h b/src/storage/jani/Location.h index 9de4b683f..a2328cb22 100644 --- a/src/storage/jani/Location.h +++ b/src/storage/jani/Location.h @@ -33,6 +33,11 @@ namespace storm { * Adds the given transient assignment to this location. */ void addTransientAssignment(storm::jani::Assignment const& assignment); + + /*! + * Substitutes all variables in all expressions according to the given substitution. + */ + void substitute(std::map const& substitution); /*! * Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments. diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 9a9a95d8f..fc170ac58 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -200,6 +200,12 @@ namespace storm { return automata[it->second]; } + uint64_t Model::getAutomatonIndex(std::string const& name) const { + auto it = automatonToIndex.find(name); + STORM_LOG_THROW(it != automatonToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve unknown automaton '" << name << "'."); + return it->second; + } + std::size_t Model::getNumberOfAutomata() const { return automata.size(); } diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 375c4d792..2fc06b18f 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -196,6 +196,11 @@ namespace storm { * Retrieves the automaton with the given name. */ Automaton const& getAutomaton(std::string const& name) const; + + /*! + * Retrieves the index of the given automaton. + */ + uint64_t getAutomatonIndex(std::string const& name) const; /*! * Retrieves the number of automata in this model.