sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

improved .dot export of models with choice labeling

main
TimQu 8 years ago
parent
6537fd8b72
commit
db31c1cb11
10 changed files with 53 additions and 153 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/storm/models/sparse/ChoiceLabeling.cpp
  2. 2
      src/storm/models/sparse/DeterministicModel.cpp
  3. 1
      src/storm/models/sparse/Dtmc.cpp
  4. 83
      src/storm/models/sparse/MarkovAutomaton.cpp
  5. 2
      src/storm/models/sparse/MarkovAutomaton.h
  6. 1
      src/storm/models/sparse/Mdp.cpp
  7. 6
      src/storm/models/sparse/Model.cpp
  8. 53
      src/storm/models/sparse/NondeterministicModel.cpp
  9. 1
      src/storm/models/sparse/StateLabeling.cpp
  10. 56
      src/storm/utility/graph.cpp

1
src/storm/models/sparse/ChoiceLabeling.cpp
View File

@ -76,6 +76,7 @@ namespace storm {
std::ostream& operator<<(std::ostream& out, ChoiceLabeling const& labeling) {
out << "Choice ";
labeling.printLabelingInformationToStream(out);
return out;
}

2
src/storm/models/sparse/DeterministicModel.cpp
View File

@ -56,8 +56,6 @@ namespace storm {
}
template class DeterministicModel<double>;
template class DeterministicModel<float>;
#ifdef STORM_HAVE_CARL
template class DeterministicModel<storm::RationalNumber>;

1
src/storm/models/sparse/Dtmc.cpp
View File

@ -28,7 +28,6 @@ namespace storm {
template class Dtmc<double>;
template class Dtmc<float>;
#ifdef STORM_HAVE_CARL
template class Dtmc<storm::RationalNumber>;

83
src/storm/models/sparse/MarkovAutomaton.cpp
View File

@ -155,88 +155,6 @@ namespace storm {
}
}
template <typename ValueType, typename RewardModelType>
void MarkovAutomaton<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const {
Model<ValueType, RewardModelType>::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<ValueType>::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 <typename ValueType, typename RewardModelType>
void MarkovAutomaton<ValueType, RewardModelType>::turnRatesToProbabilities() {
this->exitRates.resize(this->getNumberOfStates());
@ -348,7 +266,6 @@ namespace storm {
template class MarkovAutomaton<double>;
// template class MarkovAutomaton<float>;
#ifdef STORM_HAVE_CARL
template class MarkovAutomaton<storm::RationalNumber>;

2
src/storm/models/sparse/MarkovAutomaton.h
View File

@ -191,8 +191,6 @@ namespace storm {
*/
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCTMC() const;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override;
virtual void printModelInformationToStream(std::ostream& out) const override;
private:

1
src/storm/models/sparse/Mdp.cpp
View File

@ -50,7 +50,6 @@ namespace storm {
}
template class Mdp<double>;
template class Mdp<float>;
#ifdef STORM_HAVE_CARL
template class Mdp<storm::RationalNumber>;

6
src/storm/models/sparse/Model.cpp
View File

@ -207,7 +207,11 @@ namespace storm {
void Model<ValueType, RewardModelType>::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;
}

53
src/storm/models/sparse/NondeterministicModel.cpp
View File

@ -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<ValueType, RewardModelType> const* ma = dynamic_cast<MarkovAutomaton<ValueType, RewardModelType> 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<double>;
template class NondeterministicModel<float>;
#ifdef STORM_HAVE_CARL
template class NondeterministicModel<storm::RationalNumber>;

1
src/storm/models/sparse/StateLabeling.cpp
View File

@ -74,6 +74,7 @@ namespace storm {
std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling) {
out << "State ";
labeling.printLabelingInformationToStream(out);
return out;
}

56
src/storm/utility/graph.cpp
View File

@ -1226,62 +1226,6 @@ namespace storm {
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<float> 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<float> const& transitionMatrix);
template std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<float> 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<float> 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<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<float> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<float> 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<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> 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<float> const& model, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<float> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<float> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<float> const& matrix);
// Instantiations for storm::RationalNumber.
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);

Write Preview
Loading…
Cancel
Save