From e0ee4ea2fd3d36a5ab13f028e1a527b9f27dddba Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Fri, 20 Sep 2013 14:31:29 +0200
Subject: [PATCH] Implemented a method for generating a choiceLabeling based on
the stateIds
Former-commit-id: d1eedecc22f8053137653c0ec12ec01f7142282a
---
src/models/AbstractDeterministicModel.h | 17 +++++++++++++++++
src/models/AbstractModel.h | 10 +++++++---
src/models/AbstractNondeterministicModel.h | 21 ++++++++++++++++++++-
3 files changed, 44 insertions(+), 4 deletions(-)
diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h
index b76211a92..53d95449e 100644
--- a/src/models/AbstractDeterministicModel.h
+++ b/src/models/AbstractDeterministicModel.h
@@ -110,6 +110,23 @@ class AbstractDeterministicModel: public AbstractModel<T> {
outStream << "}" << std::endl;
}
}
+
+ /*!
+ * Assigns this model a new set of choiceLabels, giving each state a label with the stateId
+ * @return void
+ */
+ virtual void setStateIdBasedChoiceLabeling() override {
+ std::vector<std::list<uint_fast64_t>> newChoiceLabeling;
+
+ size_t stateCount = this->getNumberOfStates();
+ newChoiceLabeling.resize(stateCount);
+
+ for (size_t state = 0; state < stateCount; ++state) {
+ newChoiceLabeling.at(state).push_back(state);
+ }
+
+ this->choiceLabeling.reset(newChoiceLabeling);
+ }
};
} // namespace models
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 760fb6cc5..03a0eade1 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -443,6 +443,11 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
return result;
}
+ /*!
+ * Assigns this model a new set of choiceLabels, giving each choice the stateId
+ * @return void
+ */
+ virtual void setStateIdBasedChoiceLabeling() = 0;
protected:
/*!
* Exports the model to the dot-format and prints the result to the given stream.
@@ -523,6 +528,8 @@ protected:
/*! A matrix representing the likelihoods of moving between states. */
storm::storage::SparseMatrix<T> transitionMatrix;
+ /*! The labeling that is associated with the choices for each state. */
+ boost::optional<std::vector<std::list<uint_fast64_t>>> choiceLabeling;
private:
/*! The labeling of the states of the model. */
storm::models::AtomicPropositionsLabeling stateLabeling;
@@ -532,9 +539,6 @@ private:
/*! The transition-based rewards of the model. */
boost::optional<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
- /*! The labeling that is associated with the choices for each state. */
- boost::optional<std::vector<std::list<uint_fast64_t>>> choiceLabeling;
};
} // namespace models
diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h
index 516238e14..9e01e224f 100644
--- a/src/models/AbstractNondeterministicModel.h
+++ b/src/models/AbstractNondeterministicModel.h
@@ -219,7 +219,26 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
outStream << "}" << std::endl;
}
}
-
+
+ /*!
+ * Assigns this model a new set of choiceLabels, giving each choice a label with the stateId
+ * @return void
+ */
+ virtual void setStateIdBasedChoiceLabeling() override {
+ std::vector<std::list<uint_fast64_t>> newChoiceLabeling;
+
+ size_t stateCount = this->getNumberOfStates();
+ size_t choiceCount = this->getNumberOfChoices();
+ newChoiceLabeling.resize(choiceCount);
+
+ for (size_t state = 0; state < stateCount; ++state) {
+ for (size_t choice = this->nondeterministicChoiceIndices.at(state); choice < this->nondeterministicChoiceIndices.at(state + 1); ++choice) {
+ newChoiceLabeling.at(choice).push_back(state);
+ }
+ }
+
+ this->choiceLabeling.reset(newChoiceLabeling);
+ }
private:
/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
std::vector<uint_fast64_t> nondeterministicChoiceIndices;