/* These methods are callbacks called by the model-checking engine
* to get and display information about the current state of the
/* These methods are callbacks called by the model-checking engine
* to get and display information about the current state of the