Browse Source

remove debug output and choose sylvan automatically in exact mode

tempestpy_adaptions
dehnert 7 years ago
parent
commit
bf727a28fd
  1. 8
      src/storm-cli-utilities/model-handling.h
  2. 4
      src/storm/settings/modules/CoreSettings.cpp
  3. 7
      src/storm/settings/modules/CoreSettings.h
  4. 7
      src/storm/solver/EigenLinearEquationSolver.cpp

8
src/storm-cli-utilities/model-handling.h

@ -645,8 +645,12 @@ namespace storm {
template <typename ValueType>
void processInputWithValueType(SymbolicInput const& input) {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && generalSettings.isExactSet()) {
STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);
} else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, ValueType>(input);
} else {
STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library.");

4
src/storm/settings/modules/CoreSettings.cpp

@ -129,6 +129,10 @@ namespace storm {
}
}
bool CoreSettings::isDdLibraryTypeSetFromDefaultValue() const {
return !this->getOption(ddLibraryOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(ddLibraryOptionName).getArgumentByName("name").wasSetFromDefaultValue();
}
bool CoreSettings::isShowStatisticsSet() const {
return this->getOption(statisticsOptionName).getHasOptionBeenSet();
}

7
src/storm/settings/modules/CoreSettings.h

@ -109,6 +109,13 @@ namespace storm {
*/
storm::dd::DdType getDdLibraryType() const;
/*!
* Retrieves whether the selected DD library is set from its default value.
*
* @return True iff if it is set from its default value.
*/
bool isDdLibraryTypeSetFromDefaultValue() const;
/*!
* Retrieves whether statistics are to be shown for counterexample generation.
*

7
src/storm/solver/EigenLinearEquationSolver.cpp

@ -359,13 +359,6 @@ namespace storm {
solver.compute(*eigenA);
solver._solve_impl(eigenB, eigenX);
std::cout << "solution" << std::endl;
uint64_t pos = 0;
for (auto const& e : x) {
std::cout << "[" << pos << "] " << e << std::endl;
++pos;
}
return solver.info() == StormEigen::ComputationInfo::Success;
}

Loading…
Cancel
Save