Inferring State (Part XI) / Day 36

Although I think I have a working system for state inference in jpf-prism, I don't think it's perfect yet (those small technical details have yet to be resolved, and I'm still not sure about scalability). One of the ways I might get to a better system was to ask my mentors. You might recall that one of the big issues with JPF "state" is that a variable can occasionally take multiple values in a state because JPF's search can choose to re-use an old state and update the value of a variable within it. I had corrected this by recording these changes to the state as "substates", which are nice because they are external to JPF's notion of state (and thus also to notions of state as recorded by, say, jpf-probabilistic, whose search mechanism we're using for the moment). So when we get a Markov chain out of JPF using this code, we see what we would expect: the Markov chain for the examples has the appropriate number of states, but also, we have what my code outputs: the details of the substates, and if a transition comes from a state with substates, we also know what substate it comes from--but if you don't care about this much detail (as in the case with jpf-probabilistic), you can ignore that.

The alternative is to change how the search object classifies a new state: make it so that any change in variable is a new JPF-state, and then proceed as before by using breakTransition() (a method in the VM I was unaware of until today). This is the method that is used by jpf-ltl, which was suggested by one of my mentors. This approach is probably safer, but it also might lead to confusion: if you're expecting a particular Markov chain, you might get one with extra states as no state will be reused, and so every variable change corresponds to a new entry in the chain. This method is what I was implementing today, and I think I had some good success--though I want to check it in greater detail tomorrow, and I'll need to modify it a bit still. I would have been done today, but some of my printing methods failed under the new state structure and I have to repair them a bit still. And there's optimization to be done: using the breakTransition method I was initially getting 33 states instead of the usual 8--I'm sure I don't need to break all of these transitions. Since then it's down to 21 (since some memory stores don't actually matter, for example, class loads). I think I can do a bit better still.

Further, borrowing ideas from jpf-ltl, I am also implementing ways of flagging certain variables to watch, or consider important during model checking, in addition to specifying a property before hand so that we can pass it through to PRISM--which will likely be necessary unless we're going to be generating all of the properties we're going to be checking in PRISM. This is not yet done, but it's not hard: maybe another hour of work tomorrow.