Browse Source

Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC

tempestpy_adaptions
dehnert 12 years ago
parent
commit
cdc24b1456
  1. 4
      src/formula/ProbabilisticIntervalOperator.h
  2. 14
      src/modelChecker/EigenDtmcPrctlModelChecker.h
  3. 7
      src/storage/SquareSparseMatrix.h
  4. 76
      src/utility/ConstTemplates.h

4
src/formula/ProbabilisticIntervalOperator.h

@ -49,8 +49,8 @@ public:
* Empty constructor
*/
ProbabilisticIntervalOperator() {
upper = mrmc::utility::constGetZero(upper);
lower = mrmc::utility::constGetZero(lower);
upper = mrmc::utility::constGetZero<T>();
lower = mrmc::utility::constGetZero<T>();
pathFormula = NULL;
}

14
src/modelChecker/EigenDtmcPrctlModelChecker.h

@ -64,9 +64,7 @@ public:
std::vector<Type>* result = new std::vector<Type>(stateCount);
// Dummy Type variable for const templates
Type dummy;
mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne(dummy));
mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne<Type>());
Type *p = &((*result)[0]); // get the address storing the data for result
MapType vectorMap(p, result->size()); // vectorMap shares data
@ -94,8 +92,8 @@ public:
// Create the vector with which to multiply and initialize it correctly.
std::vector<Type> x(this->getModel().getNumberOfStates());
Type dummy;
mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne(dummy));
mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne<Type>());
// Delete not needed next states bit vector.
delete nextStates;
@ -213,10 +211,8 @@ public:
delete eigenSubMatrix;
}
// Dummy Type variable for const templates
Type dummy;
mrmc::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero(dummy));
mrmc::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne(dummy));
mrmc::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero<Type>());
mrmc::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne<Type>());
return result;
}

7
src/storage/SquareSparseMatrix.h

@ -742,12 +742,12 @@ public:
uint_fast64_t rowEnd = rowIndications[row + 1];
while (rowStart < rowEnd) {
valueStorage[rowStart] = mrmc::utility::constGetZero(valueStorage[rowStart]);
valueStorage[rowStart] = mrmc::utility::constGetZero<T>();
++rowStart;
}
// Set the element on the diagonal to one.
diagonalStorage[row] = mrmc::utility::constGetOne(diagonalStorage[row]);
diagonalStorage[row] = mrmc::utility::constGetOne<T>();
return true;
}
@ -885,10 +885,9 @@ public:
// no entries apart from those on the diagonal
resultDinv->initialize(0);
// copy diagonal entries to other matrix
T dummy;
for (int i = 0; i < rowCount; ++i) {
resultDinv->addNextValue(i, i, resultLU->getValue(i, i));
resultLU->getValue(i, i) = mrmc::utility::constGetZero(&dummy);
resultLU->getValue(i, i) = mrmc::utility::constGetZero<T>();
}
return new mrmc::storage::JacobiDecomposition<T>(resultLU, resultDinv);

76
src/utility/ConstTemplates.h

@ -17,75 +17,97 @@ namespace utility {
* As (at least) gcc has problems to use the correct template by the return value
* only, the function gets a pointer as a parameter to infer the return type.
*
* <b>Parameter</b>
* @note
* The template parameter is just inferred by the return type; GCC is not able to infer this
* automatically, hence the type should always be stated explicitly (e.g. @c constGetZero<int>();)
*
* The parameter is a reference which is used to infer the return type (So, if you want
* the return value to be of type double, the parameter has to be a double variable).
* In most cases, it is a good choice to use the the variable that is to be set.
* @return Value 0, fit to the return type
*/
template<typename _Scalar>
static inline _Scalar constGetZero(_Scalar&) {
static inline _Scalar constGetZero() {
return _Scalar(0);
}
/*! @cond TEMPLATE_SPECIALIZATION
* (exclude the specializations from the documentation) */
* (By default, the template specifications are not included in the documentation)
*/
/*!
* Template specification for int_fast32_t
* @return Value 0, fit to the type int_fast32_t
*/
template <>
inline int_fast32_t constGetZero(int_fast32_t&) {
inline int_fast32_t constGetZero() {
return 0;
}
/*! @cond TEMPLATE_SPECIALIZATION
* (exclude the specializations from the documentation) */
/*!
* Template specification for uint_fast64_t
* @return Value 0, fit to the type uint_fast64_t
*/
template <>
inline uint_fast64_t constGetZero(uint_fast64_t&) {
inline uint_fast64_t constGetZero() {
return 0;
}
/*! @cond TEMPLATE_SPECIALIZATION
* Specialization of constGetZero for double
/*!
* Template specification for double
* @return Value 0.0, fit to the type double
*/
template <>
inline double constGetZero(double&) {
inline double constGetZero() {
return 0.0;
}
/*! @endcond */
/*!
* Returns a constant value of 0 that is fit to the type it is being written to.
* Returns a constant value of 1 that is fit to the type it is being written to.
* As (at least) gcc has problems to use the correct template by the return value
* only, the function gets a pointer as a parameter to infer the return type.
*
* <b>Parameter</b>
* @note
* The template parameter is just inferred by the return type; GCC is not able to infer this
* automatically, hence the type should always be stated explicitly (e.g. @c constGetOne<int>();)
*
* The parameter is a reference which is used to infer the return type (So, if you want
* the return value to be of type double, the parameter has to be a double variable).
* In most cases, it is a good choice to use the the variable that is to be set. */
* @return Value 1, fit to the return type
*/
template<typename _Scalar>
static inline _Scalar constGetOne(_Scalar&) {
static inline _Scalar constGetOne() {
return _Scalar(1);
}
/*! @cond TEMPLATE_SPECIALIZATION
* (exclude the specializations from the documentation) */
* (By default, the template specifications are not included in the documentation)
*/
/*!
* Template specification for int_fast32_t
* @return Value 1, fit to the type int_fast32_t
*/
template<>
inline int_fast32_t constGetOne(int_fast32_t&) {
inline int_fast32_t constGetOne() {
return 1;
}
/*! @cond TEMPLATE_SPECIALIZATION
* (exclude the specializations from the documentation) */
/*!
* Template specification for uint_fast64_t
* @return Value 1, fit to the type uint_fast61_t
*/
template<>
inline uint_fast64_t constGetOne(uint_fast64_t&) {
inline uint_fast64_t constGetOne() {
return 1;
}
/*! @cond TEMPLATE_SPECIALIZATION
* (exclude the specializations from the documentation) */
/*!
* Template specification for double
* @return Value 1.0, fit to the type double
*/
template<>
inline double constGetOne(double&) {
inline double constGetOne() {
return 1.0;
}
/*! @endcond */
} //namespace utility

Loading…
Cancel
Save