Day 46 - Tuesday July 30th
Breaking transitions based on expression evaluation
appears to be working, though it is currently limited to expressions regarding
integer variables--I think that for our purposes, this will be sufficient, and the step to changing it to support, say real values, is not hard, it's just a matter of adding more cases to some statements and making sure some parsing and type-checking works. I've omitted this for now, but I mean to get back to it very shortly for completeness. I'll try to explain how this system works below.
At a high level, what I've done is connected the Search class, that actually determines new states and stores them (or indicates the VM to store them) within the JPF VM, a listener that watches for InstructionExecuted notifications, which observes what variables take what values, with our StateRecord class, which records the state of the system, and has been since modified to keep track of the properties as well.
The system starts in an initial state, parses the properties, detects what variables to watch, and proceeds to execute instructions according to the search class, in this case, RandomSearch (initially supplied by jpf-probabilistic), which has been modified to prohibit the calls of notifyStateStored, notifyStateAdvanced, and other similar state-traversal methods (and those that label the state of the system) unless it has been allowed to by the monitoring listeners. Execution of instructions is monitored by the VarRecorder listener class, which determines if the search class can proceed to store a state and consider a new (or old) state.
If the instruction executed does not affect watched variables (or variables included in the property definition), then the listener instructs the search that it can proceed to the next instruction to be executed, but without updating the state number, or considering this a new system state (though, since instructions are executed, I believe the kernel state in JPF to be changing--but this is not something we're ever dealing with, so I'm side-stepping this). On the other hand, if the variable is watched and included in a property, then we observe what value this property had before executing the instruction, compare it to the evaluation of the property after the executed instruction, and if this changes, we let the search class proceed, but this time telling it to consider this a new system state, as the evaluation of the property expression has changed. And this process is repeated for every executed instruction.
Basically, we're only considering new states if it changes a property's evaluation, otherwise we're in the same state. For example, consider a system with variable var, and property var != 2, under the following instructions taken by JPF's search (where state will serve to track the system state we're in), omitting probabilities for simplicity:
1. Initial state is populated:
state = 0
var = undefined
2. JPF executes "var = 0;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, and this is state other than the initial JPF state)
var = 0
3. JPF executes "var = 1;"
state = 1 (nothing happens: the evaluation of var != 2 still returns true, so we don't consider this a new JPF state; with respect to our properties, nothing new has really happened here)
var = 1
4. JPF executes "var = 2;"
state = 2 (this happens since this is an evaluation of var != 2 returns false, so we know something has changed with respect to a property, and we need a new state)
var = 2
5. JPF executes "var = 3;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, so we know something has changed with respect to a property, and since we've seen this before, we'll reuse state 1)
var = 3
6. JPF terminates
The state space with transitions would be three states, with transitions from 0->1, 1->2, and 2->1, with appropriate probabilities in the real thing.
The system starts in an initial state, parses the properties, detects what variables to watch, and proceeds to execute instructions according to the search class, in this case, RandomSearch (initially supplied by jpf-probabilistic), which has been modified to prohibit the calls of notifyStateStored, notifyStateAdvanced, and other similar state-traversal methods (and those that label the state of the system) unless it has been allowed to by the monitoring listeners. Execution of instructions is monitored by the VarRecorder listener class, which determines if the search class can proceed to store a state and consider a new (or old) state.
If the instruction executed does not affect watched variables (or variables included in the property definition), then the listener instructs the search that it can proceed to the next instruction to be executed, but without updating the state number, or considering this a new system state (though, since instructions are executed, I believe the kernel state in JPF to be changing--but this is not something we're ever dealing with, so I'm side-stepping this). On the other hand, if the variable is watched and included in a property, then we observe what value this property had before executing the instruction, compare it to the evaluation of the property after the executed instruction, and if this changes, we let the search class proceed, but this time telling it to consider this a new system state, as the evaluation of the property expression has changed. And this process is repeated for every executed instruction.
Basically, we're only considering new states if it changes a property's evaluation, otherwise we're in the same state. For example, consider a system with variable var, and property var != 2, under the following instructions taken by JPF's search (where state will serve to track the system state we're in), omitting probabilities for simplicity:
1. Initial state is populated:
state = 0
var = undefined
2. JPF executes "var = 0;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, and this is state other than the initial JPF state)
var = 0
3. JPF executes "var = 1;"
state = 1 (nothing happens: the evaluation of var != 2 still returns true, so we don't consider this a new JPF state; with respect to our properties, nothing new has really happened here)
var = 1
4. JPF executes "var = 2;"
state = 2 (this happens since this is an evaluation of var != 2 returns false, so we know something has changed with respect to a property, and we need a new state)
var = 2
5. JPF executes "var = 3;"
state = 1 (this happens since this is an evaluation of var != 2 returns true, so we know something has changed with respect to a property, and since we've seen this before, we'll reuse state 1)
var = 3
6. JPF terminates
The state space with transitions would be three states, with transitions from 0->1, 1->2, and 2->1, with appropriate probabilities in the real thing.
Day 47 - Thursday August 1st
Yesterday I was largely travelling, but I had several hours
on a plane in order to translate a few examples to test our code on, and I did spend today translating code. The code
was provided in C by one of my mentors, and show it had to translated into Java
to be run on our code. I won't describe the notion of examples, because I been asked not to release them yet, but I will say that there are about 12 of them (though 5 are already in Java). I spent most of the day translating the C examples into Java and making sure something runs with them, not yet with an eye towards checking the output of the examples, aside from making sure that at a glance it doesn't break anything. And so far, that was successful.
Day 48 - Friday August 2nd
I started today by supporting real-valued variables as mentioned in an earlier post; it didn't take long and I'm glad I got it out of the way. The rest of the day was committed to making sure that the example outputs were more than just functional: making sure that the results that we're getting are the one's we're expecting--this did not go well. Although I had mentioned in the past that I can parse properties successfully, I forgot that I only really had this working at a very syntactic level. I should explain, though I do recall mentioning this in the Skype meeting we had during the last week of July. Basically, in the past I had parsed properties to get them into memory on the JPF side: this involved ensuring the syntax was correct, that we had values for property expressions (at least when necessary), and of course breaking transitions and creating new JPF-states as a result of these properties changing. However, on the PRISM side of the code, which was largely untouched for quite some time, I had been passing in the same generic property to check reach-ability for: not the one that I was dealing with on the JPF-side. And while I had all this information, I didn't bother to update the PRISM calls. This was of course where the output started to falter, but I soon realized this, and spent the day parsing the property in a more semantic-case: understanding the property in terms of what state's it was targeting, and conveying this information to PRISM dynamically based on the property. The day was mostly spent on this issue.
Day 49 - Sunday August 4th
Today was spent towards the same issue as above: getting properties into PRISM in a suitable manner. It looks like the problem was resolved after some time for simple cases involving only a single property. The idea here is that since we break transitions based on properties, and each state corresponds to an evaluation of a property, we simply flag the state that corresponds to the true evaluation of the property, and ask PRISM to get the reach-ability of that state. (Of course, what happens if there is no such state? Then we don't even bother with any PRISM calls, and can return from the JPF-side code directly stating this. I think this makes sense--I will put this in an e-mail shortly.) The case with multiple properties doesn't seem any harder conceptually, but it required too many technical changes for today.
Day 50 - Monday August 5th
Again, and unfortunately, more of the same: getting multiple properties into PRISM in a meaningful sense. Conceptually, this was not hard, except that now there might be a number of states in which a given property is evaluated as true, and so we have to pass a number of states to PRISM. This I don't think required any special re-tooling on the PRISM side, as the computeUntilProbs (and similar) method takes a set of states to target. The changes to support these multiple states seems to have been implemented without cause for concern, but I want to test them. I started, again, to play around with translated examples, but I was actually pretty tired and my experiments didn't last long. I'll re-visit them, with some concrete news on their results tomorrow.
No comments:
Post a Comment