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.

Deterministic

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;

Nonterminating

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.