From ee0e90462f0e1b3286dc0d0432e7981fe445cb01 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 20 May 2020 15:47:03 +0200 Subject: [PATCH] Fixed incorrect result of canHandleStatic for multi-objective formulas for MDP in hybrid engine and MA in sparse engine. --- .../modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp | 1 + src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 10e3355f9..eac2e12a8 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -42,6 +42,7 @@ namespace storm { if (requiresSingleInitialState) { *requiresSingleInitialState = true; } + return true; } return false; } diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index c4099bb5b..b3bd5ed1c 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -46,6 +46,7 @@ namespace storm { if (requiresSingleInitialState) { *requiresSingleInitialState = true; } + return true; } return false; }