PAT: Process Analysis Toolkit

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

Monthly archives for August, 2008

Accept C# code as customized functions

To make the evaluation more efficient, we allow any math functions to be declared as static methods, which can be used directly in the model.
The static varaibles are be used as well.

To edit the math library code, click “Tools” -> “Math Library”.

for example, if you declare the following static methods in math library code.

public static int max(int a, int b)
if(a > b)
return a;
return b;

In your model, you can use max as a function like following:

a = 0;
b = 15;
P() = event{a = call(max, 10, b);} -> Skip;

Also the full set C# math library can be used directly in the model:
Method Returns
Abs Returns the absolute value of a number.
Ceiling Returns a value that is the smallest whole number greater than or equal to a given number.
Exp Returns E raised to a given power. This is the inverse of Log.
Floor Returns a value that is the largest whole number that is less than or equal to the given number.
IEEERemainder Returns the result of a division of two specified numbers. (This division operation conforms to the remainder operation stated within Section 5.1 of ANSI/IEEE Std.

8, Aug, 2008: PAT 1.2.3 is released!

PAT 1.2.3 is released with the support of user defined math library. Also the c# math functions are supported. look Accept C# code as customized functions for details.

Performance Study of Leader Election Protocols

We conducted experiments of 5 leader election protocols for PAT version 1.2.2. The performance result can be found in here. The 5 protocols are built inside PAT examples. Regarding the Spin model, they can be downloaded here.

The experiments is conducted in a Core 2 CPU 6600 @ 2.40GHz with 2GB RAM.

6, Aug, 2008: PAT User Manual is updated

The PDF version of the PAT User Manual can be downloaded here. We are keeping on working on a better version.