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

Export to dot format allows for maximal line width in state labels and valuations

tempestpy_adaptions
Matthias Volk 5 years ago
parent
9a5a6d72c6
commit
bb71c078fa
13 changed files with 84 additions and 72 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
      CHANGELOG.md
  2. 2
      src/storm-cli-utilities/model-handling.h
  3. 5
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  4. 4
      src/storm/api/export.h
  5. 17
      src/storm/models/sparse/DeterministicModel.cpp
  6. 2
      src/storm/models/sparse/DeterministicModel.h
  7. 30
      src/storm/models/sparse/Model.cpp
  8. 4
      src/storm/models/sparse/Model.h
  9. 22
      src/storm/models/sparse/NondeterministicModel.cpp
  10. 2
      src/storm/models/sparse/NondeterministicModel.h
  11. 11
      src/storm/settings/modules/IOSettings.cpp
  12. 8
      src/storm/settings/modules/IOSettings.h
  13. 48
      src/storm/utility/export.h

1
CHANGELOG.md
View File

@ -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 <width>`)
- `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.

2
src/storm-cli-utilities/model-handling.h
View File

@ -399,7 +399,7 @@ namespace storm {
}
if (ioSettings.isExportDotSet()) {
storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename());
storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth());
}
}

5
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -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

4
src/storm/api/export.h
View File

@ -32,10 +32,10 @@ namespace storm {
}
template <typename ValueType>
void exportSparseModelAsDot(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::string const& filename) {
void exportSparseModelAsDot(std::shared_ptr<storm::models::sparse::Model<ValueType>> 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);
}

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

@ -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 <typename ValueType, typename RewardModelType>
void DeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, 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, linebreakLabel, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
void DeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, 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, 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;
}

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

@ -30,7 +30,7 @@ namespace storm {
DeterministicModel(DeterministicModel<ValueType, RewardModelType>&& other) = default;
DeterministicModel<ValueType, RewardModelType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, bool linebreakLabeling = false, 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 writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, 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;
};
} // namespace sparse

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

@ -2,16 +2,16 @@
#include <boost/algorithm/string/join.hpp>
#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<typename ValueType, typename RewardModelType>
void Model<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, 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>*, bool finalizeOutput) const {
void Model<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, 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>*, 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<std::string> 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 << "}";
}

4
src/storm/models/sparse/Model.h
View File

@ -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<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;
virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, 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;
/*!
* Retrieves the set of labels attached to the given state.

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

@ -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<typename ValueType, typename RewardModelType>
void NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, 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, linebreakLabel, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
void NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, 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, 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() << "\" ]";

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

@ -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<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 writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, 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;
};
} // namespace sparse

11
src/storm/settings/modules/IOSettings.cpp
View File

@ -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();
}

8
src/storm/settings/modules/IOSettings.h
View File

@ -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;

48
src/storm/utility/export.h
View File

@ -8,40 +8,37 @@
#include "storm/utility/file.h"
namespace storm {
namespace utility {
template <typename DataType, typename Header1Type = DataType, typename Header2Type = DataType>
template<typename DataType, typename Header1Type = DataType, typename Header2Type = DataType>
inline void exportDataToCSVFile(std::string filepath, std::vector<std::vector<DataType>> const& data, boost::optional<std::vector<Header1Type>> const& header1 = boost::none, boost::optional<std::vector<Header2Type>> 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<typename Container>
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;
}
}
}
}
}

Write Preview
Loading…
Cancel
Save