diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h
index 5d7d6e281..d0ee74efd 100644
--- a/src/formula/AbstractPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -61,7 +61,7 @@ public:
*
* @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
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 3bb72d07e..fe7776f33 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -36,7 +36,7 @@ class IBoundedEventuallyModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h
index 91bd44713..7c98af61e 100644
--- a/src/formula/BoundedNaryUntil.h
+++ b/src/formula/BoundedNaryUntil.h
@@ -37,7 +37,7 @@ class IBoundedNaryUntilModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 7b4a7e07c..de0a88d2c 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -34,7 +34,7 @@ class IBoundedUntilModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index e89bcfbaf..6275621db 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -35,7 +35,7 @@ class ICumulativeRewardModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 53b7b0dd1..668546f0c 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -33,7 +33,7 @@ class IEventuallyModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 05041ee17..7b58580e9 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -34,7 +34,7 @@ class IGloballyModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index 8f55b2c7c..ed0f7affa 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -35,7 +35,7 @@ class IInstantaneousRewardModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/Next.h b/src/formula/Next.h
index a91a39ce1..91d68d05a 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -33,7 +33,7 @@ class INextModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index a725e202a..ff8155eb5 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -32,7 +32,7 @@ class IReachabilityRewardModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 82ac05c9d..29c0e497d 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -32,7 +32,7 @@ class IUntilModelChecker {
* @param obj Formula object with subformulas.
* @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.
*/
- 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);
}
/*!
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 991a7edc7..244b35df1 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -110,7 +110,7 @@ public:
*/
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.
- 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.
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 {
// 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.
storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size());
diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h
index 5b1f16600..61a9b2ffd 100644
--- a/src/modelchecker/DtmcPrctlModelChecker.h
+++ b/src/modelchecker/DtmcPrctlModelChecker.h
@@ -160,17 +160,6 @@ public:
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
* in its formula tree
@@ -183,18 +172,7 @@ public:
if (formula.isOptimalityOperator()) {
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
* @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
@@ -211,7 +189,7 @@ public:
* @param formula The Next path formula to check
* @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
@@ -220,10 +198,10 @@ public:
* @param formula The Bounded Eventually path formula to check
* @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.
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
* @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.
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
* @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.
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.
storm::utility::subtractFromConstantOneVector(result);
@@ -260,7 +238,7 @@ public:
* @param formula The Until path formula to check
* @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
@@ -269,7 +247,7 @@ public:
* @param formula The Instantaneous Reward formula to check
* @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
@@ -278,7 +256,7 @@ public:
* @param formula The Cumulative Reward formula to check
* @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
@@ -287,7 +265,7 @@ public:
* @param formula The Reachbility Reward formula to check
* @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:
storm::models::Dtmc<Type>& model;
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index ac5d97158..a75276405 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -45,10 +45,10 @@ public:
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.
- 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.
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
@@ -81,9 +81,9 @@ public:
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.
- 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.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
@@ -106,10 +106,10 @@ public:
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.
- 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.
// all states that have probability 0 and 1 of satisfying the until-formula.
@@ -169,7 +169,7 @@ public:
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.
if (!this->getModel().hasStateRewards()) {
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
@@ -198,7 +198,7 @@ public:
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.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
@@ -241,7 +241,7 @@ public:
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.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
@@ -249,7 +249,7 @@ public:
}
// 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.
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h
index 41efbd145..1c8741ebd 100644
--- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h
@@ -43,10 +43,10 @@ public:
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.
- 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.
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
@@ -88,9 +88,9 @@ public:
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.
- 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.
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
@@ -124,10 +124,10 @@ public:
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.
- 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.
// all states that have probability 0 and 1 of satisfying the until-formula.
@@ -191,7 +191,7 @@ public:
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.
if (!this->getModel().hasStateRewards()) {
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
@@ -220,7 +220,7 @@ public:
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.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
@@ -263,7 +263,7 @@ public:
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.
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
@@ -271,7 +271,7 @@ public:
}
// 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.
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
diff --git a/src/modelchecker/MdpPrctlModelChecker.h b/src/modelchecker/MdpPrctlModelChecker.h
index d1a948ed5..c2fad0b21 100644
--- a/src/modelchecker/MdpPrctlModelChecker.h
+++ b/src/modelchecker/MdpPrctlModelChecker.h
@@ -140,17 +140,6 @@ public:
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
*
@@ -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.";
}
minimumOperatorStack.push(formula.isMinimumOperator());
- std::vector<Type>* result = formula.getPathFormula().check(*this);
+ std::vector<Type>* result = formula.getPathFormula().check(*this, false);
minimumOperatorStack.pop();
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
*
* @param formula The Bounded Until path formula to check
* @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
@@ -217,7 +195,7 @@ public:
* @param formula The Next path formula to check
* @returns for each state the probability that the path formula holds.
*/
- virtual std::vector<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
@@ -226,10 +204,10 @@ public:
* @param formula The Bounded Eventually path formula to check
* @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.
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
* @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.
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
* @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.
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.
storm::utility::subtractFromConstantOneVector(result);
@@ -266,7 +244,7 @@ public:
* @param formula The Until path formula to check
* @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
@@ -275,7 +253,7 @@ public:
* @param formula The Instantaneous Reward formula to check
* @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
@@ -284,7 +262,7 @@ public:
* @param formula The Cumulative Reward formula to check
* @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
@@ -293,7 +271,7 @@ public:
* @param formula The Reachbility Reward formula to check
* @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:
storm::models::Mdp<Type>& model;