PAT: Process Analysis Toolkit

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

13, Apr, 2009: PAT 2.3.0 is released!

What’s new in PAT 2.3.0

In this release, PAT supports several new language features to increase the expressiveness. Library support is improved to make it more useful. New examples are added. The details are explained as follows.

Language Changes of CSP module
1 Array can be passed in both synchronous and asynchronous channels
2 N-dimensional array is supported by converting them into one dimensional array in the parsing.
var matrix[N][10];
matrix[1][2] = 1;
3 Compound channel data are support. since FDR and SPIN support this. We adopted FDR’s syntax
c?x.y.z or c!x.y.z
4 Array of size 0 is supported, you can use 0 size array as set of List with the help of C# library. See the library update below for more details.

User Interface
1 Bugs in model checking window are fixed.
2 Cut number display in the simulator is added if there is a one.
3 C# code library editor and compiler is improved.

C# library support
Users can create the external methods with int, bool or int array type parameters, with possible return type int, bool and int array. The number of parameters can be 0 to many now. PAT is abled to support multiple C# libraries. Currently two Libraries are implemented: Array and Set. More are coming. 🙂

6 User manual is updated, you can find info about all these update in the manual.

Newly added examples
a) Meta-Lock Example is added for the parameterized systems
b) Language feature demonstration example is added