From 909c035c5218fa4f09a3096503182ff74fb58991 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 15 Nov 2018 11:09:53 +0100 Subject: [PATCH] Dot export can insert linebreaks between labels --- src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 5 ++++- src/storm/models/sparse/DeterministicModel.cpp | 4 ++-- src/storm/models/sparse/DeterministicModel.h | 2 +- src/storm/models/sparse/Model.cpp | 10 +++++++--- src/storm/models/sparse/Model.h | 3 ++- src/storm/models/sparse/NondeterministicModel.cpp | 4 ++-- src/storm/models/sparse/NondeterministicModel.h | 2 +- 7 files changed, 19 insertions(+), 11 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 35367ed3a..658ed75c6 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -359,7 +359,10 @@ namespace storm { storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames); } if (ioSettings.isExportDotSet()) { - storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); + std::ofstream stream; + storm::utility::openFile(ioSettings.getExportDotFilename(), stream); + model->writeDotToStream(stream, true, true); + storm::utility::closeFile(stream); } // Model checking diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 5e2b85fe4..9073e35f9 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -20,8 +20,8 @@ namespace storm { } template - void DeterministicModel::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); + void DeterministicModel::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, 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, linebreakLabel, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // iterate over all transitions and draw the arrows with probability information attached. auto rowIt = this->getTransitionMatrix().begin(); diff --git a/src/storm/models/sparse/DeterministicModel.h b/src/storm/models/sparse/DeterministicModel.h index 13486ef5c..01c2f3247 100644 --- a/src/storm/models/sparse/DeterministicModel.h +++ b/src/storm/models/sparse/DeterministicModel.h @@ -30,7 +30,7 @@ namespace storm { DeterministicModel(DeterministicModel&& other) = default; DeterministicModel& operator=(DeterministicModel&& model) = default; - 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 writeDotToStream(std::ostream& outStream, bool includeLabeling = true, bool linebreakLabeling = false, 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; }; } // namespace sparse diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 7393ad698..b9554c75c 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -334,9 +334,9 @@ namespace storm { } template - void Model::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*, bool finalizeOutput) const { + void Model::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector*, bool finalizeOutput) const { outStream << "digraph model {" << std::endl; - + // Write all states to the stream. for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { if (subsystem == nullptr || subsystem->get(state)) { @@ -358,7 +358,11 @@ namespace storm { bool includeComma = false; for (std::string const& label : this->getLabelsOfState(state)) { if (includeComma) { - outStream << ", "; + if (linebreakLabel) { + outStream << ",\n"; + } else { + outStream << ", "; + } } else { includeComma = true; } diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index aa61eb3bd..cc2fd3779 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -324,6 +324,7 @@ namespace storm { * * @param outStream The stream to which the model is to be written. * @param includeLabling If set to true, the states will be exported with their labels. + * @param linebreakLabel If set to true, a linebreak is introduced after each label. * @param subsystem If not null, this represents the subsystem that is to be exported. * @param firstValue If not null, the values in this vector are attached to the states. * @param secondValue If not null, the values in this vector are attached to the states. @@ -332,7 +333,7 @@ namespace storm { * @param finalizeOutput A flag that sets whether or not the dot stream is closed with a curly brace. * @return A string containing the exported model in dot-format. */ - 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; + virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, bool linebreakLabel = false, 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; /*! * Retrieves the set of labels attached to the given state. diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 08331c6f5..7329f9f19 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -61,8 +61,8 @@ namespace storm { } template - void NondeterministicModel::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); + void NondeterministicModel::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, 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, linebreakLabel, 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) { diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index 5280ba962..8210ec13f 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -61,7 +61,7 @@ namespace storm { virtual void printModelInformationToStream(std::ostream& out) const override; - 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 writeDotToStream(std::ostream& outStream, bool includeLabeling = true, bool linebreakLabel = false, 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; }; } // namespace sparse