moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
138 stars 75 forks source link

Error when using action labels to specify players in SMGs #609

Closed weiss-i-net closed 2 months ago

weiss-i-net commented 2 months ago

When specifying the players in an SMG using action labels, storm incorrectly complains, that there are modules with unlabeled commands. Prism games can correctly handle this situation.

Steps for reproducing:

action_labels.prism
===================

smg

global state : [0..2];

player p1 [a1] endplayer
player p2 [a2] endplayer
player p3 [a3] endplayer

module m1
    [a1] state=0 -> 1/2 : (state'=1) + 1/2 : (state'=2);
endmodule

module m2
    [a2] state=1 -> 1/2 : (state'=0) + 1/2 : (state'=2);
endmodule

module m3
    [a3] state=2 -> 1/2 : (state'=0) + 1/2 : (state'=1);
endmodule

Call storm with:

./storm --prism action_labels.prism

Output:

Storm 1.8.1

Date: Fri Aug 30 17:24:02 2024
Command line arguments: --prism action_labels.prism
Current working directory: /home/jannik/ba/storm_test

Time for model input parsing: 0.166s.

ERROR (PrismNextStateGenerator.cpp:663): Module m1 is not owned by any player but has at least one enabled, unlabeled command.
ERROR (storm-cli.cpp:63): An exception caused Storm to terminate. The message of the exception is: WrongFormatException: Module m1 is not owned by any player but has at least one enabled, unlabeled command.