From 44378ac9a173be92c8cac37a9a4b3ef417cbd95b Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 08:32:29 +0100 Subject: [PATCH] fix for playerIndex in Choice --- src/storm/generator/Choice.cpp | 4 ++-- src/storm/generator/Choice.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index 27ae916d1..ef5d0ab4a 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -97,8 +97,8 @@ namespace storm { } template - bool Choice::hasPlayer() const { - return player.is_initialized(); + bool Choice::hasPlayerIndex() const { + return playerIndex.is_initialized(); } template diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h index 445560939..acd6f29b4 100644 --- a/src/storm/generator/Choice.h +++ b/src/storm/generator/Choice.h @@ -102,7 +102,7 @@ namespace storm { /*! * Returns whether there is an index for the player defined for this choice. */ - bool hasPlayer() const; + bool hasPlayerIndex() const; /*! * Retrieves the players index associated with this choice