PAT: Process Analysis Toolkit

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

25, Nov, 2008: PAT 1.3.0 is released!

In the early version, due to the difficulty of calculating alphabet of the process for parallel composition, PAT does not allow global variables in events or process invocations. But there are a lot of models needs this features.

In this release, we added the support of use of global variables in event and process invocation if there is no parallel composition involving. Runtime exceptions will be thrown if there is a difficult to calculate the alphabet due to usage of global varaibles.

We also add a single lift system example. Some examples are simplied after the new language feature.

Bugs fixing in simulator.

Optimizations are implemented as well for numerous places.