Tuesday, June 25, 2013

Markov Chains and Dealing with Updates/ Days 17-20

Day 17 - Thursday June 20
Today was going to I spend time looking into different methods for random choice generation, as I mentioned in the last post. But after some quick searching (and not wanting to spend too much time on this task), I decided to give up--I could find nothing that looked like it was worth implementing and not spending a whole bunch of time on, I looked for examples of other Markov chain problems that I could test my understanding of modelling probabilistic programs on. The web was unsurprisingly full of these, and I picked the first one I could find, state charts (not really creative, but not explicitly provided in the code I'm playing around with). I modeled a few and checked the resulting chain against the expected results, and everything went as planned.

Day 18 - Friday June 21
Deciding to take a small break from coding probabilistic models on the JPF side, I decided to see what could be done the PRISM side. I didn't do any coding, but I spent time looking at the 6 tutorials here. They were interesting, but I'll be much more interested to run those examples programmatically through JPF first.

Day 19 - Monday June 24
Today was not fun! I updated the jpf-core project I've been using to v7 and was excited to make any corrections that I needed to do for my example code to continue to function. So I went to test various applications, and while basic listeners worked, jpf-probabilistic did not! Instead of providing the proper Markov chains for the example programs, it printed single line chain  ("0 ------> 1"), which is about 15 lines too short. After a day of attempted repairs, I was unable to solve the problem.

Day 20 - Tuesday June 25
Today I had a Skype meeting with one of my supervisors, and spent more time trying to repair the jpf-probabilistic code to work with v7. I still wasn't successful, but I think I'm getting close, and now the code is annotated so I can see everything, so I'm going to risk spending one more day on it tomorrow (I still think this would be quicker than coding the necessary classes again from scratch, even if they are only temporary). After that, the immediate next steps are to get Markov chains from jpf-probabilistic working again so that I can just pass them into PRISM as a sanity check to make sure that I am in fact linking the model checkers properly. After that, we'll start to stray a fair bit from jpf-probabilistic and start coding up some new ideas--I'm looking forward to that.

Thursday, June 20, 2013

Probabilistic Test Listener / Days 15 & 16

Day 15 -- Tuesday Jun 18
JPF Probabilistic coding. Today was spent with the goal of doing more than just reading and compiling the jpf-probabilistic code that was found online. One of my mentors suggested working on getting the jpf-prism listener to process the test cases (there are three) that jpf-probabilistic included. Of course, getting the listener to work on the code that is supplied in the tutorial, and getting it to work on different code (without directly copying the jpf-probabilistic code) is not the most challenging thing I'll have to do, but it wasn't trivial. Perhaps a better phrasing would be to say that it is exercising all that reading and experimenting I did in the weeks prior to this one. Overriding listener code for the sake see what happens is easy and fun, picking the right ones for the job is the interesting part, and this is the first time that this has been necessary. I got it to replicate a fair bit of the same behavior, but not entirely without cheating (I had to use some of the classes in jpf-probabilistic). Tomorrow I'm going to see if I can lessen this dependence, though I realize that may not be strictly necessary.

Day 16 - Wednesday June 19
Coding continues. I think I realized that somethings are probably going to be very likely okay to borrow from jpf-probabilistic, like the "Choice" class that probabilistic programs will have to use to indicate some sort of randomized choice that our listener will have to look for. And it may very well need to changed, replaced, or supplemented for our needs, but for now I think it's okay if I use this class explicitly. Of course, once this was realized, somethings were sped up to the point where it looks like my listener does process probabilistic programs similar to jpf-probabilistic; that is, it identifies and uses the choice methods in a similar manner and it can also print the Markov chains--but in this sense it is very similar to the existing code, so while it was worth re-coding for my sake, its not technically impressive. What I'm more interested to do tomorrow is to see if I can find other examples on the internet to test this implementation against the existing code (it should do well, it does look very similar) but then also to see if I can get good results by writing different "Choice" (or other dependent) classes. For example, jpf-probabilistic also has a "UniformChoice" class, but maybe I can encode different distributions for probabilities against well-documented (but still relatively quick) examples to make sure I'm really writing good code.
I'll polish the code a bit and then commit them to the repositories after this blog post as well; I'm not yet tired and I want to play around a bit more, then submit once for the last two days. I only say this because it's the last time I'll mention committing code; after tonight I'll do this at least daily, if not hourly or more frequently--like this code (which I'm still only considering experimental) was important. Even if it is only experimental code, I might as well commit in case some of it is useful later.

Tuesday, June 18, 2013

Catch-up Blog / Days 8 - 14

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.

Thursday, June 6, 2013

Reading / Day 7

Today, I spent a large amount of time re-reading "A Game-based Abstraction-Refinement Framework for Markov Decision Processes" which is a fairly lengthy paper that can be found here.

Tuesday, June 4, 2013

Populating Repositories / Day 6

Today, I actually put code into the Bitbucket repositories (after waking up to note that in the end, Cygwin downloaded 22GB of data). There are two important repositories: the first, JPF-PRISM, is the code for the primarily JPF-based code, like listeners and other custom code. The second, PRISM-JPF, is a branch of the PRISM code trunk, which can be modified in the event we need it to. I don't expect the second repository to have code that isn't directly embedded into PRISM. I also re-read Abstraction Refinement for Probabilistic Software (available here).

Days 4 & 5

Friday, I didn't post much as I didn't accomplish a whole lot: I was running errands and so had some, limited time to do things. I did spend some time looking at (and writing) code, in particular seeing what the different methods new listeners could override to see what types of behavior my listeners might implement. It was fun, but I forgot to blog (and that's bad...but I'll always include missed days in the next post).

Today, I was going to actually populate the repository I set up last week, but I decided I might also want to develop on Windows (in addition to Ubuntu), and thought I would set up the required tools first. What a poor idea: Cygwin has literally been downloading and installing for hours. I think this is why I put it off when I first got this laptop a year ago. I should probably have requested fewer packages, but I never know what I strictly speaking need, so I end up getting way too many. Oh well. Tomorrow, code will be uploaded.