Browse Source

Added debug output.

Former-commit-id: 20ee3ec777
tempestpy_adaptions
dehnert 10 years ago
parent
commit
43a1d0bc73
  1. 1
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 8
      src/stormParametric.cpp

1
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@ -538,6 +538,7 @@ namespace storm {
}
// Now, we return the value for the only initial state.
STORM_LOG_DEBUG("Simplifying and returning result.");
if (stateRewards) {
return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
} else {

8
src/stormParametric.cpp

@ -197,10 +197,6 @@ void check() {
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula);
ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
if (storm::settings::parametricSettings().exportResultToFile()) {
storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
}
// Report the result.
STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
result->writeToStream(std::cout, model->getInitialStates());
@ -209,6 +205,10 @@ void check() {
}
std::cout << std::endl;
if (storm::settings::parametricSettings().exportResultToFile()) {
storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
}
// Generate derivatives for sensitivity analysis if requested.
if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) {
ValueType function = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];

Loading…
Cancel
Save