After some efforts, we glad to release PAT 3.1.0, which can run in all platforms: Linux, Mac OS and more!
The solution is to use Mono, which is an open source, cross-platform, implementation of C# and the CLR that is binary compatible with Microsoft.NET.

Install PAT 3.x in Linux, Unix, Mac OS or more, please follow these steps:

• You should install mono tool in your system which is freely available. Please download from here according to your OS.
• Download PAT 3.x. But choose the directly executable version to some place in your computer.
• In your computer, start terminal application, using the command cd to the directory where you put “PAT 3.exe”;
• Type the command mono “PAT 3.exe” into terminal. Bingo! You will see the GUI of our PAT.

Note that running PAT in Mono, the performance can be (much) slower than runing PAT in Windows.
Here is some prelimenary experiment on the CSP linearizability Stack example, with same laptop but different OS.

stack length: 875.39s24.69sstack length: 986.42s30.74sstack length: 10111.04s39.55s

There are some known bugs when running PAT in Mono:
1) Email sending in Mac OS is not working. This is an issue of Mono library.
2) Sometimes the first line of the model (or part of the model) is invisible, and user should click there to see the text.
3) in simulation window, it works very well except the Save and Export buttons. These two buttons are invisible before you click them.

If you find bugs and issues when running PAT in Mono, please do About Us.

Other update in the version 3.1.0 including bug fixing and new examples.

Search and Post your questions in the forum: http://patroot.forummotion.com/

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.

What’s new in PAT 2.9.0

In this release, there are three new modules are released: Probability CSP Module, Orc Module and NesC module. There are a lot of changes from the user interface, language syntax and verification algorithms. So we decide to make it a beta release before it becomes stable.

Probability CSP Module
PCSP module extends CSP module with probabilistic behaviors. With the introducting of probability choice in the modeling, PCSP module supports the verification of deadlock, reachability and LTL properties with probability queries.

Orc Module
Orc module supports the modeling and verification of Orc language, developed by the UT austin university. This is a beta release. More examples and testing are needed.

NesC module
NesC module supports the modeling and verification of NesC language. This is a beta release. More syntax of NesC language will supported soon.

Language Changes
1 with clause is supported in CSP module, RTS module and PCSP module for reachability properties.
To further query about variable values, PAT allows user to find the minimum value or maximum value of some expressions in all reachable traces. The following coin changing example show how to minimize the number of coins during the reachability search.

var x = 0;
var weight = 0;
P() = if(x <= 14)
{
coin1{x = x + 1; weight =weight + 1;} -> P() [] coin2{x = x + 2; weight = weight + 1;} -> P() [] coin5{x = x + 5; weight = weight + 1;} -> P()
};
#define goal x == 14;
#assert P() reaches goal with min(weight);

2 ‘new’ keyword is supported for the user defined data structures.
Var<HashTable> x = new HashTable(100);

3 ‘byte’ ‘short’ are supported in the return type of user defined methods.
But not supported for the method parameters.

3 nested if-then-else are supported
if (cond) { P } else if (cond2) { Q }

GUI updates
The search depth option is removed from the verifier. We implement the shortest witness trace option to find the shortest counterexample or witness trace for deadlock, reachability and refinement checks. The shortest witness searching algorithms are based on Breadth First Search.

The simulator is added with the option of hiding tau events.

Performance Improvement
1 Refinement verification algorithm is updated and improved.
2 Parallel execution is simplied.

Others
1 User manual is updated to latest implementation.
2 Bug fixing in refinement checking algorithm
3 Bug fixing in LTL safety checking algorithm
4 LTL safety checking algorithms are implemented.
5 Examples are added for PCSP module and RTS module.
6 Parsers are improved for some error input.