PAT: Process Analysis Toolkit

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

Monthly archives for April, 2009

30, Apr, 2009: http://www.patroot.com is online

We registered a new domain name for PAT: http://www.patroot.com. Later on, we will graduately move the website under this domain. Currently it will redirect to http://www.comp.nus.edu.sg/~pat/

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.

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