PAT: Process Analysis Toolkit

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

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;
else
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.