sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

fixed a ton of warnings

tempestpy_adaptions
dehnert 7 years ago
parent
bb890cb91f
commit
8204c03c0b
13 changed files with 41 additions and 117 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/settings/ArgumentBase.cpp
  2. 11
      src/storm/settings/ArgumentTypeInferationHelper.cpp
  3. 3
      src/storm/solver/EigenLinearEquationSolver.cpp
  4. 3
      src/storm/solver/LinearEquationSolver.cpp
  5. 9
      src/storm/storage/dd/DdManager.cpp
  6. 1
      src/storm/storage/dd/cudd/InternalCuddDdManager.cpp
  7. 38
      src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
  8. 3
      src/storm/storage/jani/Automaton.cpp
  9. 2
      src/storm/utility/ConstantsComparator.cpp
  10. 61
      src/storm/utility/constants.cpp
  11. 13
      src/storm/utility/eigen.h
  12. 11
      src/storm/utility/gmm.h
  13. 1
      src/storm/utility/stateelimination.cpp

2
src/storm/settings/ArgumentBase.cpp
View File

@ -56,11 +56,9 @@ namespace storm {
} }
// Explicitly instantiate the templates. // Explicitly instantiate the templates.
template std::string ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template int_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful); template int_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template uint_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful); template uint_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template double ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful); template double ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template bool ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template std::string ArgumentBase::convertToString(std::string const& value); template std::string ArgumentBase::convertToString(std::string const& value);
template std::string ArgumentBase::convertToString(int_fast64_t const& value); template std::string ArgumentBase::convertToString(int_fast64_t const& value);

11
src/storm/settings/ArgumentTypeInferationHelper.cpp
View File

@ -89,40 +89,29 @@ namespace storm {
} }
// Explicitly instantiate the templates. // Explicitly instantiate the templates.
template ArgumentType inferToEnumType<std::string>();
template ArgumentType inferToEnumType<int_fast64_t>();
template ArgumentType inferToEnumType<uint_fast64_t>();
template ArgumentType inferToEnumType<double>();
template ArgumentType inferToEnumType<bool>();
template std::string const& inferToString<std::string>(ArgumentType const& argumentType, std::string const& value);
template std::string const& inferToString<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value); template std::string const& inferToString<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template std::string const& inferToString<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value); template std::string const& inferToString<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template std::string const& inferToString<double>(ArgumentType const& argumentType, double const& value); template std::string const& inferToString<double>(ArgumentType const& argumentType, double const& value);
template std::string const& inferToString<bool>(ArgumentType const& argumentType, bool const& value); template std::string const& inferToString<bool>(ArgumentType const& argumentType, bool const& value);
template int_fast64_t inferToInteger<std::string>(ArgumentType const& argumentType, std::string const& value); template int_fast64_t inferToInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
template int_fast64_t inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template int_fast64_t inferToInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value); template int_fast64_t inferToInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template int_fast64_t inferToInteger<double>(ArgumentType const& argumentType, double const& value); template int_fast64_t inferToInteger<double>(ArgumentType const& argumentType, double const& value);
template int_fast64_t inferToInteger<bool>(ArgumentType const& argumentType, bool const& value); template int_fast64_t inferToInteger<bool>(ArgumentType const& argumentType, bool const& value);
template uint_fast64_t inferToUnsignedInteger<std::string>(ArgumentType const& argumentType, std::string const& value); template uint_fast64_t inferToUnsignedInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
template uint_fast64_t inferToUnsignedInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value); template uint_fast64_t inferToUnsignedInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template uint_fast64_t inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template uint_fast64_t inferToUnsignedInteger<double>(ArgumentType const& argumentType, double const& value); template uint_fast64_t inferToUnsignedInteger<double>(ArgumentType const& argumentType, double const& value);
template uint_fast64_t inferToUnsignedInteger<bool>(ArgumentType const& argumentType, bool const& value); template uint_fast64_t inferToUnsignedInteger<bool>(ArgumentType const& argumentType, bool const& value);
template double inferToDouble<std::string>(ArgumentType const& argumentType, std::string const& value); template double inferToDouble<std::string>(ArgumentType const& argumentType, std::string const& value);
template double inferToDouble<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value); template double inferToDouble<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template double inferToDouble<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value); template double inferToDouble<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template double inferToDouble<double>(ArgumentType const& argumentType, double const& value);
template double inferToDouble<bool>(ArgumentType const& argumentType, bool const& value); template double inferToDouble<bool>(ArgumentType const& argumentType, bool const& value);
template bool inferToBoolean<std::string>(ArgumentType const& argumentType, std::string const& value); template bool inferToBoolean<std::string>(ArgumentType const& argumentType, std::string const& value);
template bool inferToBoolean<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value); template bool inferToBoolean<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template bool inferToBoolean<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value); template bool inferToBoolean<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template bool inferToBoolean<double>(ArgumentType const& argumentType, double const& value); template bool inferToBoolean<double>(ArgumentType const& argumentType, double const& value);
template bool inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value);
} }
} }

