diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index caa946c35..99f80b29f 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -23,12 +23,11 @@ namespace storm { public: MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector&& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, - storm::storage::BitVector const& markovianChoices, std::vector const& exitRates, + std::vector&& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, boost::optional>> const& optionalChoiceLabeling) : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling), - markovianStates(markovianStates), markovianChoices(markovianChoices), exitRates(exitRates) { + markovianStates(markovianStates), exitRates(exitRates) { if (this->hasTransitionRewards()) { if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); @@ -40,13 +39,12 @@ namespace storm { MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, std::vector&& nondeterministicChoiceIndices, - storm::storage::BitVector const& markovianStates, - storm::storage::BitVector const& markovianChoices, std::vector const& exitRates, + storm::storage::BitVector const& markovianStates, std::vector const& exitRates, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, boost::optional>>&& optionalChoiceLabeling) : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), - std::move(optionalChoiceLabeling)), markovianStates(markovianStates), markovianChoices(std::move(markovianChoices)), exitRates(std::move(exitRates)) { + std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)) { if (this->hasTransitionRewards()) { if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); @@ -55,11 +53,11 @@ namespace storm { } } - MarkovAutomaton(MarkovAutomaton const& markovAutomaton) : AbstractNondeterministicModel(markovAutomaton), exitRates(markovAutomaton.exitRates), markovianStates(markovAutomaton.markovianStates), markovianChoices(markovAutomaton.markovianChoices) { + MarkovAutomaton(MarkovAutomaton const& markovAutomaton) : AbstractNondeterministicModel(markovAutomaton), exitRates(markovAutomaton.exitRates), markovianStates(markovAutomaton.markovianStates) { // Intentionally left empty. } - MarkovAutomaton(MarkovAutomaton&& markovAutomaton) : AbstractNondeterministicModel(std::move(markovAutomaton)), markovianStates(std::move(markovAutomaton.markovianStates)), markovianChoices(std::move(markovAutomaton.markovianChoices)), exitRates(std::move(markovAutomaton.exitRates)) { + MarkovAutomaton(MarkovAutomaton&& markovAutomaton) : AbstractNondeterministicModel(std::move(markovAutomaton)), markovianStates(std::move(markovAutomaton.markovianStates)), exitRates(std::move(markovAutomaton.exitRates)) { // Intentionally left empty. } @@ -91,7 +89,9 @@ namespace storm { } } - if (!markovianChoices.get(this->getNondeterministicChoiceIndices()[state] + row)) { + // If it's not a Markovian state or the current row is the first choice for this state, then we + // are dealing with a probabilitic choice. + if (!markovianStates.get(state) || row != 0) { // For each nondeterministic choice, we draw an arrow to an intermediate node to better display // the grouping of transitions. outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\""; diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index e367c2987..28b91b6d9 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -19,7 +19,7 @@ namespace storm { throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata."; } - storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.markovianChoices), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); + storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); return resultingAutomaton; } diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index f5805ed2c..912524ee5 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -194,8 +194,7 @@ namespace storm { if (strcmp(actionNameBuffer, "!") == 0) { isMarkovianChoice = true; - // Mark the current choice and state as a Markovian one. - result.markovianChoices.set(currentChoice, true); + // Mark the current state as a Markovian one. result.markovianStates.set(source, true); } else { isMarkovianChoice = false;