They say that football is a game of inches; if so, model checking is a game of variables. The game is, essentially, how can I reduce the state of the model & shrink its representation?
Yesterday we were slightly past the edge of what can be analyzed in a reasonable amount of time using a BDD-based model checker. After looking at it a while, I came up with an optimization that removes one variable from a Simulink subsystem in a rather arcane clock mode. This one tweak made the difference; we got rid of 5 state variables and the model went through. It was, one of those rare (small) epiphanies -- a good hack.
No comments:
Post a Comment