sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Moved model checking of DTMCs to superclass. Now, each DTMC model checker only needs to implement matrix-vector multiplication and linear equation solving to be able to fully model check DTMCs. Added subset/disjoint functionality to bit vector. Changed tests for MDP and DTMC model checking a bit.

main
dehnert 12 years ago
parent
4bcb26ab96
commit
34b85b956e
9 changed files with 648 additions and 603 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 79
      src/modelchecker/AbstractModelChecker.h
  2. 334
      src/modelchecker/DtmcPrctlModelChecker.h
  3. 196
      src/modelchecker/EigenDtmcPrctlModelChecker.h
  4. 354
      src/modelchecker/GmmxxDtmcPrctlModelChecker.h
  5. 17
      src/storage/BitVector.h
  6. 3
      src/utility/ConstTemplates.h
  7. 164
      test/functional/EigenDtmcPrctModelCheckerTest.cpp
  8. 20
      test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
  9. 36
      test/functional/GmmxxMdpPrctModelCheckerTest.cpp

79
src/modelchecker/AbstractModelChecker.h
View File

@ -71,6 +71,85 @@ public:
return nullptr; return nullptr;
} }
/*!
* Checks the given state formula on the DTMC and prints the result (true/false) for all initial
* states.
* @param stateFormula The formula to be checked.
*/
void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
storm::storage::BitVector* result = nullptr;
try {
result = stateFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : model.getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
}
delete result;
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
if (result != nullptr) {
delete result;
}
}
std::cout << std::endl;
storm::utility::printSeparationLine(std::cout);
}
/*!
* Checks the given operator (with no bound) on the DTMC and prints the result
* (probability/rewards) for all initial states.
* @param noBoundFormula The formula to be checked.
*/
void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const {
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
std::vector<Type>* result = nullptr;
try {
result = noBoundFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : *model.getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
}
delete result;
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
if (result != nullptr) {
delete result;
}
}
std::cout << std::endl;
storm::utility::printSeparationLine(std::cout);
}
/*!
* The check method for a formula with an AP node as root in its formula tree
*
* @param formula The Ap state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& formula) const {
if (formula.getAp().compare("true") == 0) {
return new storm::storage::BitVector(model.getNumberOfStates(), true);
} else if (formula.getAp().compare("false") == 0) {
return new storm::storage::BitVector(model.getNumberOfStates());
}
if (!model.hasAtomicProposition(formula.getAp())) {
LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid.");
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
}
return new storm::storage::BitVector(*model.getLabeledStates(formula.getAp()));
}
/*! /*!
* The check method for a state formula with an And node as root in its formula tree * The check method for a state formula with an And node as root in its formula tree
* *

334
src/modelchecker/DtmcPrctlModelChecker.h
View File

@ -8,6 +8,8 @@
#ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ #ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_
#define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ #define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_
#include <vector>
#include "src/formula/Formulas.h" #include "src/formula/Formulas.h"
#include "src/utility/Vector.h" #include "src/utility/Vector.h"
#include "src/storage/SparseMatrix.h" #include "src/storage/SparseMatrix.h"
@ -16,12 +18,11 @@
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidPropertyException.h"
#include "src/utility/Vector.h" #include "src/utility/Vector.h"
#include "src/utility/GraphAnalyzer.h"
#include "src/modelchecker/AbstractModelChecker.h" #include "src/modelchecker/AbstractModelChecker.h"
#include <vector>
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
namespace storm { namespace storm {
@ -38,8 +39,7 @@ namespace modelChecker {
* @attention This class is abstract. * @attention This class is abstract.
*/ */
template<class Type> template<class Type>
class DtmcPrctlModelChecker :
public AbstractModelChecker<Type> {
class DtmcPrctlModelChecker : public AbstractModelChecker<Type> {
public: public:
/*! /*!
@ -47,8 +47,7 @@ public:
* *
* @param model The dtmc model which is checked. * @param model The dtmc model which is checked.
*/ */
explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model)
: AbstractModelChecker<Type>(model) {
explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model) : AbstractModelChecker<Type>(model) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -58,6 +57,7 @@ public:
* @param modelChecker The model checker that is copied. * @param modelChecker The model checker that is copied.
*/ */
explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) : AbstractModelChecker<Type>(modelChecker) { explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) : AbstractModelChecker<Type>(modelChecker) {
// Intentionally left empty.
} }
/*! /*!
@ -74,93 +74,6 @@ public:
return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>(); return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>();
} }
/*!
* Sets the DTMC model which is checked
* @param model
*/
void setModel(storm::models::Dtmc<Type>& model) {
AbstractModelChecker<Type>::setModel(model);
}
/*!
* The check method for a formula with an AP node as root in its formula tree
*
* @param formula The Ap state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& formula) const {
if (formula.getAp().compare("true") == 0) {
return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true);
} else if (formula.getAp().compare("false") == 0) {
return new storm::storage::BitVector(this->getModel().getNumberOfStates());
}
if (!this->getModel().hasAtomicProposition(formula.getAp())) {
LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid.");
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
}
return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp()));
}
/*!
* Checks the given state formula on the DTMC and prints the result (true/false) for all initial
* states.
* @param stateFormula The formula to be checked.
*/
void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
storm::storage::BitVector* result = nullptr;
try {
result = stateFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : *this->getModel().getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
}
delete result;
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
if (result != nullptr) {
delete result;
}
}
std::cout << std::endl;
storm::utility::printSeparationLine(std::cout);
}
/*!
* Checks the given operator (with no bound) on the DTMC and prints the result
* (probability/rewards) for all initial states.
* @param noBoundFormula The formula to be checked.
*/
void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const {
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
std::vector<Type>* result = nullptr;
try {
result = noBoundFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : *this->getModel().getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
}
delete result;
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
if (result != nullptr) {
delete result;
}
}
std::cout << std::endl;
storm::utility::printSeparationLine(std::cout);
}
/*! /*!
* The check method for a state formula with a probabilistic operator node without bounds as root * The check method for a state formula with a probabilistic operator node without bounds as root
* in its formula tree * in its formula tree
@ -182,7 +95,31 @@ public:
* @param formula The Bounded Until path formula to check * @param formula The Bounded Until path formula to check
* @returns for each state the probability that the path formula holds. * @returns for each state the probability that the path formula holds.
*/ */
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const = 0;
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
storm::storage::BitVector* rightStates = formula.getRight().check(*this);
// Copy the matrix before we make any changes.
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
// Delete obsolete intermediates.
delete leftStates;
delete rightStates;
// Create the vector with which to multiply.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
// Perform the matrix vector multiplication as often as required by the formula bound.
this->performMatrixVectorMultiplication(tmpMatrix, &result, nullptr, formula.getBound());
// Return result.
return result;
}
/*! /*!
* The check method for a path formula with a Next operator node as root in its formula tree * The check method for a path formula with a Next operator node as root in its formula tree
@ -190,7 +127,23 @@ public:
* @param formula The Next path formula to check * @param formula The Next path formula to check
* @returns for each state the probability that the path formula holds. * @returns for each state the probability that the path formula holds.
*/ */
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const = 0;
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the child formula of the next-formula.
storm::storage::BitVector* nextStates = formula.getChild().check(*this);
// Create the vector with which to multiply and initialize it correctly.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne<Type>());
// Delete obsolete intermediate.
delete nextStates;
// Perform one single matrix-vector multiplication.
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result);
// Return result.
return result;
}
/*! /*!
* The check method for a path formula with a Bounded Eventually operator node as root in its * The check method for a path formula with a Bounded Eventually operator node as root in its
@ -239,7 +192,68 @@ public:
* @param formula The Until path formula to check * @param formula The Until path formula to check
* @returns for each state the probability that the path formula holds. * @returns for each state the probability that the path formula holds.
*/ */
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const = 0;
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
storm::storage::BitVector* rightStates = formula.getRight().check(*this);
// 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.
storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
// Delete intermediate results that are obsolete now.
delete leftStates;
delete rightStates;
// Perform some logging.
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Only try to solve system if there are states for which the probability is unknown.
uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
if (maybeStatesSetBitCount > 0 && !qualitative) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix->convertToEquationSystem();
// 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<Type>* x = new std::vector<Type>(maybeStatesSetBitCount, 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<Type> b(maybeStatesSetBitCount);
this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b);
this->solveEquationSystem(*submatrix, &x, b);
// Delete the created submatrix.
delete submatrix;
// Set values of resulting vector according to result.
storm::utility::setVectorValues<Type>(result, maybeStates, *x);
} else if (qualitative) {
// If we only need a qualitative result, we can safely assume that the results will only be compared to
// bounds which are either 0 or 1. Setting the value to 0.5 is thus safe.
storm::utility::setVectorValues<Type>(result, maybeStates, Type(0.5));
}
// Set values of resulting vector that are known exactly.
storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
return result;
}
/*! /*!
* The check method for a path formula with an Instantaneous Reward operator node as root in its * The check method for a path formula with an Instantaneous Reward operator node as root in its
@ -248,7 +262,22 @@ public:
* @param formula The Instantaneous Reward formula to check * @param formula The Instantaneous Reward formula to check
* @returns for each state the reward that the instantaneous reward yields * @returns for each state the reward that the instantaneous reward yields
*/ */
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const = 0;
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const {
// Only compute the result if the model has a state-based reward model.
if (!this->getModel().hasStateRewards()) {
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula.";
}
// Initialize result to state rewards of the model.
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result, nullptr, formula.getBound());
// Return result.
return result;
}
/*! /*!
* The check method for a path formula with a Cumulative Reward operator node as root in its * The check method for a path formula with a Cumulative Reward operator node as root in its
@ -257,7 +286,32 @@ public:
* @param formula The Cumulative Reward formula to check * @param formula The Cumulative Reward formula to check
* @returns for each state the reward that the cumulative reward yields * @returns for each state the reward that the cumulative reward yields
*/ */
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const = 0;
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const {
// Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
}
// Compute the reward vector to add in each step based on the available reward models.
std::vector<Type>* totalRewardVector = nullptr;
if (this->getModel().hasTransitionRewards()) {
totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
if (this->getModel().hasStateRewards()) {
gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
}
} else {
totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
}
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result, totalRewardVector, formula.getBound());
// Delete temporary variables and return result.
delete totalRewardVector;
return result;
}
/*! /*!
* The check method for a path formula with a Reachability Reward operator node as root in its * The check method for a path formula with a Reachability Reward operator node as root in its
@ -266,10 +320,90 @@ public:
* @param formula The Reachbility Reward formula to check * @param formula The Reachbility Reward formula to check
* @returns for each state the reward that the reachability reward yields * @returns for each state the reward that the reachability reward yields
*/ */
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const = 0;
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const {
// Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
}
// Determine the states for which the target predicate holds.
storm::storage::BitVector* targetStates = formula.getChild().check(*this);
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates);
infinityStates.complement();
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Check whether there are states for which we have to compute the result.
storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
if (maybeStatesSetBitCount > 0) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix->convertToEquationSystem();
// Initialize the x vector with 1 for each element. This is the initial guess for
// the iterative solvers.
std::vector<Type>* x = new std::vector<Type>(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
// Prepare the right-hand side of the equation system.
std::vector<Type>* b = new std::vector<Type>(maybeStatesSetBitCount);
if (this->getModel().hasTransitionRewards()) {
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
// of the transition probability matrix and the transition reward matrix.
std::vector<Type>* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector);
delete pointwiseProductRowSumVector;
if (this->getModel().hasStateRewards()) {
// If a state-based reward model is also available, we need to add this vector
// as well. As the state reward vector contains entries not just for the states
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStatesSetBitCount);
storm::utility::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
gmm::add(*subStateRewards, *b);
delete subStateRewards;
}
} else {
// If only a state-based reward model is available, we take this vector as the
// right-hand side. As the state reward vector contains entries not just for the
// states that we still consider (i.e. maybeStates), we need to extract these values
// first.
storm::utility::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector());
}
this->solveEquationSystem(*submatrix, &x, *b);
// Set values of resulting vector according to result.
storm::utility::setVectorValues<Type>(result, maybeStates, *x);
// Delete temporary matrix and right-hand side.
delete submatrix;
delete b;
}
// Set values of resulting vector that are known exactly.
storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>());
storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
// Delete temporary storages and return result.
delete targetStates;
return result;
}
private: private:
// storm::models::Dtmc<Type>& model;
virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const = 0;
virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>& b) const = 0;
}; };
} //namespace modelChecker } //namespace modelChecker

