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

Added boolean parameter qualitative to all path formulas, i.e. to the checking and the callback methods.

main
dehnert 12 years ago
parent
5ba7f63bc2
commit
73623ff3f6
16 changed files with 83 additions and 127 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. 2
      src/formula/AbstractPathFormula.h
  2. 6
      src/formula/BoundedEventually.h
  3. 6
      src/formula/BoundedNaryUntil.h
  4. 6
      src/formula/BoundedUntil.h
  5. 6
      src/formula/CumulativeReward.h
  6. 6
      src/formula/Eventually.h
  7. 6
      src/formula/Globally.h
  8. 6
      src/formula/InstantaneousReward.h
  9. 6
      src/formula/Next.h
  10. 6
      src/formula/ReachabilityReward.h
  11. 6
      src/formula/Until.h
  12. 4
      src/modelchecker/AbstractModelChecker.h
  13. 48
      src/modelchecker/DtmcPrctlModelChecker.h
  14. 24
      src/modelchecker/GmmxxDtmcPrctlModelChecker.h
  15. 24
      src/modelchecker/GmmxxMdpPrctlModelChecker.h
  16. 48
      src/modelchecker/MdpPrctlModelChecker.h

2
src/formula/AbstractPathFormula.h
View File

@ -61,7 +61,7 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const = 0;
virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
}; };
} //namespace formula } //namespace formula

6
src/formula/BoundedEventually.h
View File

@ -36,7 +36,7 @@ class IBoundedEventuallyModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -157,8 +157,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
} }
/*! /*!

6
src/formula/BoundedNaryUntil.h
View File

@ -37,7 +37,7 @@ class IBoundedNaryUntilModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj) const = 0;
virtual std::vector<T>* checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -179,8 +179,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
} }
/*! /*!

6
src/formula/BoundedUntil.h
View File

@ -34,7 +34,7 @@ class IBoundedUntilModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -186,8 +186,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
} }
/*! /*!

6
src/formula/CumulativeReward.h
View File

@ -35,7 +35,7 @@ class ICumulativeRewardModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkCumulativeReward(const CumulativeReward<T>& obj) const = 0;
virtual std::vector<T>* checkCumulativeReward(const CumulativeReward<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -121,8 +121,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this, qualitative);
} }
/*! /*!

6
src/formula/Eventually.h
View File

@ -33,7 +33,7 @@ class IEventuallyModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkEventually(const Eventually<T>& obj) const = 0;
virtual std::vector<T>* checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -131,8 +131,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
} }
/*! /*!

6
src/formula/Globally.h
View File

@ -34,7 +34,7 @@ class IGloballyModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkGlobally(const Globally<T>& obj) const = 0;
virtual std::vector<T>* checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -132,8 +132,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
} }
/*! /*!

6
src/formula/InstantaneousReward.h
View File

@ -35,7 +35,7 @@ class IInstantaneousRewardModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj) const = 0;
virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -121,8 +121,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this, qualitative);
} }
/*! /*!

6
src/formula/Next.h
View File

@ -33,7 +33,7 @@ class INextModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
virtual std::vector<T>* checkNext(const Next<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -133,8 +133,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INextModelChecker>()->checkNext(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
} }
/*! /*!

6
src/formula/ReachabilityReward.h
View File

@ -32,7 +32,7 @@ class IReachabilityRewardModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj) const = 0;
virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -127,8 +127,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this, qualitative);
} }
/*! /*!

6
src/formula/Until.h
View File

@ -32,7 +32,7 @@ class IUntilModelChecker {
* @param obj Formula object with subformulas. * @param obj Formula object with subformulas.
* @return Result of the formula for every node. * @return Result of the formula for every node.
*/ */
virtual std::vector<T>* checkUntil(const Until<T>& obj) const = 0;
virtual std::vector<T>* checkUntil(const Until<T>& obj, bool qualitative) const = 0;
}; };
/*! /*!
@ -160,8 +160,8 @@ public:
* *
* @returns A vector indicating the probability that the formula holds for each state. * @returns A vector indicating the probability that the formula holds for each state.
*/ */
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
} }
/*! /*!

4
src/modelchecker/AbstractModelChecker.h
View File

@ -110,7 +110,7 @@ public:
*/ */
storm::storage::BitVector* checkProbabilisticBoundOperator(const storm::formula::ProbabilisticBoundOperator<Type>& formula) const { storm::storage::BitVector* checkProbabilisticBoundOperator(const storm::formula::ProbabilisticBoundOperator<Type>& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state. // First, we need to compute the probability for satisfying the path formula for each state.
std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this);
std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false);
// Create resulting bit vector, which will hold the yes/no-answer for every state. // Create resulting bit vector, which will hold the yes/no-answer for every state.
storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size()); storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size());
@ -137,7 +137,7 @@ public:
*/ */
storm::storage::BitVector* checkRewardBoundOperator(const storm::formula::RewardBoundOperator<Type>& formula) const { storm::storage::BitVector* checkRewardBoundOperator(const storm::formula::RewardBoundOperator<Type>& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state. // First, we need to compute the probability for satisfying the path formula for each state.
std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this);
std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false);
// Create resulting bit vector, which will hold the yes/no-answer for every state. // Create resulting bit vector, which will hold the yes/no-answer for every state.
storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size()); storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size());

