|
@ -683,7 +683,9 @@ namespace storm { |
|
|
} else { |
|
|
} else { |
|
|
filter = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(states, false)); |
|
|
filter = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(states, false)); |
|
|
} |
|
|
} |
|
|
result->filter(filter->asQualitativeCheckResult()); |
|
|
|
|
|
|
|
|
if (result && filter) { |
|
|
|
|
|
result->filter(filter->asQualitativeCheckResult()); |
|
|
|
|
|
} |
|
|
return result; |
|
|
return result; |
|
|
}); |
|
|
}); |
|
|
} |
|
|
} |
|
@ -703,8 +705,9 @@ namespace storm { |
|
|
} else { |
|
|
} else { |
|
|
filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false)); |
|
|
filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false)); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
result->filter(filter->asQualitativeCheckResult()); |
|
|
|
|
|
|
|
|
if (result && filter) { |
|
|
|
|
|
result->filter(filter->asQualitativeCheckResult()); |
|
|
|
|
|
} |
|
|
return result; |
|
|
return result; |
|
|
}); |
|
|
}); |
|
|
} |
|
|
} |
|
@ -724,8 +727,9 @@ namespace storm { |
|
|
} else { |
|
|
} else { |
|
|
filter = storm::api::verifyWithDdEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false)); |
|
|
filter = storm::api::verifyWithDdEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false)); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
result->filter(filter->asQualitativeCheckResult()); |
|
|
|
|
|
|
|
|
if (result && filter) { |
|
|
|
|
|
result->filter(filter->asQualitativeCheckResult()); |
|
|
|
|
|
} |
|
|
return result; |
|
|
return result; |
|
|
}); |
|
|
}); |
|
|
} |
|
|
} |
|
|