Inferring State (Parts VI & VII) / Days 31 & 32

Day 31 - Tuesday July 9th
Today, I was looking into how JPF actually defines "state" of a system. This was a bit confusing: System-Under-Test (SUT) state appears to be saved in the KernelState and SystemState classes, but neither of these seem to describe the abstractions used: at least, there are no concise representation of the abstractions, and it looks like several other classes call the setID method for these objects, and so there was a lot of reading, searching for method invocations, and general understanding of the JPF VM code undertaken. I understand a lot more now, but still not sure where the code says that an integer variable in the same state can take multiple values. Continued reading is in order.

Day 32 - Wednesday July 10th
Today (after having my power connected again - no more coffee shops for posting!), I was continuing the search for how JPF defines a state, or what abstractions it uses, or what conditions allow a variable to change values within a state. From the looks of it, it depends largely on the ChoiceGenerators and Search objects: the latter control when state is advanced or backtracked, but the former can (possibly) make a different choice in the same state. For example, a search might encounter state A, generate a choice a1, proceed to state B, backtrack, and this time, make another choice a2. In this way, the number of states has not increased, but JPF can search multiple paths based on the choice generator. So this looks like a good way to define "state"--by looking at the possible options in the choice generator. In particular, for our code, this information is relatively easily defined: as a probability distribution. All I need to know is what variables in each state are subject to those distributions, then I can look at the distribution, and have the entire range established. I did start along this path a few days ago (Day 27), but it didn't seem promising at the time. I guess it's time to re-visit that code and see if I can get this finished up in the next day: it definitely sounds promising.