diff --git a/src/formula/AP.h b/src/formula/AP.h index 4b7d18011..990365ff0 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -38,18 +38,6 @@ public: this->ap = ap; } - /*! - * Constructor - * - * Creates a new atomic proposition leaf, with the label AP - * - * @param ap The string representing the atomic proposition - */ - AP(char* ap) { - //TODO: Does that really work? - this->ap = ap; - } - /*! * Destructor. * At this time, empty... @@ -90,7 +78,7 @@ public: * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkAP(this); + return modelChecker.checkAP(*this); } private: diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h new file mode 100644 index 000000000..58b679d8b --- /dev/null +++ b/src/formula/Formulas.h @@ -0,0 +1,23 @@ +/* + * Formulas.h + * + * Created on: 06.12.2012 + * Author: chris + */ + +#ifndef FORMULAS_H_ +#define FORMULAS_H_ + +#include "And.h" +#include "AP.h" +#include "BoundedUntil.h" +#include "Next.h" +#include "Not.h" +#include "Or.h" +#include "PCTLformula.h" +#include "PCTLPathFormula.h" +#include "PCTLStateFormula.h" +#include "ProbabilisticOperator.h" +#include "Until.h" + +#endif /* FORMULAS_H_ */ diff --git a/src/formula/Until.h b/src/formula/Until.h index f6bf62a98..1b492e68b 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -141,7 +141,7 @@ public: * @returns A vector indicating the probability that the formula holds for each state. */ virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkUntil(this); + return modelChecker.checkUntil(*this); } private: diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 83e29e38b..7923f592d 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -103,8 +103,8 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) { - return formula.check(this); + virtual mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) const { + return formula.check(*this); } /*! @@ -113,9 +113,9 @@ public: * @param formula The And formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkAnd(const mrmc::formula::And& formula) { - mrmc::storage::BitVector* result = check(formula.getLeft()); - mrmc::storage::BitVector* right = check(formula.getRight()); + virtual mrmc::storage::BitVector* checkAnd(const mrmc::formula::And& formula) const { + mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft()); + mrmc::storage::BitVector* right = checkStateFormula(formula.getRight()); (*result) &= (*right); delete right; return result; @@ -127,7 +127,12 @@ public: * @param formula The AP state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkAP(const mrmc::formula::AP& formula) { + virtual mrmc::storage::BitVector* checkAP(const mrmc::formula::AP& formula) const { + if (formula.getAP().compare("true") == 0) { + return new mrmc::storage::BitVector(model->getNumberOfStates(), 1); + } else if (formula.getAP().compare("false") == 0) { + return new mrmc::storage::BitVector(model->getNumberOfStates()); + } return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAP())); } @@ -137,8 +142,8 @@ public: * @param formula The Not state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkNot(const mrmc::formula::Not& formula) { - mrmc::storage::BitVector* result = check(formula.getChild()); + virtual mrmc::storage::BitVector* checkNot(const mrmc::formula::Not& formula) const { + mrmc::storage::BitVector* result = checkStateFormula(formula.getChild()); result->complement(); return result; } @@ -149,9 +154,9 @@ public: * @param formula The Or state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkOr(const mrmc::formula::Or& formula) { - mrmc::storage::BitVector* result = check(formula.getLeft()); - mrmc::storage::BitVector* right = check(formula.getRight()); + virtual mrmc::storage::BitVector* checkOr(const mrmc::formula::Or& formula) const { + mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft()); + mrmc::storage::BitVector* right = checkStateFormula(formula.getRight()); (*result) |= (*right); delete right; return result; @@ -163,7 +168,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula); + virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const = 0; /*! * The check method for a path formula; Will infer the actual type of formula and delegate it @@ -172,8 +177,8 @@ public: * @param formula The path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) { - return formula.check(this); + virtual std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) const { + return formula.check(*this); } /*! @@ -182,7 +187,7 @@ public: * @param formula The Bounded Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) = 0; + virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) const = 0; /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -190,7 +195,7 @@ public: * @param formula The Next path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkNext(const mrmc::formula::Next& formula) = 0; + virtual std::vector* checkNext(const mrmc::formula::Next& formula) const = 0; /*! * The check method for a path formula with an Until operator node as root in its formula tree @@ -198,7 +203,7 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkUntil(const mrmc::formula::Until& formula) = 0; + virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const = 0; private: mrmc::models::Dtmc* model; diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 0493cda1a..9d9c0aad2 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -11,6 +11,7 @@ #include "src/utility/vector.h" #include "src/models/dtmc.h" +#include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" #include "gmm/gmm_matrix.h" @@ -19,7 +20,7 @@ #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" -log4cplus::Logger logger; +extern log4cplus::Logger logger; namespace mrmc { @@ -28,31 +29,46 @@ namespace modelChecker { /* * A model checking engine that makes use of the gmm++ backend. */ -template -class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { +template +class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { public: - explicit GmmxxDtmcPrctlModelChecker(const mrmc::models::Dtmc* dtmc) : DtmcPrctlModelChecker(dtmc) { } + explicit GmmxxDtmcPrctlModelChecker(mrmc::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } virtual ~GmmxxDtmcPrctlModelChecker() { } - virtual std::vector* checkBoundedUntil(mrmc::formula::BoundedUntil& formula) { + virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const { + std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); + + mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); + Type lower = formula.getLowerBound(); + Type upper = formula.getUpperBound(); + for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { + if ((*probabilisticResult)[i] >= lower && (*probabilisticResult)[i] <= upper) result->set(i, true); + } + + delete probabilisticResult; + + return result; + } + + virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - mrmc::storage::BitVector* leftStates = this->check(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->check(formula.getRight()); + mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Copy the matrix before we make any changes. - mrmc::storage::SquareSparseMatrix* tmpMatrix(dtmc.getTransitionProbabilityMatrix()); + mrmc::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing((~leftStates & rightStates) | rightStates); + tmpMatrix.makeRowsAbsorbing((~*leftStates & *rightStates) | *rightStates); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix(); // Create the vector with which to multiply. - std::vector* result = new st::vector(dtmc.getNumberOfStates()); - mrmc::utility::setVectorValue(result, *rightStates, 1); + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + mrmc::utility::setVectorValues(result, *rightStates, static_cast(1.0)); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { @@ -66,22 +82,22 @@ public: return result; } - virtual std::vector* checkNext(const mrmc::formula::Next& formula) { + virtual std::vector* checkNext(const mrmc::formula::Next& formula) const { // First, we need to compute the states that satisfy the sub-formula of the next-formula. - mrmc::storage::BitVector* nextStates = this->check(formula.getChild()); + mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = dtmc.getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); + gmm::csr_matrix* gmmxxMatrix = this->getModel().getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); // Create the vector with which to multiply and initialize it correctly. - std::vector x(dtmc.getNumberOfStates()); - mrmc::utility::setVectorValue(x, nextStates, 1); + std::vector x(this->getModel().getNumberOfStates()); + mrmc::utility::setVectorValues(&x, *nextStates, static_cast(1.0)); // Delete not needed next states bit vector. delete nextStates; // Create resulting vector. - std::vector* result = new std::vector(dtmc.getNumberOfStates()); + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); // Perform the actual computation. gmm::mult(*gmmxxMatrix, x, *result); @@ -91,17 +107,17 @@ public: return result; } - virtual std::vector* checkUntil(const mrmc::formula::Until& formula) { + virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - mrmc::storage::BitVector* leftStates = this->check(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->check(formula.getRight()); + mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - mrmc::storage::BitVector notExistsPhiUntilPsiStates(dtmc.getNumberOfStates()); - mrmc::storage::BitVector alwaysPhiUntilPsiStates(dtmc.getNumberOfStates()); - mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(dtmc, *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); - notExistsPhiUntilPsiStates->complement(); + mrmc::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); + mrmc::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); + mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + notExistsPhiUntilPsiStates.complement(); delete leftStates; delete rightStates; @@ -109,12 +125,15 @@ public: LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states."); LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states."); mrmc::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); - LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " maybe states."); + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Create resulting vector and set values accordingly. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); // Only try to solve system if there are states for which the probability is unknown. if (maybeStates.getNumberOfSetBits() > 0) { // Now we can eliminate the rows and columns from the original transition probability matrix. - mrmc::storage::SquareSparseMatrix* submatrix = dtmc.getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + mrmc::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); // Converting the matrix to the form needed for the equation system. That is, we go from // x = A*x + b to (I-A)x = b. submatrix->convertToEquationSystem(); @@ -125,12 +144,12 @@ public: // Initialize the x vector with 0.5 for each element. This is the initial guess for // the iterative solvers. It should be safe as for all 'maybe' states we know that the // probability is strictly larger than 0. - std::vector* x = new std::vector(maybeStates.getNumberOfSetBits(), 0.5); + std::vector x(maybeStates.getNumberOfSetBits(), Type(0.5)); // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. std::vector b(maybeStates.getNumberOfSetBits()); - dtmc.getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); + this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); // Set up the precondition of the iterative solver. gmm::ilu_precond> P(*gmmxxMatrix); @@ -139,24 +158,26 @@ public: gmm::iteration iter(0.000001); // Now do the actual solving. - LOG4CPLUS_INFO(logger, "Starting iterations..."); + LOG4CPLUS_INFO(logger, "Starting iterative solver."); gmm::bicgstab(*gmmxxMatrix, x, b, P, iter); - LOG4CPLUS_INFO(logger, "Done with iterations."); + LOG4CPLUS_INFO(logger, "Iterative solver converged."); - // Create resulting vector and set values accordingly. - std::vector* result = new std::vector(dtmc.getNumberOfStates()); - mrmc::utility::setVectorValues>(result, maybeStates, x); + // Set values of resulting vector according to result. + mrmc::utility::setVectorValues(result, maybeStates, x); - // Delete temporary matrix and return result. - delete x; + // Delete temporary matrix. delete gmmxxMatrix; } - mrmc::utility::setVectorValue>(result, notExistsPhiUntilPsiStates, 0); - mrmc::utility::setVectorValue>(result, alwaysPhiUntilPsiStates, 1); + mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, static_cast(0)); + mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, static_cast(1.0)); return result; } }; +} //namespace modelChecker + +} //namespace mrmc + #endif /* GMMXXDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/mrmc.cpp b/src/mrmc.cpp index baa2f20d5..a63ea0f4e 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -21,11 +21,13 @@ #include "src/models/Dtmc.h" #include "src/storage/SquareSparseMatrix.h" #include "src/models/AtomicPropositionsLabeling.h" +#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" #include "src/parser/readLabFile.h" #include "src/parser/readTraFile.h" #include "src/parser/readPrctlFile.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/settings.h" +#include "src/formula/Formulas.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -102,6 +104,16 @@ int main(const int argc, const char* argv[]) { dtmc.printModelInformationToStream(std::cout); + // Uncomment this if you want to see the first model checking procedure in action. :) + /* + mrmc::modelChecker::GmmxxDtmcPrctlModelChecker mc(dtmc); + mrmc::formula::AP* trueFormula = new mrmc::formula::AP(std::string("true")); + mrmc::formula::AP* ap = new mrmc::formula::AP(std::string("observe0Greater1")); + mrmc::formula::Until* until = new mrmc::formula::Until(trueFormula, ap); + mc.checkPathFormula(*until); + delete until; + */ + if (s != nullptr) { delete s; } diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index a81302b1c..4e433816a 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -71,8 +71,8 @@ public: * @param ssm A reference to the matrix to be copied. */ SquareSparseMatrix(const SquareSparseMatrix &ssm) - : internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow), - rowCount(ssm.rowCount), nonZeroEntryCount(ssm.nonZeroEntryCount) { + : rowCount(ssm.rowCount), nonZeroEntryCount(ssm.nonZeroEntryCount), + internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow) { LOG4CPLUS_WARN(logger, "Invoking copy constructor."); // Check whether copying the matrix is safe. if (!ssm.hasError()) { @@ -454,7 +454,7 @@ public: * Checks whether the internal state of the matrix signals an error. * @return True iff the internal state of the matrix signals an error. */ - bool hasError() { + bool hasError() const { return (internalStatus == MatrixStatus::Error); } @@ -663,15 +663,16 @@ public: /*! * This function makes the rows given by the bit vector absorbing. + * @param rows A bit vector indicating which rows to make absorbing. + * @return True iff the operation was successful. */ bool makeRowsAbsorbing(const mrmc::storage::BitVector rows) { + bool result = true; for (auto row : rows) { - makeRowAbsorbing(row); + result &= makeRowAbsorbing(row); } - //FIXME: Had no return value; as I compile with -Werror ATM, build did not work so I added: - return false; - //(Thomas Heinemann, 06.12.2012) + return result; } /*! @@ -733,7 +734,7 @@ public: void getConstrainedRowCountVector(const mrmc::storage::BitVector& rowConstraint, const mrmc::storage::BitVector& columnConstraint, std::vector* resultVector) { uint_fast64_t currentRowCount = 0; for (auto row : rowConstraint) { - resultVector[currentRowCount++] = getConstrainedRowSum(row, columnConstraint); + (*resultVector)[currentRowCount++] = getConstrainedRowSum(row, columnConstraint); } } diff --git a/src/utility/vector.h b/src/utility/vector.h index 393151745..eff5f02b9 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -12,18 +12,18 @@ namespace mrmc { namespace utility { -template -void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& positions, std::vector* values) { +template +void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& positions, const std::vector values) { uint_fast64_t oldPosition = 0; for (auto position : positions) { - vector[position] = values[oldPosition++]; + (*vector)[position] = values[oldPosition++]; } } -template -void setVectorValue(std::vector* vector, const mrmc::storage::BitVector& positions, T value) { +template +void setVectorValues(std::vector* vector, const mrmc::storage::BitVector& positions, T value) { for (auto position : positions) { - vector[position] = value; + (*vector)[position] = value; } }