Strategy Generation Error on Windows

[ribsthakkar]

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)

An aside, 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?

[ribsthakkar]

I ran the same model through the command line and see the following stack trace appear:

java.lang.IllegalStateException: Trying to write to an invalid file handle (already closed?)
    at prism.PrismFileLog.printToLog(PrismFileLog.java:219)
    at prism.PrismFileLog.print(PrismFileLog.java:204)
    at prism.PrismLog.println(PrismLog.java:263)
    at explicit.STPGModelChecker.computeReachRewardsValIter(STPGModelChecker.java:1063)
    at explicit.STPGModelChecker.computeReachRewardsCumulative(STPGModelChecker.java:1377)
    at explicit.STPGModelChecker.computeReachRewards(STPGModelChecker.java:931)
    at explicit.SMGModelChecker.computeReachRewards(SMGModelChecker.java:2648)
    at explicit.SMGModelChecker.checkRewardCoSafeLTL(SMGModelChecker.java:1341)
    at explicit.ProbModelChecker.checkRewardPathFormula(ProbModelChecker.java:1415)
    at explicit.ProbModelChecker.checkRewardFormula(ProbModelChecker.java:1253)
    at explicit.ProbModelChecker.checkExpressionReward(ProbModelChecker.java:1176)
    at explicit.ProbModelChecker.checkExpressionStrategy(ProbModelChecker.java:587)
    at explicit.ProbModelChecker.checkExpression(ProbModelChecker.java:510)
    at explicit.StateModelChecker.checkExpressionFilter(StateModelChecker.java:1075)
    at explicit.StateModelChecker.checkExpression(StateModelChecker.java:709)
    at explicit.NonProbModelChecker.checkExpression(NonProbModelChecker.java:76)
    at explicit.ProbModelChecker.checkExpression(ProbModelChecker.java:530)
    at explicit.StateModelChecker.check(StateModelChecker.java:627)
    at prism.Prism.modelCheck(Prism.java:3199)
    at prism.PrismCL.run(PrismCL.java:395)
    at prism.PrismCL.go(PrismCL.java:221)
    at prism.PrismCL.main(PrismCL.java:2640)