Day 41 - Monday July 22nd & Tuesday July 23rd
I'm splitting this work day in two because I was fairly distracted again: on Monday I was finding an apartment (which I did!) for my upcoming move, and Tuesday was a half-day trip to the dentist. So I will have to make up a day of work.
Anyways, what I did work on was to see if I could parse more interesting state/property descriptions. The initial parser I had written was sloppy and didn't quite work as well as I had initially thought. So I spent the day re-writing this; I'm still not particularly happy with it (it's not a standard LALR parser, so it's likely slower than other existing parsers, like SableCC.), but it will do for now, and it parses based on variable/value, as opposed to state number. That is, we accept markov.properties="[](<> \"x.y.outValue:5\")"), type properties. That being said, although it parses better, I'm not yet doing anything with the property: I'm still checking nothing related to it. But the parser did need the fix, so this was the first step.
Day 42 - Wednesday July 24th
Today the day was started with a demo of the code and an outline of it to my mentors on Skype. The talk was very helpful and productive, and suggested many changes to the code and outlined a concrete direction to take for the immediate next steps of the project. There were some small changes that were easily fixed: moving some classes to the appropriate packages in the source and moving a parameter from the .jpf files to the jpf.properties file. Easily done. Only slightly harder was building the Markov Chain in PRISM on-the-fly (as opposed to when the search was finished), and that too is now implemented. This should reduce our memory footprint when checking models. The system can now also export the Markov chain in a DotFile for use with visualization with Graphviz. The most interesting ideas were the next steps: to get the the properties that we're interested in checking to be represented not as states, or particular variable values, but rather to be handled as Java expressions. Further, we could use these expressions to break transitions (or not) and use this to also trim the search space. The rest of the day was focused on introducing myself to the tools I was suggested as a starting point: the PreCondition class from the gov.nasa.jpf.symbc.numeric package.
Day 43 - Thursday July 25th
Today was more looking at using expressions as properties. The class listed in yesterday's entry is interesting, but unfortunately, the code itself (as well as jpf-symbc, where it comes from), doesn't compile. Instead of debugging someone else's code (again), I copied the relevant code, repaired those files (much quicker than getting the whole project working, I imagine), and I'm going to implement on top of these--which are already well coded. I managed to get the code recognizing the expression, which is step one. Next, I need to augment the code so that it breaks transitions when the value changes.
Day 44 - Friday July 26th
Today I was working towards more than just parsing of the new property syntax. In particular, in order to use the expressions I need to have a working system to access them and check their values during transitions, to determine if it needs to break into a new state or not. There was a fair bit of work to implementing this, and although I'm not done, I think I'm close. All the appropriate classes seem to have all the necessary information, I just haven't been able to access it all in the right way from what I can tell. But I have some ideas and I think this should be relatively easy--I'm expecting to spend no more than half a day on it on Monday.
great
ReplyDelete