I was without stable internet access for the last week, so I was unable to update this blog regularly. However, I did not stop learning about JPF and PRISM, and the blog should be updated accordingly. This week, with internet access restored (and not expected to go missing again), back to daily updates! I was also very fortunate to have downloaded the JPF website pages before this happened (though I'll admit I thought this would be in case I found myself on the TTC or a plane a needing a quick reference without internet connectivity, not for such a long offline period).
Day 8 - Friday June 7
Continuing with the theme of reading for the week, I spent the day reading PRISM papers. I had previously read two noted papers in my proposal, but I figured more reading on the PRISM model checker wouldn't hurt, and most of the other papers are also interesting but also shorter. Further, "Pareto Curves for Probabilistic Model Checking" was actually in the proposal description so I thought that was definitely necessary to re-read. But I also read "Model Repair for Markov Decision Processes" and "Incremental Quantitative Verification for Markov Decision Processes". For the latter two, I'll probably have to re-read them again, though now I can probably read them during the weekend or periods of down-time; I don't want to commit any more full days to reading unless I absolutely have to. (All of the papers can be found from here.)
Day 9 - Monday June 10
I looked largely into JPF-Probabilistic. This was one of those background topics that was supplied by my mentor during the application process. This was a bit of a challenge: the code didn't initially compile, so there were some fixes necessary. Luckily these were overcome with a bit of time debugging and renaming of several import statements. The only part that I would still like to consider is the reference provided by the link, but I can't find a digital copy. When I have a desk at the University of Toronto again next week, I'll head over to see if my library card still works and if they have the reference.
Day 10 - Tuesday June 11
JPF Tests! I took a look at the JPF developers guide to see what else there might be to learn. I saw JPF-Tests and was immediately interested--after all, my proposal did list tests. Beyond that, I want to actually engineer something properly given that code is the primary artifact of the GSoC program and I would like to think that eventually the code might actually be used in academia or elsewhere--and in those cases I want to make sure I'll have done everything I can to make sure I can stand behind it. The tutorial for tests was easily followed and I created some quick tests.
Day 11 - Wednesday June 12
Today I looked towards more of the downloaded JPF website and looked towards logging and reporting. These are more things that I was going to put off until I actually had to write them, as they didn't look complicated, but it was worth looking at now; might help some debugging as well. I also looked at the coding conventions, but they were almost trivial, and not something I spent a lot of time on.
Day 12 - Thursday June 13
Following the same pattern, today was devoted largely to to the thorough understanding of JPF ChoiceGenerators. This would have been helpful when reading the JPF-probabilistic code, as that certainly has some code that inherits generators; of course on the other hand, relating that information to another example was helpful. The next page was On-The-Fly Partial Order Reduction so I naturally kept reading. This topic was a bit more involved: it didn't have a coding example; in the end, I'm not sure I got thorough understanding of it in all aspects: for examples, listeners can modify the scheduling described, and I think I can do that, but I've never modified the scheduler using Attributor elements. I've made a note to come back to that when I have more time.
Day 13 - Friday June 14
The last day in the week was dedicated to learning about the other extension points for JPF, namely native peers and bytecode factories. They both seem like they could be used in this solution, but it also looks like they are are more low-level or allow for finer control over the Java classes considered. (Or at the very least they seem more complicated). For example, bytecode factories are used to change execution semantics, and this seems useful: one example suggests changing them so that information is collected and passed to an external SAT solver to trim generated choices. I thought maybe something will eventually need to be passed to PRISM this way; maybe not. I think that will depend on the actual implementation but I'm happy I read what I did in these areas, so that I can keep them in mind during the next phases of the project.
Day 14 - Monday June 17
Today was technically the first official start of the coding phase! The first month is to successfully identify requirements for the connector and the extension points. From a very high level, the latter looks straightforward: JPF listeners, with minimal changes to the PRISM code-base. The requirements are also understood at a very high level, but I would like to enumerate them at a much lower-level. I was hoping to do this today, but I got an e-mail last week to look into jpf-v7, a newer version of JPF that I was going to port to after coding was performed. So I was looking into the changes for the code and ideas that were in the v7 code as found here. I looked over the code of the basic listener I had created and I don't think much will have to be changed.
No comments:
Post a Comment