This release mainly introduce more language syntax sugers, latest Antlr Parser library, GUI improvement and bug fixing.

Language changes:
1 The indexed booleans expressions are supported in CSP Module.
The indexed expression is a syntax sugar for grouping a list of OR or AND expressions together overal a range of variables. The syntax is following:
A typical example is as follows:
var x[3];
P = if(&& i:{0..2}@(x[i] == 0)){bingo -> Skip};

2 Index events are supported in CSP Module.
The syntax sugar indexed event list can be used in the definition of alphabets. For example:
#define N 2;
P = e.0.0 -> e.0.1 -> e.0.2 -> turns -> e.1.0 -> e.1.1 -> e.1.2 -> e.2.0 -> e.2.1 -> e.2.2 -> P;
#alphabet P { x:{0..N}; y:{0..N} @ e.x.y };
The above definitions define the alphabet of process P as the set of all events except event turns appearing in its proces definition.

The syntax sugar indexed event list can be used for defining a set of events with the same prefix. For example, the definition for process dashPhil() can be rewritten as the following.
dashPhil() = Phil() { x:{1..2} @ getfork.x, y:{1..2} @ putfork.y};

3 Warning is added for non-synchronization of events and data operations.
This is a common problem raised by many users that, for the following program, can the two processes P() and Q() synchronise on the event a? If not, then how to make them synchronise on ‘a’ and preserve the execution of statement block ({x++}) in an atomic fashion?
var x=0;
P() = a{x++} -> b -> P();
Q() = a -> c -> P();
System() = P() || Q();

Answer:
No-Synchronization on Data Operations is a design decision to void data race. If two data operations can synchronize, the update of the same global variable can lead to data race. Therefore, PAT will give a warning that if there one data operation and an event with same in different processes running in parallel.

Back to the question, a intuitive solution is to put the event ‘a’ and increment statement in an atomic action as follows:
P() = atomic{a -> update{x++} -> Skip};b -> Skip;
Q() = a -> c -> Skip;
aSystem() = P() || Q();
Then x will be updated right after a is engaged, and a will be synchronised.

The other possible solution could be:
P() = a -> update{x++} -> a1 -> b -> P();
Q() = a -> a1 -> c -> P();

4 Parsers are updated to the latest version of Antlr C# library.

GUI
1 Splash screen is added
2 Multi asseertion selection in the Model Checking
3 More high-lighting in the model checking output form
4 Bug fixing in the GUI

Examples
1 More examples are added in the LTS module.
2 Simulation Image is added to Kight Tour example in CSP Module

Bug Fixing
1 Bugs in external choices are fixed in all modules