Browse Source

Added rowMapping to MDP transition parser.

the rowMapping is a bijective mapping (-> boost::bimap) between the row number and the (node,choice) pair.
tempestpy_adaptions
gereon 12 years ago
parent
commit
78c0245d16
  1. 13
      src/parser/NonDeterministicSparseTransitionParser.cpp
  2. 10
      src/parser/NonDeterministicSparseTransitionParser.h

13
src/parser/NonDeterministicSparseTransitionParser.cpp

@ -209,6 +209,11 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
}
this->matrix->initialize(nonzero);
/*
* Create row mapping.
*/
this->rowMapping = std::shared_ptr<RowMapping>(new RowMapping());
/*
* Parse file content.
*/
@ -234,11 +239,12 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/*
* Check if we have skipped any source node, i.e. if any node has no
* outgoing transitions. If so, insert a self-loop.
* Also add self-loops to rowMapping.
*/
for (uint_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true;
if (fixDeadlocks) {
// TODO: add (curRow <-> (node,"")) to rowMapping
this->rowMapping->insert( RowMapping::value_type( curRow, std::pair<uint_fast64_t,std::string>(node, "")) );
this->matrix->addNextValue(curRow, node, 1);
curRow++;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
@ -248,7 +254,10 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
}
lastsource = source;
// TODO: add (curRow <-> (node,choice)) to rowMapping
/*
* Add this source-choice pair to rowMapping.
*/
this->rowMapping->insert( RowMapping::value_type( curRow, std::pair<uint_fast64_t,std::string>(source, choice)) );
/*
* Skip name of choice.

10
src/parser/NonDeterministicSparseTransitionParser.h

@ -6,6 +6,8 @@
#include "src/parser/Parser.h"
#include "src/utility/OsDetection.h"
#include <boost/bimap.hpp>
#include <utility>
#include <memory>
#include <vector>
@ -20,12 +22,18 @@ class NonDeterministicSparseTransitionParser : public Parser {
public:
NonDeterministicSparseTransitionParser(std::string const &filename);
std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
return this->matrix;
}
typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowMapping;
inline std::shared_ptr<RowMapping> getRowMapping() const {
return this->rowMapping;
}
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::shared_ptr<RowMapping> rowMapping;
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode);

Loading…
Cancel
Save