|
|
@ -122,14 +122,14 @@ namespace storm { |
|
|
|
checker.printStatisticsToStream(std::cout); |
|
|
|
if (result) { |
|
|
|
if (storm::utility::resources::isTerminate()) { |
|
|
|
STORM_PRINT_AND_LOG("Result till abort: ") |
|
|
|
STORM_PRINT_AND_LOG("\nResult till abort: ") |
|
|
|
} else { |
|
|
|
STORM_PRINT_AND_LOG("Result: ") |
|
|
|
STORM_PRINT_AND_LOG("\nResult: ") |
|
|
|
} |
|
|
|
printResult(result->underApproxValue, result->overApproxValue); |
|
|
|
STORM_PRINT_AND_LOG(std::endl); |
|
|
|
} else { |
|
|
|
STORM_PRINT_AND_LOG("Result: Not available." << std::endl); |
|
|
|
STORM_PRINT_AND_LOG("\nResult: Not available." << std::endl); |
|
|
|
} |
|
|
|
analysisPerformed = true; |
|
|
|
} |
|
|
@ -157,7 +157,9 @@ namespace storm { |
|
|
|
STORM_PRINT_AND_LOG("Analyzing the formula on the fully observable MDP ... "); |
|
|
|
auto result = storm::api::verifyWithSparseEngine<ValueType>(pomdp->template as<storm::models::sparse::Mdp<ValueType>>(), storm::api::createTask<ValueType>(formula.asSharedPointer(), true))->template asExplicitQuantitativeCheckResult<ValueType>(); |
|
|
|
result.filter(storm::modelchecker::ExplicitQualitativeCheckResult(pomdp->getInitialStates())); |
|
|
|
STORM_PRINT_AND_LOG("Result: " << result.getMax() << std::endl); |
|
|
|
STORM_PRINT_AND_LOG("\nResult: "); |
|
|
|
printResult(result.getMin(), result.getMax()); |
|
|
|
STORM_PRINT_AND_LOG(std::endl); |
|
|
|
analysisPerformed = true; |
|
|
|
} |
|
|
|
return analysisPerformed; |
|
|
|