From de385b0527798c5adc1168b39d5b5e7c3dcd119e Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Tue, 22 Dec 2020 16:57:42 +0100
Subject: [PATCH] added method for lra game transition type

also added the according template class constructions.
---
 .../helper/infinitehorizon/internal/LraViHelper.cpp      | 9 ++++++++-
 .../helper/infinitehorizon/internal/LraViHelper.h        | 4 +++-
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
index 2a4f6950a..101d21543 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
@@ -492,9 +492,16 @@ namespace storm {
                 bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetIs() const {
                     return TransitionsType == LraViTransitionsType::DetTsNondetIs;
                 }
-                
+
+                template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
+                bool LraViHelper<ValueType, ComponentType, TransitionsType>::gameNondetTs() const {
+                    return TransitionsType == LraViTransitionsType::GameNondetTsNoIs;
+                }
+
                 template class LraViHelper<double, storm::storage::MaximalEndComponent, LraViTransitionsType::NondetTsNoIs>;
                 template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::NondetTsNoIs>;
+                template class LraViHelper<double, storm::storage::MaximalEndComponent, LraViTransitionsType::GameNondetTsNoIs>;
+                template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::GameNondetTsNoIs>;
                 template class LraViHelper<double, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>;
                 template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>;
                 
diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h
index db1a30a01..c800a9976 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h
+++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h
@@ -128,7 +128,9 @@ namespace storm {
                     /// @return true iff there potentially is a nondeterministic choice at instant states. Returns false if there are no instant states.
                     bool nondetIs() const;
 
-                    
+                    /// @return true iff there potentially are nondeterministic choices for different players at timed states
+                    bool gameNondetTs() const;
+
                     void setComponent(ComponentType component);
                     
                     // We need to make sure that states/choices will be processed in ascending order