Thursday, September 26, 2013

End of Google Summer of Code - Concluding Remarks

Since the program is officially ending, everyone should know the state of the jpf-prism code at this end. In case there is anyone reading this blog that I don't email updates to, I'm going post some concluding remarks here, taken from an email I sent to my advisers/supervisors.

All the code for the project is found at the BitBucket repository, https://bitbucket.org/jpfprism/jpf-prism, which is still private, but hopefully we'll open it up soon. The Javadoc for the code, which unfortunately cannot be hosted on the same page, is located on my department webpage: http://www.math.uvic.ca/~jgorzny/jpf-prism-doc/ (and is included in the repository). A pointer to this link, as well as brief tutorials on how to install the code, run the code, and specify properties to check, can be found on the wiki on the BitBucket repository: https://bitbucket.org/jpfprism/jpf-prism/wiki/Home

As for the final state of the code in terms of functionality, I think it went pretty well (though not everyone was finished, I'm afraid). The short of it is that we can check any Java program that uses probabilistic functions based on Java's Random() (or jpf-probabilistic's Choice()) method. By "check" I mean that PRISM will be invoked on the states of the system and compute the probability of reaching a state with that property being true. Further, in case verification takes too long, or to confirm results, jpf-prism can be used to run the Java code repeatedly without interference, to get an empirical measure of the probability of reaching such a state. Further, the code will optimize the states of the systems if possible: it will reduce chains of states that are connected with probability 1 to a single state, unless it cannot (e.g., a choice was made, or a property must be evaluated in one, but not all of the chain's states).

So I think the project was mostly a success: the basic goal of leveraging the ease of checking a Java program with JPF and the support of probabilistic programs of PRISM has been accomplished. 
Finally, if you play around with any of the code, and something goes wrong, please let me know! I'd like to think I've got a pretty stable version of the code in the end, but if you find a bug I will be more than happy to fix it.

Wednesday, September 18, 2013

JUnit Tests / Day 72

Today I spent the majority of the day working on making some JUnit tests for many of the methods I've written in the past months. In some cases, this was not easy as setting up a "fake" JPF instance (used in tests) so that I can properly test methods involved setting up a lot of things that I had previously taken for granted due to configuration options or default settings. But the good news is that so far, I haven't had any tests fail! So things should be working as intended, and finding more bugs really was something I was hoping to avoid so late in the program, so I was happy with the tests.

Tuesday, September 17, 2013

Javadoc Generation and More Cleanup / Day 71

So I noticed for Friday's post I didn't actually say what I did, so I'll just note here that it was largely more of the same: cleanup, documentation and other non-functionality related things. I'll also note that I was busy in class all day today, as well as on Thursday so I don't have a post for that day.

As for today, the goal was to generate Javadoc, maybe start writing a (JUnit) test or two, and put the example description onto the wiki, and re-do the overview page on the BitBucket page. I didn't get around to anything but the Javadoc, and since BitBucket doesn't host Javadoc (at least, not externally to the repository's copy), I've hosted them on my department website which should have pretty good up-time. The URL for the Javadoc is therefore: http://www.math.uvic.ca/~jgorzny/jpf-prism-doc/. Since this is external to the repository's version, I'll try to keep it updated but no promises that the updates will happen as quickly as the code changes. So if you want the most updated Javadoc, you can checkout the repository (or update it, as the case may be), and look in the "doc" directory (assuming I remember to keep writing comments and generating the Javadoc before each commit!).

Sunday, September 15, 2013

Example (Finally!) / Day 70

Day 70 - Friday September 13th

Today I'm going to show a quick example of the kinds of output you might see when running jpf-prism. To do this, I'll talk about the Biased Die example that is provided by jpf-probabilistic (and has been copied into our repository), since this one is already publicly available. Over simplifying, the example is of a system that generates the roll of a die with some bias during computation. The computation of the roll result is done by an algorithm from Knuth and Yao in '76; the jpf-probabilistic repository describes it in greater detail, so check it out there if you're unfamiliar with it. jpf-probabilistic would display the something similar to following (taken from the jpf-probabilistic repository, note that in this case there's no bias, since the probabilities are all 0.5):
0 ------> 1
1 ------> 2
2 -0.50-> 3
3 -0.50-> 4
4 -0.50-> 3
4 -0.50-> 5 *
3 -0.50-> 6
6 -0.50-> 5 *
6 -0.50-> 5 *
2 -0.50-> 7
7 -0.50-> 8
8 -0.50-> 5 *
8 -0.50-> 5 *
7 -0.50-> 9
9 -0.50-> 7
9 -0.50-> 5 *

For this example, the property we'll check is whether or not the roll is less than 2 (i.e., a 1 is rolled).

While in jpf-prism we can do something similar, we only get an output like that if we're in debugging mode, and then we get a whole more (probably uninteresting) information, so don't expect quite that. We do display the Markov chain for our SUT, but only after we've built it, passed it to PRISM, and then queried for it. In short, this means a less pretty output for the chain itself. So what we actually get is the following:

Executing command: java -jar C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\src\examples\prism\probabilistic\BiasedDieTest.jpf 
JavaPathfinder v7.0 (rev 1067+) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
prism.probabilistic.BiasedDieTest.main()

====================================================== search started: 15/09/13 5:19 PM
a: 1
a: 5
a: 4
a: 6
a: 2
a: 3

====================================================== Exporting to PRISM
Search finished, printing PRISM's interpretation of the Markov Chain
trans: [ 0: {1=1.0}, 1: {2=0.5, 3=0.5}, 2: {4=0.5, 5=0.5}, 3: {6=0.5, 7=0.5}, 4: {2=0.5, 8=0.5}, 5: {8=1.0}, 6: {8=0.5, 9=0.5}, 7: {3=0.5, 8=0.5}, 8: {}, 9: {8=1.0} ]
Printing to dot file "C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\dotfile.txt"


In order to make this easier to read, I suggest exporting the chain to a dotfile, and viewing the result with Graphviz. The result is an image like the following:



Which is much easier to read than a text representation anyways. Note that there may also be more or fewer states, depending on if we can condense a chain of probability 1 transition/state pairs, or if we need to add states because a property's evaluation in the SUT becomes different and we need to track that to determine which state to pass to PRISM.

After jpf-prism outputs this information, PRISM will then compute the reachability probabilities for each of the probabilities, and that will look something like this.

Starting probabilistic reachability...
Starting Prob0...
Prob0 took 4 iterations and 0.001 seconds.
Starting Prob1...
Prob1 took 8 iterations and 0.0 seconds.
target=1, yes=1, no=5, maybe=4
Starting Gauss-Seidel...
Gauss-Seidel took 17 iterations and 0.001 seconds.
Probabilistic reachability took 0.002 seconds.
0.16666666651144624


And then JPF will finish its output:

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=10, visited=7, backtracked=17, end=6
search:             maxDepth=0, constraints hit=0
choice generators:  thread=3 (signal=0, lock=1, shared ref=0), data=7
heap:               new=690, released=95, max live=0, gc-cycles=17
instructions:       10829
max memory:         120MB
loaded code:        classes=65, methods=1334

====================================================== search finished: 15/09/13 5:19 PM

And that's it! To verify the accuracy, you might simulate the SUT a few times to see if this value matches in practice. If you did that, the output would look something like this:

Executing command: java -jar C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\src\examples\prism\probabilistic\BiasedDieTest.jpf 
JavaPathfinder v7.0 (rev 1067+) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
prism.probabilistic.BiasedDieTest.main()

====================================================== search started: 15/09/13 5:14 PM

====================================================== Simulation #0
a: 3

...(omitted)

====================================================== Simulation #9999
a: 1
p1 was true in this simulation.

====================================================== Simulations over: results
p1 was true at the end of the simulation 1694/10000 = 0.1694% of the time.

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:01:46
states:             new=0, visited=0, backtracked=0, end=0
search:             maxDepth=0, constraints hit=0
choice generators:  thread=22793 (signal=0, lock=10000, shared ref=0), data=36708
heap:               new=4210184, released=200000, max live=0, gc-cycles=59501
instructions:       104953788
max memory:         0MB
loaded code:        classes=65, methods=1334

====================================================== search finished: 15/09/13 5:15 PM

Note that this value is pretty close to the one above, so things went as expected. And for a fair die, the probability of rolling a 1 should be 1/6 = ~0.166666..., so we have even more confidence in the answer.

Thursday, September 12, 2013

Documentation & Package Separation / Day 69

Today was spent equal parts writing comments & documentation and separating the packages used in the code. Documentation wise, I added two pages to the wiki on the jpf-prism repository: one to describe the command line interface (though not yet any problems with compiling it!), and one to describe how to specify a jpf-prism property. Tomorrow I hope to put up some examples on the Wiki as well. That brings me to my second point: separating packages. Recall that I was borrowing some classes from jpf-probabilistic, and that I had copied them into our repository. However, I didn't change the package names. So while this was not a big issue while also requiring jpf-probabilistic, I'm trying to free us of that requirement by excluding it. This means in some cases changing our classes so that the correct classes are being used. This was a fair bit of work, because apparently sometimes the behaviour didn't quite copy over to new class names, opting instead to try to find old (non-classpath-included) classes. But that was fairly straightforward to resolve, even if it was tedious.  I also cleaned up a few "TODO" comments in the code, by handling more corner cases or cleaning up output.

Wednesday, September 11, 2013

Winding Down / Day 68

After getting settled into my new program, I'm back to concentrating on this project. I hadn't really meant to put this aside last week, but the first week was full of classes and orientation sessions to sit in on, so I didn't have any real time to work on this. That being said, I'm back to nearly full concentration on this project, though it's unfortunate that this week has to be used in order to prepare for the pencils down portion of the program. That being said, I'm definitely planning to continue working on the project after the Google program ends, but this pencils down period must still be observed.

Today was spent doing things towards exactly that end. The day started with an early Skype meeting, which outlined some tasks to be done before the pencils down deadline. First, there was some issues with compiling my wrapper script, so I may look into simplifying that further, but it's not a big priority. Second, an issue regarding properties which I thought I had fixed resurfaced; I think I've got it fixed for sure this time, but only future testing will confirm this. Third, much was discussed about cleaning up the code, documentation, and other things that need to be done that I've been putting off.

To that end, the wrapper lacks a "-debug" option, that I've put in. I'll put out an "official" guide for command line calls to it on the page tomorrow, as well as a description of how to specify properties.

I've also started actually cleaning up code and separating anything from other packages (like jpf-probabilistic) and removing classes that aren't used anymore. And code documentation needs to be updated for most of the code, and so I spent some time doing that as well.

Simulating might still have a bug too, as during the meeting an attempt to simulate the BiasedDie example didn't terminate quickly. Might just be due to the Math.Random native peer enumerating too many options. I'm investigating. Along with that is checking various properties to see if they converge to values suggested by the PRISM output for the probability of the property being true. I'm not going to compile a formal report of these examples, but I'll probably make a spreadsheet and describe them here on the blog.


Monday, September 2, 2013

Multiple Updates / Days 62-67

Day 62 - Wednesday August 21st
Again, looking at the Random native peer from JPF. I was under the impression the whole day that I had to write a new ChoiceGenerator to invoke the peer, or methods from it, but this doesn't seem to work, and it seems that my code doesn't quite like accepting new ChoiceGenerators, so I'm not sure this is the way to go. I was also looking at modifying search classes to work with Random calls, but that seems even harder. I'm still committed to getting arbitrary Random method calls to work though!

Day 63 - Thursday August 22nd
Today was another Skype meeting, and I didn't do a whole lot prior to it. The meeting was quite productive I think, serving at the very least to alert me to some bugs in the code that I was not aware of (always fun to have during a demo situation!). In addition, installation seemed to be a bit of an issue so I also resolved to test the installation (and functionality) on Mac and Linux systems, though I don't have access to the former. I might be able to use a Mac when I start up studies again in September, so I'll keep this in mind. I did install things on my Ubuntu installation, and all seemed to go well. I had a few environment variables not set on another Windows install, but beyond that it did seem to work well on a fresh install (though I may have done something to ease the process without knowing it).

Beyond the demo-related incidents, the meeting served to discuss the code I had worked on the previous week, and we certainly cleared up some issues. There was a lot of talk about getting the Random calls to work and that seems to be the best way to go. Also a small issue of where properties that don't have a location specified are checked. For ease of use, I'll also develop a wrapper to automate .jpf file creation and calls to JPF.

Day 64 - Friday August 23rd
Random() method calls work! The fix was extraordinarily easy too: a parameter passed into the configuration, and a few checks to see what ChoiceGenerators are already registered to JPF when using those options. Then it was just a matter of finding the right one(s) and getting the probabilities out of them. I'm very glad that was accomplished.

Moved to Victoria between these days!

Day 65 - Monday August 26th
Today was a bug fixing day -- as I mentioned above, the Skype meeting revealed some deadly bugs that I had to squash, and they were a welcome change from looking at native peer code all day.

Day 66 - Tuesday August 27th
After fixing the bugs, I was confirming behavior should work as required, and I started by looking at where properties that are specified but never marked with a location (using a method to specify where in the code) are marked to be checked by PRISM. They were supposed to be checked at end states, but somewhere during the last few weeks that must have been changed, and they were not. Sadly (and rather unproductively), I spent the day working on fixing that.

Day 67 - Wednesday August 28th/Thursday August 29th
To sum up today: clean up. Specifically, testing, translation fixes, and a wrapper class for use by command line users. The examples provided were a mix of Java programs and C programs as I've said; the Java ones work, but the C ones did not, largely due to my translation to Java. I think I have some of those working now too though (though since some functions are defined in libraries I external to the provided code, they may not be truly correct; I need to confirm some of the implementations). Regardless, there was work to be done cleaning up things and using Random calls instead of Choice calls.

Beyond that, I developed the wrapper class for command line calls. The idea is to simplify use and avoid having to create .jpf files. For example, instead of having to create a few lines to run the simulation-aspect of the code, a user can now simply run

jpf-prism-run -simulate [-d:dotfilepath] -n class propertiesfile 

from the command line (after appropriate environment variables are set, as I think will always be necessary), where n is the number of times to simulate the specified class (which must contain the main method to run) with the properties contained in the propertiesfile. Generating a dotfile can be done using -d:dotfilepath to specify a file to output it to. "Standard" (non-simulation) verification is even easier:

jpf-prism-run [-d:dotfilepath] class propertiesfile

where the user no longer has to specify watched variables: only those in a property will be watched.


Wednesday, August 21, 2013

Random class and code maintenance / Days 60 - 61

Day 60 - Monday August 19th
Today, I was running more experiments while also looking into the jpf-core version of the Native Peer for java.util.Random(), which of course I was not aware of last week! From the looks of it, it would not have been particularly helpful for the current translations, as it is almost too powerful for the work around that was implemented. But this of course might be better. I spent some time looking at it, and seeing if I can use a modification of it to make translations even more straightforward, or to require to no translations at all. That would be really nice. No progress there yet!

(And I know I said results today, but I was distracted. They will be ready very soon!)

Day 61 - Tuesday August 20th
Today, I was looking at the jpf-core implementation of Random again. I haven't made a whole lot of progress, but I would really like to get this version working, with at least the simulation aspect of the code. The idea of not having to translate many Java programs is just too irresistible, and I feel it will make the the code much more easily usable. I think the problem is that the class tries to enumerate all random choices, and this causes the run-time to sky-rocket, although in most cases we only need a small subset of all possible random choices. And I don't yet know how to control this behavior.  I spent some time cleaning up the code just as a change: there was a fair bit of dead code, old comments, and not-commented code, so I cleared many of these issues.

Monday, August 19, 2013

Approximating results listener / Days 58 - 59

Day 58 - Thursday August  15th
A new listener made up much of today's work, and the idea is observation only. The listener is not meant to interfere with choice generation at all, but rather to run the SUT as if the JPF VM was any old Java VM, and have it run it's course. Then it looks to see at given times (or at the end of the run) is a given property is true or false (e.g. through a new method similar to others added this week: EvaluateHere(String propertyName), and similarly for many properties). Then it records this information, and then runs it all again, and again, up to a given bound, to see how many times each property was true or false, and reports this. Today was the start of that listener (which for the most part is a re-purpose of VarRecorder, with some changes), but unfortunately not the end of it.

Day 59 - Friday August 16th
Friday was a continuation and completion of Thursday's work. It looks like I've got the listener running the way it should, and I spent a bit of the day testing it, and comparing results with that of results from earlier runs. I also toyed around with the notion of letting it run the SUT for as many runs as it can before X minutes pass, but I wasn't really successful there.

I was also updating data for all the examples and I still had some larger examples to try that I'll just leave running at various times over the weekend so that I can get some really interesting (read: larger size) scalability results, and possible track memory usage in addition to time), so that I can pass off that report/spreadsheet I mentioned earlier. Expect that Monday (though probably not on this blog!).

Property locations, native peer execution and examples (again) / Days 55 - 57

Day 55 - Monday August 12th
Let me start the blog post by quickly adding that during the Skype meeting last week we also spoke about one other issue: tracking not only when a property becomes true or false, but where it does so: that is, tracking the location in the program where this could happen, as well as being able to ask jpf-prism not about about an expression, but an expression being true at a given line of code in the SUT. This is what I started off the day implementing, and I think it went well. The idea I used here was to give each property in the .jpf file a name (so that the syntax is name: expression), and then to add a JPF utility class with static methods PropertyIsTrueHere(String propertyName) and PropertyIsFalseHere(String propertyName) that the SUT can call at the appropriate code location with the name of desired property passed in. Then jpf-prism will look at method it enters, and if it's one of these, it'll flag the state and pass it to PRISM for the appropriate checks.

The rest of the day was committed to the native-peer programming. The issues I had were largely technical, and were overcame today, so it was a pretty good day; I'll omit the details, and instead talk about the solution. The idea was that the Choice class was unable to re-size its arrays dynamically for the SUT, and so translations were rather difficult (or at least tedious). In order to fix this, I created a new method in the Choice class that not only gets a random choice from an array of probabilities, but then also returns a new probability array with the choice removed, and the probability of that choice uniformly distributed to the remaining entries in the array. This way a SUT can use a dynamically shrinking probability array much more easily (two lines for every random() call, instead of the previous five or size). But beyond this, there might be other situations where you need to change the array, so I also created a few other methods: for example, if you're only making the call on one such array (that only shrinks throughout execution) we can further reduce this to a single call that will do the same thing as above but with a single call after providing an initial array to the peer. Or if you need to change the probability of the resulting array with a bias, there's a method to do that so that the new array returned is modified with a bias (supplied as an array) added to the appropriate terms (though in this case it's up to the SUT to make sure the probabilities sum to 1).

Day 56 - Tuesday August 13th
Today was spent dealing with examples again. This was also a good test of the new native peer code, but I was looking more to dealing with issues of scalability. Again, examples are not yet public, but one deals with dealing random playing cards out, and for small deck sizes (< 6), the code returns almost instantly, but for larger values it does take a fair bit longer, for example a deck size of  8 took about 30 minutes, and 7 was somewhere in between. I'm hoping still that might be because I'm not correctly abstracting states, but at this point I'm not so sure. (And in case any one is wondering, the PC I'm using is an Intel Core i7 2.8Ghz with two cores and 8GB of RAM on Windows 7, so while it's not the best, it's not a slow system.)

Day 57 - Wednesday August 14th
Today was more dealing with examples; I'm compiling a report of the results to send to the mentors, but I also had to re-do some of the translations I had done last week. And there were a few more issues with my code finding bad indexes or null pointers, so I had to make a few fixes, change them, and re-run all the results again.

Additionally, I updated the PropertyIsTrueHere (and similarly, false) to support many properties at once: PropertiesAreTrueHere(String[] propertyNames), just for convenience. 

Tuesday, August 13, 2013

Examples and clarifications / Days 51 - 54

Day 51 - Tuesday August 6
Today I was working on making sure that the examples worked in more than just a syntactic manner. And, unsurprisingly, they did not. There were several issues discovered across the examples, some of which are most like bugs in my code, others that are slightly more fundamental, and a few that may just be translation issues. Since the examples are not public, I won't talk about the specific issues in each example, but try to summarize the high level concerns. First, ignoring the issues that I think are related to my code functioning properly, there are issues translating arbitrary random codes: they each have their own notion of random(), which makes translation difficult, and in some cases, impossible, at least without further changes. In particular, for each call that should return a new "random" number, or get one from a choice, we (JPF) need a native-peer to execute, so that we (specifically, our choice generator class), can see what choices were possible, and what was made, to exhaustively check choices correctly. So a Java program calling just calling random() needs to be modified, so we know what the context is, and what the options are (that make sense). So we need something like jpf-probabilistic's Choice class, that is executed on the JPF side so that everything works. In some cases, we can use this class, but that also causes other issues: we need to know the possible choices not only at the beginning, but every time we need a choice, so that if our possible choices change, the program is then also responsible for tracking that, and updating the Choice class as necessary. So there isn't always a 1-1 call replacement in translation.  Of course, if we don't do this, and run the examples with Java's random(), then JPF returns rather quickly, because it thought it didn't have to make any choices, and so there wasn't a whole lot to model check: but this means nothing was really accomplished.

Day 52 - Wednesday August 7th
Today I managed to get some of the examples working with this extra code that tracks choice/probability changes across program execution so that we could get something to work. This was somewhat successful: the code seems to do everything correctly (at least on one example), but I have hit some issues with scalability. For a program with about 12 (uniform) choice options, my patience ran out before the system returned (but after waiting at least half an hour). I was deterred because of this, and spent the rest of the day trying to convert other examples to resolve the issues mentioned above.

Day 53 - Thursday August 8th
Today was marked by a Skype meeting with one of my mentors, that set the stage for the next week and clarification of the ideas that I was working on during this week and last week. First, we talked about breaking transitions on expression evaluations, and there were some changes that I implemented: it shouldn't be quite as simple as I was making it: we do want to track every choice and note with special concern when states change due to an expression evaluation changing. So I went back and modified this so that every choice generated is a new state, and when an evaluation changes. The idea now is that we only merge or condense states if they're linked by a transition of probability 1.  For the resolution of the random() function, we've decided that we can almost certainly get a work-around using the Choice class that will offload much of the tracking of probabilities during execution to this class, as opposed to the SUT. I won't go into detail on this until I'm done implementing it, so as to avoid confusion if I have to change anything. In addition, if I have time next week, I'm to start working on something like a statistical estimator for checking probabilistic systems: basically, run the SUT in JPF-prism X times without modification to choices (i.e. as if we're running it on any other Java VM), and watch the variables/property expressions. Then we can count Y/X, an empirical estimate of a property becoming true based on what we've seen.

Day 54 - Friday August 9th
Today was working on augmenting the Choice class to accommodate changes with respect to the notes above. This was somewhat complicated, as I have to make sure that I get the base class working correctly and modifying the JPF native-peer correctly, the latter of which is a new concept to me, and one that stood in my way a bit. As a result, I'm still working on this.

Tuesday, August 6, 2013

Expression based properties, examples & test cases, and some under-the-hood changes / Days 46 - 50

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->11->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.

Tuesday, July 30, 2013

Expressions for Properties (Part II) / Day 45

Day 45 - Monday July 29th

Today I was working on getting transitions to break on the evaluation of Java expressions, as mentioned in the last post. The back-end code was in place and all I had to do was populate a symbol table of watched variables in order to see when the expression’s Boolean value changes.  Although this was simple, I have some concerns regarding whether or not to change JPF’s state (i.e. modify the search class that is in use) or track state externally again (more complicated). I have opted for the first.  Still some minor corner cases to handle, but on the whole this is looking pretty good. On the administrative side of the program, I also wrote up a draft of the midterm evaluation, and I’ll revise it and upload it (to Melange) tomorrow.

Sunday, July 28, 2013

Parsing Fixes & Expressions for Properties / Days 41 - 44

Day 41 - Monday July 22nd & Tuesday July 23rd
I'm splitting this work day in two because I was fairly distracted again: on Monday I was finding an apartment (which I did!) for my upcoming move, and Tuesday was a half-day trip to the dentist. So I will have to make up a day of work.

Anyways, what I did work on was to see if I could parse more interesting state/property descriptions. The initial parser I had written was sloppy and didn't quite work as well as I had initially thought. So I spent the day re-writing this; I'm still not particularly happy with it (it's not a standard LALR parser, so it's likely slower than other existing parsers, like SableCC.), but it will do for now, and it parses based on variable/value, as opposed to state number. That is, we accept markov.properties="[](<> \"x.y.outValue:5\")"), type properties. That being said, although it parses better, I'm not yet doing anything with the property: I'm still checking nothing related to it. But the parser did need the fix, so this was the first step.

Day 42 - Wednesday July 24th
Today the day was started with a demo of the code and an outline of it to my mentors on Skype. The talk was very helpful and productive, and suggested many changes to the code and outlined a concrete direction to take for the immediate next steps of the project. There were some small changes that were easily fixed: moving some classes to the appropriate packages in the source and moving a parameter from the .jpf files to the jpf.properties file. Easily done. Only slightly harder was building the Markov Chain in PRISM on-the-fly (as opposed to when the search was finished), and that too is now implemented. This should reduce our memory footprint when checking models. The system can now also export the Markov chain in a DotFile for use with visualization with Graphviz. The most interesting ideas were the next steps: to get the the properties that we're interested in checking to be represented not as states, or particular variable values, but rather to be handled as Java expressions. Further, we could use these expressions to break transitions (or not) and use this to also trim the search space. The rest of the day was focused on introducing myself to the tools I was suggested as a starting point: the PreCondition class from the gov.nasa.jpf.symbc.numeric package.

Day 43 - Thursday July 25th
Today was more looking at using expressions as properties. The class listed in yesterday's entry is interesting, but unfortunately, the code itself (as well as jpf-symbc, where it comes from), doesn't compile. Instead of debugging someone else's code (again), I copied the relevant code, repaired those files (much quicker than getting the whole project working, I imagine), and I'm going to implement on top of these--which are already well coded. I managed to get the code recognizing the expression, which is step one. Next, I need to augment the code so that it breaks transitions when the value changes.

Day 44 - Friday July 26th
Today I was working towards more than just parsing of the new property syntax. In particular, in order to use the expressions I need to have a working system to access them and check their values during transitions, to determine if it needs to break into a new state or not. There was a fair bit of work to implementing this, and although I'm not done, I think I'm close. All the appropriate classes seem to have all the necessary information, I just haven't been able to access it all in the right way from what I can tell. But I have some ideas and I think this should be relatively easy--I'm expecting to spend no more than half a day on it on Monday.

Monday, July 22, 2013

State Reduction / Day 40

Day 40 - Friday July 19th
Today most of the work was again centered around the idea of reducing the number of states that JPF creates. There was a simple fix: I was not checking the relevance of the store instruction in the right spot. The idea is to break transitions only if the store instruction is storing into a watched variable (since now that we have a list, and won't print the other variables anyways, it makes no sense to break on all store instructions), but I was breaking all instructions, then checking to see if I should record the data--this was backwards. This put the state count at 15. I think I'm going to leave this issue alone for a bit (or ask around as to possible causes), because after looking at the code for 2 days I still don't have any other ideas, and it's pretty close to optimal. I can revisit this after a break, or if I get some new insights.

Thursday, July 18, 2013

Misc. Fixes / Days 37 - 39

Day 37  - Tuesday July 16th
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.

Monday, July 15, 2013

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.

Sunday, July 14, 2013

Inferring State (Part X) / Day 35

Day 35 - Saturday July 13th
Despite the successes described in the last post, I had omitted some other small flaws. Particularly, if a single instruction changes the state of the system, and we're only looking at that instruction, then at most we've noted one variable has changed and we're in a new state. But if that is all you look at, then when you get into this state and start recording variable values, you find only the one that has changed. So you're (probably) missing a lot of information. This can be resolved by identifying the prior state, and importing or inheriting all the other variables with their unchanged values (if they were changed, you would have observed a new store instruction). That's what I implemented today.

Still, not everything is perfect: if a variable goes out of scope from one state to the next, the code will currently import that variable and its last value anyways. Further, the method for tracking the store instructions does not seem to support even primitive typed arrays.

Inferring State (Parts VIII & IX) / Days 33 & 34

Day 33 - Thursday July 11
Today was spent implementing the ideas of the last post: the idea that within a certain state, a choice generator may be invoked several times, and that this results in transitions from a state to itself. This was not entirely correct, from the looks of it: the transitions can go back to a similar state, but the choice generator won't make a new choice for that particular choice call--it will execute the program in this state until a new choice is necessary (which may be the same choice). For example, consider the following code:

if(makeChoice()){
   variable = 1;
} else {
   variable = 2;
}

In this case, if the choice returns true so that variable is set to 1, then that might cause JPF to create a new state, where variable takes on a value of one (and of course, the search object determines when a new state is created or when one is re-used). If the choice returns false, then the variable is set to 2, but in this example, this would likely not create a new state--JPF (or, rather, the search object) will reuse the state that it was in before reaching the branching code.

So basically, looking at probabilities does not define the abstractions over the state variables (there are none) or the set of possible values, but it does provide the probabilities for these transitions, so it's still useful to get this information from the Probabilistic search object.

Day 34 - Friday July 12
Despite the ideas changing a bit in the last few days rather quickly, I always kept in mind that the end goal was to make sure that in a given JPF state, we also have the explicit state of the variables, as well as the transitions between states, and the probabilities that each transition was taken. The transitions were easy; the states a bit harder. The transitions, as alluded to in the last couple of posts can be exactly determined by the Probabilistic Search object and the listener's we're already using. The states were harder: defining what they were was hard: there's no way in JPF (at least not one that I know of) to ask it what the value of a variable in the SUT is in a given state (that would be a great extension!). So instead you need to track them by observing the instructions that JPF executes, looking out for the store instructions that modify a variable's value, and record those. And you need to make sure you're aware of when the state changes, and what it changes to. A small hiccup comes when it's realized that although instructions are executed in a transition, a transition doesn't know what state it's leading to until it completes and the search object tells the VM. So you need to store the result of the execution outside of the transition or the VM and then clean it up by putting those results in whatever state you now know you're in. I'm a bit concerned this will lead to greater memory bottlenecks, but for now it works.

The upside of monitoring instructions like this is that every explicit state of the SUT can be monitored: anytime a variable changes, we're aware. So that means when a state changes it's values, we can choose to either keep this information as a set, for example in state X, we know variable a = {1, 0} for exactly one of these values, or we can generate new (non-JPF-SystemState) "sub-states" that make it explicit: in state X, variable a = 1, but in state X.1, variable a = 0. The "set" method was in use early in the week but I wasn't satisfied, so now jpf-prism works with the latter system. The benefits of this is now that I track that a transition from a state to itself changes a variable in that state (and how it changes), but also if a transition into or out of state X is from anywhere in X, or in exactly X.Y (some substate). So now I exactly know the execution trace of the SUT. The disadvantage is that I'm storing much more information: in addition to tracking what state preceded another, I also now store a new substate for every value a variable can take. This will undoubtedly increase memory overhead.

Thursday, July 11, 2013

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.

Tuesday, July 9, 2013

Inferring State (Part V) / Day 30

Today was a productive day: some important lessons were learned. First, return values from methods that are not also stored in a variable are not considered by the JPF VM to be a StoreInstruction. This means that I was looking for variables to take the values that methods, like roll(), would return. I couldn't find them, and then I realized this was the case. I modified the BiasedDie example to assign the return value to a variable first, in order to check it better—but this may not be the case in arbitrary code. I’m mentioning it here (as well as making it an issue) so that I look into it later. Second, and much more concerning, I discovered that variables can take on different values in the same JPF state! So I was initially looking for a specific value for each variable in each state, but that’s not the case. This is a bit disconcerting, as it means I’m not doing enough to determine the “state”. I need to do more than look for specific values: I need to look into how JPF characterizes or abstracts a state, and find a way to transfer that to PRISM. That seems much harder, and I left it to tomorrow. Today, code-wise, I did get VarRecorder to work, and now I have a small hash table of states, variables, and their possible values. With this, and a bit of work, I could probably transfer this information to PRISM. I’m concerned that the hash table will not scale well, but I want to get past this problem, so for now I’m going to run with this and find some time to do scalability testing. I figure that if it doesn't scale well, I’ll see if I can pass state information into PRISM directly and on-the-fly, so that scaling is only limited by PRISM’s capabilities: one that I wouldn't be able to overcome anyways.


Unfortunately, as I’m writing this, Toronto has suffered severe storms bad enough to cause some minor street-level  flood downtown (not near me), but worse, to knock out power in many areas: myself included. I'm posting this a day late now from a coffee shop: the next post might also be similarly delayed.

Monday, July 8, 2013

Inferring State (Part IV) / Days 28 & Day 29

Day 28 - Saturday July 6
Today I was working on inferring state again. I was a bit surprised to find that in the JPF listeners directory, there are two, VarTracker and VarRecorder that appear to do much of what I was trying to do before (certainly these do what the goal of the code for Day 26 would be re-purposed for in the future), and they do so much better than I could probably do it. I'm rather quite happy that I found them: they don't solve the entire problem, but I think they're a good start. Of course, they don't work with our test examples yet: debugging & configuring them is the goal here. But I'm hopeful, and I think as long as they do work, I'm going to use them to track state in an internal state and worry about scalability later--I think any method would require something like this anyways, and we can possibly prune what we store later in order to handle larger programs.

Day 29 - Sunday July 7
Today was more debugging/configuring with the two listeners described above. Not a whole lot of luck: VarTracker was easy to change, but it doesn't actually report on the variable values: it only deals with when (with respect to what state) a variable is changed. VarRecorder on the other hand, will say explicitly what the value is, so this is the one I want to get working, but no luck yet.

Friday, July 5, 2013

Inferring State (Part III) / Day 27

Today, instead of toying around with methods to see what information I could extract from the JPF VM, I decided to take another route: to modify the ChoiceGenerator object, so that we could possibly use older methods (tracking all variables) in a smarter manner. In particular, I modified the ProbabilisticChoiceGenerator so that we can find out the last choice it made. Using this, we can query all variable information like listed two days ago (method #2), but we only need to do this once, and then we can just track changes based on the choices made. I'm under the impression that this is quicker than the alternative, at the very least, we can use both and we can track the choices for other purposes, if we need them. Of course, it's still not optimal: if the choice generated leads to other variables changing (as it almost certainly would), then we're still going to need to look for these variables changing after the choice generator returns. But maybe we can calculate dependent variables by pre-processing the code. Again, not optimal, but perhaps more clever. I'll look into it more tomorrow.

Thursday, July 4, 2013

Inferring State (Part II) / Day 26

Today I was continuing in the spirit of finding out what state corresponds to which label that jpf-probabilistic returns. The first thing I noted while looking through code was a method getStateDescription() for ThreadInfo objects, and while I didn't get my hopes up, I tried it didn't work: it returns the state of the thread. Really, no surprise there--but I thought I'd mention it in case anyone was to point it out. Simply too good to be true. Instead I was looking at the VMListener interface in JPF. It seems to implement several methods that can be used to track what goes on during verification (expanding on the ideas of the last post). I fear it might be too detailed: many methods involve threads, which probably isn't terribly important for determining what state the system is in. I wrote up a quick  implementation of the interface, but I'm not sure it'll be useful on it's own--it's got a lot of information, but I'm still not sure what I'm looking for until I settle on a method for determining state. That being said, it'll be useful in future code I'm sure. I'll be exploring more ideas tomorrow.

In addition to the above, I set up bug-tracking (and/or issue tracking) that uses FogBugz. I realize BitBucket had it's own issue tracker, but I wanted something that I could save tasks by directly using Eclipse plug-ins, and Mylyn supports FogBugz. I'm not entirely sold on it yet: I want the issues to be public ideally,  as this is an open-source project, and FogBugz doesn't seem to allow me to do this (though it's possible that anyone with a FogBugz account might be able to see them, but still, hiding them behind a log-in is not something I really like the idea of). I may switch to Bugzilla if I find out it can do that (and I find/set up a host). The bigger issues I'll also list on the BitBucket issues page.

And in case you didn't see it yesterday (I forgot to mention it in the blog), I've updated the Wiki on the jpf-prism page. It's not much, but it has the installation instructions now, and a few other obvious links. It's nice to have a place to put text that might be useful beyond the lifetime of this blog.

Inferring State / Day 25

Today's goal was to determine what state is referenced by each integer label returned by jpf-probabilistic. To this end, there were a few methods that could possibly do this. First, and easiest, but probably also least useful, was to augment the listener to look for specific variables within the code. However, there are drawbacks: 1) it appears you can only target variables at the class level (that is, variables defined in a smaller scope, say within a Java method, cannot be targeted through this method); I could be wrong, but the FieldSpec documentation in JPF didn't seem to support more than this, and 2) you need to know the variables beforehand so that you can manually enter them into the .jpf file you are verifying (this could be mitigated by writing a tool to look at the code and add all of these to the .jpf file, but it seems like this much work is not ideal before verifying arbitrary code). Second, and perhaps even easier, is to have JPF report on all variables as they are updated, and keep an internal representation of their values. This could get complicated (especially for large programs), and it has the added downside of also reporting system variables that are called, so this is not optimal. Some combination of the two might be best, or the second method with some filtering. I think for this to work (easily), we may need to pre-process the code that we want to verify and pass that to the listener so that it limits its work, or find some way to target only some classes/methods/variables--I feel like this might very well be possible, but I need to look into it more. I'm going to look into more methods tomorrow as well.

Wednesday, July 3, 2013

Model Properties / Day 24

Today I was working with checking model properties on JPF-generated Markov chains in PRISM, and trying to infer state from a given example model. The first task was relatively easy: it looks like just an appropriate set-up of the property, and the appropriate method call. The result is a bit messy: I'm toying around so I didn't make JPF publish it appropriately, so the console output is a bit out-of-order. I'll fix that tomorrow. And I plan to revisit properties: they seem easy enough but I want to run more of them to make sure things work properly and to ensure I'm setting them up correctly. Additionally, since the actual state of a model will likely be of interest, I spent a fair bit of time thinking of how to infer the state of a model (jpf-probabilistic currently only returns states with an integer label so far (and I'm not sure if the integer has any significance). I think the JPF vm can be very helpful here, but I haven't been successful here yet (and I'm not sure what degree of state inference will be considered successful--being aware of all variable values? That's the first thing that comes to mind for me). Tomorrow I'm going to talk more about this. And I also set up a blog post on how to install and run my code.

Tuesday, July 2, 2013

Installing jpf-prism

In case you were interested in running jpf-prism while it is under development, this blog post will tell you how to do that.

What you'll need: Eclipse (possibly with Mercurial and SVN), jpf-core, jpf-nhandler, jpf-probabilistic, PRISM (built from source), and of course jpf-prism.

First, if you need to install JPF, download and build jpf-core, which is available here via Mercurial:  http://babelfish.arc.nasa.gov/hg/jpf/jpf-core. If it asks for a version, take the "default" version (not v6), as the system is being developed for v7 which is default as of June 22nd (see here). Build the project, and then install the JPF Eclipse plugin and set up your site.properties file.

Second, download and build jpf-nhandler from the following Mercurial repository: https://bitbucket.org/nastaran/jpf-nhandler . Make sure that you modify your site.properties file to include it as described on the BitBucket page.

Third, download and build jpf-probabilistic from the following Mercurial repository: https://bitbucket.org/discoveri/jpf-probabilistic . Again, make sure that you modify your site.properties file to include it as described on the BitBucket page. (Note: since the interesting classes we're using in jpf-prism have been copied into jpf-prism, this might not actually be necessary, but I'm including it to be safe.)

Next, download the source for PRISM, build it (for the C/C++ parts), and set it up for Eclipse as described here (you can also get it from SVN). Then make a new a project in Eclipse and import the prism directory (as described in the last link) and build it again (for the Java files). Then add a variable, say prism-jpf, to your site.properties file pointing to the classes folder of the build, for example: prism-jpf = ${user.home}/GSoC2013 Workspace/prism-jpf/prism/classes/

Lastly, download and build jpf-prism, which is available  from the following Mercurial repository: https://bitbucket.org/jpfprism/jpf-prism . Add jpf-prism to the site.properties file, for example: jpf-prism = ${user.home}/GSoC2013 Workspace/jpf-prism (or wherever your jpf-prism project is located) and adding ${jpf-prism} to the extensions variable.

Now you should be ready to go! To test the installation, try using JPF to verify the BiasedDieTest.java by creating BiasedDieTest.jpf and putting the following in:
@using = jpf-nhandler
target=probabilistic.BiasedDieTest
classpath=${jpf-probabilistic}/build/jpf-probabilistic-examples.jar
native_classpath= ${prism-jpf}
listener=prism.listener.MarkovExporter

Then run JPF on the .jpf file. And that's it. If there are any concerns or comments, please feel free to contact me.

Communicating with PRISM / Days 21-23

Day 21 - Wednesday June 26
Today I did complete the goal I set on the last blog post: getting JPF-v7 and jpf-probabilistic to work well together. It (sadly) still took the whole day. After doing everything "by-the-book" several times, looking through compiler and debugging logs, and even resorting to putting a bunch of println calls in everywhere to debug, I was still getting really odd errors. At first they were compiler and JDK-based, but in the end resulted in run-time errors (JPF having Null pointer exceptions at start-up!). I don't know what plagued the latter few: I could never resolve that build. However, I decided to try a fresh install of Eclipse and JPF, and after installing all the appropriate plug-ins and extensions, I rebuilt all the code and it worked. I think this is a terrible fix, but it's one that works: I'm happy. I'm disappointed that I didn't try this earlier (would have saved two days) and that I didn't find the root-cause of the issue, but honestly, that was taking too long so I'm glad something worked. I also don't want to rely on this in the future, so I hope whatever caused it before doesn't re-appear.

Day 22 - Thursday June 27 & Friday June 28
I'm splitting this day in two because I was fairly distracted both days by external events, and I don't think either was really worth more than a half-day's work. That being said, I've cleared my next weekend to make up the time; I don't want to get into the habit of not putting in the time this project needs. However, I did do some work as I mentioned: the next task after repairing the code was to get a Markov chain passed into PRISM so that PRISM can check the model. Although I had played around with interfacing with PRISM, the first real task is never as smooth as when you're just having fun. So this took some time, but the end result was a success: PRISM takes in a Markov chain from the JPF listener, creates a class with it, and then prints the text representation of it. However, due to my distraction I forgot all I read before, and did this poorly: I created another running Java program, connected to it through ports, and ran the PRISM code there (because I forgot all about class-paths from my earlier reading in my distraction). It worked (as the native Java libraries didn't seem to have compilation issues like using external programs), but I wasn't proud. Read on to see that I fixed that!

Day 23 - Monday July 1
Today was also not as focused on the project because it was a national holiday here (Canada Day), and while I didn't really go out, I was often called away by family or friends for short periods of time, so this is part of the reason why I want to work both days next weekend (and given the time lost to getting v7 to work, I may very well work the weekend after that too!).  That being said, I did spend time coding: I was working towards removing the sloppy connection between JPF and PRISM: I didn't want to use ports and so I remembered that you can just modify what JPF considers as part of the native classes to load: I spent all day undoing the old code and making the much, much simpler connector: only a listener (and whatever classes I've used from jpf-probabilistic). I also spent some time cleaning up the code, and the day ended when I pushed a new update--which is a habit I want to make daily (and these posts, since I have been slacking on writing them on same-day).

For an example, jpf-probabilistic generates the following Markov chain of a Biased Die:
0 ------> 1
1 -0.30-> 2
2 -0.30-> 3
3 -0.30-> 2
3 -0.70-> 4 *
2 -0.70-> 5
5 -0.30-> 4 *
5 -0.70-> 4 *
1 -0.70-> 6
6 -0.30-> 7
7 -0.30-> 4*
7 -0.70-> 4*
6 -0.70-> 8
8 -0.30-> 4*
8 -0.70-> 6
which I then use to create a basic model in PRISM, and I call toString() on, and that gives me:
trans: [ 0: {}, 1: {2=0.3, 6=0.7}, 2: {3=0.3, 5=0.7}, 3: {2=0.3, 4=0.7}, 4: {}, 5: {4=1.0}, 6: {7=0.3, 8=0.7}, 7: {4=1.0}, 8: {4=0.3, 6=0.7}, 9: {}, 10: {}, 11: {}, 12: {}, 13: {}, 14: {}, 15: {} ]
It's not much--but it shows that PRISM and JPF are connected--which was the goal here. Up next will be some more interesting things.