From fabf662edd88df8babd8348468e628744c4f42d0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Jun 2013 17:15:37 +0200 Subject: [PATCH] Added dot output for both deterministic and nondeterministic models. Fixed iterator bug in sparse matrix. --- src/models/AbstractDeterministicModel.h | 14 ++++- src/models/AbstractModel.h | 65 +++++++++++---------- src/models/AbstractNondeterministicModel.h | 67 ++++++++++++++++++++++ src/storage/SparseMatrix.h | 4 +- src/utility/Settings.cpp | 11 ++-- src/utility/Settings.h | 5 -- 6 files changed, 121 insertions(+), 45 deletions(-) diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 88ed50979..9cb6990e9 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -66,10 +66,22 @@ class AbstractDeterministicModel: public AbstractModel { return this->transitionMatrix->constColumnIteratorEnd(state); } + 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 { + AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + + for (auto const& transition : *this->transitionMatrix) { + if (transition.value() != storm::utility::constGetZero()) { + outStream << "\t" << transition.row() << " -> " << transition.column() << " [ label= \"" << transition.value() << "\" ];" << std::endl; + } + } + + if (finalizeOutput) { + outStream << "}" << std::endl; + } + } }; } // namespace models - } // namespace storm #endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */ diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index aaae20f71..b1233f1c0 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -315,6 +315,21 @@ class AbstractModel: public std::enable_shared_from_this> { return result; } + /*! + * Prints information about the model to the specified stream. + * @param out The stream the information is to be printed to. + */ + void printModelInformationToStream(std::ostream& out) const { + out << "-------------------------------------------------------------- " << std::endl; + out << "Model type: \t\t" << this->getType() << std::endl; + out << "States: \t\t" << this->getNumberOfStates() << std::endl; + out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + this->getStateLabeling().printAtomicPropositionsInformationToStream(out); + out << "Size in memory: \t" << (this->getSizeInMemory())/1024 << " kbytes" << std::endl; + out << "-------------------------------------------------------------- " << std::endl; + } + +protected: /*! * Exports the model to the dot-format and prints the result to the given stream. * @@ -325,41 +340,45 @@ class AbstractModel: public std::enable_shared_from_this> { * @param secondValue If not null, the values in this vector are attached to the states. * @param stateColoring If not null, this is a mapping from states to color codes. * @param colors A mapping of color codes to color names. + * @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) const { + 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 { outStream << "digraph deterministicModel {" << std::endl; - for (uint_fast64_t stateIndex = 0, highestStateIndex = this->getNumberOfStates() - 1; stateIndex <= highestStateIndex; ++stateIndex) { - outStream << "\t" << stateIndex; + for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { + outStream << "\t" << state; if (includeLabeling || firstValue != nullptr || secondValue != nullptr || stateColoring != nullptr) { outStream << " [ "; if (includeLabeling || firstValue != nullptr || secondValue != nullptr) { - outStream << "label = \""; + outStream << "label = \"" << state << ": "; // Now print the state labeling to the stream if requested. if (includeLabeling) { - bool insertComma = true; - for (std::string const& label : this->getLabelsForState(stateIndex)) { - if (insertComma) { + outStream << "{"; + bool includeComma = false; + for (std::string const& label : this->getLabelsForState(state)) { + if (includeComma) { outStream << ", "; - insertComma = false; + } else { + includeComma = true; } outStream << label; } + outStream << "}"; } // If we are to include some values for the state as well, we do so now. if (firstValue != nullptr || secondValue != nullptr) { outStream << "["; if (firstValue != nullptr) { - outStream << (*firstValue)[stateIndex]; + outStream << (*firstValue)[state]; if (secondValue != nullptr) { outStream << ", "; } } if (secondValue != nullptr) { - outStream << (*secondValue)[stateIndex]; + outStream << (*secondValue)[state]; } outStream << "]"; } @@ -368,35 +387,19 @@ class AbstractModel: public std::enable_shared_from_this> { // Now, we color the states if there were colors given. if (stateColoring != nullptr && colors != nullptr) { outStream << ", "; - outStream << " fillcolor = \"" << (*colors)[(*stateColoring)[stateIndex]] << "\""; + outStream << " fillcolor = \"" << (*colors)[(*stateColoring)[state]] << "\""; } } outStream << " ]"; } - outStream << ";"; + outStream << ";" << std::endl; } - outStream << "}" << std::endl; + if (finalizeOutput) { + outStream << "}" << std::endl; + } } - /*! - * Prints information about the model to the specified stream. - * @param out The stream the information is to be printed to. - */ - void printModelInformationToStream(std::ostream& out) const { - out << "-------------------------------------------------------------- " - << std::endl; - out << "Model type: \t\t" << this->getType() << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; - this->getStateLabeling().printAtomicPropositionsInformationToStream(out); - out << "Size in memory: \t" - << (this->getSizeInMemory())/1024 << " kbytes" << std::endl; - out << "-------------------------------------------------------------- " - << std::endl; - } - -protected: /*! A matrix representing the likelihoods of moving between states. */ std::shared_ptr> transitionMatrix; diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 0aacc698b..39b4a6ed2 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -97,6 +97,73 @@ class AbstractNondeterministicModel: public AbstractModel { return this->transitionMatrix->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); } + 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 { + AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + + // Initialize the two iterators that we are going to use. + typename storm::storage::SparseMatrix::ConstRowsIterator transitionIt = this->getTransitionMatrix().begin(); + typename storm::storage::SparseMatrix::ConstRowsIterator transitionIte = this->getTransitionMatrix().begin(); + + for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { + uint_fast64_t rowCount = (*nondeterministicChoiceIndices)[state + 1] - (*nondeterministicChoiceIndices)[state]; + bool highlightChoice = true; + for (uint_fast64_t row = 0; row < rowCount; ++row) { + if (scheduler != nullptr) { + // If the scheduler picked the current choice, we will not make it dotted, but highlight it. + if ((*scheduler)[state] == row) { + highlightChoice = true; + } else { + highlightChoice = false; + } + } + + // For each nondeterministic choice, we draw an arrow to an intermediate node to better display + // the grouping of transitions. + outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\""; + + // If we were given a scheduler to highlight, we do so now. + if (scheduler != nullptr) { + if (highlightChoice) { + outStream << ", fillcolor=\"red\""; + } + } + outStream << "];" << std::endl; + + outStream << "\t" << state << " -> \"" << state << "c" << row << "\""; + + // If we were given a scheduler to highlight, we do so now. + if (scheduler != nullptr) { + if (highlightChoice) { + outStream << " [color=\"red\", penwidth = 2]"; + } else { + outStream << " [style = \"dotted\"]"; + } + } + outStream << ";" << std::endl; + + // Now draw all probabilitic arcs that belong to this nondeterminstic choice. + transitionIte.moveToNextRow(); + for (; transitionIt != transitionIte; ++transitionIt) { + outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]"; + + // If we were given a scheduler to highlight, we do so now. + if (scheduler != nullptr) { + if (highlightChoice) { + outStream << " [color=\"red\", penwidth = 2]"; + } else { + outStream << " [style = \"dotted\"]"; + } + } + outStream << ";" << std::endl; + } + } + } + + if (finalizeOutput) { + outStream << "}" << std::endl; + } + } + private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ std::shared_ptr> nondeterministicChoiceIndices; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 4bc369a57..eb5cca456 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -1009,7 +1009,7 @@ public: * @returns A const iterator that points past the last element of the matrix. */ ConstRowsIterator end() const { - return ConstRowsIterator(this->rowCount); + return ConstRowsIterator(*this, this->rowCount); } /*! @@ -1019,7 +1019,7 @@ public: * @returns A const iterator that points to the first element after the given row. */ ConstRowsIterator end(uint_fast64_t row) const { - return ConstRowsIterator(row + 1); + return ConstRowsIterator(*this, row + 1); } /*! diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 1a071d3c0..d31eea7a2 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -137,7 +137,7 @@ void Settings::initDescriptions() { ("trace", "be extremely verbose, expect lots of output") ("logfile,l", bpo::value(), "name of the log file") ("configfile,c", bpo::value(), "name of config file") - ("explicit", bpo::value>()->notifier(&checkExplicit), "name of transition and labeling file") + ("explicit", bpo::value>()->multitoken()->notifier(&checkExplicit), "name of transition and labeling file") ("symbolic", bpo::value(), "name of prism file") ("prctl", bpo::value(), "text file containing prctl formulas") ("csl", bpo::value(), "text file containing csl formulas") @@ -151,7 +151,7 @@ void Settings::initDescriptions() { /*! * Perform a sloppy parsing run: parse command line and config file (if * given), but allow for unregistered options, do not check requirements - * from options_description objects, do not check positional arguments. + * from options_description objects. */ void Settings::firstRun(int const argc, char const * const argv[], char const * const filename) { LOG4CPLUS_DEBUG(logger, "Performing first run."); @@ -171,12 +171,12 @@ void Settings::firstRun(int const argc, char const * const argv[], char const * /*! * Perform the second parser run: parse command line and config file (if * given) and check for unregistered options, requirements from - * options_description objects and positional arguments. + * options_description objects. */ void Settings::secondRun(int const argc, char const * const argv[], char const * const filename) { LOG4CPLUS_DEBUG(logger, "Performing second run."); // Parse command line. - bpo::store(bpo::command_line_parser(argc, argv).options(*(Settings::desc)).positional(this->positional).run(), this->vm); + bpo::store(bpo::command_line_parser(argc, argv).options(*(Settings::desc)).run(), this->vm); /* * Load config file if specified. */ @@ -189,8 +189,7 @@ void Settings::secondRun(int const argc, char const * const argv[], char const * /*! - * Print a short general usage information consisting of the positional - * options and the list of available command line options. + * Print a short general usage information consisting of the the list of available command line options. * * Use it like this: * @code std::cout << storm::settings::help; @endcode diff --git a/src/utility/Settings.h b/src/utility/Settings.h index b68aa4e6f..bdf8fef63 100644 --- a/src/utility/Settings.h +++ b/src/utility/Settings.h @@ -177,11 +177,6 @@ namespace settings { */ void secondRun(int const argc, char const * const argv[], char const * const filename); - /*! - * @brief Option description for positional arguments on command line. - */ - bpo::positional_options_description positional; - /*! * @brief Collecting option descriptions. */