From ba9c0dd2ea1c8649a061ea05ac1fa88764b66fe0 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 16 Dec 2020 12:45:36 +0100 Subject: [PATCH] added transition type for games to LraViHelper --- .../helper/infinitehorizon/internal/LraViHelper.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h index bbf9207a4..db1a30a01 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h @@ -25,9 +25,10 @@ namespace storm { DetTsNoIs, /// deterministic choice at timed states, no instant states (as in DTMCs and CTMCs) DetTsNondetIs, /// deterministic choice at timed states, nondeterministic choice at instant states (as in Markov Automata) DetTsDetIs, /// deterministic choice at timed states, deterministic choice at instant states (as in Markov Automata without any nondeterminisim) - NondetTsNoIs /// nondeterministic choice at timed states, no instant states (as in MDPs) + NondetTsNoIs, /// nondeterministic choice at timed states, no instant states (as in MDPs) + GameNondetTsNoIs // nondeterministic choices of different players at timed states, no instant states (as in SMGs) }; - + /*! * Helper class that performs iterations of the value iteration method. * The purpose of the template parameters ComponentType and TransitionsType are used to make this work for various model types.