From db31c1cb11669113dd4de78b0aff3eb32ab4bcc2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 22 May 2017 22:06:22 +0200 Subject: [PATCH] improved .dot export of models with choice labeling --- src/storm/models/sparse/ChoiceLabeling.cpp | 1 + .../models/sparse/DeterministicModel.cpp | 2 - src/storm/models/sparse/Dtmc.cpp | 1 - src/storm/models/sparse/MarkovAutomaton.cpp | 83 ------------------- src/storm/models/sparse/MarkovAutomaton.h | 2 - src/storm/models/sparse/Mdp.cpp | 1 - src/storm/models/sparse/Model.cpp | 6 +- .../models/sparse/NondeterministicModel.cpp | 53 ++++++++++-- src/storm/models/sparse/StateLabeling.cpp | 1 + src/storm/utility/graph.cpp | 56 ------------- 10 files changed, 53 insertions(+), 153 deletions(-) diff --git a/src/storm/models/sparse/ChoiceLabeling.cpp b/src/storm/models/sparse/ChoiceLabeling.cpp index fe1117027..5e3c90904 100644 --- a/src/storm/models/sparse/ChoiceLabeling.cpp +++ b/src/storm/models/sparse/ChoiceLabeling.cpp @@ -76,6 +76,7 @@ namespace storm { std::ostream& operator<<(std::ostream& out, ChoiceLabeling const& labeling) { + out << "Choice "; labeling.printLabelingInformationToStream(out); return out; } diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 430c31c6f..dc3cdacc4 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -56,8 +56,6 @@ namespace storm { } template class DeterministicModel; - template class DeterministicModel; - #ifdef STORM_HAVE_CARL template class DeterministicModel; diff --git a/src/storm/models/sparse/Dtmc.cpp b/src/storm/models/sparse/Dtmc.cpp index c0ec2b933..222354b65 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -28,7 +28,6 @@ namespace storm { template class Dtmc; - template class Dtmc; #ifdef STORM_HAVE_CARL template class Dtmc; diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 9849d4f4a..32fea3edc 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -155,88 +155,6 @@ namespace storm { } } - template - void MarkovAutomaton::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { - Model::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); - - // Write the probability distributions for all the states. - for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { - uint_fast64_t rowCount = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state]; - bool highlightChoice = true; - - // For this, we need to iterate over all available nondeterministic choices in the current state. - for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { - uint_fast64_t rowIndex = this->getTransitionMatrix().getRowGroupIndices()[state] + choice; - typename storm::storage::SparseMatrix::const_rows row = this->getTransitionMatrix().getRow(rowIndex); - - if (scheduler != nullptr) { - // If the scheduler picked the current choice, we will not make it dotted, but highlight it. - if ((*scheduler)[state] == choice) { - highlightChoice = true; - } else { - highlightChoice = false; - } - } - - // 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) || choice != 0) { - // For each nondeterministic choice, we draw an arrow to an intermediate node to better display - // the grouping of transitions. - outStream << "\t\"" << state << "c" << choice << "\" [shape = \"point\""; - - // If we were given a scheduler to highlight, we do so now. - if (scheduler != nullptr) { - if (highlightChoice) { - outStream << ", fillcolor=\"red\""; - } - } - outStream << "];" << std::endl; - - outStream << "\t" << state << " -> \"" << state << "c" << choice << "\" [ label= \"" << rowIndex << "\""; - - // If we were given a scheduler to highlight, we do so now. - if (scheduler != nullptr) { - if (highlightChoice) { - outStream << ", color=\"red\", penwidth = 2"; - } else { - outStream << ", style = \"dotted\""; - } - } - outStream << "];" << std::endl; - - // Now draw all probabilitic arcs that belong to this nondeterminstic choice. - for (auto const& transition : row) { - if (subsystem == nullptr || subsystem->get(transition.getColumn())) { - outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << "\" ]"; - - // If we were given a scheduler to highlight, we do so now. - if (scheduler != nullptr) { - if (highlightChoice) { - outStream << " [color=\"red\", penwidth = 2]"; - } else { - outStream << " [style = \"dotted\"]"; - } - } - outStream << ";" << std::endl; - } - } - } else { - // In this case we are emitting a Markovian choice, so draw the arrows directly to the target states. - for (auto const& transition : row) { - if (subsystem == nullptr || subsystem->get(transition.getColumn())) { - outStream << "\t\"" << state << "\" -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << " (" << this->exitRates[state] << ")\" ]"; - } - } - } - } - } - - if (finalizeOutput) { - outStream << "}" << std::endl; - } - } - template void MarkovAutomaton::turnRatesToProbabilities() { this->exitRates.resize(this->getNumberOfStates()); @@ -348,7 +266,6 @@ namespace storm { template class MarkovAutomaton; -// template class MarkovAutomaton; #ifdef STORM_HAVE_CARL template class MarkovAutomaton; diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index 88c03a863..4ab1edaeb 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -191,8 +191,6 @@ namespace storm { */ std::shared_ptr> convertToCTMC() const; - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; - virtual void printModelInformationToStream(std::ostream& out) const override; private: diff --git a/src/storm/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index e9fdba8f3..5cfd36fa1 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -50,7 +50,6 @@ namespace storm { } template class Mdp; - template class Mdp; #ifdef STORM_HAVE_CARL template class Mdp; diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 90bafbd51..de16edab1 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -207,7 +207,11 @@ namespace storm { void Model::printModelInformationFooterToStream(std::ostream& out) const { this->printRewardModelsInformationToStream(out); this->getStateLabeling().printLabelingInformationToStream(out); - out << "choice labels: \t" << (this->hasChoiceLabeling() ? "yes" : "no") << std::noboolalpha << std::endl; + if (this->hasChoiceLabeling()) { + this->getChoiceLabeling().printLabelingInformationToStream(out); + } else { + out << "Choice Labels: \tnone"; + } out << "-------------------------------------------------------------- " << std::endl; } diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 1a49c8da0..37e72c84a 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -1,6 +1,7 @@ #include "storm/models/sparse/NondeterministicModel.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/MarkovAutomaton.h" #include "storm/adapters/CarlAdapter.h" @@ -86,8 +87,9 @@ namespace storm { // For each nondeterministic choice, we draw an arrow to an intermediate node to better display // the grouping of transitions. - outStream << "\t\"" << state << "c" << choice << "\" [shape = \"point\""; + // The intermediate node: + outStream << "\t\"" << state << "c" << choice << "\" [shape = \"point\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { if (highlightChoice) { @@ -96,17 +98,55 @@ namespace storm { } outStream << "];" << std::endl; - outStream << "\t" << state << " -> \"" << state << "c" << choice << "\" [ label= \"" << rowIndex << "\""; - + // The arrow to the intermediate node: + outStream << "\t" << state << " -> \"" << state << "c" << choice << "\""; + bool arrowHasLabel = false; + if (this->isOfType(ModelType::MarkovAutomaton)) { + // If this is a Markov automaton, we have to check whether the current choice is a Markovian choice and correspondingly print the exit rate + MarkovAutomaton const* ma = dynamic_cast const*>(this); + if (ma->isMarkovianState(state) && choice == 0) { + arrowHasLabel = true; + outStream << " [ label = \"" << ma->getExitRate(state); + } + } + if (this->hasChoiceLabeling()) { + if (arrowHasLabel) { + outStream << " | {"; + } else { + outStream << " [ label = \"{"; + } + arrowHasLabel = true; + bool firstLabel = true; + for (auto const& label : this->getChoiceLabeling().getLabelsOfChoice(rowIndex)) { + if (!firstLabel) { + outStream << ", "; + } + firstLabel = false; + outStream << label; + } + outStream << "}"; + } + if (arrowHasLabel) { + outStream << "\""; + } // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { + if (arrowHasLabel) { + outStream << ", "; + } else { + outStream << "[ "; + } if (highlightChoice) { - outStream << ", color=\"red\", penwidth = 2"; + outStream << "color=\"red\", penwidth = 2"; } else { - outStream << ", style = \"dotted\""; + outStream << "style = \"dotted\""; } } - outStream << "];" << std::endl; + + if (arrowHasLabel || scheduler != nullptr) { + outStream << "]" << std::endl; + } + outStream << ";" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. for (auto const& transition : row) { @@ -133,7 +173,6 @@ namespace storm { } template class NondeterministicModel; - template class NondeterministicModel; #ifdef STORM_HAVE_CARL template class NondeterministicModel; diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index 43ade7bac..a0efebdc2 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -74,6 +74,7 @@ namespace storm { std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling) { + out << "State "; labeling.printLabelingInformationToStream(out); return out; } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 89702c6a4..98dcd0c71 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1226,62 +1226,6 @@ namespace storm { template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - - - template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); - - template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); - - template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); - - - template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - - template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - - - template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - - template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - - template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - - - template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; - - template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - - template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - - template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - - - template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - - template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); - - // Instantiations for storm::RationalNumber. #ifdef STORM_HAVE_CARL template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);