Strategy Generation Error on Windows

[Rishabh Thakkar]

Hi, I am copying this over from GitHub issues as I didn't realize that this was the official forum help and discussion.

When I try to right click on a property and run "generate strategy," I receive an error saying:

Error: java.lang.IllegalStateException: Trying to write to an invalid file handle (already closed?) This is an unexpected error, it might be a good idea to restart PRISM.

At first I assumed it was due to the large size of my model, but I tested out the basic SMG example from the website here: http://www.prismmodelchecker.org/games/examples/smg_example.prism.php (along with its respective properties file), and it still yielded the same error. This example works fine when I run PRISM-games on my MacOS machine, but it only seems to be failing on my Windows machine.

I am running PRISM-games Version 3.0 (based on PRISM 4.6)

In addition, when I am able to generate the strategy and export it to a file, how should I interpret the resulting file or understand what actions the strategy is suggesting to choose?

[Rishabh Thakkar]

Turns out, on my MacOS machine, I am not able to a generate strategy for my model either although it does not return any error. 

I tried to do so both through the command line and the GUI. The program successfully returns the result from the model checking part, but it does not do anything further nor does it list any message regarding errors. Is there some model size limitation to export the strategy? I couldn't find anything in the source code indicating such. 

For reference, my model yields a system with 200k states, but I still think a strategy file should be able to be exported no?

Thanks,

Rishabh

[Rishabh Thakkar]

I have another update, I tried running the basic SMG examples such as dice.prism and coins.prism to generate the a strategy file, where a file is created, but the file is completely empty.

For reference, this is the command I ran:

./prism ../prism-examples/smgs/simple/coins.prism ../prism-examples/smgs/simple/coins.props -exportstrat coins.dot 

Is there some issue with SMG strategy generation?

When I do strategy generation with the rock-paper-scissors example, (which is a CSG) I am seeing a dot file generated. 

[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