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