Joker

This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B CSP and Z. However using a LTS in a specified XML format it is possible to animate further languages. Additionally the tool provides traces visualization the choices the user did in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it as the developers do for programming languages such as Java and C++.