Previously, all non-synchronizing commands were assigned to the player owning the module, even if the command has an action label. However, the correct behavior (as far as I understand the specification) is that only unlabeled commands are associated to the module player.
For a turn-based game, it needs to be specified which player controls each state. In PRISM-games, this is done by proving a list of action names and/or module names for each player. This player then controls any state where all the transitions available are either labelled with one of these actions or are unlabelled and belong to one of these modules
sjunges
commented
2 months ago
Previously, all non-synchronizing commands were assigned to the player owning the module, even if the command has an action label. However, the correct behavior (as far as I understand the specification) is that only unlabeled commands are associated to the module player.
Relevant snippet from the PRISM-games website:
Fixes #609