Happy New Year! After half year’s development. PAT 3.5.0 is out.
After PAT 3.5.0, .NET framework 4.0 is required to run PAT.
There are a number of new features and bugs fixing in this version as list below.

Update of PAT 3.5.0

1 First, PAT is now running on .NET framework 4.0 in order to benefit from the newer library, particularly the parallel library in .NET 4.0.
We have done another round of code restructuring based on the new .NET framework.

2 GUI improvement
a) Simulator is supported to display all enabled events in all states or only enabled at the current active state.
b) Parsing without output parsed specification in the output window. When some model is very big, to output the string takes very long time.
This option could help to solve this problem.

3 BDD library performance improvement

4 Bug Fixing and improvement
Bug fixing for the exception due to non-boolean expression used in LTL property
Bug fixing for searching and parsing
Bug fixing for nested IndexedProcess
String Type Event in alphabet and hiding process
Comments highlighting in the assertions section of the model

New features coming up

1 Several Multi-core model checking algorithms (Nested DFS based, Tarjon SCC search based, with fairness condition) are implemented.
These algorithms will be avaiable soon.

2 Learning based composition verification algorithms library CELL. We have implemented a number of compositional verification algorithms
and learning algorithms. This library (with source code) will be released soon.

3 New modules coming: BPEL module, Timed Automata module, UML state machine module, security module. Stay tuned.