196
src/modelchecker/EigenDtmcPrctlModelChecker.h
View File

@ -38,164 +38,92 @@ namespace modelChecker {
template <class Type> template <class Type>
class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> { class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
public:
explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) { }
virtual ~EigenDtmcPrctlModelChecker() { }
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft());
storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
// Copy the matrix before we make any changes.
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates);
// Transform the transition probability matrix to the eigen format to use its arithmetic.
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(tmpMatrix);
// Create the vector with which to multiply.
uint_fast64_t stateCount = this->getModel().getNumberOfStates();
typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
typedef Eigen::Map<VectorType> MapType;
std::vector<Type>* result = new std::vector<Type>(stateCount);
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
Type *p = &((*result)[0]); // get the address storing the data for result
MapType vectorMap(p, result->size()); // vectorMap shares data
typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
typedef Eigen::Map<VectorType> MapType;
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
for (uint_fast64_t i = 0, bound = formula.getBound(); i < bound; ++i) {
vectorMap = (*eigenMatrix) * vectorMap;
public:
explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) {
// Intentionally left empty.
} }
// Delete intermediate results.
delete leftStates;
delete rightStates;
delete eigenMatrix;
return result;
virtual ~EigenDtmcPrctlModelChecker() {
// Intentionally left empty.
} }
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula) const {
// First, we need to compute the states that satisfy the sub-formula of the next-formula.
storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
private:
virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>* summand, uint_fast64_t repetitions = 1) const {
// Transform the transition probability matrix to the eigen format to use its arithmetic. // Transform the transition probability matrix to the eigen format to use its arithmetic.
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(this->getModel().getTransitionProbabilityMatrix());
// Create the vector with which to multiply and initialize it correctly.
std::vector<Type> x(this->getModel().getNumberOfStates());
storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne<Type>());
// Delete not needed next states bit vector.
delete nextStates;
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(matrix);
typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
typedef Eigen::Map<VectorType> MapType;
Type* p = &((**vector)[0]); // get the address storing the data for result
MapType vectorMap(p, (*vector)->size()); // vectorMap shares data
Type *px = &(x[0]); // get the address storing the data for x
MapType vectorX(px, x.size()); // vectorX shares data
p = &((*summand)[0]);
MapType summandMap(p, summand->size());
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Now perform matrix-vector multiplication as long as we meet the bound.
std::vector<Type>* swap = nullptr;
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
for (uint_fast64_t i = 0; i < repetitions; ++i) {
vectorMap = (*eigenMatrix) * (vectorMap);
// Type *pr = &((*result)[0]); // get the address storing the data for result
MapType vectorResult(px, result->size()); // vectorResult shares data
// Perform the actual computation.
vectorResult = (*eigenMatrix) * vectorX;
// Delete temporary matrix and return result.
// If requested, add an offset to the current result vector.
if (summand != nullptr) {
vectorMap = vectorMap + summandMap;
}
}
delete eigenMatrix; delete eigenMatrix;
return result;
} }
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft());
storm::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.
storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
delete leftStates;
delete rightStates;
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector and set values accordingly.
uint_fast64_t stateCount = this->getModel().getNumberOfStates();
std::vector<Type>* result = new std::vector<Type>(stateCount);
// Only try to solve system if there are states for which the probability is unknown.
if (maybeStates.getNumberOfSetBits() > 0) {
typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
typedef Eigen::Map<VectorType> MapType;
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<double>* 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();
/*!
* Solves the linear equation system Ax=b with the given parameters.
*
* @param A The matrix A specifying the coefficients of the linear equations.
* @param x The vector x for which to solve the equations. The initial value of the elements of
* this vector are used as the initial guess and might thus influence performance and convergence.
* @param b The vector b specifying the values on the right-hand-sides of the equations.
* @return The solution of the system of linear equations in form of the elements of the vector
* x.
*/
virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>& b) const {
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::instance();
// Transform the submatric matrix to the eigen format to use its solvers // Transform the submatric matrix to the eigen format to use its solvers
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenSubMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix<Type>(submatrix);
delete submatrix;
// 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<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5));
// Map for x
Type *px = &(x[0]); // get the address storing the data for x
MapType vectorX(px, x.size()); // vectorX shares data
// 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<double> b(maybeStates.getNumberOfSetBits());
Type *pb = &(b[0]); // get the address storing the data for b
MapType vectorB(pb, b.size()); // vectorB shares data
this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &x);
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix<Type>(matrix);
Eigen::BiCGSTAB<Eigen::SparseMatrix<Type, 1, int_fast32_t>> solver; Eigen::BiCGSTAB<Eigen::SparseMatrix<Type, 1, int_fast32_t>> solver;
solver.compute(*eigenSubMatrix);
solver.compute(*eigenMatrix);
if(solver.info()!= Eigen::ComputationInfo::Success) { if(solver.info()!= Eigen::ComputationInfo::Success) {
// decomposition failed // decomposition failed
LOG4CPLUS_ERROR(logger, "Decomposition of Submatrix failed!");
LOG4CPLUS_ERROR(logger, "Decomposition of matrix failed!");
} }
solver.setMaxIterations(s->get<unsigned>("maxiter"));
solver.setTolerance(s->get<double>("precision"));
// Now do the actual solving.
LOG4CPLUS_INFO(logger, "Starting iterative solver.");
std::cout << matrix.toString(nullptr) << std::endl;
std::cout << **vector << std::endl;
std::cout << b << std::endl;
solver.setTolerance(0.000001);
std::cout << *eigenMatrix << std::endl;
// Map for x
Type *px = &((**vector)[0]); // get the address storing the data for x
MapType vectorX(px, (*vector)->size()); // vectorX shares data
Type *pb = &(b[0]); // get the address storing the data for b
MapType vectorB(pb, b.size()); // vectorB shares data
vectorX = solver.solveWithGuess(vectorB, vectorX); vectorX = solver.solveWithGuess(vectorB, vectorX);
std::cout << **vector << std::endl;
if(solver.info() == Eigen::ComputationInfo::InvalidInput) { if(solver.info() == Eigen::ComputationInfo::InvalidInput) {
// solving failed // solving failed
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput"); LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput");
} else if(solver.info() == Eigen::ComputationInfo::NoConvergence) { } else if(solver.info() == Eigen::ComputationInfo::NoConvergence) {
// NoConvergence // NoConvergence
throw storm::exceptions::NoConvergenceException("Solving of Submatrix with Eigen failed", solver.iterations(), solver.maxIterations());
throw storm::exceptions::NoConvergenceException() << "Failed to converge within " << solver.iterations() << " out of a maximum of " << solver.maxIterations() << " iterations.";
} else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) { } else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) {
// NumericalIssue // NumericalIssue
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue");
@ -204,17 +132,7 @@ public:
LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success"); LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success");
} }
// Set values of resulting vector according to result.
storm::utility::setVectorValues<Type>(result, maybeStates, x);
// Delete temporary matrix.
delete eigenSubMatrix;
}
storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
return result;
delete eigenMatrix;
} }
}; };

