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.
No comments:
Post a Comment