Hi
I was trying the property <<1>> Pmax=? [ F c=2 ] from the dice example, however the strategy generated file is empty. Are there some issues? What is the file format for the strategy synthesis file? The property <<1>> P>=0.84 [ F<=3 c=2 ] generates some results but I am unable to parse the output.
The dice module for reference
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
Thanks!