354
src/modelchecker/GmmxxDtmcPrctlModelChecker.h
View File

@ -12,7 +12,6 @@
#include "src/models/Dtmc.h" #include "src/models/Dtmc.h"
#include "src/modelchecker/DtmcPrctlModelChecker.h" #include "src/modelchecker/DtmcPrctlModelChecker.h"
#include "src/utility/GraphAnalyzer.h"
#include "src/utility/Vector.h" #include "src/utility/Vector.h"
#include "src/utility/ConstTemplates.h" #include "src/utility/ConstTemplates.h"
#include "src/utility/Settings.h" #include "src/utility/Settings.h"
@ -36,300 +35,15 @@ namespace modelChecker {
* A model checking engine that makes use of the gmm++ backend. * A model checking engine that makes use of the gmm++ backend.
*/ */
template <class Type> template <class Type>
class GmmxxDtmcPrctlModelChecker
: public DtmcPrctlModelChecker<Type> {
class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
public: public:
explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc)
: DtmcPrctlModelChecker<Type>(dtmc) {
explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) {
// Intentionally left empty. // Intentionally left empty.
} }
virtual ~GmmxxDtmcPrctlModelChecker() { }
virtual ~GmmxxDtmcPrctlModelChecker() {
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
storm::storage::BitVector* rightStates = formula.getRight().check(*this);
// Copy the matrix before we make any changes.
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(tmpMatrix);
// Create the vector with which to multiply.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
std::vector<Type>* swap = nullptr;
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
gmm::mult(*gmmxxMatrix, *result, *tmpResult);
swap = tmpResult;
tmpResult = result;
result = swap;
}
delete tmpResult;
// Delete intermediate results and return result.
delete gmmxxMatrix;
delete leftStates;
delete rightStates;
return result;
}
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formula of the next-formula.
storm::storage::BitVector* nextStates = formula.getChild().check(*this);
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
// Create the vector with which to multiply and initialize it correctly.
std::vector<Type> x(this->getModel().getNumberOfStates());
storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne<Type>());
// Delete obsolete sub-result.
delete nextStates;
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Perform the actual computation, namely matrix-vector multiplication.
gmm::mult(*gmmxxMatrix, x, *result);
// Delete temporary matrix and return result.
delete gmmxxMatrix;
return result;
}
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
storm::storage::BitVector* rightStates = formula.getRight().check(*this);
// 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.
storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
// Delete sub-results that are obsolete now.
delete leftStates;
delete rightStates;
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Only try to solve system if there are states for which the probability is unknown.
uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits();
if (mayBeStatesSetBitCount > 0 && !qualitative) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix->convertToEquationSystem();
// Transform the submatrix to the gmm++ format to use its solvers.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix);
delete submatrix;
// 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<Type> x(mayBeStatesSetBitCount, 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<Type> b(mayBeStatesSetBitCount);
this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b);
// Solve the corresponding system of linear equations.
this->solveLinearEquationSystem(*gmmxxMatrix, x, b);
// Set values of resulting vector according to result.
storm::utility::setVectorValues<Type>(result, maybeStates, x);
// Delete temporary matrix.
delete gmmxxMatrix;
} else if (qualitative) {
// If we only need a qualitative result, we can safely assume that the results will only be compared to
// bounds which are either 0 or 1. Setting the value to 0.5 is thus safe.
storm::utility::setVectorValues<Type>(result, maybeStates, Type(0.5));
}
// Set values of resulting vector that are known exactly.
storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
return result;
}
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const {
// Only compute the result if the model has a state-based reward model.
if (!this->getModel().hasStateRewards()) {
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula.";
}
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
// Initialize result to state rewards of the model.
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
std::vector<Type>* swap = nullptr;
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
gmm::mult(*gmmxxMatrix, *result, *tmpResult);
swap = tmpResult;
tmpResult = result;
result = swap;
}
// Delete temporary variables and return result.
delete tmpResult;
delete gmmxxMatrix;
return result;
}
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const {
// Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
}
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
// Compute the reward vector to add in each step based on the available reward models.
std::vector<Type>* totalRewardVector = nullptr;
if (this->getModel().hasTransitionRewards()) {
totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
if (this->getModel().hasStateRewards()) {
gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
}
} else {
totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
}
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
std::vector<Type>* swap = nullptr;
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
gmm::mult(*gmmxxMatrix, *result, *tmpResult);
swap = tmpResult;
tmpResult = result;
result = swap;
// Add the reward vector to the result.
gmm::add(*totalRewardVector, *result);
}
// Delete temporary variables and return result.
delete tmpResult;
delete gmmxxMatrix;
delete totalRewardVector;
return result;
}
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const {
// Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
}
// Determine the states for which the target predicate holds.
storm::storage::BitVector* targetStates = formula.getChild().check(*this);
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates);
infinityStates.complement();
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Check whether there are states for which we have to compute the result.
storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
if (maybeStatesSetBitCount > 0) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix->convertToEquationSystem();
// Transform the submatrix to the gmm++ format to use its solvers.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix);
delete submatrix;
// Initialize the x vector with 1 for each element. This is the initial guess for
// the iterative solvers.
std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
// Prepare the right-hand side of the equation system.
std::vector<Type>* b = new std::vector<Type>(maybeStatesSetBitCount);
if (this->getModel().hasTransitionRewards()) {
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
// of the transition probability matrix and the transition reward matrix.
std::vector<Type>* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector);
delete pointwiseProductRowSumVector;
if (this->getModel().hasStateRewards()) {
// If a state-based reward model is also available, we need to add this vector
// as well. As the state reward vector contains entries not just for the states
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStatesSetBitCount);
storm::utility::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
gmm::add(*subStateRewards, *b);
delete subStateRewards;
}
} else {
// If only a state-based reward model is available, we take this vector as the
// right-hand side. As the state reward vector contains entries not just for the
// states that we still consider (i.e. maybeStates), we need to extract these values
// first.
storm::utility::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector());
}
// Solve the corresponding system of linear equations.
this->solveLinearEquationSystem(*gmmxxMatrix, x, *b);
// Set values of resulting vector according to result.
storm::utility::setVectorValues<Type>(result, maybeStates, x);
// Delete temporary matrix and right-hand side.
delete gmmxxMatrix;
delete b;
}
// Set values of resulting vector that are known exactly.
storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>());
storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
// Delete temporary storages and return result.
delete targetStates;
return result;
} }
/*! /*!
@ -337,7 +51,7 @@ public:
* @return The name of this module. * @return The name of this module.
*/ */
static std::string getModuleName() { static std::string getModuleName() {
return "gmm++det";
return "gmm++";
} }
/*! /*!
@ -381,6 +95,29 @@ public:
} }
private: private:
virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>* summand, uint_fast64_t repetitions = 1) const {
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
// Now perform matrix-vector multiplication as long as we meet the bound.
std::vector<Type>* swap = nullptr;
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
for (uint_fast64_t i = 0; i < repetitions; ++i) {
gmm::mult(*gmmxxMatrix, **vector, *tmpResult);
swap = tmpResult;
tmpResult = *vector;
*vector = swap;
// If requested, add an offset to the current result vector.
if (summand != nullptr) {
gmm::add(*summand, **vector);
}
}
delete tmpResult;
delete gmmxxMatrix;
}
/*! /*!
* Solves the linear equation system Ax=b with the given parameters. * Solves the linear equation system Ax=b with the given parameters.
* *
@ -391,10 +128,13 @@ private:
* @return The solution of the system of linear equations in form of the elements of the vector * @return The solution of the system of linear equations in form of the elements of the vector
* x. * x.
*/ */
void solveLinearEquationSystem(gmm::csr_matrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const {
virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>& b) const {
// Get the settings object to customize linear solving. // Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::instance(); storm::settings::Settings* s = storm::settings::instance();
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
gmm::csr_matrix<Type>* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
// Prepare an iteration object that determines the accuracy, maximum number of iterations // Prepare an iteration object that determines the accuracy, maximum number of iterations
// and the like. // and the like.
gmm::iteration iter(s->get<double>("precision"), 0, s->get<unsigned>("maxiter")); gmm::iteration iter(s->get<double>("precision"), 0, s->get<unsigned>("maxiter"));
@ -415,13 +155,13 @@ private:
if (s->getString("lemethod") == "bicgstab") { if (s->getString("lemethod") == "bicgstab") {
LOG4CPLUS_INFO(logger, "Using BiCGStab method."); LOG4CPLUS_INFO(logger, "Using BiCGStab method.");
if (precond == "ilu") { if (precond == "ilu") {
gmm::bicgstab(A, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(A), iter);
gmm::bicgstab(*A, **vector, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*A), iter);
} else if (precond == "diagonal") { } else if (precond == "diagonal") {
gmm::bicgstab(A, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(A), iter);
gmm::bicgstab(*A, **vector, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*A), iter);
} else if (precond == "ildlt") { } else if (precond == "ildlt") {
gmm::bicgstab(A, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(A), iter);
gmm::bicgstab(*A, **vector, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*A), iter);
} else if (precond == "none") { } else if (precond == "none") {
gmm::bicgstab(A, x, b, gmm::identity_matrix(), iter);
gmm::bicgstab(*A, **vector, b, gmm::identity_matrix(), iter);
} }
// Check if the solver converged and issue a warning otherwise. // Check if the solver converged and issue a warning otherwise.
@ -430,28 +170,16 @@ private:
} else { } else {
LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
} }
// FIXME: gmres has been disabled, because it triggers gmm++ compilation errors
/* } else if (s->getString("lemethod").compare("gmres") == 0) {
LOG4CPLUS_INFO(logger, "Using GMRES method.");
if (precond.compare("ilu")) {
gmm::gmres(A, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(A), s->get<unsigned>("restart"), iter);
} else if (precond == "diagonal") {
gmm::gmres(A, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(A), s->get<unsigned>("restart"), iter);
} else if (precond == "ildlt") {
gmm::gmres(A, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(A), s->get<unsigned>("restart"), iter);
} else if (precond == "none") {
gmm::gmres(A, x, b, gmm::identity_matrix(), s->get<unsigned>("restart"), iter);
} */
} else if (s->getString("lemethod") == "qmr") { } else if (s->getString("lemethod") == "qmr") {
LOG4CPLUS_INFO(logger, "Using QMR method."); LOG4CPLUS_INFO(logger, "Using QMR method.");
if (precond == "ilu") { if (precond == "ilu") {
gmm::qmr(A, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(A), iter);
gmm::qmr(*A, **vector, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*A), iter);
} else if (precond == "diagonal") { } else if (precond == "diagonal") {
gmm::qmr(A, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(A), iter);
gmm::qmr(*A, **vector, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*A), iter);
} else if (precond == "ildlt") { } else if (precond == "ildlt") {
gmm::qmr(A, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(A), iter);
gmm::qmr(*A, **vector, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*A), iter);
} else if (precond == "none") { } else if (precond == "none") {
gmm::qmr(A, x, b, gmm::identity_matrix(), iter);
gmm::qmr(*A, **vector, b, gmm::identity_matrix(), iter);
} }
// Check if the solver converged and issue a warning otherwise. // Check if the solver converged and issue a warning otherwise.
@ -462,8 +190,10 @@ private:
} }
} else if (s->getString("lemethod") == "jacobi") { } else if (s->getString("lemethod") == "jacobi") {
LOG4CPLUS_INFO(logger, "Using Jacobi method."); LOG4CPLUS_INFO(logger, "Using Jacobi method.");
solveLinearEquationSystemWithJacobi(A, x, b);
solveLinearEquationSystemWithJacobi(*A, **vector, b);
} }
delete A;
} }
/*! /*!

17
src/storage/BitVector.h
View File

@ -409,6 +409,23 @@ public:
return true; return true;
} }
/*!
* Checks whether none of the bits that are set in the current bit vector are also set in the
* given bit vector.
* @param bv A reference to the bit vector whose bits are (possibly) disjoint from the bits in
* the current bit vector.
* @returns True iff none of the bits that are set in the current bit vector are also set in the
* given bit vector.
*/
bool isDisjointFrom(BitVector const& bv) const {
for (uint_fast64_t i = 0; i < this->bucketCount; ++i) {
if ((this->bucketArray[i] & bv.bucketArray[i]) != 0) {
return false;
}
}
return true;
}
/*! /*!
* Adds all indices of bits set to one to the provided list. * Adds all indices of bits set to one to the provided list.
* @param list The list to which to append the indices. * @param list The list to which to append the indices.

3
src/utility/ConstTemplates.h
View File

@ -18,6 +18,9 @@
#include <limits> #include <limits>
#include "src/exceptions/InvalidArgumentException.h"
#include "src/storage/BitVector.h"
namespace storm { namespace storm {
namespace utility { namespace utility {

164
test/functional/EigenDtmcPrctModelCheckerTest.cpp
View File

@ -0,0 +1,164 @@
/*
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/utility/Settings.h"
#include "src/modelchecker/EigenDtmcPrctlModelChecker.h"
#include "src/parser/AutoParser.h"
TEST(EigenDtmcPrctModelCheckerTest, Die) {
storm::settings::Settings* s = storm::settings::instance();
s->set("fix-deadlocks");
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew");
ASSERT_EQ(parser.getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 14);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28);
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("one");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
std::vector<double>* result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::formula::Ap<double>("two");
eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::formula::Ap<double>("three");
eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
delete probFormula;
delete result;
storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
result = rewardFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->get<double>("precision"));
delete rewardFormula;
delete result;
}
TEST(EigenDtmcPrctModelCheckerTest, Crowds) {
storm::settings::Settings* s = storm::settings::instance();
s->set("fix-deadlocks");
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", "");
ASSERT_EQ(parser.getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 8608);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22461);
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("observe0Greater1");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
std::vector<double>* result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::formula::Ap<double>("observeIGreater1");
eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::formula::Ap<double>("observeOnlyTrueSender");
eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->get<double>("precision"));
delete probFormula;
delete result;
}
TEST(EigenDtmcPrctModelCheckerTest, SynchronousLeader) {
storm::settings::Settings* s = storm::settings::instance();
s->set("fix-deadlocks");
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew");
ASSERT_EQ(parser.getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 12401);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28895);
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc);
storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
std::vector<double>* result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::formula::Ap<double>("elected");
storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), apFormula, 20);
probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
result = probFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::formula::Ap<double>("elected");
storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
result = rewardFormula->check(mc);
ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->get<double>("precision"));
delete rewardFormula;
delete result;
}
*/

