diff --git a/src/formula/abstract/IOptimizingOperator.h b/src/formula/abstract/IOptimizingOperator.h new file mode 100644 index 000000000..bbe5e896d --- /dev/null +++ b/src/formula/abstract/IOptimizingOperator.h @@ -0,0 +1,41 @@ +/* + * IOptimizingOperator.h + * + * Created on: 17.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_ABSTRACT_IOPTIMIZINGOPERATOR_H_ +#define STORM_FORMULA_ABSTRACT_IOPTIMIZINGOPERATOR_H_ + +namespace storm { +namespace formula { +namespace abstract { + +/*! + * @brief Interface for optimizing operators + * + * Needed to link abstract classes in concrete logics with the logic-abstract implementation. + */ +class IOptimizingOperator { +public: + + /*! + * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator. + * @returns True if the operator is an optimizing operator. + */ + virtual bool isOptimalityOperator() const = 0; + + /*! + * Retrieves whether the operator is a minimizing operator given that it is an optimality + * operator. + * @returns True if the operator is an optimizing operator and it is a minimizing operator and + * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator. + */ + virtual bool isMinimumOperator() const = 0; +}; + +} /* namespace abstract */ +} /* namespace formula */ +} /* namespace storm */ +#endif /* IOPTIMIZINGOPERATOR_H_ */ diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h index c0ad5b5cf..9f3951f85 100644 --- a/src/formula/abstract/PathNoBoundOperator.h +++ b/src/formula/abstract/PathNoBoundOperator.h @@ -65,8 +65,7 @@ public: * * @param pathFormula The child node. */ - PathNoBoundOperator(FormulaType* pathFormula) : - OptimizingOperator(false) { + PathNoBoundOperator(FormulaType* pathFormula) { this->pathFormula = pathFormula; } diff --git a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp index 30256ed3a..52edd991a 100644 --- a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp @@ -22,7 +22,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { storm::formula::prctl::Eventually* eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); storm::formula::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - std::vector* result = probFormula->check(mc); + std::vector* result = mc.checkNoBoundOperator(*probFormula); ASSERT_NE(nullptr, result); @@ -35,7 +35,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get("precision")); @@ -46,7 +46,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get("precision")); @@ -57,7 +57,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get("precision")); @@ -68,7 +68,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get("precision")); @@ -79,7 +79,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get("precision")); @@ -90,7 +90,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { storm::formula::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); storm::formula::prctl::RewardNoBoundOperator* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = rewardFormula->check(mc); + result = mc.checkNoBoundOperator(*rewardFormula); ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); @@ -101,7 +101,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = rewardFormula->check(mc); + result = mc.checkNoBoundOperator(*rewardFormula);; ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); @@ -120,7 +120,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = rewardFormula->check(stateRewardModelChecker); + result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); @@ -131,7 +131,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = rewardFormula->check(stateRewardModelChecker); + result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); @@ -150,7 +150,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = rewardFormula->check(stateAndTransitionRewardModelChecker); + result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get("precision")); @@ -161,7 +161,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = rewardFormula->check(stateAndTransitionRewardModelChecker); + result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get("precision")); @@ -186,7 +186,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::formula::prctl::Eventually* eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); storm::formula::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - std::vector* result = probFormula->check(mc); + std::vector* result = mc.checkNoBoundOperator(*probFormula); ASSERT_NE(nullptr, result); @@ -199,7 +199,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { eventuallyFormula = new storm::formula::prctl::Eventually(apFormula); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_NE(nullptr, result); @@ -212,7 +212,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::formula::prctl::BoundedEventually* boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually(apFormula, 25); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_NE(nullptr, result); @@ -225,7 +225,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { boundedEventuallyFormula = new storm::formula::prctl::BoundedEventually(apFormula, 25); probFormula = new storm::formula::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); - result = probFormula->check(mc); + result = mc.checkNoBoundOperator(*probFormula); ASSERT_NE(nullptr, result); @@ -238,7 +238,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::formula::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); storm::formula::prctl::RewardNoBoundOperator* rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = rewardFormula->check(mc); + result = mc.checkNoBoundOperator(*rewardFormula);; ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); @@ -249,7 +249,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { reachabilityRewardFormula = new storm::formula::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::formula::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = rewardFormula->check(mc); + result = mc.checkNoBoundOperator(*rewardFormula);; ASSERT_NE(nullptr, result);