Format of Strategy File in PrismGames and Empty Strategies

40 views
Skip to first unread message

raykau...@gmail.com

unread,
Aug 22, 2020, 12:37:22 PM8/22/20
to PRISM model checker

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

unread,
Aug 23, 2020, 2:59:58 AM8/23/20
to PRISM model checker
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

unread,
Jul 29, 2023, 7:11:41 AM7/29/23
to PRISM model checker
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

unread,
Jul 31, 2023, 3:34:15 AM7/31/23
to prismmod...@googlegroups.com
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

unread,
Jul 31, 2023, 10:08:59 AM7/31/23
to prismmod...@googlegroups.com
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.
Reply all
Reply to author
Forward
0 new messages