20
test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -25,7 +25,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
std::vector<double>* result = probFormula->check(mc); std::vector<double>* result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -36,7 +36,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -47,7 +47,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -59,7 +59,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
result = rewardFormula->check(mc); result = rewardFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - ((double)11/3)) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -85,7 +85,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
std::vector<double>* result = probFormula->check(mc); std::vector<double>* result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - 0.3328800375801578281) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -96,7 +96,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - 0.1522173670950556501) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -107,7 +107,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - 0.32153724292835045) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -133,7 +133,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
std::vector<double>* result = probFormula->check(mc); std::vector<double>* result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - 1) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - 1), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -144,7 +144,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - 0.9999965911265462636) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -155,7 +155,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
result = rewardFormula->check(mc); result = rewardFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[1] - 1.0448979591835938496) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;

36
test/functional/GmmxxMdpPrctModelCheckerTest.cpp
View File

@ -24,7 +24,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
std::vector<double>* result = probFormula->check(mc); std::vector<double>* result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.0277777612209320068) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -35,7 +35,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.0277777612209320068) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -46,7 +46,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.0555555224418640136) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -57,7 +57,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.0555555224418640136) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -68,7 +68,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.083333283662796020508) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -79,7 +79,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.083333283662796020508) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -90,7 +90,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = rewardFormula->check(mc); result = rewardFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -101,7 +101,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = rewardFormula->check(mc); result = rewardFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -120,7 +120,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = rewardFormula->check(stateRewardModelChecker); result = rewardFormula->check(stateRewardModelChecker);
ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -131,7 +131,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = rewardFormula->check(stateRewardModelChecker); result = rewardFormula->check(stateRewardModelChecker);
ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -150,7 +150,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = rewardFormula->check(stateAndTransitionRewardModelChecker); result = rewardFormula->check(stateAndTransitionRewardModelChecker);
ASSERT_TRUE(std::abs((*result)[0] - (2 * 7.3333272933959960938)) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333272933959960938)), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -161,7 +161,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
result = rewardFormula->check(stateAndTransitionRewardModelChecker); result = rewardFormula->check(stateAndTransitionRewardModelChecker);
ASSERT_TRUE(std::abs((*result)[0] - (2 * 7.3333272933959960938)) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333272933959960938)), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -186,7 +186,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
std::vector<double>* result = probFormula->check(mc); std::vector<double>* result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 1) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -197,7 +197,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 1) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -208,7 +208,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.0625) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -219,7 +219,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
result = probFormula->check(mc); result = probFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 0.0625) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
@ -230,7 +230,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
result = rewardFormula->check(mc); result = rewardFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 4.28568908480604982) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
@ -241,7 +241,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
result = rewardFormula->check(mc); result = rewardFormula->check(mc);
ASSERT_TRUE(std::abs((*result)[0] - 4.2856904354441400784) < s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;

Write Preview
Loading…
Cancel
Save