From 87c855531219755df5920538dca0c7755462a1b0 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 30 Mar 2020 12:20:13 +0200 Subject: [PATCH] Using the new reward functionalities of BliefGrid. This also fixes setting rewards in a wrong way (previously, the same reward was assigned to states with the same observation). Added auxiliary functions for creating properties. --- src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp index 3aeb81d18..eac2dad1b 100644 --- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp +++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp @@ -1207,8 +1207,8 @@ namespace storm { auto property = createStandardProperty(min, computeRewards); auto task = createStandardCheckTask(property, std::vector()); - statistics.underApproximationCheckTime.start(); + std::unique_ptr res(storm::api::verifyWithSparseEngine(model, task)); statistics.underApproximationCheckTime.stop(); if (storm::utility::resources::isTerminate() && !res) {