3
src/storm/solver/EigenLinearEquationSolver.cpp
View File

@ -403,9 +403,6 @@ namespace storm {
template class EigenLinearEquationSolverFactory<double>; template class EigenLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class EigenLinearEquationSolverSettings<storm::RationalNumber>;
template class EigenLinearEquationSolverSettings<storm::RationalFunction>;
template class EigenLinearEquationSolver<storm::RationalNumber>; template class EigenLinearEquationSolver<storm::RationalNumber>;
template class EigenLinearEquationSolver<storm::RationalFunction>; template class EigenLinearEquationSolver<storm::RationalFunction>;

3
src/storm/solver/LinearEquationSolver.cpp
View File

@ -241,9 +241,6 @@ namespace storm {
template class LinearEquationSolverFactory<storm::RationalNumber>; template class LinearEquationSolverFactory<storm::RationalNumber>;
template class LinearEquationSolverFactory<storm::RationalFunction>; template class LinearEquationSolverFactory<storm::RationalFunction>;
template class GeneralLinearEquationSolverFactory<storm::RationalNumber>;
template class GeneralLinearEquationSolverFactory<storm::RationalFunction>;
#endif #endif
} }

9
src/storm/storage/dd/DdManager.cpp
View File

@ -173,11 +173,20 @@ namespace storm {
return result; return result;
} }
#if defined(__clang__)
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Winfinite-recursion"
#endif
template<DdType LibraryType> template<DdType LibraryType>
Bdd<LibraryType> DdManager<LibraryType>::getCube(storm::expressions::Variable const& variable) const { Bdd<LibraryType> DdManager<LibraryType>::getCube(storm::expressions::Variable const& variable) const {
return getCube({variable}); return getCube({variable});
} }
#if defined(__clang__)
#pragma clang diagnostic pop
#endif
template<DdType LibraryType> template<DdType LibraryType>
Bdd<LibraryType> DdManager<LibraryType>::getCube(std::set<storm::expressions::Variable> const& variables) const { Bdd<LibraryType> DdManager<LibraryType>::getCube(std::set<storm::expressions::Variable> const& variables) const {
Bdd<LibraryType> result = this->getBddOne(); Bdd<LibraryType> result = this->getBddOne();

1
src/storm/storage/dd/cudd/InternalCuddDdManager.cpp
View File

@ -179,6 +179,5 @@ namespace storm {
template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getConstant(double const& value) const; template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getConstant(double const& value) const;
template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const; template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const;
template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getConstant(storm::RationalNumber const& value) const;
} }
} }

38
src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
View File

@ -19,6 +19,12 @@ namespace storm {
namespace dd { namespace dd {
#ifndef NDEBUG #ifndef NDEBUG
#if defined(__clang__)
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wzero-length-array"
#pragma clang diagnostic ignored "-Wc99-extensions"
#endif
VOID_TASK_0(gc_start) { VOID_TASK_0(gc_start) {
STORM_LOG_TRACE("Starting sylvan garbage collection..."); STORM_LOG_TRACE("Starting sylvan garbage collection...");
} }
@ -26,6 +32,11 @@ namespace storm {
VOID_TASK_0(gc_end) { VOID_TASK_0(gc_end) {
STORM_LOG_TRACE("Sylvan garbage collection done."); STORM_LOG_TRACE("Sylvan garbage collection done.");
} }
#if defined(__clang__)
#pragma clang diagnostic pop
#endif
#endif #endif
uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0; uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0;
@ -237,24 +248,6 @@ namespace storm {
return nextFreeVariableIndex; return nextFreeVariableIndex;
} }
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const;
template InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalDdManager<DdType::Sylvan>::getAddOne() const;
#ifdef STORM_HAVE_CARL
template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const;
#endif
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const;
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const;
template InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalDdManager<DdType::Sylvan>::getAddZero() const;
#ifdef STORM_HAVE_CARL
template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const;
#endif
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddUndefined() const; template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddUndefined() const;
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddUndefined() const; template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddUndefined() const;
@ -263,14 +256,5 @@ namespace storm {
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddUndefined() const; template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddUndefined() const;
#endif #endif
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const;
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
template InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalNumber const& value) const;
#ifdef STORM_HAVE_CARL
template InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const;
#endif
} }
} }

