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