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