PAT: Process Analysis Toolkit

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

Monthly archives for March, 2010

18, March, 2010: PAT 2.9.1 is released!

What’s new in PAT 2.9.1

In this minor release, we introduced two new assertion: nonterminating and deterministic. Also a lot of bugs in CPS, RTS and PCSP modules are fixed. The most significant change is the Graph difference comparison function of any two simulation graph, which is a joined work with Dr Xing ZhenChang.


Given P() as a process, the following assertion asks whether P() is deterministic or not.

#assert P() deterministic;

Where both assert and deterministic are reserved keywords. Given a process, if it is deterministic, then for any state, there is no two out-going transitions leading to different states but with same events. E.g, the following process is not deterministic.

P = a -> Stop [] a -> Skip;


Given P() as a process, the following assertion asks whether P() is nonterminating or not.

#assert P() nonterminating;

Where both assert and nonterminating are reserved keywords. PAT’s model checker performs Depth-First-Search or Breath-First-Search algorithm to repeatedly explore unvisited states until a terminating state (i.e., a state with no further move, including successfully terminated state) is found or all states have been visited. The following process is deadlockfree, but not nonterminating.

P = a -> Skip;

Graph Difference Comparison
To compare the diffference between any two simulation graph can give user the feedback for the difference of the specifications.

In this version, we have implemented the first version of graph comparison of any two opened simulators. After the comparison, the differernce are highlighted in different colors.

16, March, 2010: Appreciation for PAT Japanese User Group

We would like to thank PAT Japanese User Group for supporting the PAT development (by providing Japanese translation and valuable feedback), promoting PAT tool and hosting us in Japan. We have special thank to Kenji Taguchi, Hiroshi Fujimoto, Masaru Nagaku, Toshiyuki Fujikura. We wish to extend the collaboration and achieve more fruitful results.