diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index c0a6ae09f..f81e21ab9 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -147,6 +147,9 @@ namespace storm { // The meta variables used to encode the remaining nondeterminism. std::vector localNondeterminismVariables; + // The meta variable used to distinguish Markovian from probabilistic choices in Markov automata. + storm::expressions::Variable markovNondeterminismVariable; + // The meta variables used to encode the actions and nondeterminism. std::set allNondeterminismVariables; @@ -238,6 +241,11 @@ namespace storm { result.allNondeterminismVariables.insert(variablePair.first); } + if (this->model.getModelType() == storm::jani::ModelType::MA) { + result.markovNondeterminismVariable = result.manager->addMetaVariable("markov").first; + result.allNondeterminismVariables.insert(result.markovNondeterminismVariable); + } + for (auto const& automaton : this->model.getAutomata()) { // 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); @@ -924,10 +932,13 @@ 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& transientEdgeAssignments = {}, std::set const& writtenGlobalVariables = {}) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), writtenGlobalVariables(writtenGlobalVariables) { + EdgeDd(bool isMarkovian, storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::map> const& transientEdgeAssignments = {}, std::set const& writtenGlobalVariables = {}) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), writtenGlobalVariables(writtenGlobalVariables) { // Intentionally left empty. } + // A flag storing whether this edge is a Markovian one (i.e. one with a rate). + bool isMarkovian; + // A DD that represents all states that have this edge enabled. storm::dd::Add guard; @@ -1137,28 +1148,41 @@ namespace storm { for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) { auto const& synchVector = synchronizationVectors[synchVectorIndex]; - // Determine the indices of input (at the current automaton position) and the output. - uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex)); - actionsInSynch.insert(inputActionIndex); - - // Either set the action (if it's the first of the ones to compose) or compose the actions directly. - if (automatonIndex == 0) { - // If the action cannot be found, the particular spot in the output will be left empty. - auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); - if (inputActionIt != subautomaton.actionIndexToAction.end()) { - synchronizationVectorActions[synchVectorIndex] = inputActionIt->second; + if (synchVector.isNoActionInput(synchVector.getInput(automatonIndex))) { + if (automatonIndex == 0) { + // Create a new action that is the identity over the first automaton. + synchronizationVectorActions[synchVectorIndex] = ActionDd(this->variables.manager->template getAddOne(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero()); + } else { + // If there is no action in the output spot, this means that some other subcomposition did + // not provide the action necessary for the synchronization vector to resolve. + if (synchronizationVectorActions[synchVectorIndex]) { + synchronizationVectorActions[synchVectorIndex].transitions *= subautomaton.identity; + } } } else { - // If there is no action in the output spot, this means that some other subcomposition did - // not provide the action necessary for the synchronization vector to resolve. - if (synchronizationVectorActions[synchVectorIndex]) { + // Determine the indices of input (at the current automaton position) and the output. + uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex)); + actionsInSynch.insert(inputActionIndex); + + // Either set the action (if it's the first of the ones to compose) or compose the actions directly. + if (automatonIndex == 0) { + // If the action cannot be found, the particular spot in the output will be left empty. auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); if (inputActionIt != subautomaton.actionIndexToAction.end()) { - synchronizationVectorActions[synchVectorIndex] = combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get(), inputActionIt->second); - } else { - // If the current subcomposition does not provide the required action for the synchronization - // vector, we clear the action. - synchronizationVectorActions[synchVectorIndex] = boost::none; + synchronizationVectorActions[synchVectorIndex] = inputActionIt->second; + } + } else { + // If there is no action in the output spot, this means that some other subcomposition did + // not provide the action necessary for the synchronization vector to resolve. + if (synchronizationVectorActions[synchVectorIndex]) { + auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); + if (inputActionIt != subautomaton.actionIndexToAction.end()) { + synchronizationVectorActions[synchVectorIndex] = combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get(), inputActionIt->second); + } else { + // If the current subcomposition does not provide the required action for the synchronization + // vector, we clear the action. + synchronizationVectorActions[synchVectorIndex] = boost::none; + } } } } @@ -1436,8 +1460,17 @@ namespace storm { } // If the edge has a rate, we multiply it to the DD. + bool isMarkovian = false; if (edge.hasRate()) { - transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); + transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); + isMarkovian = true; + if (this->model.getModelType() == storm::jani::ModelType::MA) { + transitions *= this->variables.manager->getEncoding(this->variables.markovNondeterminismVariable, 1); + } + } else { + if (this->model.getModelType() == storm::jani::ModelType::MA) { + transitions *= this->variables.manager->getEncoding(this->variables.markovNondeterminismVariable, 0); + } } // Finally treat the transient assignments. @@ -1446,33 +1479,67 @@ namespace storm { 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, transientEdgeAssignments, globalVariablesInSomeDestination); + return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); } else { - return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); + return EdgeDd(false, this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); + } + } + + EdgeDd combineMarkovianEdges(std::vector const& edgeDds) { + storm::dd::Bdd guard = this->variables.manager->getBddZero(); + storm::dd::Add transitions = this->variables.manager->template getAddZero(); + std::map> transientEdgeAssignments; + std::set writtenVariables; + + for (auto const& edge : edgeDds) { + STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::InvalidArgumentException, "Can only combine Markovian edges."); + + guard |= edge.guard.toBdd(); + transitions += edge.transitions; + for (auto const& variable : edge.writtenGlobalVariables) { + writtenVariables.insert(variable); + } + + // FIXME: This is not correct, need to consider guards. However, the semantics is not currently clear. + joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments); } + + return ActionDd(true, guard.template toAdd(), transitions, transientEdgeAssignments, writtenVariables); } ActionDd buildActionDdForActionIndex(storm::jani::Automaton const& automaton, uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) { // Translate the individual edges. - std::vector edgeDds; + std::vector markovianEdges; + std::vector nonMarkovianEdges; + uint64_t numberOfEdges = 0; for (auto const& edge : automaton.getEdges()) { + ++numberOfEdges; if (edge.getActionIndex() == actionIndex) { - edgeDds.push_back(buildEdgeDd(automaton, edge)); + EdgeDd result = buildEdgeDd(automaton, edge); + if (result.isMarkovian) { + markovianEdges.push_back(result); + } else { + nonMarkovianEdges.push_back(result); + } } } // Now combine the edges to a single action. - if (!edgeDds.empty()) { - switch (this->model.getModelType()){ - case storm::jani::ModelType::DTMC: - case storm::jani::ModelType::CTMC: - return combineEdgesToActionMarkovChain(edgeDds); - break; - case storm::jani::ModelType::MDP: - return combineEdgesToActionMdp(edgeDds, localNondeterminismVariableOffset); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type."); + if (numberOfEdges > 0) { + storm::jani::ModelType modelType = this->model.getModelType(); + if (modelType == storm::jani::ModelType::DTMC) { + STORM_LOG_THROW(markovianEdges.empty(), storm::exceptions::WrongFormatException, "Illegal Markovian edges in DTMC."); + return combineEdgesToActionDeterministic(nonMarkovianEdges); + } else if (modelType == storm::jani::ModelType::CTMC) { + STORM_LOG_THROW(markovianEdges.empty(), storm::exceptions::WrongFormatException, "Illegal non-Markovian edges in CTMC."); + return combineEdgesToActionDeterministic(markovianEdges); + } else if (modelType == storm::jani::ModelType::MDP) { + STORM_LOG_THROW(markovianEdges.empty(), storm::exceptions::WrongFormatException, "Illegal Markovian edges in MDP."); + return combineEdgesToActionNondeterministic(nonMarkovianEdges, boost::none, localNondeterminismVariableOffset); + } else if (modelType == storm::jani::ModelType::MA) { + return combineEdgesToActionNondeterministic(nonMarkovianEdges, markovianEdges, localNondeterminismVariableOffset); + } else { + 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()); @@ -1514,7 +1581,7 @@ namespace storm { return result; } - ActionDd combineEdgesToActionMarkovChain(std::vector const& edgeDds) { + ActionDd combineEdgesToActionDeterministic(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; @@ -1594,19 +1661,26 @@ namespace storm { return ActionDd(guard, transitions, transientEdgeAssignments, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } - ActionDd combineEdgesToActionMdp(std::vector const& edges, uint64_t localNondeterminismVariableOffset) { + ActionDd combineEdgesToActionNondeterministic(std::vector const& nonMarkovianEdges, boost::optional> const& markovianEdges, uint64_t localNondeterminismVariableOffset) { // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. storm::dd::Bdd allGuards = this->variables.manager->getBddZero(); storm::dd::Add sumOfGuards = this->variables.manager->template getAddZero(); + bool hasMarkovianEdge = false; for (auto const& edge : edges) { + if (edge.isMarkovian) { + hasMarkovianEdge = true; + continue; + } + sumOfGuards += edge.guard; allGuards |= edge.guard.toBdd(); } uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); - STORM_LOG_TRACE("Found " << maxChoices << " local choices."); + STORM_LOG_TRACE("Found " << maxChoices << " local (non-Markovian) choices."); // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. if (maxChoices <= 1) { + return combineEdgesBySummation(allGuards.template toAdd(), edges); } else { // Calculate number of required variables to encode the nondeterminism. diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index b329cd42f..1e83b2812 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -53,6 +53,16 @@ namespace storm { } VariableInformation::VariableInformation(storm::jani::Model const& model) : totalBitOffset(0) { + // Check that the model does not contain unbounded integer or non-real transient variables. + STORM_LOG_THROW(!model.getGlobalVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global unbounded integer variables."); + for (auto const& automaton : model.getAutomata()) { + STORM_LOG_THROW(!automaton.getVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains unbounded integer variables in automaton '" << automaton.getName() << "'."); + } + STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global non-transient real variables."); + for (auto const& automaton : model.getAutomata()) { + STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'."); + } + for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); ++totalBitOffset; diff --git a/src/storage/jani/CompositionActionInformationVisitor.cpp b/src/storage/jani/CompositionActionInformationVisitor.cpp index 683995d07..292ab2c17 100644 --- a/src/storage/jani/CompositionActionInformationVisitor.cpp +++ b/src/storage/jani/CompositionActionInformationVisitor.cpp @@ -102,13 +102,18 @@ namespace storm { std::set localEffectiveSynchVectors; for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); - uint64_t synchVectorActionIndex = nameToIndexMap.at(synchVector.getInput(subresultIndex)); - actionsInSynch.insert(synchVectorActionIndex); - // If the action of they synchronization vector at this position is one that is actually contained - // in the corresponding subcomposition, the synchronization vector is effective. - if (subresults[subresultIndex].find(synchVectorActionIndex) != subresults[subresultIndex].end()) { + if (synchVector.isNoActionInput(synchVector.getInput(subresultIndex))) { effectiveSynchronizationVectors.insert(synchVectorIndex); + } else { + uint64_t synchVectorActionIndex = nameToIndexMap.at(synchVector.getInput(subresultIndex)); + actionsInSynch.insert(synchVectorActionIndex); + + // If the action of they synchronization vector at this position is one that is actually contained + // in the corresponding subcomposition, the synchronization vector is effective. + if (subresults[subresultIndex].find(synchVectorActionIndex) != subresults[subresultIndex].end()) { + effectiveSynchronizationVectors.insert(synchVectorIndex); + } } } diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index fac8e2ad7..366c0372c 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -10,6 +10,8 @@ namespace storm { namespace jani { + const std::string SynchronizationVector::noAction = "-"; + SynchronizationVector::SynchronizationVector(std::vector const& input, std::string const& output) : input(input), output(output) { // Intentionally left empty. } @@ -26,10 +28,18 @@ namespace storm { return input[index]; } + std::string const& SynchronizationVector::getNoActionInput() const { + return SynchronizationVector::noAction; + } + std::string const& SynchronizationVector::getOutput() const { return output; } + bool SynchronizationVector::isNoActionInput(std::string const& action) const { + return action == noAction; + } + std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector) { bool first = true; stream << "("; diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h index 3138261a8..30a15ef51 100644 --- a/src/storage/jani/ParallelComposition.h +++ b/src/storage/jani/ParallelComposition.h @@ -16,10 +16,17 @@ namespace storm { std::size_t size() const; std::vector const& getInput() const; + std::string const& getNoActionInput() const; std::string const& getInput(uint64_t index) const; std::string const& getOutput() const; + bool isNoActionInput(std::string const& action) const; + private: + // A marker that can be used as one of the inputs. The semantics is that no action of the corresponding + // automaton takes part in the synchronization. + static const std::string noAction; + /// The input to the synchronization. std::vector input; @@ -94,4 +101,4 @@ namespace storm { }; } -} \ No newline at end of file +} diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 08819964a..0a5594427 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -209,7 +209,7 @@ namespace storm { } if (rateExpression) { - destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, manager->integer(1) / rateExpression.get(), assignments)); + destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, update.getLikelihoodExpression() / rateExpression.get(), assignments)); } else { destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, update.getLikelihoodExpression(), assignments)); } @@ -266,4 +266,4 @@ namespace storm { } } -} \ No newline at end of file +}