Animation, Verification and Visualisation of Prolog Transition Systems with ProB

This paper presents existing and recently extended capabilities for animating transition systems defined by Prolog predicates in ProB, a Prolog-based model checker, animator, and constraint solver. The extensions include simulation for statistical checks, more reliable trace replay, user-input-driven transitions, and improved state visualisation. Case studies, including different Connect Four gameplay strategies, demonstrate how the features can support validation and experimentation. The authors also point to applications in ProB’s new sequent prover for Event-B proof obligations and in interactive teaching demonstrations. The abstract does not provide quantitative evaluation results or detailed implementation benchmarks.