-
Notifications
You must be signed in to change notification settings - Fork 27
Open
Labels
Description
The simulator does not detect/report errors arising in states due to erroneous player definitions, like normal model construction does. E.g. the model below would result in the error Error: No player owns state (0,0) (because no player owns action send2)..
smg
player p1
host, [send1] //, [send2]
endplayer
player p2
client
endplayer
module host
h : [0..2] init 0;
[send1] h=0 -> (h'=1); // send message 1
[send2] h=0 -> (h'=2); // send message 2
[] c=0 -> (h'=0); // restart
endmodule
module client
c : [0..2] init 0;
[send1] c=0 -> 0.85 : (c'=1) + 0.15 : (c'=0); // receive message 1
[send2] c=0 -> 0.85 : (c'=2) + 0.15 : (c'=0); // receive message 2
[] c!=0 -> (c'=0); // request another message
[] c!=0 -> true; // wait
endmodule
Reactions are currently unavailable