From 60d71416b02e9d3202d20d66e9d35a66ddff184b 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