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

Dot export can insert linebreaks between labels

main
Matthias Volk 7 years ago
parent
d4f4961eb0
commit
909c035c52
7 changed files with 19 additions and 11 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. 5
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  2. 4
      src/storm/models/sparse/DeterministicModel.cpp
  3. 2
      src/storm/models/sparse/DeterministicModel.h
  4. 10
      src/storm/models/sparse/Model.cpp
  5. 3
      src/storm/models/sparse/Model.h
  6. 4
      src/storm/models/sparse/NondeterministicModel.cpp
  7. 2
      src/storm/models/sparse/NondeterministicModel.h

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

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

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

@ -20,8 +20,8 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
void DeterministicModel<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);
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);
// iterate over all transitions and draw the arrows with probability information attached.
auto rowIt = this->getTransitionMatrix().begin();

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, 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, 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;
};
} // namespace sparse

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

@ -334,9 +334,9 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
void Model<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>*, bool finalizeOutput) const {
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 {
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;
}

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

@ -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<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, 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;
/*!
* Retrieves the set of labels attached to the given state.

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

@ -61,8 +61,8 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
void NondeterministicModel<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);
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);
// Write the probability distributions for all the states.
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {

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, 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, 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;
};
} // namespace sparse

Write Preview
Loading…
Cancel
Save