A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker
Tam Thi Thanh Nguyen, Kazuhiro Ogata · 2017
A counterexample generated by a model checker, such as Maude LTL model checker, consists of a sequence s0;...;smof states and a loop (sm+1;...;sn)∞ of states such that sm+1is a successor state of sm and sn. A counterexample generated by the Maude LTL model checker is not necessarily the shortest one. The shorter a counterexample, the easier it is to comprehend the counter example. Therefore, we have implemented a meta-program in Maude that takes a counterexample and generates a shorter one. We had implemented a state machine graphical animation tool so that human users could recognize some patterns in animated computations. We realized the tool helps human users comprehend counterexamples. Thus, we have extended the tool such that it takes a counterexample and plays its animation. Some examples are used to demonstrate the usefulness of the meta-program and the extended state machine graphical animation tool.