From 8c248c05c553118db4cb73adad471bd491610983 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 11 Feb 2013 20:47:47 +0100 Subject: [PATCH] Renamed NonDeterministic to Nondeterministic in all places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A algorithm. --- ...odel.h => AbstractNondeterministicModel.h} | 28 ++++++++---- src/models/Ctmdp.h | 8 ++-- src/models/Mdp.h | 8 ++-- src/parser/AutoParser.h | 6 +-- ...er.cpp => NondeterministicModelParser.cpp} | 8 ++-- ...Parser.h => NondeterministicModelParser.h} | 7 ++- ...ondeterministicSparseTransitionParser.cpp} | 6 +-- ... NondeterministicSparseTransitionParser.h} | 4 +- src/utility/GraphAnalyzer.h | 44 ++++++++++++++++--- test/parser/ParseMdpTest.cpp | 6 +-- test/storage/SparseMatrixTest.cpp | 8 ++-- 11 files changed, 88 insertions(+), 45 deletions(-) rename src/models/{AbstractNonDeterministicModel.h => AbstractNondeterministicModel.h} (65%) rename src/parser/{NonDeterministicModelParser.cpp => NondeterministicModelParser.cpp} (87%) rename src/parser/{NonDeterministicModelParser.h => NondeterministicModelParser.h} (93%) rename src/parser/{NonDeterministicSparseTransitionParser.cpp => NondeterministicSparseTransitionParser.cpp} (97%) rename src/parser/{NonDeterministicSparseTransitionParser.h => NondeterministicSparseTransitionParser.h} (88%) diff --git a/src/models/AbstractNonDeterministicModel.h b/src/models/AbstractNondeterministicModel.h similarity index 65% rename from src/models/AbstractNonDeterministicModel.h rename to src/models/AbstractNondeterministicModel.h index 257644093..0ca1dea37 100644 --- a/src/models/AbstractNonDeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -16,7 +16,7 @@ namespace models { * This is base class defines a common interface for all non-deterministic models. */ template -class AbstractNonDeterministicModel: public AbstractModel { +class AbstractNondeterministicModel: public AbstractModel { public: /*! Constructs an abstract non-determinstic model from the given parameters. @@ -27,27 +27,27 @@ class AbstractNonDeterministicModel: public AbstractModel { * @param stateRewardVector The reward values associated with the states. * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ - AbstractNonDeterministicModel(std::shared_ptr> transitionMatrix, + AbstractNondeterministicModel(std::shared_ptr> transitionMatrix, std::shared_ptr stateLabeling, - std::shared_ptr> choiceIndices, + std::shared_ptr> nondeterministicChoiceIndices, std::shared_ptr> stateRewardVector, std::shared_ptr> transitionRewardMatrix) : AbstractModel(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), - choiceIndices(choiceIndices) { + nondeterministicChoiceIndices(nondeterministicChoiceIndices) { } /*! * Destructor. */ - virtual ~AbstractNonDeterministicModel() { + virtual ~AbstractNondeterministicModel() { // Intentionally left empty. } /*! * Copy Constructor. */ - AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel(other), - choiceIndices(other.choiceIndices) { + AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel(other), + nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) { // Intentionally left empty. } @@ -57,12 +57,22 @@ class AbstractNonDeterministicModel: public AbstractModel { * measured in bytes. */ virtual uint_fast64_t getSizeInMemory() const { - return AbstractModel::getSizeInMemory() + choiceIndices->size() * sizeof(uint_fast64_t); + return AbstractModel::getSizeInMemory() + nondeterministicChoiceIndices->size() * sizeof(uint_fast64_t); + } + + /*! + * Retrieves the vector indicating which matrix rows represent non-deterministic choices + * of a certain state. + * @param the vector indicating which matrix rows represent non-deterministic choices + * of a certain state. + */ + std::shared_ptr> getNondeterministicChoiceIndices() const { + return nondeterministicChoiceIndices; } private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ - std::shared_ptr> choiceIndices; + std::shared_ptr> nondeterministicChoiceIndices; }; } // namespace models diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index 3e1f8f5b8..e693c70a1 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -12,7 +12,7 @@ #include #include "AtomicPropositionsLabeling.h" -#include "AbstractNonDeterministicModel.h" +#include "AbstractNondeterministicModel.h" #include "src/storage/SparseMatrix.h" #include "src/utility/Settings.h" @@ -25,7 +25,7 @@ namespace models { * labeled with atomic propositions. */ template -class Ctmdp : public storm::models::AbstractNonDeterministicModel { +class Ctmdp : public storm::models::AbstractNondeterministicModel { public: //! Constructor @@ -42,7 +42,7 @@ public: std::shared_ptr> choiceIndices, std::shared_ptr> stateRewardVector = nullptr, std::shared_ptr> transitionRewardMatrix = nullptr) - : AbstractNonDeterministicModel(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) { + : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -54,7 +54,7 @@ public: * Copy Constructor. Performs a deep copy of the given CTMDP. * @param ctmdp A reference to the CTMDP that is to be copied. */ - Ctmdp(const Ctmdp &ctmdp) : AbstractNonDeterministicModel(ctmdp) { + Ctmdp(const Ctmdp &ctmdp) : AbstractNondeterministicModel(ctmdp) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; diff --git a/src/models/Mdp.h b/src/models/Mdp.h index dc92dfda6..515a1842e 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -16,7 +16,7 @@ #include "AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" #include "src/utility/Settings.h" -#include "src/models/AbstractNonDeterministicModel.h" +#include "src/models/AbstractNondeterministicModel.h" namespace storm { @@ -27,7 +27,7 @@ namespace models { * labeled with atomic propositions. */ template -class Mdp : public storm::models::AbstractNonDeterministicModel { +class Mdp : public storm::models::AbstractNondeterministicModel { public: //! Constructor @@ -44,7 +44,7 @@ public: std::shared_ptr> choiceIndices, std::shared_ptr> stateRewardVector = nullptr, std::shared_ptr> transitionRewardMatrix = nullptr) - : AbstractNonDeterministicModel(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) { + : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -56,7 +56,7 @@ public: * Copy Constructor. Performs a deep copy of the given MDP. * @param mdp A reference to the MDP that is to be copied. */ - Mdp(const Mdp &mdp) : AbstractNonDeterministicModel(mdp) { + Mdp(const Mdp &mdp) : AbstractNondeterministicModel(mdp) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index d7337ae54..f7331da7e 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -7,7 +7,7 @@ #include "src/exceptions/WrongFileFormatException.h" #include "src/models/AbstractModel.h" #include "src/parser/DeterministicModelParser.h" -#include "src/parser/NonDeterministicModelParser.h" +#include "src/parser/NondeterministicModelParser.h" #include #include @@ -57,12 +57,12 @@ class AutoParser : Parser { break; } case storm::models::MDP: { - NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); this->model = parser.getMdp(); break; } case storm::models::CTMDP: { - NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); this->model = parser.getCtmdp(); break; } diff --git a/src/parser/NonDeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp similarity index 87% rename from src/parser/NonDeterministicModelParser.cpp rename to src/parser/NondeterministicModelParser.cpp index 017d3b31e..036f0dc9b 100644 --- a/src/parser/NonDeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -10,7 +10,7 @@ #include #include -#include "src/parser/NonDeterministicSparseTransitionParser.h" +#include "src/parser/NondeterministicSparseTransitionParser.h" #include "src/parser/AtomicPropositionLabelingParser.h" #include "src/parser/SparseStateRewardParser.h" @@ -27,9 +27,9 @@ namespace parser { * @param stateRewardFile String containing the location of the state reward file (...srew) * @param transitionRewardFile String containing the location of the transition reward file (...trew) */ -NonDeterministicModelParser::NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, +NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { - storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile); + storm::parser::NondeterministicSparseTransitionParser tp(transitionSystemFile); uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); @@ -38,7 +38,7 @@ NonDeterministicModelParser::NonDeterministicModelParser(std::string const & tra this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { - storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile); + storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile); this->transitionRewardMatrix = trp.getMatrix(); } diff --git a/src/parser/NonDeterministicModelParser.h b/src/parser/NondeterministicModelParser.h similarity index 93% rename from src/parser/NonDeterministicModelParser.h rename to src/parser/NondeterministicModelParser.h index 379fdf07c..bdc4c42d4 100644 --- a/src/parser/NonDeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -13,6 +13,7 @@ #include "src/models/Ctmdp.h" namespace storm { + namespace parser { /*! @@ -23,9 +24,9 @@ namespace parser { * * @note The labeling representation in the file may use at most as much nodes as are specified in the mdp. */ -class NonDeterministicModelParser: public storm::parser::Parser { +class NondeterministicModelParser: public storm::parser::Parser { public: - NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, + NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); std::shared_ptr> getMdp() { @@ -58,5 +59,7 @@ private: }; } /* namespace parser */ + } /* namespace storm */ + #endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */ diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp similarity index 97% rename from src/parser/NonDeterministicSparseTransitionParser.cpp rename to src/parser/NondeterministicSparseTransitionParser.cpp index 26436fb55..a17f48552 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -5,7 +5,7 @@ * Author: Gereon Kremer */ -#include "src/parser/NonDeterministicSparseTransitionParser.h" +#include "src/parser/NondeterministicSparseTransitionParser.h" #include #include @@ -49,7 +49,7 @@ namespace parser { * @param maxnode Is set to highest id of all nodes. * @return The number of non-zero elements. */ -uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) { +uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) { /* * Check file header and extract number of transitions. */ @@ -154,7 +154,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_ * @return a pointer to the created sparse matrix. */ -NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename) +NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename) : matrix(nullptr) { /* * Enforce locale where decimal point is '.'. diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h similarity index 88% rename from src/parser/NonDeterministicSparseTransitionParser.h rename to src/parser/NondeterministicSparseTransitionParser.h index a0d9ea50a..209c0e7a0 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -17,9 +17,9 @@ namespace parser { * @brief Load a nondeterministic transition system from file and create a * sparse adjacency matrix whose entries represent the weights of the edges */ -class NonDeterministicSparseTransitionParser : public Parser { +class NondeterministicSparseTransitionParser : public Parser { public: - NonDeterministicSparseTransitionParser(std::string const &filename); + NondeterministicSparseTransitionParser(std::string const &filename); inline std::shared_ptr> getMatrix() const { return this->matrix; diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 3464c9710..4b1db5178 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -9,7 +9,7 @@ #define STORM_UTILITY_GRAPHANALYZER_H_ #include "src/models/AbstractDeterministicModel.h" -#include "src/models/AbstractNonDeterministicModel.h" +#include "src/models/AbstractNondeterministicModel.h" #include "src/exceptions/InvalidArgumentException.h" #include "log4cplus/logger.h" @@ -149,7 +149,7 @@ public: } template - static void performProb01Max(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { + static void performProb01Max(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); @@ -166,17 +166,47 @@ public: } template - static void performProb0A(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { + static void performProb0A(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { + // Check for valid parameter. + if (statesWithProbability0 == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); + } + + // Get the backwards transition relation from the model to ease the search. + storm::models::GraphTransitions backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false); + + // Add all psi states as the already satisfy the condition. + *statesWithProbability0 |= psiStates; + + // Initialize the stack used for the DFS with the states + std::vector stack; + stack.reserve(model.getNumberOfStates()); + psiStates.getList(stack); + // Perform the actual DFS. + while(!stack.empty()) { + uint_fast64_t currentState = stack.back(); + stack.pop_back(); + + for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + if (phiStates.get(*it) && !statesWithProbability0->get(*it)) { + statesWithProbability0->set(*it, true); + stack.push_back(*it); + } + } + } + + statesWithProbability0->complement(); } template - static void performProb1E(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { + static void performProb1E(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { } template - static void performProb01Min(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { + static void performProb01Min(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); @@ -193,12 +223,12 @@ public: } template - static void performProb0E(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { + static void performProb0E(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { } template - static void performProb1A(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { + static void performProb1A(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { // This result is a rough guess and does not compute all states with probability 1. // TODO: Check whether it makes sense to implement the precise but complicated algorithm here. *statesWithProbability1 = psiStates; diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp index 0dd6a4e3b..02302dc2a 100644 --- a/test/parser/ParseMdpTest.cpp +++ b/test/parser/ParseMdpTest.cpp @@ -8,12 +8,12 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/parser/NonDeterministicModelParser.h" +#include "src/parser/NondeterministicModelParser.h" #include "src/utility/IoUtility.h" TEST(ParseMdpTest, parseAndOutput) { - storm::parser::NonDeterministicModelParser* mdpParser = nullptr; - ASSERT_NO_THROW(mdpParser = new storm::parser::NonDeterministicModelParser( + storm::parser::NondeterministicModelParser* mdpParser = nullptr; + ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser( STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp index 6a20050dd..69d11cc37 100644 --- a/test/storage/SparseMatrixTest.cpp +++ b/test/storage/SparseMatrixTest.cpp @@ -80,7 +80,7 @@ TEST(SparseMatrixTest, Test) { int position_row[50] = { 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, /* first row empty, one full row ��������� 25 minus the diagonal entry */ + 2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */ 4, 4, /* one empty row, then first and last column */ 13, 13, 13, 13, /* a few empty rows, middle columns */ 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, @@ -288,9 +288,9 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) { ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - const std::vector rowP = ssm->getRowIndicationsPointer(); - const std::vector colP = ssm->getColumnIndicationsPointer(); - const std::vector valP = ssm->getStoragePointer(); + const std::vector rowP = ssm->getRowIndications(); + const std::vector colP = ssm->getColumnIndications(); + const std::vector valP = ssm->getStorage(); int target = -1; for (auto &coeff: tripletList) {