From bb71c078fa6ce699525dfddb458f88d999e3c8db Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 Oct 2019 16:54:30 +0100 Subject: [PATCH] Export to dot format allows for maximal line width in state labels and valuations --- CHANGELOG.md | 1 + src/storm-cli-utilities/model-handling.h | 2 +- .../modelchecker/dft/DFTModelChecker.cpp | 5 +- src/storm/api/export.h | 4 +- .../models/sparse/DeterministicModel.cpp | 17 +++---- src/storm/models/sparse/DeterministicModel.h | 2 +- src/storm/models/sparse/Model.cpp | 30 ++++-------- src/storm/models/sparse/Model.h | 4 +- .../models/sparse/NondeterministicModel.cpp | 22 +++------ .../models/sparse/NondeterministicModel.h | 2 +- src/storm/settings/modules/IOSettings.cpp | 11 ++++- src/storm/settings/modules/IOSettings.h | 8 ++++ src/storm/utility/export.h | 48 ++++++++++++++----- 13 files changed, 84 insertions(+), 72 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8dcf4eb55..c67e2e75c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,6 +25,7 @@ Version 1.3.x - Support for export of MTBDDs from Storm. - New settings module `transformation` for Markov chain transformations. Use `--help transformation` to get a list of available transformations. - Support for eliminating chains of Non-Markovian states in MAs via `--eliminate-chains`. +- Export to dot format allows for maximal line width in states (argument `--dot-maxwidth `) - `storm-conv` can now apply transformations on a prism file. - `storm-dft`: Support partial-order for state space generation. - `storm-dft`: Compute lower and upper bounds for number of BE failures via SMT. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 9d4306b48..815332974 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -399,7 +399,7 @@ namespace storm { } if (ioSettings.isExportDotSet()) { - storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); + storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth()); } } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 4940dc0e6..5bc4b0f4c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -424,10 +424,7 @@ namespace storm { storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames); } if (ioSettings.isExportDotSet()) { - std::ofstream stream; - storm::utility::openFile(ioSettings.getExportDotFilename(), stream); - model->writeDotToStream(stream, true, true); - storm::utility::closeFile(stream); + storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth()); } // Model checking diff --git a/src/storm/api/export.h b/src/storm/api/export.h index f3064b538..ca05b7a47 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -32,10 +32,10 @@ namespace storm { } template - void exportSparseModelAsDot(std::shared_ptr> const& model, std::string const& filename) { + void exportSparseModelAsDot(std::shared_ptr> const& model, std::string const& filename, size_t maxWidth = 30) { std::ofstream stream; storm::utility::openFile(filename, stream); - model->writeDotToStream(stream); + model->writeDotToStream(stream, maxWidth); storm::utility::closeFile(stream); } diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 9073e35f9..06419a6c0 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -1,7 +1,9 @@ #include "storm/models/sparse/DeterministicModel.h" + +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/constants.h" -#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/utility/export.h" namespace storm { namespace models { @@ -20,8 +22,8 @@ namespace storm { } template - 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); + void DeterministicModel::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, 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, maxWidthLabel, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // iterate over all transitions and draw the arrows with probability information attached. auto rowIt = this->getTransitionMatrix().begin(); @@ -33,14 +35,7 @@ namespace storm { arrowOrigin = "\"" + arrowOrigin + "c\""; outStream << "\t" << arrowOrigin << " [shape = \"point\"]" << std::endl; outStream << "\t" << i << " -> " << arrowOrigin << " [label= \"{"; - bool firstLabel = true; - for (auto const& label : this->getChoiceLabeling().getLabelsOfChoice(i)) { - if (!firstLabel) { - outStream << ", "; - } - firstLabel = false; - outStream << label; - } + storm::utility::outputFixedWidth(outStream, this->getChoiceLabeling().getLabelsOfChoice(i), maxWidthLabel); outStream << "}\"];" << std::endl; } diff --git a/src/storm/models/sparse/DeterministicModel.h b/src/storm/models/sparse/DeterministicModel.h index 01c2f3247..09a8d7ce7 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, 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; + virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, 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; }; } // namespace sparse diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index a5b0e6002..1fe875ab9 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -2,16 +2,16 @@ #include -#include "storm/models/sparse/StandardRewardModel.h" - -#include "storm/utility/vector.h" #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/utility/NumberTraits.h" - #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/vector.h" +#include "storm/utility/export.h" +#include "storm/utility/NumberTraits.h" + namespace storm { namespace models { @@ -336,7 +336,7 @@ namespace storm { } template - 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 { + void Model::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, 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 { outStream << "digraph model {" << std::endl; // Write all states to the stream. @@ -350,26 +350,16 @@ namespace storm { if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) { outStream << "label = \"" << state; if (hasStateValuations()) { - outStream << " " << getStateValuations().getStateInfo(state); + std::vector results; + boost::split(results, getStateValuations().getStateInfo(state), [](char c) { return c == ',';}); + storm::utility::outputFixedWidth(outStream, results, maxWidthLabel); } outStream << ": "; // Now print the state labeling to the stream if requested. if (includeLabeling) { outStream << "{"; - bool includeComma = false; - for (std::string const& label : this->getLabelsOfState(state)) { - if (includeComma) { - if (linebreakLabel) { - outStream << ",\n"; - } else { - outStream << ", "; - } - } else { - includeComma = true; - } - outStream << label; - } + storm::utility::outputFixedWidth(outStream, this->getLabelsOfState(state), maxWidthLabel); outStream << "}"; } diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 885374ab6..d1ef45bc1 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -323,8 +323,8 @@ namespace storm { * Exports the model to the dot-format and prints the result to the given stream. * * @param outStream The stream to which the model is to be written. + * @param maxWidthLabel Maximal width of the labeling before a linebreak is inserted. Value 0 represents no linebreaks. * @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. @@ -333,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, 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; + virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, 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; /*! * 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 1a5cfd7b1..635cfee7b 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -1,15 +1,14 @@ #include "storm/models/sparse/NondeterministicModel.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/storage/Scheduler.h" #include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/transformer/SubsystemBuilder.h" - -#include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm/exceptions/InvalidOperationException.h" +#include "storm/utility/export.h" namespace storm { namespace models { @@ -72,8 +71,8 @@ namespace storm { } template - 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); + void NondeterministicModel::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, 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, maxWidthLabel, 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) { @@ -125,14 +124,7 @@ namespace storm { outStream << " [ label = \"{"; } arrowHasLabel = true; - bool firstLabel = true; - for (auto const& label : this->getChoiceLabeling().getLabelsOfChoice(rowIndex)) { - if (!firstLabel) { - outStream << ", "; - } - firstLabel = false; - outStream << label; - } + storm::utility::outputFixedWidth(outStream, this->getChoiceLabeling().getLabelsOfChoice(rowIndex), maxWidthLabel); outStream << "}"; } if (arrowHasLabel) { @@ -157,7 +149,7 @@ namespace storm { } outStream << ";" << std::endl; - // Now draw all probabilitic arcs that belong to this nondeterminstic choice. + // Now draw all probabilistic arcs that belong to this non-deterministic choice. for (auto const& transition : row) { if (subsystem == nullptr || subsystem->get(transition.getColumn())) { outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << "\" ]"; diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index 8210ec13f..2a76c1ee0 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, 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; + virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, 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; }; } // namespace sparse diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 583f37c7f..edfc2eaae 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; + const std::string IOSettings::exportDotMaxWidthOptionName = "dot-maxwidth"; const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; const std::string IOSettings::exportDdOptionName = "exportdd"; const std::string IOSettings::exportJaniDotOptionName = "exportjanidot"; @@ -50,9 +51,11 @@ namespace storm { const std::string IOSettings::qvbsRootOptionName = "qvbsroot"; IOSettings::IOSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced() + this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, false, "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced() + this->addOption(storm::settings::OptionBuilder(moduleName, exportDotMaxWidthOptionName, false, "The maximal width for labels in the dot format. For longer lines a linebreak is inserted. Value 0 represents no linebreaks.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("width", "The maximal line width for the dot format.").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, false, "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build()); @@ -112,6 +115,10 @@ namespace storm { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } + size_t IOSettings::getExportDotMaxWidth() const { + return this->getOption(exportDotMaxWidthOptionName).getArgumentByName("width").getValueAsUnsignedInteger(); + } + bool IOSettings::isExportJaniDotSet() const { return this->getOption(exportJaniDotOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 9731a272c..91cc3b765 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -37,6 +37,13 @@ namespace storm { */ std::string getExportDotFilename() const; + /*! + * Retrieves the maximal width for labels in the dot format. + * + * @return The maximal width. + */ + size_t getExportDotMaxWidth() const; + /*! * Retrieves whether the export-to-dot option for jani was set. * @@ -325,6 +332,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string exportDotOptionName; + static const std::string exportDotMaxWidthOptionName; static const std::string exportJaniDotOptionName; static const std::string exportExplicitOptionName; static const std::string exportDdOptionName; diff --git a/src/storm/utility/export.h b/src/storm/utility/export.h index babf90d63..f067f88b3 100644 --- a/src/storm/utility/export.h +++ b/src/storm/utility/export.h @@ -8,40 +8,37 @@ #include "storm/utility/file.h" - namespace storm { namespace utility { - - - template + template inline void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& header1 = boost::none, boost::optional> const& header2 = boost::none) { std::ofstream filestream; storm::utility::openFile(filepath, filestream); - + if (header1) { - for(auto columnIt = header1->begin(); columnIt != header1->end(); ++columnIt) { - if(columnIt != header1->begin()) { + for (auto columnIt = header1->begin(); columnIt != header1->end(); ++columnIt) { + if (columnIt != header1->begin()) { filestream << ","; } filestream << *columnIt; } filestream << std::endl; } - + if (header2) { - for(auto columnIt = header2->begin(); columnIt != header2->end(); ++columnIt) { - if(columnIt != header2->begin()) { + for (auto columnIt = header2->begin(); columnIt != header2->end(); ++columnIt) { + if (columnIt != header2->begin()) { filestream << ","; } filestream << *columnIt; } filestream << std::endl; } - + for (auto const& row : data) { - for(auto columnIt = row.begin(); columnIt != row.end(); ++columnIt) { - if(columnIt != row.begin()) { + for (auto columnIt = row.begin(); columnIt != row.end(); ++columnIt) { + if (columnIt != row.begin()) { filestream << ","; } filestream << *columnIt; @@ -50,6 +47,31 @@ namespace storm { } storm::utility::closeFile(filestream); } + + /*! + * Output list of strings with linebreaks according to fixed width. + * Strings are printed with comma separator. + * If the length of the current line is greater than maxWidth, a linebreak is inserted. + * @param stream Output stream. + * @param output List of strings to output. + * @param maxWidth Maximal width after which a linebreak is inserted. Value 0 represents no linebreaks. + */ + template + inline void outputFixedWidth(std::ostream& stream, Container const& output, size_t maxWidth = 30) { + size_t curLength = 0; + for (auto s : output) { + if (curLength > 0) { + stream << ", "; + curLength += 2; + } + stream << s; + curLength += s.length(); + if (maxWidth > 0 && curLength >= maxWidth) { + stream << std::endl; + curLength = 0; + } + } + } } }