DTMCUniformisedSimple.getDeadlockStates() crashes to NullPointerException

[ghost]

Hello! These are the only two constructors for class DTMCUniformisedSimple. Neither has a initialise() call.

        public DTMCUniformisedSimple(CTMCSimple ctmc, double q)
    {
        this.ctmc = ctmc;
        this.numStates = ctmc.getNumStates();
        this.q = q;
        numExtraTransitions = 0;
        for (int i = 0; i < numStates; i++) {
            if (ctmc.getTransitions(i).get(i) == 0 && ctmc.getTransitions(i).sumAllBut(i) < q) {
                numExtraTransitions++;
            }
        }
    }

    public DTMCUniformisedSimple(CTMCSimple ctmc)
    {
        this(ctmc, ctmc.getDefaultUniformisationRate());
        }

Without a call to initialise(), attributes such as protected TreeSet<Integer> deadlocks; remain null. DTMCUniformisedSimple does not override getDeadlockStates(), so getDeadlockStates() returns null. For example, constructing DTMCSparse from DTMCUniformisedSimple using this constructor crashes due to a NullPointerException.

    public DTMCSparse(final DTMC dtmc) {
                ...
        initialise(dtmc.getNumStates());
        for (Integer state : dtmc.getDeadlockStates()) {
            deadlocks.add(state);
        }
                ...
    }

It seems that the best solution would be to add implementation of getDeadlockStates() to DTMCUniformisedSimple so that it overrides the one from ModelExplicit, because that one causes the NullPointerException.

[ghost]

EDIT: identified the actual problem and proposed a solution

[kleinj]

Hi,

thanks. Yes, you are right, the deadlock states accessor methods should be added to DTMCUniformisedSimple, just calling the same methods in the underlying CTMC.

I can prepare a fix tomorrow.

Just curious: Were you able to trigger this during "normal" operations of PRISM or is this due to you using DTMCUniformisedSimple in a way that it has not been used before, thus revealing these missing methods?

[ghost]

No problem. No, I definitely did not find this during any normal or intended usage. Just me being silly, I guess.

I was working on implementing steady-state analysis for ACTMC in our PRISM fork, https://github.com/VojtechRehak/prism-gsmp. This involved reducing ACTMC (which extends CTMCSimple) to a DTMC. To be perfectly honest, I did not notice CTMC has buildUniformisedDTMC(double q), and I was using buildImplicitUniformisedDTMC(double q) instead. I thought buildImplicitUniformisedDTMC(double q) was the only way. Only later I noticed the word implicit in it, and dug a little deeper. I realised having to perform extra division for each element of vmMult(double vect[], double result[]) is probably not so great for performance. However, I still did not realise buildUniformisedDTMC(double q) exists, so I wanted to fix this by constructing DTMCSparse from the undesirable DTMCUniformisedSimple. Something like this, DTMC dtmc = new DTMCSparse(ctmc.buildImplicitUniformisedDTMC(q)); which kept crashing due to NullPointerException each time.

Before that, I also wasted a bit of time implementing

    public SuccessorsIterator getSuccessors(final int s)
    {
        // TODO
        throw new Error("Not yet supported");
    }

for DTMCUniformisedSimple because it may have been required for mvMult() or something, I am not sure anymore. At this point I started realising that DTMCUniformisedSimple looks quite bare-bones (or even unfinished) and that there must be a better way.

Since then, I have already discovered buildUniformisedDTMC(double q) to construct DTMCSimple and lived happily ever after.

[kleinj]

Ok, that's helpful. Glad you found the alternate way to obtain the uniformised DTMC.

I've pushed accessors for the deadlock methods and added a note in the JavaDoc pointing to the buildUniformisedDTMC to make finding that a bit easier.

There's also ongoing work to make these thin wrapper models more full featured.