Browse Source

Improved Jani-to-dot:

- Fixed problems when the model name contained a dot
- Edges are displayed nicer
- Action names are displayed.
main
Sebastian Junges 8 years ago
parent
commit
6a3310f7ee
  1. 6
      src/storm/storage/jani/Automaton.cpp
  2. 2
      src/storm/storage/jani/Automaton.h
  3. 22
      src/storm/storage/jani/Model.cpp

6
src/storm/storage/jani/Automaton.cpp

@ -529,7 +529,7 @@ namespace storm {
return result; return result;
} }
void Automaton::writeDotToStream(std::ostream& outStream) const {
void Automaton::writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const {
outStream << "\tsubgraph " << name << " {" << std::endl; outStream << "\tsubgraph " << name << " {" << std::endl;
// Write all locations to the stream. // Write all locations to the stream.
@ -541,14 +541,14 @@ namespace storm {
// Write for each edge an node to the stream; // Write for each edge an node to the stream;
uint64_t edgeIndex = 0; uint64_t edgeIndex = 0;
for (auto const& edge : edges) { for (auto const& edge : edges) {
outStream << "\t" << name << "_e" << edgeIndex << ";" << std::endl;
outStream << "\t" << name << "_e" << edgeIndex << "[ label=\"\" , shape=circle, width=.2, style=filled, fillcolor=\"black\"];" << std::endl;
++edgeIndex; ++edgeIndex;
} }
// Connect edges // Connect edges
edgeIndex = 0; edgeIndex = 0;
for (auto const& edge : edges) { for (auto const& edge : edges) {
outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << ";" << std::endl;
outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << " [label=\"" << actionNames.at(edge.getActionIndex()) << "\"];" << std::endl;
for (auto const& edgeDest : edge.getDestinations()) { for (auto const& edgeDest : edge.getDestinations()) {
outStream << "\t" << name << "_e" << edgeIndex << " -> " << name << "_s" << edgeDest.getLocationIndex() << ";" << std::endl; outStream << "\t" << name << "_e" << edgeIndex << " -> " << name << "_s" << edgeDest.getLocationIndex() << ";" << std::endl;
} }

2
src/storm/storage/jani/Automaton.h

@ -372,7 +372,7 @@ namespace storm {
*/ */
bool isLinear() const; bool isLinear() const;
void writeDotToStream(std::ostream& outStream = std::cout) const;
void writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const;
private: private:
/// The name of the automaton. /// The name of the automaton.

22
src/storm/storage/jani/Model.cpp

@ -1,5 +1,7 @@
#include "storm/storage/jani/Model.h" #include "storm/storage/jani/Model.h"
#include <algorithm>
#include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/ExpressionManager.h"
@ -1166,11 +1168,27 @@ namespace storm {
return newModel; return newModel;
} }
// Helper for writeDotToStream:
std::string filterName(std::string const& text) {
std::string result = text;
std::replace_if(result.begin() , result.end() ,
[] (const char& c) { return std::ispunct(c) ;},'_');
return result;
}
void Model::writeDotToStream(std::ostream& outStream) const { void Model::writeDotToStream(std::ostream& outStream) const {
outStream << "digraph " << name << " {" << std::endl;
outStream << "digraph " << filterName(name) << " {" << std::endl;
std::vector<std::string> actionNames;
for (auto const& act : actions) {
actionNames.push_back(act.getName());
}
for (auto const& automaton : automata) { for (auto const& automaton : automata) {
automaton.writeDotToStream(outStream);
automaton.writeDotToStream(outStream, actionNames);
outStream << std::endl; outStream << std::endl;
} }

Loading…
Cancel
Save