Browse Source

Enabled output file, this time fo' real.

Former-commit-id: 64c17ea23e
main
dehnert 10 years ago
parent
commit
d63086d7e3
  1. 9
      src/stormParametric.cpp

9
src/stormParametric.cpp

@ -193,14 +193,19 @@ void check() {
storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
constraintCollector(*dtmc);
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());
if (std::is_same<ValueType, storm::RationalFunction>::value) {
printApproximateResult(result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]);
printApproximateResult(valueFunction);
}
std::cout << std::endl;
}

Loading…
Cancel
Save