From f39fb24f6547d7de6781d7ca3f96d065663f5f8d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 26 Sep 2013 13:16:07 +0200
Subject: [PATCH] Removed pointers from Model Checker Interface (and callback
methods in formulas). From now on, the results are returned in form of an
object. Because of the existing move semantics for the types in question,
this does not come at a performance penalty.
Former-commit-id: 5befdebd9270a1303eec8feb1ea4a1d74fa19693
---
src/formula/Csl/AbstractNoBoundOperator.h | 4 +-
src/formula/Csl/AbstractPathFormula.h | 2 +-
src/formula/Csl/AbstractStateFormula.h | 2 +-
src/formula/Csl/And.h | 4 +-
src/formula/Csl/Ap.h | 4 +-
src/formula/Csl/Eventually.h | 4 +-
src/formula/Csl/Globally.h | 4 +-
src/formula/Csl/Next.h | 4 +-
src/formula/Csl/Not.h | 4 +-
src/formula/Csl/Or.h | 4 +-
src/formula/Csl/ProbabilisticBoundOperator.h | 4 +-
.../Csl/ProbabilisticNoBoundOperator.h | 2 +-
src/formula/Csl/SteadyStateBoundOperator.h | 4 +-
src/formula/Csl/SteadyStateNoBoundOperator.h | 4 +-
src/formula/Csl/TimeBoundedEventually.h | 4 +-
src/formula/Csl/TimeBoundedUntil.h | 4 +-
src/formula/Csl/Until.h | 4 +-
src/formula/Ltl/AbstractLtlFormula.h | 2 +-
src/formula/Ltl/And.h | 4 +-
src/formula/Ltl/Ap.h | 4 +-
src/formula/Ltl/BoundedEventually.h | 4 +-
src/formula/Ltl/BoundedUntil.h | 4 +-
src/formula/Ltl/Eventually.h | 4 +-
src/formula/Ltl/Globally.h | 4 +-
src/formula/Ltl/Next.h | 4 +-
src/formula/Ltl/Not.h | 4 +-
src/formula/Ltl/Or.h | 4 +-
src/formula/Ltl/Until.h | 4 +-
src/formula/Prctl/AbstractNoBoundOperator.h | 4 +-
src/formula/Prctl/AbstractPathFormula.h | 2 +-
src/formula/Prctl/AbstractStateFormula.h | 2 +-
src/formula/Prctl/And.h | 4 +-
src/formula/Prctl/Ap.h | 4 +-
src/formula/Prctl/BoundedEventually.h | 4 +-
src/formula/Prctl/BoundedNaryUntil.h | 4 +-
src/formula/Prctl/BoundedUntil.h | 4 +-
src/formula/Prctl/CumulativeReward.h | 4 +-
src/formula/Prctl/Eventually.h | 4 +-
src/formula/Prctl/Globally.h | 4 +-
src/formula/Prctl/InstantaneousReward.h | 4 +-
src/formula/Prctl/Next.h | 4 +-
src/formula/Prctl/Not.h | 4 +-
src/formula/Prctl/Or.h | 4 +-
.../Prctl/ProbabilisticBoundOperator.h | 4 +-
.../Prctl/ProbabilisticNoBoundOperator.h | 2 +-
src/formula/Prctl/ReachabilityReward.h | 4 +-
src/formula/Prctl/RewardBoundOperator.h | 4 +-
src/formula/Prctl/RewardNoBoundOperator.h | 2 +-
src/formula/Prctl/SteadyStateReward.h | 4 +-
src/formula/Prctl/Until.h | 4 +-
src/modelchecker/csl/AbstractModelChecker.h | 46 +++----
src/modelchecker/ltl/AbstractModelChecker.h | 22 +---
src/modelchecker/prctl/AbstractModelChecker.h | 60 ++++-----
.../prctl/SparseDtmcPrctlModelChecker.h | 109 +++++++--------
.../prctl/SparseMdpPrctlModelChecker.h | 124 ++++++++----------
src/storage/BitVector.h | 3 +-
.../GmmxxDtmcPrctlModelCheckerTest.cpp | 56 ++------
.../GmmxxMdpPrctlModelCheckerTest.cpp | 70 +++-------
.../SparseMdpPrctlModelCheckerTest.cpp | 69 +++-------
.../GmmxxDtmcPrctModelCheckerTest.cpp | 34 ++---
.../GmmxxMdpPrctModelCheckerTest.cpp | 68 +++-------
.../SparseMdpPrctlModelCheckerTest.cpp | 65 +++------
62 files changed, 345 insertions(+), 565 deletions(-)
diff --git a/src/formula/Csl/AbstractNoBoundOperator.h b/src/formula/Csl/AbstractNoBoundOperator.h
index f2b56711a..8a4badbf8 100644
--- a/src/formula/Csl/AbstractNoBoundOperator.h
+++ b/src/formula/Csl/AbstractNoBoundOperator.h
@@ -33,7 +33,7 @@ public:
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkNoBoundOperator(const AbstractNoBoundOperator<T>& obj) const = 0;
+ virtual std::vector<T> checkNoBoundOperator(const AbstractNoBoundOperator<T>& obj) const = 0;
};
@@ -74,7 +74,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
};
} /* namespace csl */
diff --git a/src/formula/Csl/AbstractPathFormula.h b/src/formula/Csl/AbstractPathFormula.h
index 63b20feaa..a61cab96f 100644
--- a/src/formula/Csl/AbstractPathFormula.h
+++ b/src/formula/Csl/AbstractPathFormula.h
@@ -71,7 +71,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
};
} //namespace csl
diff --git a/src/formula/Csl/AbstractStateFormula.h b/src/formula/Csl/AbstractStateFormula.h
index d96f02f5d..c54d318d5 100644
--- a/src/formula/Csl/AbstractStateFormula.h
+++ b/src/formula/Csl/AbstractStateFormula.h
@@ -65,7 +65,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const = 0;
+ virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const = 0;
};
} //namespace csl
diff --git a/src/formula/Csl/And.h b/src/formula/Csl/And.h
index f5bfe4eff..efed92f17 100644
--- a/src/formula/Csl/And.h
+++ b/src/formula/Csl/And.h
@@ -35,7 +35,7 @@ class IAndModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkAnd(const And<T>& obj) const = 0;
};
/*!
@@ -114,7 +114,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
diff --git a/src/formula/Csl/Ap.h b/src/formula/Csl/Ap.h
index d04ab56f4..cebd9aa49 100644
--- a/src/formula/Csl/Ap.h
+++ b/src/formula/Csl/Ap.h
@@ -34,7 +34,7 @@ class IApModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkAp(const Ap<T>& obj) const = 0;
};
/*!
@@ -91,7 +91,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
diff --git a/src/formula/Csl/Eventually.h b/src/formula/Csl/Eventually.h
index 33d86bc1e..5553d16c7 100644
--- a/src/formula/Csl/Eventually.h
+++ b/src/formula/Csl/Eventually.h
@@ -34,7 +34,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -108,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
}
};
diff --git a/src/formula/Csl/Globally.h b/src/formula/Csl/Globally.h
index 7da3ca072..954b59fd4 100644
--- a/src/formula/Csl/Globally.h
+++ b/src/formula/Csl/Globally.h
@@ -35,7 +35,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -110,7 +110,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
}
};
diff --git a/src/formula/Csl/Next.h b/src/formula/Csl/Next.h
index 31d978264..338d119e5 100644
--- a/src/formula/Csl/Next.h
+++ b/src/formula/Csl/Next.h
@@ -34,7 +34,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkNext(const Next<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -108,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
}
};
diff --git a/src/formula/Csl/Not.h b/src/formula/Csl/Not.h
index 413ba49ed..dd0c2a705 100644
--- a/src/formula/Csl/Not.h
+++ b/src/formula/Csl/Not.h
@@ -34,7 +34,7 @@ class INotModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkNot(const Not<T>& obj) const = 0;
};
/*!
@@ -104,7 +104,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
};
diff --git a/src/formula/Csl/Or.h b/src/formula/Csl/Or.h
index bf7f48de1..29add98cc 100644
--- a/src/formula/Csl/Or.h
+++ b/src/formula/Csl/Or.h
@@ -33,7 +33,7 @@ class IOrModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkOr(const Or<T>& obj) const = 0;
};
/*!
@@ -113,7 +113,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
};
diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/Csl/ProbabilisticBoundOperator.h
index d4e4f7326..75a985e91 100644
--- a/src/formula/Csl/ProbabilisticBoundOperator.h
+++ b/src/formula/Csl/ProbabilisticBoundOperator.h
@@ -28,7 +28,7 @@ template <class T> class ProbabilisticBoundOperator;
template <class T>
class IProbabilisticBoundOperatorModelChecker {
public:
- virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
};
/*!
@@ -109,7 +109,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
}
};
diff --git a/src/formula/Csl/ProbabilisticNoBoundOperator.h b/src/formula/Csl/ProbabilisticNoBoundOperator.h
index 41e0bcf64..63c9a501e 100644
--- a/src/formula/Csl/ProbabilisticNoBoundOperator.h
+++ b/src/formula/Csl/ProbabilisticNoBoundOperator.h
@@ -103,7 +103,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
return this->getPathFormula().check(modelChecker, qualitative);
}
};
diff --git a/src/formula/Csl/SteadyStateBoundOperator.h b/src/formula/Csl/SteadyStateBoundOperator.h
index 5120b632c..a63c64196 100644
--- a/src/formula/Csl/SteadyStateBoundOperator.h
+++ b/src/formula/Csl/SteadyStateBoundOperator.h
@@ -35,7 +35,7 @@ class ISteadyStateBoundOperatorModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkSteadyStateBoundOperator(const SteadyStateBoundOperator<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkSteadyStateBoundOperator(const SteadyStateBoundOperator<T>& obj) const = 0;
};
/*!
@@ -105,7 +105,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<ISteadyStateBoundOperatorModelChecker>()->checkSteadyStateBoundOperator(*this);
}
diff --git a/src/formula/Csl/SteadyStateNoBoundOperator.h b/src/formula/Csl/SteadyStateNoBoundOperator.h
index 47485256d..b92526d47 100644
--- a/src/formula/Csl/SteadyStateNoBoundOperator.h
+++ b/src/formula/Csl/SteadyStateNoBoundOperator.h
@@ -33,7 +33,7 @@ class ISteadyStateNoBoundOperatorModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkSteadyStateNoBoundOperator(const SteadyStateNoBoundOperator<T>& obj) const = 0;
+ virtual std::vector<T> checkSteadyStateNoBoundOperator(const SteadyStateNoBoundOperator<T>& obj) const = 0;
};
template <class T>
@@ -87,7 +87,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
return modelChecker.template as<ISteadyStateNoBoundOperatorModelChecker>()->checkSteadyStateNoBoundOperator(*this);
}
diff --git a/src/formula/Csl/TimeBoundedEventually.h b/src/formula/Csl/TimeBoundedEventually.h
index edce482d9..3b443938a 100644
--- a/src/formula/Csl/TimeBoundedEventually.h
+++ b/src/formula/Csl/TimeBoundedEventually.h
@@ -33,7 +33,7 @@ class ITimeBoundedEventuallyModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkTimeBoundedEventually(const TimeBoundedEventually<T>& obj, bool qualitative) const = 0;
+ virtual std::vector<T> checkTimeBoundedEventually(const TimeBoundedEventually<T>& obj, bool qualitative) const = 0;
};
@@ -85,7 +85,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*this, qualitative);
}
};
diff --git a/src/formula/Csl/TimeBoundedUntil.h b/src/formula/Csl/TimeBoundedUntil.h
index 54a660169..7b2044daa 100644
--- a/src/formula/Csl/TimeBoundedUntil.h
+++ b/src/formula/Csl/TimeBoundedUntil.h
@@ -33,7 +33,7 @@ class ITimeBoundedUntilModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkTimeBoundedUntil(const TimeBoundedUntil<T>& obj, bool qualitative) const = 0;
+ virtual std::vector<T> checkTimeBoundedUntil(const TimeBoundedUntil<T>& obj, bool qualitative) const = 0;
};
template <class T>
@@ -99,7 +99,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*this, qualitative);
}
};
diff --git a/src/formula/Csl/Until.h b/src/formula/Csl/Until.h
index 16f62611e..6f6d68086 100644
--- a/src/formula/Csl/Until.h
+++ b/src/formula/Csl/Until.h
@@ -34,7 +34,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkUntil(const Until<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -113,7 +113,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
}
};
diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h
index 8286f75db..65c31bdef 100644
--- a/src/formula/Ltl/AbstractLtlFormula.h
+++ b/src/formula/Ltl/AbstractLtlFormula.h
@@ -55,7 +55,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const = 0;
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const = 0;
/*!
* Clones the called object.
diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h
index 887941d6f..f7c901de3 100644
--- a/src/formula/Ltl/And.h
+++ b/src/formula/Ltl/And.h
@@ -35,7 +35,7 @@ class IAndModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkAnd(const And<T>& obj) const = 0;
+ virtual std::vector<T> checkAnd(const And<T>& obj) const = 0;
};
/*!
@@ -131,7 +131,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h
index e978d9d32..d5a0069f8 100644
--- a/src/formula/Ltl/Ap.h
+++ b/src/formula/Ltl/Ap.h
@@ -32,7 +32,7 @@ class IApModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkAp(const Ap<T>& obj) const = 0;
+ virtual std::vector<T> checkAp(const Ap<T>& obj) const = 0;
};
@@ -103,7 +103,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h
index 3dbbf1849..2cbbc4c4a 100644
--- a/src/formula/Ltl/BoundedEventually.h
+++ b/src/formula/Ltl/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) const = 0;
};
/*!
@@ -130,7 +130,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
}
diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h
index 64e594085..8d6f2fcf3 100644
--- a/src/formula/Ltl/BoundedUntil.h
+++ b/src/formula/Ltl/BoundedUntil.h
@@ -35,7 +35,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) const = 0;
};
/*!
@@ -147,7 +147,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
}
diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h
index 2988b2ac4..2ca73607c 100644
--- a/src/formula/Ltl/Eventually.h
+++ b/src/formula/Ltl/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) const = 0;
};
/*!
@@ -124,7 +124,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
}
diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h
index 17ba20674..21bacaf14 100644
--- a/src/formula/Ltl/Globally.h
+++ b/src/formula/Ltl/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) const = 0;
};
/*!
@@ -126,7 +126,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
}
diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h
index 1e7bcfb9f..44d98e12f 100644
--- a/src/formula/Ltl/Next.h
+++ b/src/formula/Ltl/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) const = 0;
};
/*!
@@ -124,7 +124,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INextModelChecker>()->checkNext(*this);
}
diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h
index 915e9ac19..bcf510999 100644
--- a/src/formula/Ltl/Not.h
+++ b/src/formula/Ltl/Not.h
@@ -33,7 +33,7 @@ class INotModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkNot(const Not<T>& obj) const = 0;
+ virtual std::vector<T> checkNot(const Not<T>& obj) const = 0;
};
/*!
@@ -120,7 +120,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h
index 0693c598d..511420d5d 100644
--- a/src/formula/Ltl/Or.h
+++ b/src/formula/Ltl/Or.h
@@ -32,7 +32,7 @@ class IOrModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkOr(const Or<T>& obj) const = 0;
+ virtual std::vector<T> checkOr(const Or<T>& obj) const = 0;
};
/*!
@@ -125,7 +125,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h
index d64b373e1..359e64a0a 100644
--- a/src/formula/Ltl/Until.h
+++ b/src/formula/Ltl/Until.h
@@ -33,7 +33,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) const = 0;
};
/*!
@@ -141,7 +141,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
}
diff --git a/src/formula/Prctl/AbstractNoBoundOperator.h b/src/formula/Prctl/AbstractNoBoundOperator.h
index e28c0df34..c73c4ed6f 100644
--- a/src/formula/Prctl/AbstractNoBoundOperator.h
+++ b/src/formula/Prctl/AbstractNoBoundOperator.h
@@ -33,7 +33,7 @@ public:
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkNoBoundOperator(const AbstractNoBoundOperator<T>& obj) const = 0;
+ virtual std::vector<T> checkNoBoundOperator(const AbstractNoBoundOperator<T>& obj) const = 0;
};
@@ -74,7 +74,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
};
} /* namespace prctl */
diff --git a/src/formula/Prctl/AbstractPathFormula.h b/src/formula/Prctl/AbstractPathFormula.h
index 62c788452..c3c2cfc1b 100644
--- a/src/formula/Prctl/AbstractPathFormula.h
+++ b/src/formula/Prctl/AbstractPathFormula.h
@@ -66,7 +66,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
};
} //namespace prctl
diff --git a/src/formula/Prctl/AbstractStateFormula.h b/src/formula/Prctl/AbstractStateFormula.h
index d06c48b30..0a313bfd1 100644
--- a/src/formula/Prctl/AbstractStateFormula.h
+++ b/src/formula/Prctl/AbstractStateFormula.h
@@ -61,7 +61,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const = 0;
+ virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const = 0;
};
} //namespace prctl
diff --git a/src/formula/Prctl/And.h b/src/formula/Prctl/And.h
index 8bdfb148a..eca17d73d 100644
--- a/src/formula/Prctl/And.h
+++ b/src/formula/Prctl/And.h
@@ -35,7 +35,7 @@ class IAndModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkAnd(const And<T>& obj) const = 0;
};
/*!
@@ -114,7 +114,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
diff --git a/src/formula/Prctl/Ap.h b/src/formula/Prctl/Ap.h
index 898d78f13..d2df03951 100644
--- a/src/formula/Prctl/Ap.h
+++ b/src/formula/Prctl/Ap.h
@@ -34,7 +34,7 @@ class IApModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkAp(const Ap<T>& obj) const = 0;
};
/*!
@@ -91,7 +91,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h
index 32825a23c..870d88e1d 100644
--- a/src/formula/Prctl/BoundedEventually.h
+++ b/src/formula/Prctl/BoundedEventually.h
@@ -37,7 +37,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkBoundedEventually(const BoundedEventually<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -114,7 +114,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h
index ed865c98c..e01169496 100644
--- a/src/formula/Prctl/BoundedNaryUntil.h
+++ b/src/formula/Prctl/BoundedNaryUntil.h
@@ -40,7 +40,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -128,7 +128,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
}
diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h
index 2bc4b8f49..f17c9b743 100644
--- a/src/formula/Prctl/BoundedUntil.h
+++ b/src/formula/Prctl/BoundedUntil.h
@@ -36,7 +36,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkBoundedUntil(const BoundedUntil<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -119,7 +119,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h
index 3cca28792..e1db7cb21 100644
--- a/src/formula/Prctl/CumulativeReward.h
+++ b/src/formula/Prctl/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, bool qualitative) const = 0;
+ virtual std::vector<T> checkCumulativeReward(const CumulativeReward<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -98,7 +98,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h
index 27fc77213..4a0624df6 100644
--- a/src/formula/Prctl/Eventually.h
+++ b/src/formula/Prctl/Eventually.h
@@ -34,7 +34,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -108,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h
index db507bd53..272bbab26 100644
--- a/src/formula/Prctl/Globally.h
+++ b/src/formula/Prctl/Globally.h
@@ -35,7 +35,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -110,7 +110,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h
index a1905d4ae..b28effffe 100644
--- a/src/formula/Prctl/InstantaneousReward.h
+++ b/src/formula/Prctl/InstantaneousReward.h
@@ -36,7 +36,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkInstantaneousReward(const InstantaneousReward<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -99,7 +99,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h
index 498fd2b86..7197da30c 100644
--- a/src/formula/Prctl/Next.h
+++ b/src/formula/Prctl/Next.h
@@ -34,7 +34,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkNext(const Next<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -108,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h
index 18c6c3c03..7f6a992ab 100644
--- a/src/formula/Prctl/Not.h
+++ b/src/formula/Prctl/Not.h
@@ -34,7 +34,7 @@ class INotModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkNot(const Not<T>& obj) const = 0;
};
/*!
@@ -104,7 +104,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
};
diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h
index 799d2000c..a13c385e3 100644
--- a/src/formula/Prctl/Or.h
+++ b/src/formula/Prctl/Or.h
@@ -33,7 +33,7 @@ class IOrModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkOr(const Or<T>& obj) const = 0;
};
/*!
@@ -113,7 +113,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
};
diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h
index d65611b8d..5f6253e93 100644
--- a/src/formula/Prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticBoundOperator.h
@@ -28,7 +28,7 @@ template <class T> class ProbabilisticBoundOperator;
template <class T>
class IProbabilisticBoundOperatorModelChecker {
public:
- virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
};
/*!
@@ -127,7 +127,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
}
};
diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
index 1f3a5f24f..5591a9555 100644
--- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
@@ -103,7 +103,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
return this->getPathFormula().check(modelChecker, qualitative);
}
};
diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h
index c75ff21fc..d0bcdfc69 100644
--- a/src/formula/Prctl/ReachabilityReward.h
+++ b/src/formula/Prctl/ReachabilityReward.h
@@ -34,7 +34,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkReachabilityReward(const ReachabilityReward<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -105,7 +105,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h
index 412371c10..5aa4d83c0 100644
--- a/src/formula/Prctl/RewardBoundOperator.h
+++ b/src/formula/Prctl/RewardBoundOperator.h
@@ -28,7 +28,7 @@ template <class T> class RewardBoundOperator;
template <class T>
class IRewardBoundOperatorModelChecker {
public:
- virtual storm::storage::BitVector* checkRewardBoundOperator(const RewardBoundOperator<T>& obj) const = 0;
+ virtual storm::storage::BitVector checkRewardBoundOperator(const RewardBoundOperator<T>& obj) const = 0;
};
/*!
@@ -120,7 +120,7 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
+ virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IRewardBoundOperatorModelChecker>()->checkRewardBoundOperator(*this);
}
};
diff --git a/src/formula/Prctl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h
index 676517b0b..97a8dfeaa 100644
--- a/src/formula/Prctl/RewardNoBoundOperator.h
+++ b/src/formula/Prctl/RewardNoBoundOperator.h
@@ -96,7 +96,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const override {
return this->getPathFormula().check(modelChecker, qualitative);
}
};
diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h
index 958537a45..f7c87e90d 100644
--- a/src/formula/Prctl/SteadyStateReward.h
+++ b/src/formula/Prctl/SteadyStateReward.h
@@ -35,7 +35,7 @@ class ISteadyStateRewardModelChecker {
* @param obj Formula object with subformulas.
* @return Result of the formula for every node.
*/
- virtual std::vector<T>* checkSteadyStateReward(const SteadyStateReward<T>& obj, bool qualitative) const = 0;
+ virtual std::vector<T> checkSteadyStateReward(const SteadyStateReward<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -80,7 +80,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<ISteadyStateRewardModelChecker>()->checkSteadyStateReward(*this, qualitative);
}
};
diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h
index 643c174d3..53fb92f6b 100644
--- a/src/formula/Prctl/Until.h
+++ b/src/formula/Prctl/Until.h
@@ -34,7 +34,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, bool qualitative) const = 0;
+ virtual std::vector<T> checkUntil(const Until<T>& obj, bool qualitative) const = 0;
};
/*!
@@ -113,7 +113,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
+ virtual std::vector<T> check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const override {
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
}
};
diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h
index e25cd52f5..67c9e512f 100644
--- a/src/modelchecker/csl/AbstractModelChecker.h
+++ b/src/modelchecker/csl/AbstractModelChecker.h
@@ -185,11 +185,11 @@ public:
* @param formula The formula to be checked.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkAp(storm::property::csl::Ap<Type> const& formula) const {
+ storm::storage::BitVector checkAp(storm::property::csl::Ap<Type> const& formula) const {
if (formula.getAp() == "true") {
- return new storm::storage::BitVector(model.getNumberOfStates(), true);
+ return storm::storage::BitVector(model.getNumberOfStates(), true);
} else if (formula.getAp() == "false") {
- return new storm::storage::BitVector(model.getNumberOfStates());
+ return storm::storage::BitVector(model.getNumberOfStates());
}
if (!model.hasAtomicProposition(formula.getAp())) {
@@ -197,7 +197,7 @@ public:
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
}
- return new storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
+ return storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
}
/*!
@@ -206,11 +206,10 @@ public:
* @param formula The formula to be checked.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkAnd(storm::property::csl::And<Type> const& formula) const {
- storm::storage::BitVector* result = formula.getLeft().check(*this);
- storm::storage::BitVector* right = formula.getRight().check(*this);
- (*result) &= (*right);
- delete right;
+ storm::storage::BitVector checkAnd(storm::property::csl::And<Type> const& formula) const {
+ storm::storage::BitVector result = formula.getLeft().check(*this);
+ storm::storage::BitVector right = formula.getRight().check(*this);
+ result &= right;
return result;
}
@@ -220,11 +219,10 @@ public:
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- virtual storm::storage::BitVector* checkOr(storm::property::csl::Or<Type> const& formula) const {
- storm::storage::BitVector* result = formula.getLeft().check(*this);
- storm::storage::BitVector* right = formula.getRight().check(*this);
- (*result) |= (*right);
- delete right;
+ virtual storm::storage::BitVector checkOr(storm::property::csl::Or<Type> const& formula) const {
+ storm::storage::BitVector result = formula.getLeft().check(*this);
+ storm::storage::BitVector right = formula.getRight().check(*this);
+ result |= right;
return result;
}
@@ -234,9 +232,9 @@ public:
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkNot(const storm::property::csl::Not<Type>& formula) const {
- storm::storage::BitVector* result = formula.getChild().check(*this);
- result->complement();
+ storm::storage::BitVector checkNot(const storm::property::csl::Not<Type>& formula) const {
+ storm::storage::BitVector result = formula.getChild().check(*this);
+ result.complement();
return result;
}
@@ -247,23 +245,21 @@ public:
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator<Type> const& formula) const {
+ storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator<Type> const& 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, false);
+ std::vector<Type> quantitativeResult = formula.getPathFormula().check(*this, false);
// Create resulting bit vector that will hold the yes/no-answer for every state.
- storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size());
+ storm::storage::BitVector result(quantitativeResult.size());
// Now, we can compute which states meet the bound specified in this operator and set the
// corresponding bits to true in the resulting vector.
- for (uint_fast64_t i = 0; i < quantitativeResult->size(); ++i) {
- if (formula.meetsBound((*quantitativeResult)[i])) {
- result->set(i, true);
+ for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) {
+ if (formula.meetsBound(quantitativeResult[i])) {
+ result.set(i, true);
}
}
- // Delete the probabilities computed for the states and return result.
- delete quantitativeResult;
return result;
}
diff --git a/src/modelchecker/ltl/AbstractModelChecker.h b/src/modelchecker/ltl/AbstractModelChecker.h
index 6ed75ceb0..9a0459181 100644
--- a/src/modelchecker/ltl/AbstractModelChecker.h
+++ b/src/modelchecker/ltl/AbstractModelChecker.h
@@ -140,19 +140,15 @@ public:
* @param formula The formula to be checked.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- virtual std::vector<Type>* checkAp(storm::property::ltl::Ap<Type> const& formula) const {
- return nullptr;
- }
-
+ virtual std::vector<Type> checkAp(storm::property::ltl::Ap<Type> const& formula) const = 0;
+
/*!
* Checks the given formula that is a logical "and" of two formulae.
*
* @param formula The formula to be checked.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- virtual std::vector<Type>* checkAnd(storm::property::ltl::And<Type> const& formula) const {
- return nullptr;
- }
+ virtual std::vector<Type> checkAnd(storm::property::ltl::And<Type> const& formula) const = 0;
/*!
* Checks the given formula that is a logical "or" of two formulae.
@@ -160,20 +156,16 @@ public:
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- virtual std::vector<Type>* checkOr(storm::property::ltl::Or<Type> const& formula) const {
- return nullptr;
- }
-
+ virtual std::vector<Type> checkOr(storm::property::ltl::Or<Type> const& formula) const = 0;
+
/*!
* Checks the given formula that is a logical "not" of a sub-formula.
*
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- virtual std::vector<Type>* checkNot(const storm::property::ltl::Not<Type>& formula) const {
- return nullptr;
- }
-
+ virtual std::vector<Type> checkNot(const storm::property::ltl::Not<Type>& formula) const = 0;
+
private:
/*!
diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h
index b3ae46bd2..7a2bf666e 100644
--- a/src/modelchecker/prctl/AbstractModelChecker.h
+++ b/src/modelchecker/prctl/AbstractModelChecker.h
@@ -208,11 +208,11 @@ public:
* @param formula The formula to be checked.
* @return The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkAp(storm::property::prctl::Ap<Type> const& formula) const {
+ storm::storage::BitVector checkAp(storm::property::prctl::Ap<Type> const& formula) const {
if (formula.getAp() == "true") {
- return new storm::storage::BitVector(model.getNumberOfStates(), true);
+ return storm::storage::BitVector(model.getNumberOfStates(), true);
} else if (formula.getAp() == "false") {
- return new storm::storage::BitVector(model.getNumberOfStates());
+ return storm::storage::BitVector(model.getNumberOfStates());
}
if (!model.hasAtomicProposition(formula.getAp())) {
@@ -220,7 +220,7 @@ public:
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
}
- return new storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
+ return storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
}
/*!
@@ -229,11 +229,10 @@ public:
* @param formula The formula to be checked.
* @return The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkAnd(storm::property::prctl::And<Type> const& formula) const {
- storm::storage::BitVector* result = formula.getLeft().check(*this);
- storm::storage::BitVector* right = formula.getRight().check(*this);
- (*result) &= (*right);
- delete right;
+ storm::storage::BitVector checkAnd(storm::property::prctl::And<Type> const& formula) const {
+ storm::storage::BitVector result = formula.getLeft().check(*this);
+ storm::storage::BitVector right = formula.getRight().check(*this);
+ result &= right;
return result;
}
@@ -243,11 +242,10 @@ public:
* @param formula The formula to check.
* @return The set of states satisfying the formula represented by a bit vector.
*/
- virtual storm::storage::BitVector* checkOr(storm::property::prctl::Or<Type> const& formula) const {
- storm::storage::BitVector* result = formula.getLeft().check(*this);
- storm::storage::BitVector* right = formula.getRight().check(*this);
- (*result) |= (*right);
- delete right;
+ virtual storm::storage::BitVector checkOr(storm::property::prctl::Or<Type> const& formula) const {
+ storm::storage::BitVector result = formula.getLeft().check(*this);
+ storm::storage::BitVector right = formula.getRight().check(*this);
+ result |= right;
return result;
}
@@ -257,9 +255,9 @@ public:
* @param formula The formula to check.
* @return The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkNot(const storm::property::prctl::Not<Type>& formula) const {
- storm::storage::BitVector* result = formula.getChild().check(*this);
- result->complement();
+ storm::storage::BitVector checkNot(const storm::property::prctl::Not<Type>& formula) const {
+ storm::storage::BitVector result = formula.getChild().check(*this);
+ result.complement();
return result;
}
@@ -270,23 +268,21 @@ public:
* @param formula The formula to check.
* @return The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& formula) const {
+ storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& 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, false);
+ std::vector<Type> quantitativeResult = formula.getPathFormula().check(*this, false);
// Create resulting bit vector that will hold the yes/no-answer for every state.
- storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size());
+ storm::storage::BitVector result(quantitativeResult.size());
// Now, we can compute which states meet the bound specified in this operator and set the
// corresponding bits to true in the resulting vector.
- for (uint_fast64_t i = 0; i < quantitativeResult->size(); ++i) {
- if (formula.meetsBound((*quantitativeResult)[i])) {
- result->set(i, true);
+ for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) {
+ if (formula.meetsBound(quantitativeResult[i])) {
+ result.set(i, true);
}
}
- // Delete the probabilities computed for the states and return result.
- delete quantitativeResult;
return result;
}
@@ -296,23 +292,21 @@ public:
* @param formula The formula to check.
* @return The set of states satisfying the formula represented by a bit vector.
*/
- storm::storage::BitVector* checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator<Type>& formula) const {
+ storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::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, false);
+ std::vector<Type> quantitativeResult = formula.getPathFormula().check(*this, false);
// Create resulting bit vector that will hold the yes/no-answer for every state.
- storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size());
+ storm::storage::BitVector result(quantitativeResult.size());
// Now, we can compute which states meet the bound specified in this operator and set the
// corresponding bits to true in the resulting vector.
- for (uint_fast64_t i = 0; i < quantitativeResult->size(); ++i) {
- if (formula.meetsBound((*quantitativeResult)[i])) {
- result->set(i, true);
+ for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) {
+ if (formula.meetsBound(quantitativeResult[i])) {
+ result.set(i, true);
}
}
- // Delete the probabilities computed for the states and return result.
- delete quantitativeResult;
return result;
}
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index 23e18f4fc..01e1eb8eb 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@@ -66,7 +66,7 @@ public:
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- std::vector<Type>* checkNoBoundOperator(storm::property::prctl::AbstractNoBoundOperator<Type> const& formula) const {
+ std::vector<Type> checkNoBoundOperator(storm::property::prctl::AbstractNoBoundOperator<Type> const& formula) const {
// Check if the operator was an optimality operator and report a warning in that case.
if (formula.isOptimalityOperator()) {
LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");
@@ -85,15 +85,15 @@ public:
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkBoundedUntil(storm::property::prctl::BoundedUntil<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkBoundedUntil(storm::property::prctl::BoundedUntil<Type> const& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula.
- storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
- storm::storage::BitVector* rightStates = formula.getRight().check(*this);
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ storm::storage::BitVector leftStates = formula.getLeft().check(*this);
+ storm::storage::BitVector rightStates = formula.getRight().check(*this);
+ std::vector<Type> result(this->getModel().getNumberOfStates());
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the
// further analysis.
- storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates, true, formula.getBound());
+ storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), leftStates, rightStates, true, formula.getBound());
LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
// Check if we already know the result (i.e. probability 0) for all initial states and
@@ -103,7 +103,7 @@ public:
<< " No exact probabilities were computed.");
// Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and
// not necessarily 1).
- storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, Type(0.5));
+ storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, Type(0.5));
} else {
// In this case we have have to compute the probabilities.
@@ -111,7 +111,7 @@ public:
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system.
- storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % *rightStates;
+ storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % rightStates;
// Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
@@ -128,13 +128,10 @@ public:
}
// Set the values of the resulting vector accordingly.
- storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, subresult);
- storm::utility::vector::setVectorValues<Type>(*result, ~statesWithProbabilityGreater0, storm::utility::constGetZero<Type>());
+ storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
+ storm::utility::vector::setVectorValues<Type>(result, ~statesWithProbabilityGreater0, storm::utility::constGetZero<Type>());
}
- // Delete obsolete intermediates and return result.
- delete leftStates;
- delete rightStates;
return result;
}
@@ -149,25 +146,21 @@ public:
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkNext(storm::property::prctl::Next<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkNext(storm::property::prctl::Next<Type> const& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the child formula of the next-formula.
- storm::storage::BitVector* nextStates = formula.getChild().check(*this);
+ storm::storage::BitVector nextStates = formula.getChild().check(*this);
// Create the vector with which to multiply and initialize it correctly.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
- storm::utility::vector::setVectorValues(*result, *nextStates, storm::utility::constGetOne<Type>());
-
- // Delete obsolete intermediate.
- delete nextStates;
+ std::vector<Type> result(this->getModel().getNumberOfStates());
+ storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constGetOne<Type>());
// Perform one single matrix-vector multiplication.
if (linearEquationSolver != nullptr) {
- this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result);
+ this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result);
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
- // Return result.
return result;
}
@@ -182,7 +175,7 @@ public:
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkBoundedEventually(storm::property::prctl::BoundedEventually<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkBoundedEventually(storm::property::prctl::BoundedEventually<Type> const& formula, bool qualitative) const {
// Create equivalent temporary bounded until formula and check it.
storm::property::prctl::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::property::prctl::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
@@ -199,7 +192,7 @@ public:
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkEventually(storm::property::prctl::Eventually<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkEventually(storm::property::prctl::Eventually<Type> const& formula, bool qualitative) const {
// Create equivalent temporary until formula and check it.
storm::property::prctl::Until<Type> temporaryUntilFormula(new storm::property::prctl::Ap<Type>("true"), formula.getChild().clone());
return this->checkUntil(temporaryUntilFormula, qualitative);
@@ -216,13 +209,13 @@ public:
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkGlobally(storm::property::prctl::Globally<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkGlobally(storm::property::prctl::Globally<Type> const& formula, bool qualitative) const {
// Create "equivalent" (equivalent up to negation) temporary eventually formula and check it.
storm::property::prctl::Eventually<Type> temporaryEventuallyFormula(new storm::property::prctl::Not<Type>(formula.getChild().clone()));
- std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative);
+ std::vector<Type> result = this->checkEventually(temporaryEventuallyFormula, qualitative);
// Now subtract the resulting vector from the constant one vector to obtain final result.
- storm::utility::vector::subtractFromConstantOneVector(*result);
+ storm::utility::vector::subtractFromConstantOneVector(result);
return result;
}
@@ -237,20 +230,16 @@ public:
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkUntil(storm::property::prctl::Until<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkUntil(storm::property::prctl::Until<Type> const& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
- storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
- storm::storage::BitVector* rightStates = formula.getRight().check(*this);
+ 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.
- std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), *leftStates, *rightStates);
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), leftStates, rightStates);
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
-
- // Delete intermediate results that are obsolete now.
- delete leftStates;
- delete rightStates;
// Perform some logging.
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
@@ -259,7 +248,7 @@ public:
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact probabilities for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
@@ -271,7 +260,7 @@ public:
}
// Set the values for all maybe-states to 0.5 to indicate that their probability values
// are neither 0 nor 1.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, Type(0.5));
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, Type(0.5));
} else {
// In this case we have have to compute the probabilities.
@@ -298,12 +287,12 @@ public:
}
// Set values of resulting vector according to result.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
}
// Set values of resulting vector that are known exactly.
- storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability0, storm::utility::constGetZero<Type>());
- storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability1, storm::utility::constGetOne<Type>());
+ storm::utility::vector::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+ storm::utility::vector::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
return result;
}
@@ -319,7 +308,7 @@ public:
* @returns The reward values for the given formula for every state of the model associated with this model
* checker. If the qualitative flag is set, exact values might not be computed.
*/
- virtual std::vector<Type>* checkInstantaneousReward(storm::property::prctl::InstantaneousReward<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkInstantaneousReward(storm::property::prctl::InstantaneousReward<Type> const& 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.");
@@ -327,16 +316,15 @@ public:
}
// Initialize result to state rewards of the model.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getStateRewardVector());
+ std::vector<Type> result(this->getModel().getStateRewardVector());
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
if (linearEquationSolver != nullptr) {
- this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
+ this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, nullptr, formula.getBound());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
- // Return result.
return result;
}
@@ -351,7 +339,7 @@ public:
* @returns The reward values for the given formula for every state of the model associated with this model
* checker. If the qualitative flag is set, exact values might not be computed.
*/
- virtual std::vector<Type>* checkCumulativeReward(storm::property::prctl::CumulativeReward<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkCumulativeReward(storm::property::prctl::CumulativeReward<Type> const& 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.");
@@ -370,21 +358,20 @@ public:
}
// Initialize result to either the state rewards of the model or the null vector.
- std::vector<Type>* result = nullptr;
+ std::vector<Type> result;
if (this->getModel().hasStateRewards()) {
- result = new std::vector<Type>(this->getModel().getStateRewardVector());
+ result = std::vector<Type>(this->getModel().getStateRewardVector());
} else {
- result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ result.resize(this->getModel().getNumberOfStates());
}
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
if (linearEquationSolver != nullptr) {
- this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound());
+ this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
- // Return result.
return result;
}
@@ -399,7 +386,7 @@ public:
* @returns The reward values for the given formula for every state of the model associated with this model
* checker. If the qualitative flag is set, exact values might not be computed.
*/
- virtual std::vector<Type>* checkReachabilityReward(storm::property::prctl::ReachabilityReward<Type> const& formula, bool qualitative) const {
+ virtual std::vector<Type> checkReachabilityReward(storm::property::prctl::ReachabilityReward<Type> const& 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");
@@ -407,19 +394,19 @@ public:
}
// Determine the states for which the target predicate holds.
- storm::storage::BitVector* targetStates = formula.getChild().check(*this);
+ storm::storage::BitVector targetStates = formula.getChild().check(*this);
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
- storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, *targetStates);
+ storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, targetStates);
infinityStates.complement();
- storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
+ storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
- LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states.");
+ LOG4CPLUS_INFO(logger, "Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact rewards for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates)) {
@@ -427,7 +414,7 @@ public:
<< " No exact rewards were computed.");
// Set the values for all maybe-states to 1 to indicate that their reward values
// are neither 0 nor infinity.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, storm::utility::constGetOne<Type>());
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, storm::utility::constGetOne<Type>());
} else {
// In this case we have to compute the reward values for the remaining states.
// We can eliminate the rows and columns from the original transition probability matrix.
@@ -474,15 +461,13 @@ public:
}
// Set values of resulting vector according to result.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
}
// Set values of resulting vector that are known exactly.
- storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero<Type>());
- storm::utility::vector::setVectorValues(*result, infinityStates, storm::utility::constGetInfinity<Type>());
+ storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constGetZero<Type>());
+ storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
- // Delete temporary storages and return result.
- delete targetStates;
return result;
}
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index 2d55539e1..e6a4ff69c 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -63,14 +63,14 @@ namespace storm {
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
*/
- virtual std::vector<Type>* checkNoBoundOperator(const storm::property::prctl::AbstractNoBoundOperator<Type>& formula) const {
+ virtual std::vector<Type> checkNoBoundOperator(const storm::property::prctl::AbstractNoBoundOperator<Type>& formula) const {
// Check if the operator was an non-optimality operator and report an error in that case.
if (!formula.isOptimalityOperator()) {
LOG4CPLUS_ERROR(logger, "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());
- std::vector<Type>* result = formula.check(*this, false);
+ std::vector<Type> result = formula.check(*this, false);
minimumOperatorStack.pop();
return result;
}
@@ -86,18 +86,18 @@ namespace storm {
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkBoundedUntil(const storm::property::prctl::BoundedUntil<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkBoundedUntil(const storm::property::prctl::BoundedUntil<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
- storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
- storm::storage::BitVector* rightStates = formula.getRight().check(*this);
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ storm::storage::BitVector leftStates = formula.getLeft().check(*this);
+ storm::storage::BitVector rightStates = formula.getRight().check(*this);
+ std::vector<Type> result(this->getModel().getNumberOfStates());
// Determine the states that have 0 probability of reaching the target states.
storm::storage::BitVector statesWithProbabilityGreater0;
if (this->minimumOperatorStack.top()) {
- statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound());
+ statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(this->getModel(), this->getModel().getBackwardTransitions(), leftStates, rightStates, true, formula.getBound());
} else {
- statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(this->getModel(), this->getModel().getBackwardTransitions(), *leftStates, *rightStates, true, formula.getBound());
+ statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(this->getModel(), this->getModel().getBackwardTransitions(), leftStates, rightStates, true, formula.getBound());
}
// Check if we already know the result (i.e. probability 0) for all initial states and
@@ -107,7 +107,7 @@ namespace storm {
<< " No exact probabilities were computed.");
// Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and
// not necessarily 1).
- storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, Type(0.5));
+ storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, Type(0.5));
} else {
// In this case we have have to compute the probabilities.
@@ -118,7 +118,7 @@ namespace storm {
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system.
- storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % *rightStates;
+ storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % rightStates;
// Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices);
@@ -134,13 +134,10 @@ namespace storm {
}
// Set the values of the resulting vector accordingly.
- storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, subresult);
- storm::utility::vector::setVectorValues(*result, ~statesWithProbabilityGreater0, storm::utility::constGetZero<Type>());
+ storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
+ storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::constGetZero<Type>());
}
- // Delete intermediate results and return result.
- delete leftStates;
- delete rightStates;
return result;
}
@@ -155,24 +152,20 @@ namespace storm {
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkNext(const storm::property::prctl::Next<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkNext(const storm::property::prctl::Next<Type>& formula, bool qualitative) const {
// First, we need to compute the states that satisfy the sub-formula of the next-formula.
- storm::storage::BitVector* nextStates = formula.getChild().check(*this);
+ storm::storage::BitVector nextStates = formula.getChild().check(*this);
// Create the vector with which to multiply and initialize it correctly.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
- storm::utility::vector::setVectorValues(*result, *nextStates, storm::utility::constGetOne<Type>());
-
- // Delete obsolete sub-result.
- delete nextStates;
+ std::vector<Type> result(this->getModel().getNumberOfStates());
+ storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constGetOne<Type>());
if (linearEquationSolver != nullptr) {
- this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices());
+ this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
- // Return result.
return result;
}
@@ -187,7 +180,7 @@ namespace storm {
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkBoundedEventually(const storm::property::prctl::BoundedEventually<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkBoundedEventually(const storm::property::prctl::BoundedEventually<Type>& formula, bool qualitative) const {
// Create equivalent temporary bounded until formula and check it.
storm::property::prctl::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::property::prctl::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
@@ -204,7 +197,7 @@ namespace storm {
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkEventually(const storm::property::prctl::Eventually<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkEventually(const storm::property::prctl::Eventually<Type>& formula, bool qualitative) const {
// Create equivalent temporary until formula and check it.
storm::property::prctl::Until<Type> temporaryUntilFormula(new storm::property::prctl::Ap<Type>("true"), formula.getChild().clone());
return this->checkUntil(temporaryUntilFormula, qualitative);
@@ -221,13 +214,13 @@ namespace storm {
* @returns The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkGlobally(const storm::property::prctl::Globally<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkGlobally(const storm::property::prctl::Globally<Type>& formula, bool qualitative) const {
// Create "equivalent" temporary eventually formula and check it.
storm::property::prctl::Eventually<Type> temporaryEventuallyFormula(new storm::property::prctl::Not<Type>(formula.getChild().clone()));
- std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative);
+ std::vector<Type> result = this->checkEventually(temporaryEventuallyFormula, qualitative);
// Now subtract the resulting vector from the constant one vector to obtain final result.
- storm::utility::vector::subtractFromConstantOneVector(*result);
+ storm::utility::vector::subtractFromConstantOneVector(result);
return result;
}
@@ -245,7 +238,7 @@ namespace storm {
* @return The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkUntil(const storm::property::prctl::Until<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkUntil(const storm::property::prctl::Until<Type>& formula, bool qualitative) const {
return this->checkUntil(this->minimumOperatorStack.top(), formula, qualitative, nullptr);
}
@@ -264,18 +257,18 @@ namespace storm {
* @return The probabilities for the given formula to hold on every state of the model associated with this model
* checker. If the qualitative flag is set, exact probabilities might not be computed.
*/
- virtual std::vector<Type>* checkUntil(bool minimize, const storm::property::prctl::Until<Type>& formula, bool qualitative, std::vector<uint_fast64_t>* scheduler) const {
+ virtual std::vector<Type> checkUntil(bool minimize, const storm::property::prctl::Until<Type>& formula, bool qualitative, std::vector<uint_fast64_t>* scheduler) const {
// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
- storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
- storm::storage::BitVector* rightStates = formula.getRight().check(*this);
+ 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.
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
if (minimize) {
- statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel(), *leftStates, *rightStates);
+ statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel(), leftStates, rightStates);
} else {
- statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel(), *leftStates, *rightStates);
+ statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel(), leftStates, rightStates);
}
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
@@ -286,7 +279,7 @@ namespace storm {
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact probabilities for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
@@ -298,7 +291,7 @@ namespace storm {
}
// Set the values for all maybe-states to 0.5 to indicate that their probability values
// are neither 0 nor 1.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, Type(0.5));
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, Type(0.5));
} else {
// In this case we have have to compute the probabilities.
@@ -324,21 +317,18 @@ namespace storm {
}
// Set values of resulting vector according to result.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
}
// Set values of resulting vector that are known exactly.
- storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability0, storm::utility::constGetZero<Type>());
- storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability1, storm::utility::constGetOne<Type>());
+ storm::utility::vector::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+ storm::utility::vector::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
// If we were required to generate a scheduler, do so now.
if (scheduler != nullptr) {
- this->computeTakenChoices(this->minimumOperatorStack.top(), false, *result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
+ this->computeTakenChoices(this->minimumOperatorStack.top(), false, result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
}
- // Delete sub-results that are obsolete now.
- delete leftStates;
- delete rightStates;
return result;
}
@@ -353,7 +343,7 @@ namespace storm {
* @returns The reward values for the given formula for every state of the model associated with this model
* checker. If the qualitative flag is set, exact values might not be computed.
*/
- virtual std::vector<Type>* checkInstantaneousReward(const storm::property::prctl::InstantaneousReward<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkInstantaneousReward(const storm::property::prctl::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.");
@@ -361,15 +351,14 @@ namespace storm {
}
// Initialize result to state rewards of the model.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getStateRewardVector());
+ std::vector<Type> result(this->getModel().getStateRewardVector());
if (linearEquationSolver != nullptr) {
- this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
+ this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
- // Return result.
return result;
}
@@ -384,7 +373,7 @@ namespace storm {
* @returns The reward values for the given formula for every state of the model associated with this model
* checker. If the qualitative flag is set, exact values might not be computed.
*/
- virtual std::vector<Type>* checkCumulativeReward(const storm::property::prctl::CumulativeReward<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkCumulativeReward(const storm::property::prctl::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.");
@@ -403,20 +392,19 @@ namespace storm {
}
// Initialize result to either the state rewards of the model or the null vector.
- std::vector<Type>* result = nullptr;
+ std::vector<Type> result;
if (this->getModel().hasStateRewards()) {
- result = new std::vector<Type>(this->getModel().getStateRewardVector());
+ result = std::vector<Type>(this->getModel().getStateRewardVector());
} else {
- result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ result.resize(this->getModel().getNumberOfStates());
}
if (linearEquationSolver != nullptr) {
- this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
+ this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
- // Delete temporary variables and return result.
return result;
}
@@ -431,7 +419,7 @@ namespace storm {
* @return The reward values for the given formula for every state of the model associated with this model
* checker. If the qualitative flag is set, exact values might not be computed.
*/
- virtual std::vector<Type>* checkReachabilityReward(const storm::property::prctl::ReachabilityReward<Type>& formula, bool qualitative) const {
+ virtual std::vector<Type> checkReachabilityReward(const storm::property::prctl::ReachabilityReward<Type>& formula, bool qualitative) const {
return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula, qualitative, nullptr);
}
@@ -450,7 +438,7 @@ namespace storm {
* @return The reward values for the given formula for every state of the model associated with this model
* checker. If the qualitative flag is set, exact values might not be computed.
*/
- virtual std::vector<Type>* checkReachabilityReward(bool minimize, const storm::property::prctl::ReachabilityReward<Type>& formula, bool qualitative, std::vector<uint_fast64_t>* scheduler) const {
+ virtual std::vector<Type> checkReachabilityReward(bool minimize, const storm::property::prctl::ReachabilityReward<Type>& formula, bool qualitative, std::vector<uint_fast64_t>* scheduler) 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");
@@ -458,24 +446,24 @@ namespace storm {
}
// Determine the states for which the target predicate holds.
- storm::storage::BitVector* targetStates = formula.getChild().check(*this);
+ storm::storage::BitVector targetStates = formula.getChild().check(*this);
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates;
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
if (minimize) {
- infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates));
+ infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
} else {
- infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates));
+ infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
}
infinityStates.complement();
- storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
+ storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
- LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states.");
+ LOG4CPLUS_INFO(logger, "Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
- std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+ std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact rewards for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates)) {
@@ -483,7 +471,7 @@ namespace storm {
<< " No exact rewards were computed.");
// Set the values for all maybe-states to 1 to indicate that their reward values
// are neither 0 nor infinity.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, storm::utility::constGetOne<Type>());
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, storm::utility::constGetOne<Type>());
} else {
// In this case we have to compute the reward values for the remaining states.
@@ -533,20 +521,18 @@ namespace storm {
}
// Set values of resulting vector according to result.
- storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
+ storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
}
// Set values of resulting vector that are known exactly.
- storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero<Type>());
- storm::utility::vector::setVectorValues(*result, infinityStates, storm::utility::constGetInfinity<Type>());
+ storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constGetZero<Type>());
+ storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
// If we were required to generate a scheduler, do so now.
if (scheduler != nullptr) {
- this->computeTakenChoices(this->minimumOperatorStack.top(), true, *result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
+ this->computeTakenChoices(this->minimumOperatorStack.top(), true, result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
}
- // Delete temporary storages and return result.
- delete targetStates;
return result;
}
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index 6e78f39f2..d36b4d647 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -173,9 +173,8 @@ public:
* Move constructor. Move constructs the bit vector from the given bit vector.
*
*/
- BitVector(BitVector&& bv) : bucketCount(bv.bucketCount), bitCount(bv.bitCount), endIterator(*this, bitCount, bitCount, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) {
+ BitVector(BitVector&& bv) : bucketCount(bv.bucketCount), bitCount(bv.bitCount), bucketArray(bv.bucketArray), endIterator(*this, bitCount, bitCount, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) {
LOG4CPLUS_DEBUG(logger, "Invoking move constructor.");
- this->bucketArray = bv.bucketArray;
bv.bucketArray = nullptr;
}
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 1461da33a..228791409 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -26,14 +26,11 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
- std::vector<double>* result = probFormula->check(mc);
+ std::vector<double> result = probFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("two");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -41,12 +38,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
result = probFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -54,12 +48,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
result = probFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
storm::property::prctl::Ap<double>* done = new storm::property::prctl::Ap<double>("done");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(done);
@@ -67,12 +58,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
result = rewardFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - ((double)11/3)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - ((double)11/3)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
@@ -94,14 +82,11 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
- std::vector<double>* result = probFormula->check(mc);
-
- ASSERT_NE(nullptr, result);
+ std::vector<double> result = probFormula->check(mc);
- ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("observeIGreater1");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -109,12 +94,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
result = probFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.1522194965), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.1522194965), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("observeOnlyTrueSender");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -122,12 +104,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
result = probFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.32153724292835045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
}
TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
@@ -149,14 +128,11 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
- std::vector<double>* result = probFormula->check(mc);
-
- ASSERT_NE(nullptr, result);
+ std::vector<double> result = probFormula->check(mc);
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::property::prctl::BoundedUntil<double>(new storm::property::prctl::Ap<double>("true"), apFormula, 20);
@@ -164,12 +140,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
result = probFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -177,10 +150,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
result = rewardFormula->check(mc);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1.044879046), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.044879046), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index da942de5c..7bd87856f 100644
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -23,14 +23,11 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("two");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -38,10 +35,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -49,10 +45,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -60,10 +55,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -71,10 +65,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -82,10 +75,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -93,10 +85,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -104,10 +95,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula);;
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
storm::parser::AutoParser<double> stateRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
@@ -123,10 +113,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -134,10 +123,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
storm::parser::AutoParser<double> stateAndTransitionRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
@@ -153,10 +141,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - (2.0 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - (2.0 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -164,10 +151,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - (2.0 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - (2.0 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
@@ -187,14 +173,11 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
-
- ASSERT_NE(nullptr, result);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -202,12 +185,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
@@ -215,12 +195,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
@@ -228,12 +205,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -241,10 +215,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);;
- ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 4.28568908480604982), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -252,10 +225,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);;
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 4.2856904354441400784), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 10a0173de..c07c583e8 100644
--- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -22,13 +22,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("two");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -36,10 +34,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -47,10 +44,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -58,10 +54,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -69,10 +64,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -80,10 +74,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -91,10 +84,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -102,10 +94,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula);;
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
storm::parser::AutoParser<double> stateRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
@@ -121,10 +112,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -132,10 +122,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 7.3333294987678527832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
storm::parser::AutoParser<double> stateAndTransitionRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
@@ -151,10 +140,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - (2 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -162,10 +150,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
- ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - (2 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
@@ -185,14 +172,11 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -200,12 +184,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
@@ -213,12 +194,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
@@ -226,12 +204,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -239,10 +214,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);;
- ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 4.28568908480604982), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -250,10 +224,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);;
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 4.2856904354441400784), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index 6cb6fbb50..c8c7e1346 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -26,15 +26,12 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5...");
- std::vector<double>* result = probFormula->check(mc);
+ std::vector<double> result = probFormula->check(mc);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.2296800237), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.2296800237), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("observeIGreater1");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -44,12 +41,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
result = probFormula->check(mc);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.05073232193), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.05073232193), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("observeOnlyTrueSender");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -59,12 +53,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
result = probFormula->check(mc);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.22742171078), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.22742171078), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
}
@@ -88,15 +79,12 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8...");
- std::vector<double>* result = probFormula->check(mc);
+ std::vector<double> result = probFormula->check(mc);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::property::prctl::BoundedUntil<double>(new storm::property::prctl::Ap<double>("true"), apFormula, 20);
@@ -106,12 +94,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
result = probFormula->check(mc);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.9993949793), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.9993949793), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -121,10 +106,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
result = rewardFormula->check(mc);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1.025106273), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.025106273), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
\ No newline at end of file
diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
index 7f2d45d00..8d575caab 100644
--- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
@@ -24,15 +24,12 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F elected] on asynchronous_leader/leader7...");
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -42,12 +39,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25ull);
@@ -57,12 +51,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25ull);
@@ -72,12 +63,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -87,10 +75,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_LT(std::abs((*result)[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -100,12 +87,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
@@ -127,15 +111,12 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished] on consensus/coin4_6...");
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
-
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+
+ ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Ap<double>* apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_0");
@@ -147,12 +128,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[31168] - 0.43742828319177884388579), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.43742828319177884388579), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_1");
@@ -164,11 +142,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.52932863686144482340267813924583606421947479248047), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.52932863686144482340267813924583606421947479248047), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("agree");
@@ -181,11 +157,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.1041409700076474653673841), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.1041409700076474653673841), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
@@ -195,11 +169,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
@@ -209,11 +181,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -223,11 +193,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 1725.5933133943854045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 1725.5933133943854045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -237,10 +205,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 2183.1424220082612919213715), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 2183.1424220082612919213715), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
\ No newline at end of file
diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 877a5aaa6..2a24197a1 100644
--- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -24,14 +24,12 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F elected] on asynchronous_leader/leader7...");
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -41,12 +39,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
@@ -56,12 +51,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
@@ -71,11 +63,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -85,10 +75,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_LT(std::abs((*result)[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -98,12 +87,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
@@ -127,15 +113,12 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished] on consensus/coin4_6...");
- std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
+ std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
-
- ASSERT_LT(std::abs((*result)[31168] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Ap<double>* apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_0");
@@ -147,11 +130,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.43742828319177884388579), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.43742828319177884388579), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_1");
@@ -163,11 +144,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.52932863686144482340267813924583606421947479248047), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.52932863686144482340267813924583606421947479248047), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("agree");
@@ -180,11 +159,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.1041409700076474653673841), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.1041409700076474653673841), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
@@ -194,11 +171,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
@@ -208,12 +183,10 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*probFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
- delete result;
-
+
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
@@ -222,11 +195,9 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 1725.5933133943854045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 1725.5933133943854045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -236,10 +207,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkNoBoundOperator(*rewardFormula);
LOG4CPLUS_WARN(logger, "Done.");
- ASSERT_NE(nullptr, result);
- ASSERT_LT(std::abs((*result)[31168] - 2183.1424220082612919213715), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+ ASSERT_LT(std::abs(result[31168] - 2183.1424220082612919213715), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- delete result;
}
\ No newline at end of file