3
src/storm/storage/jani/Automaton.cpp
View File

@ -543,6 +543,9 @@ namespace storm {
for (auto const& edge : edges) { for (auto const& edge : edges) {
outStream << "\t" << name << "_e" << edgeIndex << "[ label=\"\" , shape=circle, width=.2, style=filled, fillcolor=\"black\"];" << std::endl; outStream << "\t" << name << "_e" << edgeIndex << "[ label=\"\" , shape=circle, width=.2, style=filled, fillcolor=\"black\"];" << std::endl;
++edgeIndex; ++edgeIndex;
// Silencing unused variable warning.
(void)edge;
} }
// Connect edges // Connect edges

2
src/storm/utility/ConstantsComparator.cpp
View File

@ -105,8 +105,6 @@ namespace storm {
} }
// Explicit instantiations. // Explicit instantiations.
template class ConstantsComparator<double>;
template class ConstantsComparator<float>;
template class ConstantsComparator<int>; template class ConstantsComparator<int>;
template class ConstantsComparator<storm::storage::sparse::state_type>; template class ConstantsComparator<storm::storage::sparse::state_type>;

61
src/storm/utility/constants.cpp
View File

@ -868,7 +868,6 @@ namespace storm {
template bool isZero(int const& value); template bool isZero(int const& value);
template bool isConstant(int const& value); template bool isConstant(int const& value);
template bool isInfinity(int const& value); template bool isInfinity(int const& value);
template bool isInteger(int const& number);
// uint32_t // uint32_t
template uint32_t one(); template uint32_t one();
@ -878,7 +877,6 @@ namespace storm {
template bool isZero(uint32_t const& value); template bool isZero(uint32_t const& value);
template bool isConstant(uint32_t const& value); template bool isConstant(uint32_t const& value);
template bool isInfinity(uint32_t const& value); template bool isInfinity(uint32_t const& value);
template bool isInteger(uint32_t const& number);
// storm::storage::sparse::state_type // storm::storage::sparse::state_type
template storm::storage::sparse::state_type one(); template storm::storage::sparse::state_type one();
@ -888,11 +886,8 @@ namespace storm {
template bool isZero(storm::storage::sparse::state_type const& value); template bool isZero(storm::storage::sparse::state_type const& value);
template bool isConstant(storm::storage::sparse::state_type const& value); template bool isConstant(storm::storage::sparse::state_type const& value);
template bool isInfinity(storm::storage::sparse::state_type const& value); template bool isInfinity(storm::storage::sparse::state_type const& value);
template bool isInteger(storm::storage::sparse::state_type const& number);
// other instantiations // other instantiations
template double convertNumber(long long const&);
template storm::storage::sparse::state_type convertNumber(long long const& number);
template unsigned long convertNumber(long const&); template unsigned long convertNumber(long const&);
template double convertNumber(long const&); template double convertNumber(long const&);
@ -901,20 +896,11 @@ namespace storm {
template storm::ClnRationalNumber one(); template storm::ClnRationalNumber one();
template NumberTraits<storm::ClnRationalNumber>::IntegerType one(); template NumberTraits<storm::ClnRationalNumber>::IntegerType one();
template storm::ClnRationalNumber zero(); template storm::ClnRationalNumber zero();
template storm::ClnRationalNumber infinity();
template bool isOne(storm::ClnRationalNumber const& value);
template bool isZero(NumberTraits<storm::ClnRationalNumber>::IntegerType const& value); template bool isZero(NumberTraits<storm::ClnRationalNumber>::IntegerType const& value);
template bool isZero(storm::ClnRationalNumber const& value);
template bool isConstant(storm::ClnRationalNumber const& value); template bool isConstant(storm::ClnRationalNumber const& value);
template bool isInfinity(storm::ClnRationalNumber const& value); template bool isInfinity(storm::ClnRationalNumber const& value);
template bool isInteger(storm::ClnRationalNumber const& number);
template double convertNumber(storm::ClnRationalNumber const& number);
template storm::NumberTraits<ClnRationalNumber>::IntegerType convertNumber(storm::NumberTraits<ClnRationalNumber>::IntegerType const& number); template storm::NumberTraits<ClnRationalNumber>::IntegerType convertNumber(storm::NumberTraits<ClnRationalNumber>::IntegerType const& number);
template storm::NumberTraits<ClnRationalNumber>::IntegerType convertNumber(uint64_t const& number);
template uint_fast64_t convertNumber(storm::ClnRationalNumber const& number);
template storm::ClnRationalNumber convertNumber(double const& number);
template storm::ClnRationalNumber convertNumber(storm::ClnRationalNumber const& number); template storm::ClnRationalNumber convertNumber(storm::ClnRationalNumber const& number);
template ClnRationalNumber convertNumber(std::string const& number);
template storm::ClnRationalNumber simplify(storm::ClnRationalNumber value); template storm::ClnRationalNumber simplify(storm::ClnRationalNumber value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::ClnRationalNumber>& matrixEntry);
@ -922,17 +908,10 @@ namespace storm {
template std::pair<storm::ClnRationalNumber, storm::ClnRationalNumber> minmax(std::map<uint64_t, storm::ClnRationalNumber> const&); template std::pair<storm::ClnRationalNumber, storm::ClnRationalNumber> minmax(std::map<uint64_t, storm::ClnRationalNumber> const&);
template storm::ClnRationalNumber minimum(std::map<uint64_t, storm::ClnRationalNumber> const&); template storm::ClnRationalNumber minimum(std::map<uint64_t, storm::ClnRationalNumber> const&);
template storm::ClnRationalNumber maximum(std::map<uint64_t, storm::ClnRationalNumber> const&); template storm::ClnRationalNumber maximum(std::map<uint64_t, storm::ClnRationalNumber> const&);
template std::pair<storm::ClnRationalNumber, storm::ClnRationalNumber> minmax(std::vector<storm::ClnRationalNumber> const&);
template storm::ClnRationalNumber minimum(std::vector<storm::ClnRationalNumber> const&); template storm::ClnRationalNumber minimum(std::vector<storm::ClnRationalNumber> const&);
template storm::ClnRationalNumber maximum(std::vector<storm::ClnRationalNumber> const&); template storm::ClnRationalNumber maximum(std::vector<storm::ClnRationalNumber> const&);
template storm::ClnRationalNumber max(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second); template storm::ClnRationalNumber max(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second);
template storm::ClnRationalNumber min(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second); template storm::ClnRationalNumber min(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second);
template storm::ClnRationalNumber pow(storm::ClnRationalNumber const& value, uint_fast64_t exponent);
template storm::ClnRationalNumber sqrt(storm::ClnRationalNumber const& number);
template storm::ClnRationalNumber abs(storm::ClnRationalNumber const& number);
template storm::ClnRationalNumber floor(storm::ClnRationalNumber const& number);
template storm::ClnRationalNumber ceil(storm::ClnRationalNumber const& number);
template storm::ClnRationalNumber log(storm::ClnRationalNumber const& number);
template std::string to_string(storm::ClnRationalNumber const& value); template std::string to_string(storm::ClnRationalNumber const& value);
#endif #endif
@ -941,74 +920,34 @@ namespace storm {
template storm::GmpRationalNumber one(); template storm::GmpRationalNumber one();
template NumberTraits<storm::GmpRationalNumber>::IntegerType one(); template NumberTraits<storm::GmpRationalNumber>::IntegerType one();
template storm::GmpRationalNumber zero(); template storm::GmpRationalNumber zero();
template storm::GmpRationalNumber infinity();
template bool isOne(storm::GmpRationalNumber const& value);
template bool isZero(storm::GmpRationalNumber const& value);
template bool isZero(NumberTraits<storm::GmpRationalNumber>::IntegerType const& value); template bool isZero(NumberTraits<storm::GmpRationalNumber>::IntegerType const& value);
template bool isConstant(storm::GmpRationalNumber const& value); template bool isConstant(storm::GmpRationalNumber const& value);
template bool isInfinity(storm::GmpRationalNumber const& value); template bool isInfinity(storm::GmpRationalNumber const& value);
template bool isInteger(storm::GmpRationalNumber const& number);
template double convertNumber(storm::GmpRationalNumber const& number);
template uint_fast64_t convertNumber(storm::GmpRationalNumber const& number);
template storm::NumberTraits<GmpRationalNumber>::IntegerType convertNumber(storm::NumberTraits<GmpRationalNumber>::IntegerType const& number); template storm::NumberTraits<GmpRationalNumber>::IntegerType convertNumber(storm::NumberTraits<GmpRationalNumber>::IntegerType const& number);
template storm::NumberTraits<GmpRationalNumber>::IntegerType convertNumber(uint64_t const& number);
template storm::GmpRationalNumber convertNumber(double const& number);
template storm::GmpRationalNumber convertNumber(storm::GmpRationalNumber const& number); template storm::GmpRationalNumber convertNumber(storm::GmpRationalNumber const& number);
template GmpRationalNumber convertNumber(std::string const& number);
template storm::GmpRationalNumber simplify(storm::GmpRationalNumber value); template storm::GmpRationalNumber simplify(storm::GmpRationalNumber value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::GmpRationalNumber>&& matrixEntry);
template std::pair<storm::GmpRationalNumber, storm::GmpRationalNumber> minmax(std::map<uint64_t, storm::GmpRationalNumber> const&);
template storm::GmpRationalNumber minimum(std::map<uint64_t, storm::GmpRationalNumber> const&); template storm::GmpRationalNumber minimum(std::map<uint64_t, storm::GmpRationalNumber> const&);
template storm::GmpRationalNumber maximum(std::map<uint64_t, storm::GmpRationalNumber> const&); template storm::GmpRationalNumber maximum(std::map<uint64_t, storm::GmpRationalNumber> const&);
template std::pair<storm::GmpRationalNumber, storm::GmpRationalNumber> minmax(std::vector<storm::GmpRationalNumber> const&);
template storm::GmpRationalNumber minimum(std::vector<storm::GmpRationalNumber> const&); template storm::GmpRationalNumber minimum(std::vector<storm::GmpRationalNumber> const&);
template storm::GmpRationalNumber maximum(std::vector<storm::GmpRationalNumber> const&); template storm::GmpRationalNumber maximum(std::vector<storm::GmpRationalNumber> const&);
template storm::GmpRationalNumber max(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second); template storm::GmpRationalNumber max(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second);
template storm::GmpRationalNumber min(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second); template storm::GmpRationalNumber min(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second);
template storm::GmpRationalNumber pow(storm::GmpRationalNumber const& value, uint_fast64_t exponent);
template storm::GmpRationalNumber sqrt(storm::GmpRationalNumber const& number);
template storm::GmpRationalNumber abs(storm::GmpRationalNumber const& number);
template storm::GmpRationalNumber floor(storm::GmpRationalNumber const& number);
template storm::GmpRationalNumber ceil(storm::GmpRationalNumber const& number);
template storm::GmpRationalNumber log(storm::GmpRationalNumber const& number);
template std::string to_string(storm::GmpRationalNumber const& value); template std::string to_string(storm::GmpRationalNumber const& value);
#endif #endif
#if defined(STORM_HAVE_CARL) && defined(STORM_HAVE_GMP) && defined(STORM_HAVE_CLN) #if defined(STORM_HAVE_CARL) && defined(STORM_HAVE_GMP) && defined(STORM_HAVE_CLN)
template storm::GmpRationalNumber convertNumber(storm::ClnRationalNumber const& number);
template storm::ClnRationalNumber convertNumber(storm::GmpRationalNumber const& number);
#endif #endif
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
// Instantiations for rational function. // Instantiations for rational function.
template RationalFunction one(); template RationalFunction one();
template RationalFunction zero(); template RationalFunction zero();
template storm::RationalFunction infinity();
template bool isOne(RationalFunction const& value);
template bool isZero(RationalFunction const& value);
template bool isConstant(RationalFunction const& value);
template bool isInfinity(RationalFunction const& value);
template bool isInteger(RationalFunction const&);
template storm::RationalFunction convertNumber(storm::RationalFunction const& number);
template RationalFunctionCoefficient convertNumber(RationalFunction const& number);
template RationalFunction convertNumber(storm::RationalFunctionCoefficient const& number);
template RationalFunction convertNumber(storm::storage::sparse::state_type const& number);
template RationalFunction convertNumber(double const& number);
template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
template std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::map<uint64_t, storm::RationalFunction> const&);
template storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&);
template storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&);
template std::pair<storm::RationalFunction, storm::RationalFunction> minmax(std::vector<storm::RationalFunction> const&);
template storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&);
template storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&);
template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
// Instantiations for polynomials. // Instantiations for polynomials.
template Polynomial one(); template Polynomial one();

13
src/storm/utility/eigen.h
View File

@ -3,16 +3,23 @@
// Include this utility header so we can access utility function from Eigen. // Include this utility header so we can access utility function from Eigen.
#include "storm/utility/constants.h" #include "storm/utility/constants.h"
#if defined(__clang__)
#pragma clang diagnostic push #pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wunknown-pragmas" #pragma clang diagnostic ignored "-Wunknown-pragmas"
// Finally include the parts of Eigen we need.
#elif defined(__GNUC__)
#pragma GCC diagnostic push #pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wignored-attributes" #pragma GCC diagnostic ignored "-Wignored-attributes"
#pragma GCC diagnostic ignored "-Wmisleading-indentation" #pragma GCC diagnostic ignored "-Wmisleading-indentation"
#pragma GCC diagnostic ignored "-Wunused-parameter" #pragma GCC diagnostic ignored "-Wunused-parameter"
#endif
// Finally include the parts of Eigen we need.
#include <StormEigen/Dense> #include <StormEigen/Dense>
#include <StormEigen/Sparse> #include <StormEigen/Sparse>
#include <unsupported/StormEigen/IterativeSolvers> #include <unsupported/StormEigen/IterativeSolvers>
#pragma GCC diagnostic pop
#if defined(__clang__)
#pragma clang diagnostic pop #pragma clang diagnostic pop
#elif defined(__GNUC__)
#pragma GCC diagnostic pop
#endif

11
src/storm/utility/gmm.h
View File

@ -1,20 +1,25 @@
#ifndef STORM_UTILITY_GMM_H_ #ifndef STORM_UTILITY_GMM_H_
#define STORM_UTILITY_GMM_H_ #define STORM_UTILITY_GMM_H_
#if defined(__clang__)
#pragma clang diagnostic push #pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wunused-variable" #pragma clang diagnostic ignored "-Wunused-variable"
#pragma clang diagnostic ignored "-Wunused-parameter" #pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunknown-pragmas" #pragma clang diagnostic ignored "-Wunknown-pragmas"
#elif defined(__GNUC__)
#pragma GCC diagnostic push #pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wdeprecated-declarations" #pragma GCC diagnostic ignored "-Wdeprecated-declarations"
#pragma GCC diagnostic ignored "-Wmisleading-indentation" #pragma GCC diagnostic ignored "-Wmisleading-indentation"
#endif
#include "gmm/gmm_matrix.h" #include "gmm/gmm_matrix.h"
#include "gmm/gmm_iter_solvers.h" #include "gmm/gmm_iter_solvers.h"
#pragma GCC diagnostic pop
#if defined(__clang__)
#pragma clang diagnostic pop #pragma clang diagnostic pop
#elif defined(__GNUC__)
#pragma GCC diagnostic pop
#endif
#endif /* STORM_UTILITY_GMM_H_ */ #endif /* STORM_UTILITY_GMM_H_ */

1
src/storm/utility/stateelimination.cpp
View File

@ -210,7 +210,6 @@ namespace storm {
template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward, bool reverse); template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward, bool reverse);
template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward); template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalNumber> const& oneStepProbabilities, bool forward);
template uint_fast64_t estimateComplexity(storm::RationalFunction const& value);
template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities, storm::storage::BitVector const& states); template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities, storm::storage::BitVector const& states);
template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities); template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities);
template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities); template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities);

Write Preview
Loading…
Cancel
Save