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