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.