Browse Source

changed rowMapping to vector<int>

main
gereon 12 years ago
parent
commit
54565ddd55
  1. 6
      src/models/Mdp.h
  2. 15
      src/parser/NonDeterministicSparseTransitionParser.cpp
  3. 7
      src/parser/NonDeterministicSparseTransitionParser.h

6
src/models/Mdp.h

@ -45,7 +45,7 @@ public:
*/ */
Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix, Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling, std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
std::shared_ptr<storm::parser::RowStateMapping> rowMapping, std::shared_ptr<std::vector<uint_fast64_t>> rowMapping,
std::shared_ptr<std::vector<T>> stateRewards = nullptr, std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr) std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping), : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
@ -228,8 +228,8 @@ private:
/*! The labeling of the states of the MDP. */ /*! The labeling of the states of the MDP. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling; std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
/*! The mapping from rows to (state,choice) pairs. */ /*! The mapping from states to rows. */
std::shared_ptr<storm::parser::RowStateMapping> rowMapping; std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
/*! The state-based rewards of the MDP. */ /*! The state-based rewards of the MDP. */
std::shared_ptr<std::vector<T>> stateRewards; std::shared_ptr<std::vector<T>> stateRewards;

15
src/parser/NonDeterministicSparseTransitionParser.cpp

@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/* /*
* Create row mapping. * Create row mapping.
*/ */
this->rowMapping = std::shared_ptr<RowStateMapping>(new RowStateMapping()); this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+1,0));
/* /*
* Parse file content. * Parse file content.
@ -245,7 +245,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
for (int_fast64_t node = lastsource + 1; node < source; node++) { for (int_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true; hadDeadlocks = true;
if (fixDeadlocks) { if (fixDeadlocks) {
this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, ""))); this->rowMapping->at(node) = curRow;
this->matrix->addNextValue(curRow, node, 1); this->matrix->addNextValue(curRow, node, 1);
curRow++; curRow++;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
@ -253,13 +253,14 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
} }
} }
if (source != lastsource) {
/*
* Add this source to rowMapping, if this is the first choice we encounter for this state.
*/
this->rowMapping->at(source) = curRow;
}
lastsource = source; lastsource = source;
/*
* Add this source-choice pair to rowMapping.
*/
this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
/* /*
* Skip name of choice. * Skip name of choice.
*/ */

7
src/parser/NonDeterministicSparseTransitionParser.h

@ -6,7 +6,6 @@
#include "src/parser/Parser.h" #include "src/parser/Parser.h"
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"
#include <boost/bimap.hpp>
#include <utility> #include <utility>
#include <memory> #include <memory>
#include <vector> #include <vector>
@ -14,8 +13,6 @@
namespace storm { namespace storm {
namespace parser { namespace parser {
typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowStateMapping;
/*! /*!
* @brief Load a nondeterministic transition system from file and create a * @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges * sparse adjacency matrix whose entries represent the weights of the edges
@ -28,13 +25,13 @@ class NonDeterministicSparseTransitionParser : public Parser {
return this->matrix; return this->matrix;
} }
inline std::shared_ptr<RowStateMapping> getRowMapping() const { inline std::shared_ptr<std::vector<uint_fast64_t>> getRowMapping() const {
return this->rowMapping; return this->rowMapping;
} }
private: private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix; std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::shared_ptr<RowStateMapping> rowMapping; std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode); uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);

|||||||
100:0
Loading…
Cancel
Save