Format of Strategy File in PrismGames and Empty Strategies

[raykau...@gmail.com]

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!

[raykau...@gmail.com]

Sorry there was a mistake in the message, it refers to the smg_example.prism file and not the dice example. But the strategy issue exists and I find an empty file.

Any leads would be helpful. Thanks!

[shuhao qi]

Yes, I also encountered the same issue. 

I can successfully export the strategy .dot for csg model. When I export the strategy for smg model, the generated .dot is empty even for the provided examples.

Did you solve this issue? Could you provide any advice or solutions?

best regards,

Shuhao

[Kaustabha Ray]

Can you check if adv.tra file is generated? That would contain the strategy

--
You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/38786dcb-9d13-44e4-8296-033368db6136n%40googlegroups.com.

[shuhao qi]

Yes, I write a program to achieve similar visualization based on exported states, transitions and adversary. Thanks for your prompt reply. 

Best regards,

Shuhao 

You received this message because you are subscribed to a topic in the Google Groups "PRISM model checker" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/prismmodelchecker/2ZO_NWUSDOs/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchec...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/CADQEYKGm72w%3DeV6%2ByV-R%3D_WVY5ZuP7Hv%3DUKJx_AU8kHrDv9zRA%40mail.gmail.com.