48
src/modelchecker/DtmcPrctlModelChecker.h
View File

@ -160,17 +160,6 @@ public:
storm::utility::printSeparationLine(std::cout); storm::utility::printSeparationLine(std::cout);
} }
/*!
* The check method for a state formula; Will infer the actual type of formula and delegate it
* to the specialized method
*
* @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
storm::storage::BitVector* checkStateFormula(const storm::formula::AbstractStateFormula<Type>& formula) const {
return formula.check(*this);
}
/*! /*!
* 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
@ -183,18 +172,7 @@ public:
if (formula.isOptimalityOperator()) { if (formula.isOptimalityOperator()) {
LOG4CPLUS_WARN(logger, "Formula contains min/max operator which is not meaningful over deterministic models."); LOG4CPLUS_WARN(logger, "Formula contains min/max operator which is not meaningful over deterministic models.");
} }
return formula.getPathFormula().check(*this);
}
/*!
* The check method for a path formula; Will infer the actual type of formula and delegate it
* to the specialized method
*
* @param formula The path formula to check
* @returns for each state the probability that the path formula holds.
*/
std::vector<Type>* checkPathFormula(const storm::formula::AbstractPathFormula<Type>& formula) const {
return formula.check(*this);
return formula.getPathFormula().check(*this, false);
} }
/*! /*!
@ -203,7 +181,7 @@ 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) const = 0;
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -211,7 +189,7 @@ 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) const = 0;
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -220,10 +198,10 @@ public:
* @param formula The Bounded Eventually path formula to check * @param formula The Bounded Eventually 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>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula) const {
virtual std::vector<Type>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula, bool qualitative) const {
// Create equivalent temporary bounded until formula and check it. // Create equivalent temporary bounded until formula and check it.
storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound()); storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
return this->checkBoundedUntil(temporaryBoundedUntilFormula);
return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
} }
/*! /*!
@ -232,10 +210,10 @@ public:
* @param formula The Eventually path formula to check * @param formula The Eventually 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>* checkEventually(const storm::formula::Eventually<Type>& formula) const {
virtual std::vector<Type>* checkEventually(const storm::formula::Eventually<Type>& formula, bool qualitative) const {
// Create equivalent temporary until formula and check it. // Create equivalent temporary until formula and check it.
storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone()); storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone());
return this->checkUntil(temporaryUntilFormula);
return this->checkUntil(temporaryUntilFormula, qualitative);
} }
/*! /*!
@ -244,10 +222,10 @@ public:
* @param formula The Globally path formula to check * @param formula The Globally 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>* checkGlobally(const storm::formula::Globally<Type>& formula) const {
virtual std::vector<Type>* checkGlobally(const storm::formula::Globally<Type>& formula, bool qualitative) const {
// Create "equivalent" temporary eventually formula and check it. // Create "equivalent" temporary eventually formula and check it.
storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone())); storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone()));
std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula);
std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative);
// Now subtract the resulting vector from the constant one vector to obtain final result. // Now subtract the resulting vector from the constant one vector to obtain final result.
storm::utility::subtractFromConstantOneVector(result); storm::utility::subtractFromConstantOneVector(result);
@ -260,7 +238,7 @@ 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) const = 0;
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -269,7 +247,7 @@ 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) const = 0;
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -278,7 +256,7 @@ 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) const = 0;
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -287,7 +265,7 @@ 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) const = 0;
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const = 0;
private: private:
storm::models::Dtmc<Type>& model; storm::models::Dtmc<Type>& model;

24
src/modelchecker/GmmxxDtmcPrctlModelChecker.h
View File

@ -45,10 +45,10 @@ public:
virtual ~GmmxxDtmcPrctlModelChecker() { } virtual ~GmmxxDtmcPrctlModelChecker() { }
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula) const {
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. // 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());
storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
storm::storage::BitVector* rightStates = formula.getRight().check(*this);
// Copy the matrix before we make any changes. // Copy the matrix before we make any changes.
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix()); storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
@ -81,9 +81,9 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula) const {
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. // First, we need to compute the states that satisfy the sub-formula of the next-formula.
storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
storm::storage::BitVector* nextStates = formula.getChild().check(*this);
// Transform the transition probability matrix to the gmm++ format to use its arithmetic. // 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()); gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
@ -106,10 +106,10 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula) const {
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. // 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());
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. // 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. // all states that have probability 0 and 1 of satisfying the until-formula.
@ -169,7 +169,7 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula) const {
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. // Only compute the result if the model has a state-based reward model.
if (!this->getModel().hasStateRewards()) { if (!this->getModel().hasStateRewards()) {
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
@ -198,7 +198,7 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula) const {
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. // Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
@ -241,7 +241,7 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula) const {
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. // Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
@ -249,7 +249,7 @@ public:
} }
// Determine the states for which the target predicate holds. // Determine the states for which the target predicate holds.
storm::storage::BitVector* targetStates = this->checkStateFormula(formula.getChild());
storm::storage::BitVector* targetStates = formula.getChild().check(*this);
// Determine which states have a reward of infinity by definition. // Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());

24
src/modelchecker/GmmxxMdpPrctlModelChecker.h
View File

@ -43,10 +43,10 @@ public:
virtual ~GmmxxMdpPrctlModelChecker() { } virtual ~GmmxxMdpPrctlModelChecker() { }
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula) const {
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. // 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());
storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
storm::storage::BitVector* rightStates = formula.getRight().check(*this);
// Copy the matrix before we make any changes. // Copy the matrix before we make any changes.
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix()); storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
@ -88,9 +88,9 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula) const {
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. // First, we need to compute the states that satisfy the sub-formula of the next-formula.
storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
storm::storage::BitVector* nextStates = formula.getChild().check(*this);
// Transform the transition probability matrix to the gmm++ format to use its arithmetic. // 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()); gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
@ -124,10 +124,10 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula) const {
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. // 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());
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. // 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. // all states that have probability 0 and 1 of satisfying the until-formula.
@ -191,7 +191,7 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula) const {
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. // Only compute the result if the model has a state-based reward model.
if (!this->getModel().hasStateRewards()) { if (!this->getModel().hasStateRewards()) {
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
@ -220,7 +220,7 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula) const {
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. // Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
@ -263,7 +263,7 @@ public:
return result; return result;
} }
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula) const {
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. // Only compute the result if the model has at least one reward model.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
@ -271,7 +271,7 @@ public:
} }
// Determine the states for which the target predicate holds. // Determine the states for which the target predicate holds.
storm::storage::BitVector* targetStates = this->checkStateFormula(formula.getChild());
storm::storage::BitVector* targetStates = formula.getChild().check(*this);
// Determine which states have a reward of infinity by definition. // Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());

48
src/modelchecker/MdpPrctlModelChecker.h
View File

@ -140,17 +140,6 @@ public:
storm::utility::printSeparationLine(std::cout); storm::utility::printSeparationLine(std::cout);
} }
/*!
* The check method for a state formula; Will infer the actual type of formula and delegate it
* to the specialized method
*
* @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
storm::storage::BitVector* checkStateFormula(const storm::formula::AbstractStateFormula<Type>& formula) const {
return formula.check(*this);
}
/*! /*!
* The check method for a formula with an AP node as root in its formula tree * The check method for a formula with an AP node as root in its formula tree
* *
@ -187,29 +176,18 @@ public:
throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
} }
minimumOperatorStack.push(formula.isMinimumOperator()); minimumOperatorStack.push(formula.isMinimumOperator());
std::vector<Type>* result = formula.getPathFormula().check(*this);
std::vector<Type>* result = formula.getPathFormula().check(*this, false);
minimumOperatorStack.pop(); minimumOperatorStack.pop();
return result; return result;
} }
/*!
* The check method for a path formula; Will infer the actual type of formula and delegate it
* to the specialized method
*
* @param formula The path formula to check
* @returns for each state the probability that the path formula holds.
*/
std::vector<Type>* checkPathFormula(const storm::formula::AbstractPathFormula<Type>& formula) const {
return formula.check(*this);
}
/*! /*!
* The check method for a path formula with a Bounded Until operator node as root in its formula tree * The check method for a path formula with a Bounded Until operator node as root in its formula tree
* *
* @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) const = 0;
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -217,7 +195,7 @@ 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) const = 0;
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -226,10 +204,10 @@ public:
* @param formula The Bounded Eventually path formula to check * @param formula The Bounded Eventually 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>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula) const {
virtual std::vector<Type>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula, bool qualitative) const {
// Create equivalent temporary bounded until formula and check it. // Create equivalent temporary bounded until formula and check it.
storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound()); storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
return this->checkBoundedUntil(temporaryBoundedUntilFormula);
return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
} }
/*! /*!
@ -238,10 +216,10 @@ public:
* @param formula The Eventually path formula to check * @param formula The Eventually 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>* checkEventually(const storm::formula::Eventually<Type>& formula) const {
virtual std::vector<Type>* checkEventually(const storm::formula::Eventually<Type>& formula, bool qualitative) const {
// Create equivalent temporary until formula and check it. // Create equivalent temporary until formula and check it.
storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone()); storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone());
return this->checkUntil(temporaryUntilFormula);
return this->checkUntil(temporaryUntilFormula, qualitative);
} }
/*! /*!
@ -250,10 +228,10 @@ public:
* @param formula The Globally path formula to check * @param formula The Globally 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>* checkGlobally(const storm::formula::Globally<Type>& formula) const {
virtual std::vector<Type>* checkGlobally(const storm::formula::Globally<Type>& formula, bool qualitative) const {
// Create "equivalent" temporary eventually formula and check it. // Create "equivalent" temporary eventually formula and check it.
storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone())); storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone()));
std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula);
std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative);
// Now subtract the resulting vector from the constant one vector to obtain final result. // Now subtract the resulting vector from the constant one vector to obtain final result.
storm::utility::subtractFromConstantOneVector(result); storm::utility::subtractFromConstantOneVector(result);
@ -266,7 +244,7 @@ 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) const = 0;
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -275,7 +253,7 @@ 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) const = 0;
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -284,7 +262,7 @@ 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) const = 0;
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const = 0;
/*! /*!
* 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
@ -293,7 +271,7 @@ 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) const = 0;
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const = 0;
private: private:
storm::models::Mdp<Type>& model; storm::models::Mdp<Type>& model;

Write Preview
Loading…
Cancel
Save