PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

30, July, 2012: PAT 3.4.4 is released!

1 Bug fixing for all modules for deadlock checking and divergence checking for some special cases.
2 In simulator, a Simulate Trace button is added to allow users to write a script to perform automatic simulation. After clicking it, a textbox is shown where you can writre the event trace like phil.0.0, phil.0.1, eat.0 or a, b(5), tick. Each event is seprated by comma and b(5) means you can perform b 5 times.
3 In Editior, PAT also provides another way to open the imported library directly. You can select the imported library path and then right click the button, choose “open import/include file” function to open it. This funcation can recognize absolute path, relative path to the current model file and inside lib folder of pat installation.
4 In CSP module, C++ Code generation function is improved with hardware API support and socket channel support mapping from channels.
5 For simplicity, BDD is only supporting LTS and TA module now
6 TA module performance improvement
7 our PAT.BDD library has been publish at
8 Stop button has better responsive for LTL (with fairness) verification during the counterexample searching.