Browse Source

added method for lra game transition type

also added the according template class constructions.
tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
de385b0527
  1. 7
      src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
  2. 2
      src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h

7
src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp

@ -493,8 +493,15 @@ namespace storm {
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>;

2
src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h

@ -128,6 +128,8 @@ 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);

Loading…
Cancel
Save