NullPointerException with -transient in 4.8

[ningit]

The command prism -transient 1 model.pm where model.pm is the following

dtmc
module M
    x : [0..2] init 0;

    [] x=0 -> 0.5:(x'=1) + 0.5:(x'=2);
endmodule

fails to compute the transient probabilities because of to the following exception:

java.lang.NullPointerException: Cannot invoke "explicit.Model.getNumInitialStates()" because "<parameter1>" is null
    at explicit.ProbModelChecker.buildInitialDistribution(ProbModelChecker.java:1317)
    at explicit.DTMCModelChecker.doTransient(DTMCModelChecker.java:438)
    at prism.Prism.doTransient(Prism.java:3928)
    at prism.PrismCL.doTransient(PrismCL.java:1089)
    at prism.PrismCL.run(PrismCL.java:390)
    at prism.PrismCL.go(PrismCL.java:228)
    at prism.PrismCL.main(PrismCL.java:2980)

I am using Java 21 and PRISM 4.8 from the release page of this repository. The same command works with PRISM 4.7 and previous versions in the release page.

[davexparker]

Thanks @ningit. This looks like a problem that was fixed here: 4fcd975

It has not made it into a packaged release yet, but is fixed in the main codebase on GitHub:

https://github.com/prismmodelchecker/prism

[ningit]

Thanks @davexparker for your reply. I have also tried by compiling the GitHub source (the current head, 90acc6cd) and the problem still happens. Moreover, it seems that 4fcd975 is already in 4.8.

[davexparker]

Oops - my mistake! Thanks. I'll investigate.

[davexparker]

Thanks for this @ningit. It's now fixed, and (since it seems to completely break transient probability computation) I've pushed it out as a new release (v4.8.1) too. https://www.prismmodelchecker.org/download.php

[ningit]

Thanks @davexparker. I have rerun my examples and they are working again.