From 8a9d766c73b676121825f7d79f40453fedc829eb Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 12 Feb 2013 16:58:57 +0100 Subject: [PATCH] Changed input format for non-deterministic models to PRISMs output format. Added min/max capability to probabilistic operator without bounds. Implemented Prob0E. Added a simple MDP model to example suite. --- src/formula/ProbabilisticNoBoundOperator.h | 34 ++++- src/parser/NondeterministicModelParser.cpp | 2 +- ...NondeterministicSparseTransitionParser.cpp | 126 ++++++++---------- src/storm.cpp | 13 +- src/utility/GraphAnalyzer.h | 55 ++++++++ 5 files changed, 158 insertions(+), 72 deletions(-) diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h index c3ac9c248..40c812cf7 100644 --- a/src/formula/ProbabilisticNoBoundOperator.h +++ b/src/formula/ProbabilisticNoBoundOperator.h @@ -51,7 +51,7 @@ public: /*! * Empty constructor */ - ProbabilisticNoBoundOperator() : NoBoundOperator(nullptr) { + ProbabilisticNoBoundOperator() : NoBoundOperator(nullptr), optimalityOperator(false), minimumOperator(false) { // Intentionally left empty } @@ -60,7 +60,18 @@ public: * * @param pathFormula The child node. */ - ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) : NoBoundOperator(pathFormula) { + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) : NoBoundOperator(pathFormula), + optimalityOperator(false), minimumOperator(false) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param pathFormula The child node. + */ + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) : NoBoundOperator(pathFormula), + optimalityOperator(true), minimumOperator(minimumOperator) { // Intentionally left empty } @@ -68,11 +79,28 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "P = ? ["; + std::string result = "P"; + if (optimalityOperator) { + if (minimumOperator) { + result += "min"; + } else { + result += "max"; + } + } + result += "=? ["; result += this->getPathFormula().toString(); result += "]"; return result; } + +private: + // A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator + // over a nondeterministic model. + bool optimalityOperator; + + // In the case this operator is an optimizing operator, this flag indicates whether it is + // looking for the minimum or the maximum value. + bool minimumOperator; }; } /* namespace formula */ diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 036f0dc9b..87eb3cc57 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -5,7 +5,7 @@ * Author: Philipp Berger */ -#include "src/parser/NonDeterministicModelParser.h" +#include "src/parser/NondeterministicModelParser.h" #include #include diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index a17f48552..c5118eee4 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -70,14 +70,14 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ * Parse number of transitions. * We will not actually use this value, but we will compare it to the * number of transitions we count and issue a warning if this parsed - * vlaue is wrong. + * value is wrong. */ uint_fast64_t parsed_nonzero = strtol(buf, &buf, 10); /* * Read all transitions. */ - int_fast64_t source, target; + int_fast64_t source, target, choice, lastchoice = -1; int_fast64_t lastsource = -1; uint_fast64_t nonzero = 0; double val; @@ -85,54 +85,56 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ maxnode = 0; while (buf[0] != '\0') { /* - * Read source node. - * Check if current source node is larger than current maximum node id. - * Increase number of choices. - * Check if we have skipped any source node, i.e. if any node has no - * outgoing transitions. If so, increase nonzero (and - * parsed_nonzero). + * Read source state and choice. */ source = checked_strtol(buf, &buf); - if (source > maxnode) maxnode = source; - choices++; + + // Read the name of the nondeterministic choice. + choice = checked_strtol(buf, &buf); + + // Check if we encountered a state index that is bigger than all previously seen. + if (source > maxnode) { + maxnode = source; + } + + // If we have skipped some states, we need to reserve the space for the self-loop insertion + // in the second pass. if (source > lastsource + 1) { nonzero += source - lastsource - 1; choices += source - lastsource - 1; parsed_nonzero += source - lastsource - 1; + } else if (source != lastsource || choice != lastchoice) { + // If we have switched the source state or the nondeterministic choice, we need to + // reserve one row more. + ++choices; + } + + // Read target and check if we encountered a state index that is bigger than all previously + // seen. + target = checked_strtol(buf, &buf); + if (target > maxnode) { + maxnode = target; + } + + // Read value and check whether it's positive. + val = checked_strtod(buf, &buf); + if ((val < 0.0) || (val > 1.0)) { + LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\"."); + return 0; } + + lastchoice = choice; lastsource = source; - buf = trimWhitespaces(buf); // Skip to name of choice - buf += strcspn(buf, " \t\n\r"); // Skip name of choice. /* - * Read all targets for this choice. + * Increase number of non-zero values. */ - buf = trimWhitespaces(buf); - while (buf[0] == '*') { - buf++; - /* - * Read target node and transition value. - * Check if current target node is larger than current maximum node id. - * Check if the transition value is a valid probability. - */ - target = checked_strtol(buf, &buf); - if (target > maxnode) maxnode = target; - val = checked_strtod(buf, &buf); - if ((val < 0.0) || (val > 1.0)) { - LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\"."); - return 0; - } + nonzero++; - /* - * Increase number of non-zero values. - */ - nonzero++; - - /* - * Proceed to beginning of next line. - */ - buf = trimWhitespaces(buf); - } + /* + * Proceed to beginning of next line. + */ + buf = trimWhitespaces(buf); } /* @@ -219,9 +221,8 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s /* * Parse file content. */ - int_fast64_t source, target, lastsource = -1; - uint_fast64_t curRow = 0; - std::string choice; + int_fast64_t source, target, lastsource = -1, choice, lastchoice = -1; + uint_fast64_t curRow = -1; double val; bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); bool hadDeadlocks = false; @@ -231,11 +232,16 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s */ while (buf[0] != '\0') { /* - * Read source node and choice name. + * Read source state and choice. */ source = checked_strtol(buf, &buf); - buf = trimWhitespaces(buf); // Skip to name of choice - choice = std::string(buf, strcspn(buf, " \t\n\r")); + choice = checked_strtol(buf, &buf); + + // Increase line count if we have either finished reading the transitions of a certain state + // or we have finished reading one nondeterministic choice of a state. + if ((source != lastsource || choice != lastchoice)) { + ++curRow; + } /* * Check if we have skipped any source node, i.e. if any node has no @@ -247,7 +253,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s if (fixDeadlocks) { this->rowMapping->at(node) = curRow; 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."); } else { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); @@ -259,33 +265,19 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s */ this->rowMapping->at(source) = curRow; } - lastsource = source; - /* - * Skip name of choice. - */ - buf += strcspn(buf, " \t\n\r"); + // Read target and value and write it to the matrix. + target = checked_strtol(buf, &buf); + val = checked_strtod(buf, &buf); + this->matrix->addNextValue(curRow, target, val); + + lastsource = source; + lastchoice = choice; /* - * Read all targets for this choice. + * Proceed to beginning of next line in file and next row in matrix. */ buf = trimWhitespaces(buf); - while (buf[0] == '*') { - buf++; - /* - * Read target node and transition value. - * Put it into the matrix. - */ - target = checked_strtol(buf, &buf); - val = checked_strtod(buf, &buf); - this->matrix->addNextValue(curRow, target, val); - - /* - * Proceed to beginning of next line in file and next row in matrix. - */ - buf = trimWhitespaces(buf); - } - curRow++; } this->rowMapping->at(maxnode+1) = curRow; diff --git a/src/storm.cpp b/src/storm.cpp index 26fe8d15a..a8e839595 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -205,6 +205,10 @@ void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast6 delete mc; } +void testCheckingDice(storm::models::Mdp mdp) { + +} + /*! * Simple testing procedure. */ @@ -220,7 +224,14 @@ void testChecking() { // testCheckingCrowds(*dtmc); // testCheckingSynchronousLeader(*dtmc, 4); } - else std::cout << "Input is not DTMC" << std::endl; + else if (parser.getType() == storm::models::MDP) { + std::shared_ptr> mdp = parser.getModel>(); + mdp->printModelInformationToStream(std::cout); + + // testCheckingDice(*mdp); + } else { + std::cout << "Input is neither a DTMC nor an MDP." << std::endl; + } } /*! diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 4b1db5178..a05e3705d 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -224,7 +224,62 @@ public: template static void performProb0E(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."); + } + + std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); + std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + + // Get the backwards transition relation from the model to ease the search. + storm::models::GraphTransitions backwardTransitions(transitionMatrix, nondeterministicChoiceIndices, 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)) { + + // Check whether the predecessor has at least one successor in the current state + // set for every nondeterministic choice. + bool addToStatesWithProbability0 = true; + for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) { + bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; + for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(); ++colIt) { + if (statesWithProbability0->get(*colIt)) { + hasAtLeastOneSuccessorWithProbabilityGreater0 = true; + break; + } + } + if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { + addToStatesWithProbability0 = false; + break; + } + } + + // If we need to add the state, then actually add it and perform further search + // from the state. + if (addToStatesWithProbability0) { + statesWithProbability0->set(*it, true); + stack.push_back(*it); + } + } + } + } + + statesWithProbability0->complement(); } template