PAT: Process Analysis Toolkit

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

4, Feb, 2012: PAT 3.4.2 is released!

1 Code generation is improved and supports of more syntax for CSP module (still beta version, based on QP platform)
2 BDD support for CSP module is improved. BDD doesn’t support encoding interrupt as an LTS but can encode it with compositional function.
3 Most BEEM database examples are added (work in progress)
4 RTS module bugs are fixed.
5 Monotonic engine for reachability with max or min value is added back
“Search Engine: Shortest Witness Trace using Breadth First Search with Monotonically With Value”
6 Reward calculation is supported in PRTS, and parser are improved in PRTS.
7 Indexed events are supported in all modules.
8 Macro definitions usage is improved for all modules.

Macro can take in parameters as defined below. When calling the macro, the keyword call is used. The macro expression can be any possible expression in PAT (if, local variable declarition, while, assignment).

#define multi(i,j) i*j;
System = if (call(multi, 3,4) >12 ) { a -> Skip } else { b -> Skip };

Note that following usage of macro definitions are also allowed in PAT, which means that macro definitions can be a fragment of code to be used in the model.

var x = 0;
var y = 0;
var z = 0;
#define reset1 {x = 0; y = 0};
#define reset(i) {x = i; y = i};
P = e1{z = 0; reset1} -> Skip;
Q = e2{z = 2; call(reset, 1)} -> Skip;

9 Atomic process semantics is updated
Since PAT 3.4.2, the semantics of atomic process changes a little bit. In the example below, before PAT 3.4.2, event a and d are enabled at the same time when process Sys starts. In PAT 3.4.2, only d is enabled because enabled atomic process has higher priority than enabled events. We did this change is to make the semantics for atomic process in real-time modules in PAT easy to express.

P = a -> atomic { b -> c -> Skip};
Q = atomic { d -> e -> f -> Skip};
Sys = P ||| Q

With this new syntax, parallel events can have priorities like a and d above.

In RTS module, atomic process can contain timing constructs now. Consider the following:
P = atomic{Wait[5]; a -> Skip} ||| Q;
Q = b -> Q;

The tau (time tick) transition geneated by by Wait[5] will have higher priority than b and the tau, and event a will be bundled together.