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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.