From 5bbd85c379802a6e57119e732328ce24bd98b5b4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 17 Mar 2015 10:39:13 +0100
Subject: [PATCH] Some bugfixes.

Former-commit-id: 70dcc73e910c4039a872a64b33c494d1f66b507c
---
 src/modelchecker/AbstractModelChecker.cpp | 24 +++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp
index 6b4ab55ab..ed51c16d2 100644
--- a/src/modelchecker/AbstractModelChecker.cpp
+++ b/src/modelchecker/AbstractModelChecker.cpp
@@ -161,10 +161,10 @@ namespace storm {
             if (stateFormula.hasOptimalityType()) {
                 result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType());
             } else if (stateFormula.hasBound()) {
-                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) {
-                    result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), storm::logic::OptimalityType::Maximize);
+                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
+                    result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, storm::logic::OptimalityType::Maximize);
                 } else {
-                    result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), storm::logic::OptimalityType::Minimize);
+                    result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, storm::logic::OptimalityType::Minimize);
                 }
             } else {
                 result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative);
@@ -193,10 +193,10 @@ namespace storm {
             if (stateFormula.hasOptimalityType()) {
                 result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, stateFormula.getOptimalityType());
             } else if (stateFormula.hasBound()) {
-                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) {
-                    result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), storm::logic::OptimalityType::Maximize);
+                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
+                    result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, storm::logic::OptimalityType::Maximize);
                 } else {
-                    result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), storm::logic::OptimalityType::Minimize);
+                    result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, storm::logic::OptimalityType::Minimize);
                 }
             } else {
                 result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative);
@@ -225,10 +225,10 @@ namespace storm {
             if (stateFormula.hasOptimalityType()) {
                 result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, stateFormula.getOptimalityType());
             } else if (stateFormula.hasBound()) {
-                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) {
-                    result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), storm::logic::OptimalityType::Maximize);
+                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
+                    result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, storm::logic::OptimalityType::Maximize);
                 } else {
-                    result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), storm::logic::OptimalityType::Minimize);
+                    result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, storm::logic::OptimalityType::Minimize);
                 }
             } else {
                 result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative);
@@ -249,10 +249,10 @@ namespace storm {
             if (stateFormula.hasOptimalityType()) {
                 result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType());
             } else if (stateFormula.hasBound()) {
-                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) {
-                    result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), storm::logic::OptimalityType::Maximize);
+                if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || stateFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual) {
+                    result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, storm::logic::OptimalityType::Maximize);
                 } else {
-                    result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), storm::logic::OptimalityType::Minimize);
+                    result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, storm::logic::OptimalityType::Minimize);
                 }
             } else {
                 result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false);