For the most part, state inference is complete: JPF will create a state every time a variable changes, and the code provides descriptions of the variables (that it has been instructed to watch) in that state. And of course we also know the transitions between the states, so we have a good idea of what the code in the SUT is doing. With this in mind, there were some small issues alluded to in the last post that needed some work, and most of this work has been bug-fixing, or cleaning up corner cases, or re-factoring code. Relatively small tasks that when combined, should allow for more interesting programs to be checked.
First on the list was to get the property we want to check in PRISM from the JPF configuration file. This wasn't a terribly difficult thing to import. The harder part came when trying to parse the property to get PRISM to then check for this particular property. What I did was to implement a basic parser and then invoke specific commands in the PRISM code to check various properties, based on the LTL syntax. I did this in a manner very similar to jpf-ltl, but whereas jpf-ltl annotates properties on methods in the SUT, for example,
@LTLSpec("[](<> \"done()\" && <> \"foo()\")")
public class AlwaysDoubleEventuallyFinite2 { ... }
we expect ours upfront, and phrased in terms of states, rather than methods:
markov.properties="[](<> \"state:5\")")
A current downside for this implementation is that since I'm requiring the property to be phrased in terms of system states, it currently requires two-passes to check a property: a first pass for the user to understand the states, and then a second to add a property phrased in state numbers and check it again using PRISM. What I want this to evolve into (since the checking so-far is mostly variable-centric) is to replace states with variables and values, for example:
markov.properties="[](<> \"x.y.outValue:5\")")
I think this is more flexible than jpf-ltl's technique of phrasing properties in terms of method calls (as method calls could return values as well). But I left this to another day. (And if we did want method calls in our properties, it's now easy to add them given that the underlying parsing has been implemented.)
Beyond this, I also wanted to support local variables. Currently, the way to specify what variables to watch uses JPF's pattern of package.class.variableName so that when JPF was matching variable names that it extracted during instruction executions, it could match them directly (they were extracted following the same pattern). I thought this was okay, but since we're also keeping track of all the methods being executed anyways, why not also track local variables (noting, that I'm putting off the issue, for now, of what should happen when a variable goes out of scope). So my pattern, package.class.method-methodName.localVariableName was introduced so that my code would identify when a local variable was also to be observed, in order to watch for entering and exiting of those methods, and look for those variables as well. When the variable is out of scope in a state, that variable is flagged in that state description as such.
Day 38 - Wednesday July 17th
In addition to supporting local variables, one of the issues I had pointed out in the past was that when store instructions were executed, array stores were not supported: the store would read as "?[0] = 1", which meant that I had no idea what what array was getting this value. I decided today would be a good day to look into this issue. This was a bit tougher than the last issues, and I'm not actually sure that I got anywhere. I think the solution is to build my own symbol table as JPF executes stores & loads with respect to arrays, and then track the addresses, and use those to look up the name and replace the "?" in the output above. However, that was a fairly daunting task that I couldn't complete without spending more time on (and even then, maybe not), so I put this off. I found a quick hack that will work for smaller systems; in particular, systems with at most one array variable: we can take the name of the array in the configuration file, and use that to descriptions of the array in the state descriptions (which really just adds readability). For 2 or more arrays, I still wouldn't know which is which so I couldn't make any improvements there. This is marked as an issue to revisit.
Still, the code feels much more complete and much less a prototype--though I'm sure it still is.
Day 39 - Thursday July 18th
Today's goal was to see if I could be more clever with respect to transition optimizing, thus reducing the number of states JPF generates. For example, many of the "21" states are empty states, that don't appear to change anything important in the system state, and just lead to another empty state. I found one source of this (a missing if-statement in the executed instruction method of my listener), and we dropped 3 states, but the source as to why so many other states are happening. I know from my listener there aren't more than a handful of additional changes (5) to variables in a state beyond those that caused the initial 8-state chain in the BiasedDie example listed on this blog much earlier (and as an example on the jpf-probabilistic page). So getting this down to 18 was good I suppose, but I would have liked to narrow it down to the (suspected) minimal of 13, or find an explicit reason as to why I cannot do that.
No comments:
Post a Comment