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

Added dot output for both deterministic and nondeterministic models. Fixed iterator bug in sparse matrix.

tempestpy_adaptions
dehnert 12 years ago
parent
4dadedf39d
commit
fabf662edd
6 changed files with 121 additions and 45 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. 14
      src/models/AbstractDeterministicModel.h
  2. 65
      src/models/AbstractModel.h
  3. 67
      src/models/AbstractNondeterministicModel.h
  4. 4
      src/storage/SparseMatrix.h
  5. 11
      src/utility/Settings.cpp
  6. 5
      src/utility/Settings.h

14
src/models/AbstractDeterministicModel.h
View File

@ -66,10 +66,22 @@ class AbstractDeterministicModel: public AbstractModel<T> {
return this->transitionMatrix->constColumnIteratorEnd(state);
}
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<T> const* firstValue = nullptr, std::vector<T> 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 {
AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
for (auto const& transition : *this->transitionMatrix) {
if (transition.value() != storm::utility::constGetZero<T>()) {
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_ */

65
src/models/AbstractModel.h
View File

@ -315,6 +315,21 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
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<AbstractModel<T>> {
* @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<T> const* firstValue = nullptr, std::vector<T> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr) const {
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<T> const* firstValue = nullptr, std::vector<T> 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 {
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<AbstractModel<T>> {
// 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<storm::storage::SparseMatrix<T>> transitionMatrix;

67
src/models/AbstractNondeterministicModel.h
View File

@ -97,6 +97,73 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
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<T> const* firstValue = nullptr, std::vector<T> 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 {
AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
// Initialize the two iterators that we are going to use.
typename storm::storage::SparseMatrix<T>::ConstRowsIterator transitionIt = this->getTransitionMatrix().begin();
typename storm::storage::SparseMatrix<T>::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<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;

4
src/storage/SparseMatrix.h
View File

@ -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);
}
/*!

11
src/utility/Settings.cpp
View File

@ -137,7 +137,7 @@ void Settings::initDescriptions() {
("trace", "be extremely verbose, expect lots of output")
("logfile,l", bpo::value<std::string>(), "name of the log file")
("configfile,c", bpo::value<std::string>(), "name of config file")
("explicit", bpo::value<std::vector<std::string>>()->notifier(&checkExplicit), "name of transition and labeling file")
("explicit", bpo::value<std::vector<std::string>>()->multitoken()->notifier(&checkExplicit), "name of transition and labeling file")
("symbolic", bpo::value<std::string>(), "name of prism file")
("prctl", bpo::value<std::string>(), "text file containing prctl formulas")
("csl", bpo::value<std::string>(), "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

5
src/utility/Settings.h
View File

@ -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.
*/

Write Preview
Loading…
Cancel
Save