PAT: Process Analysis Toolkit

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

30, Apr, 2009: PAT 2.4.0 is released!

What’s new in PAT 2.4.0

In this release, PAT has gone through a complete system re-design such that classes for Label Transition System, all model checking algorithms, common utility functions and simulator are centralized in PAT Common project, which can be shared by all modules. This design allows new modules to be created easily by simply creating parser, module specific language construct classes and model checking user interface.
Other updates include language enrichment, new GUI functions, new examples and bug fixing. The details are explained as follows.

Language Enrichment of CSP module
1 Quick array initialization: To ease the modeling, PAT supports fast array initialization using following syntax.

#define N 2;
var array = [1(2), 3..6, 7(N*2), 12..10];
the above is same as the following
var array = [1, 1, 3, 4, 5, 6, 7, 7, 7, 7, 12, 11, 10];

In the above syntax, 1(2) and 7(N*2) allow user to quickly create an array with same initial values. 3..6 and 12..10 allow user to write quick increasing and decreasing loop to initialize the array.

2 Process Counter Variable is Supported
User can define a special variable for a process to keep track of the number of the process in the system. This variable is very helpful when modeling of system with infinite number of identical processes so that we can use and check the number of identical processes. One example is following.

#define noOfReading #Reading();
var writing = false;

Writer() = [noOfReading == 0 && !writing]startwrite{writing = true;} -> stopwrite{writing = false;} -> Writer();
Reader() = [!writing]startread -> Reading();
Reading() = stopread -> Reader();

ReadersWriters() = |||{..} @ (Reader() ||| Writer());

3 PAT added the support for two assignment syntax sugars ++, . x++ is same as x=x+1. y is same as y = y-1. y=x++ is same as x = x +1; y = x;. There are no shorthands for other shorthands, such as ++b , b , b *= 2 , b += a , etc. Where needed, their effect can be reproduced by using the non-shortened equivalents, The following example shows the usage of ++ and , where the final values of x and y are both 3.

var x = 2; var y;
P() = add{x ++;} -> minus{x ;} -> event{y=x++;} -> Skip;

4 Event local variables are supported. The scope of the local variable is only inside the sequential program and starts from the place of declaration.

var array = [0,2,4,7,1,3];
var max = -1;

P() = findmax{
var index = 0;
while (index < 6) {
if (max < array[index]) {
max = array[index];
index = index+1;
} -> P();

Language Enrichment of Wes Service module
1 We implemented all the language features of CSP module to WS module: local variable, multi-dimensional array, array initialization and so on.
2 Channel communication allow multiple data to be passed
3 Synchronous Channel communication is supported.

User Interface
1 Bugs for text drag and drop are fixed
2 Tab navigation functions are supported: Go to Previous Tab (Ctrl+Shift+Tab), Go to Next Tab (Ctrl+Tab)
3 Drag and Drop an external model into PAT to open it quickly.
4 Simulator is shared by all modules

User manual is updated to latest implementation
1 FAQ section is added in the manual. We will add more questions asked by the users.