Prism-games command line option for exporting strategy

[Artur Rataj]

Hello, I have an SMG model, for which I can only export the strategy file using the gui. The command--line option -exportadv is ignored, e.g.

prism -s -cuddmaxmem 6000000 '4,2.nm' '4,2.pctl' -exportstates A.sta -exportadv A.tra

exports states, but no strategy. Is it intended, that the strategy can be obtained only within GUI, or is there another option? I use prism-games.beta.r5753.

Best regards,
Artur

[Vojtech Forejt]

Dear Artur,

I confirm that I can reproduce this bug and that for some properties
the strategy does not get generated. It will get fixed in the next
release of PRISM-games. To make sure I have not missed your particular
case, can you send me the content of the file '4,2.pctl'?

Vojtech

> --
> 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 post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Artur Rataj]

Dear Vojtech,

I don't have the file just now, but it only contained properties of the form

Pmin=? [ F variable=constant ]
Pmax=? [ F variable=constant ]

Thank you a lot for fixing the bug.

Artur

[Ashutosh Pandey]

I can't export strategy with -exportadv option with the latest release of prism games. Here is the command line I am using

final.smg prop.pctl -exportstates result.sta -exportadv adv.tra

Here is the log

PRISM-games

===========

Version: beta

Date: Thu Sep 10 00:13:33 EDT 2015

Hostname: ubuntu

Command line: prism final.smg prop.pctl -exportstates result.sta -exportadv adv.tra

Parsing model file "final.smg"...

Parsing properties file "prop.pctl"...

1 property:

(1) <<sys>> R{"util"}max=? [ Fc "final" ]

Type:        SMG

Modules:     environment clk controller removeServer addServer divert_traffic increaseDimmer decreaseDimmer 

Variables:   s time readyToTick active_servers_A active_servers_B active_servers_C dimmer traffic_A traffic_B traffic_C removeServer_go removeServer_used addServerA_state addServerB_state addServerC_state addServer_go divert_go increaseDimmer_go increaseDimmer_used decreaseDimmer_go decreaseDimmer_used 

Switching to explicit engine, which supports SMGs...

Building model...

Computing reachable states...

 4848 states

Reachable states exploration and model construction done in 0.289 secs.

Sorting reachable states list...

Time for model construction: 0.338 seconds.

Warning: Deadlocks detected and fixed in 294 states

Type:        SMG

States:      4848 (1 initial)

Transitions: 11642

Choices:     11642

Max/avg:     8/2.40

Exporting list of reachable states in plain text format to file "result.sta"...

---------------------------------------------------------------------

Model checking: <<sys>> R{"util"}max=? [ Fc "final" ]

Building reward structure...

Computing rewards...

Starting expected reachability...

Starting Prob1 (maxmin)...

Prob1 (maxmin) took 14 iterations and 0.075 seconds.

Starting Prob1 (maxmin)...

Starting Prob0 (maxmin)...

target=3264, inf=0, rest=1584

Starting value iteration (maxmin)...

Value iteration (maxmin) took 8 iterations and 0.034 seconds.

Expected reachability took 0.124 seconds.

Value in the initial state: 57.78443113772456

Time for model checking: 0.163 seconds.

Result: 57.78443113772456 (value in the initial state)

---------------------------------------------------------------------

Note: There was 1 warning during computation.