Animator for counterexamples generated from deadlock tests. This tests are made by FDR, the CSP refinement checker. This application is part of the scientific initiation research Integrating CSP with Programming Languages. We can check the final report here.
Clone the repository and run the application with a IDE with Java support (Eclipse or IntelliJ recommended).
Have Java installed on the machine and use an IDE.
Visualization of a deadlock generated by the animator (on the right), based on the definition of a process A that leads to a terminal failure state (on the left):
As process B indicates leading to a successful terminal state (left side), the visualization of deadlock and failure cases is undefined by the animator (right side):
Even with the definition of process C presenting deterministic choice (left side), the visualization of failure cases is presented by the animator (right side):
Make a pull request and make clear what changes have been made and which bugs persist. Do not introduce bugs, be proactive!
- MIT License - Ver detalhes