PAT: Process Analysis Toolkit

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

Version History

Version 3.7 (N-PAT)

21 Aug 2021
N-PAT is a proof of concept model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks.
To install N-PAT, please refer N-PAT installation and usage instructions.
N-PAT documentation can be found at here.
In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models.

Version 3.5.1 Build 20562

1 Bug fixing in PCSP and RTS for hiding synchronous channel communication
2 Bug fixing for PCSP configuration
3 Improvement of TA module.

Version 3.5.1 Build 21489

1 Optimization of parsing parallel composition
2 Bug in parsing some LTL properties
3 Improvement of TA module.

Version 3.5.1 Build 21466

13, Aug, 2013: PAT 3.5.1 is released!

Version 3.5.0 Build 21221

28, Dec, 2012: PAT 3.5.0 is released!

Version 3.4.4 Build 20502

30, July, 2012: PAT 3.4.4 is released!

Version 3.4.3 Build 20099

15, April, 2012: PAT 3.4.3 is released!

Version 3.4.2 Build 19913

7, March, 2012
1 Bug fixing for RTS module, particularly for the atomic keyword.
2 For RTS module, global variables are disabled in timed processed.
3 All BEEM examples are added in for PAT.
4 Bug fix in using constants in LTL properties.

Version 3.4.2 Build 19689

4, Feb, 2012: PAT 3.4.2 is released!

Version 3.4.1 Build 19499

19, Jan, 2012
1 in CSP module, macro support if and while in the declaration.
2 Better self-composition detection is implemented in CSP module to avoid crash of PAT
3 More BEEM exampels are added (work in progress)
4 Invalided statement checking is added in all modules.
5 Flashing in the model checking window when the verification is finished.
6 Auto-update is avaiable for this release.

Version 3.4.1 Build 19462

14, Jan, 2012
1 in CSP module, channels can attach programs

For the synchronous and asynchronous channel,
channel c 0; or channel c 1;
var x = 1;

P = c!x{ x = 2 } -> P;
Q = c?y{ x = y; } -> Q;
A = P ||| Q;

The execution sequence is c!x -> (x = 2) -> c?y -> (x = y)

2 Bugs fixing in CSP module and RTS module
3 More BEEM exampels are added (work in progress)

Version 3.4.1 Build 19371

5, Jan, 2012
1 Code generation is supported for CSP module (beta version, based on QP platform)
2 BDD support for CSP module is done
3 Bitwise operator for integers is supported in all basic 5 modules: & (and), | (or) and xor (^)
4 Some BEEM database examples are added (work in progress)
5 RTS module parser update to support channel array and process parameter range
6 Parser bug fixing and macro is supported in all basic 5 modules
7 RTS non-zeno checking with zone abstraction performance improvement

Version 3.4.1 (Beta) Build 19079

7, Dec, 2011
1 Fix the semantics of interrupt
2 Disable the support for BDD if there is a hiding in the process.
3 Support Macro in the CSP and RTS module.
#define multi(i,j) i*j;
System = if (call(multi, 3,4) >12 ) { a -> Skip } else { b -> Skip };
This could be useful to define some functions then you can use the function directly in the model.
Before you have to use C# static method to do this, now PAT offers another choices.

Version 3.4.1 (Beta) Build 19066

23, Nov, 2011
1 Performance improvement for BDD verification of CSP module
2 RTS module bug fixing and simulation display improvement
3 Bug fixed for the array index assignment in all modules
4 Verification result with improved coloring
5 Add exception stack display in the method call exception.
6 Statistic display improvement for all modules in verification window.

Version 3.4.1 (Beta) Build 18833

15, Nov, 2011
1 BDD support for CSP module is ready for testing. Wild Variable is also supported.
2 RTS module supports guard and ifa now. Parsing will fail if timed process is immediately following the guard and ifa.
e.g., P = [cond](Wait[5]);
3 A number of bug fixing for parsers in all modules.
4 Skip checking inside sequential composition is added and improved for all modules.
5 using direct array in process arguments and call arguments are supported.
var <IntArrayList> intList;
intList.Add([1, 2, 3, 4, 5]);
6 font fixing for 64bit Windows machine.

Version 3.4.0 Build 18776

06, Nov, 2011
1 xor operator is supported in CSP/RTS/PCSP module.
2 Generate witness trace check box is supported in verification window. you can uncheck it if the counterexample takes too long to generate or not important.
3 LTL parser bug is fixed
4 Bugs fixing in call method
5 Auto update is released.

Version 3.4.0 Build 18671

20, Oct, 2011
1 Select is supported in LTS
2 Global variable update fixing in all modules.
3 Bug fixing in PCASE in PCSP module.
4 Auto update is released.

Version 3.4.0 Build 18653

18, Oct, 2011
1 Bug fixing for variable range checking.
2 Bug fixing for RTS module, particularly digitalization.
3 Auto update is released for Version 3.4.0

Version 3.4.0 Build 18600

5, Oct, 2011
1 Bug fixing for parallel compositional pattern.
2 Some examples update for CSP module.

Version 3.4.0 Build 18595

2, Oct, 2011
1 Cancel and excepiton during the verification will give more infomation now
2 Parser for all modules are updated for the case that user defined data structure is used in the process parameters.
3 TA module updated with BDD support, also automata local variables are supported.
4 Self-looping process is detected in parser to avoid PAT easy crash
5 New BFS search engine is added for reachablity checking with min/max conditions (Beta).
6 Compositional detection of Skip in the sequential composition. Previously, P = (Skip ||| Skip); a -> Skip; has 3 states. Now it has only 2 states.
7 BDD for CSP module is disabled since it is not stable at the moment.

Version 3.4.0 Build 18409

31, Aug, 2011
1 PAT now supports channel arrays, which is a syntax suger to make the modeling easier if the channels are parameterized. The following syntax demonstrates how to use the channel array.
channel c[3] 1;
Sender(i) = c[i]!i -> Sender(i);
Receiver() = c[0]?x -> a.x -> Receiver() [] c[1]?x -> a.x -> Receiver() [] c[2]?x -> a.x -> Receiver();
System() = (||| i:{0..2}@Sender(0) ) ||| Receiver();
Note: Two or N dimentional channel array can be simulated by using 1 dimentional channel array. Hence, we don’t provide syntax support for that. For example channel c[3][5] 1 is same as channel c[15] 1, and c[2][3]!4 -> Skip is same as c[2*N+3]!4 -> Skip, where N is the first dimention.
2 3. CSP Module supports symbolic model checking using BDD (Beta version, under testing and optimization)

Version 3.4.0 Build 18350

28, Aug, 2011: PAT 3.4 (beta) is released!

Version 3.3.1 Build 17101

27, April, 2011: PAT 3.3.1 is released!

Version 3.3.0 Build 16884

2, April, 2011
1 File Inclusion is improved to allow nested inclusion.
User can split the big models in several files for better orginization.
Find Usage, Go to declarision, and model explorer is improved to support multiple files.
2 Auto-updating checking is improved by a separate thread in the backend.
3 Calling C code is possible in PAT with one demonstrating example
4 GUI bug fixing.

Version 3.3.0 Build 16818

1 Include keyword is added in CSP, PCSP, RTS and PRTS module to include other models in the current working model.
2 GUI bug fixing and enhancemant.
3 Auto-updating form is blocked by the splash screen

Version 3.3.0 Build 16750

18, March, 2011: PAT 3.3.0 is released!

Version 3.2.3 Build 16562

28, Feb, 2011: PAT 3.2.3 is released!

Version 3.2.2 Build 16422

30, Jan, 2011
1 Renaming Functions is supported in the Editor
2 Module Generator is improved with better GUI, complete generated code. Module icon is also supportted in the
generated code.
3 Minor Bugs in the GUI are fixed.

Version 3.2.2 Build 16302

21, Jan, 2011: PAT 3.2.2 is released!

Version 3.2.1 Build 16181

26, Dec, 2010
1 Bugs for alphabet calculation are fixed in all modules.
2 Model Explorer is added in the GUI.

3 More examples are added in the CSP module.

Version 3.2.0 Build 16032

8, Dec, 2010
1 Intellesense bug is fixed.
2 Bugs in PCSP module is fixed.
3 Precision in PCSP module is changed from float to double, so that we can handle precision at level of 10^-15.
4 BDD is working in 64 Bit now.
When you update the old version of 64 bit to new version using auto-update, please replace the CUDDHelper.dll
in the installation folder using the one under 64Bit folder. Otherwise the BDD funtion will not work correctly.

Version 3.2.0 Build 16003

3, Dec, 2010
1 Bug in PCSP is fixed.
2 Auto-update is ready for the new version.

Version 3.2.0 Build 15997

26, Nov, 2010
1. Some parsing errors are fixed.
e.g. P = e{;} ->Skip;
2. Intelli-sense is disabled when in comment
3. DLLs can be put under the same folder as in Model.
4. Other bug fixing.
5. Manual update

Version 3.2.0 Build 15962

23, Nov, 2010
1 Mono execution is fixed in Mac and Linux.
2 LTL verification algorithms are reimplemented.
3 Bugs in RTS timed divergence checking are fixed.
4 Arrays are supported in local variables.
5 MDP verification are speed up (experimenting)

Version 3.2.0 Beta Build 15605

22, Oct, 2010
1 Bug fixing on GUI and Mono execution.
2 Language localization for Chinese, Traditional Chinese and Vietnamese are improved.

Version 3.2.0 Beta Build 15506

6, Oct, 2010
1 Bug fixing for all modules
2 TA module supports select syntax, examples are added
3 Refinement checking’s performance is improved significantly
4 LTS module is re-structured
5 RTS module’s performance is improved by using maximun delay after one step.

Version 3.2.0 Beta Build 15288

2, Sep, 2010
2, Sep, 2010: PAT 3.2.0 (beta) is released!

Version 3.1.0 Build 146599

1, Aug, 2010
1, Aug, 2010: PAT 3.1.0 is released. PAT is cross-platform now: running on Linux, Mac OS and more!

Version 3.0.0 Build 14419

19, July, 2010
1 Bug fixed in the auto-updating file
2 Directory mode is added in PAT.Console. User can put all models into a directory and use console to run all all of them.

Version 3.0.0 Build 14399

15, July, 2010
14, July, 2010: PAT 3.0.0 is released!

Version 3.0.0 Build 14150

1, June, 2010
Fix the bug for auto updating, please reinstall PAT 3.0 in order to make auto update working.

Version 3.0.0 Build 14116

30, May, 2010
Bug fixing, mainly for RTS module

Version 3.0.0 Build 14000

22, May, 2010
22, May, 2010: PAT 3.0.0 beta is released!

Version 2.9.1 Build 12592

18, March, 2010
18, March, 2010: PAT 2.9.1 is released!

Version 2.9.0 Build 12592

23, Feb, 2010
1 Bug fixing for refinement checking with failures and divergence.
2 User manual is updated.

Version 2.9.0 Build 12511

10, Feb, 2010
1 Bug fixing and improvement in all parsers.
2 Simulator is improved with complete state display
3 Images are added for sliding game and shunting game in the simulator (Contributed by Tian Huat)
4 User manuals are updated (by Liu Yan)
5 New example is added for DBM testing

Version 2.9.0 Build 12259

4, Feb, 2010
1 Bugs fixed for parallel operator and refinement checking (for all modules)
2 Performance improved for refinement checking (10% – 15% speedup)
3 PAT.Math is supported for normal math functions
4 Duplicated edges are removed for hiding tau event in simulation

Version 2.9.0 Build 12259

29, Jan, 2010
29, Jan, 2010: PAT 2.9.0 is released!

Version 2.8.0 Build 11674

16, Dec, 2009
1 Several Bug logic and UI fix
2 Beta LTL to Rabin automata translator is implemented
3 Simplification for Skip and Stop in parallel/interleave/sequential processes.

Version 2.8.0 Build 11481

05, Dec, 2009
1 Bug fix in verifier for reachability testing result display

Version 2.8.0 Build 11481

04, Dec, 2009
1 Bug fix in parser

Version 2.8.0 Build 11465

03, Dec, 2009
1 Bug fix in counter example display for safety property.
2 Shunting game example is added.

Version 2.8.0 Build 11450

02, Dec, 2009
02, Dec, 2009: PAT 2.8.0 is released!

Version 2.7.0 Build 11273

13, Nov, 2009
1 Bug fixing for the self choice composition in parsers.
2 Bug fixing for parallel alphabet calculation of recursive processes.
3 Bug fix for LTL like !(<>P || <>!P).
4 OutOfMemory exception is caught properly and PAT will not crash for it.

Version 2.7.0 Build 11141

24, Oct, 2009
1 24, Oct, 2009: Warning List is supported. PAT makes the modeling easier!

Version 2.7.0 Build 11121

23, Oct, 2009
1 Process Counter Variable is supported in event prefix
2 Bug fixing for using atomic with parallel operator
3 Exceptions are caught for config files missing or no-writting access rights.
4 Bug fixing for using local variables

Version 2.7.0 Build 11055

09, Oct, 2009
1 Japaness Language is updated
2 Bug fixing.

Version 2.7.0 Build 10964

25, Sep, 2009
1 Bugs are fixed for RTS module.
2 C# library supporting is improved. 25, Sep, 2009: PAT supports user defined data structures
3 Performance improvement for all modules by changing the expression evaluation.
4 Examples for alternating bit protocols are added.

Version 2.7.0 Build 10711

15, Sep, 2009
1 Bugs are fixed for RTS module.
2 PaceMaker example is completed for 16 modes.
3 Performance improvement for all modules. We implemented a Hashtable by ourself to replace the .NET built-in Dictionary class.
4 ifa and guard constructs are disabled in RTS module for the confusing semantics.

Version 2.7.0 Build 10511

08, Sep, 2009
05, Sep, 2009: PAT 2.7.0 is released!
1 (Timed) Divergence-free assertion is supported.
2 Bugs fixing in the RTS module.

Version 2.7.0 Build 10427

05, Sep, 2009
05, Sep, 2009: PAT 2.7.0 is released!

Version 2.6.0 Build 10063

10, July, 2009
1 parser supports multi-dimentional array initialization for all the three modules.
2 change Submit model to Email model to allow user to send model to others quickly.
3 Two new puzzle examples are added.
4 user manual update for new parser and user feedback.

Version 2.6.0 Build 10016

24, June, 2009
1 Several bug fixing in RTS module.
2 Implemented the latex generation function for RTS, and fixed some bugs in CSP latex generation functions

Version 2.6.0 Build 9922

15, June, 2009
1 Bug in parsers are fixed for Constants used as Integer directly
2 X operator is not allowed in RTS module
3 User Manual is updated to the latest version 2.6.

Version 2.6.0 Build 9909

12, June, 2009
09, Jun, 2009: PAT 2.6.0 is released!

Version 2.6.0 Build 9847

9, June, 2009
09, Jun, 2009: PAT 2.6.0 is released!

Version 2.5.0 Build 9622

4, June, 2009
1 Bugs in the Real-Time System Module are fixed.
2 within syntax is supported in Real-Time System Module. e.g., P within[4]/ P within[3,10]. User Manual is to be updated.
3 Railway control example is added in for RTS module.

Version 2.5.0 Build 9580

3, June, 2009
1 Bugs in the Real-Time Module are fixed.
2 Event level fairness checking are considering tau and termination events now.

Version 2.5.0 Build 9544

2, June, 2009
02, Jun, 2009: PAT 2.5.0 is released!

Version 2.4.0 Build 8808

7, May, 2009
1 The Needham-Schroeder Public Key Protocol example is added.
2 Process parameters can be used in channel input for both CSP and WS module
3 Model Checking forms are made consistent
4 Bugs of parallel verification are fixed.
5 UI bugs fixed
6 User Manual is updated to the latest syntax

Version 2.4.0 Build 8710

30, April, 2009
30, Apr, 2009: PAT 2.4.0 is released!

Version 2.3.0 Build 8000

13, April, 2009
13, Apr, 2009: PAT 2.3.0 is released!

Version 2.2.0 Build 7862

8, April, 2009
1 Rubik’s Cube example is added.
2 Cut number popup is added in the simulator for infinite processes.
3 Updated Parameterized Leader Election to make it smaller.
4 Constants are allowed in the process invocation
5 parser checking for array index is added: must be an integer value or expression.
6 enum is supported. see user manual.
7 Latex buttons and icons are added (beta version)
8 Parallel model checking bug fixed.
9 Fairness check for concrete counterexample is added.

Version 2.2.0 Build 7760

2, April, 2009
1 External Choice will not distinguish tau event and normal event. Although this is different from the original CSP semantics, but for the simplicity of the modeling, we adopt this new semantics.
2 Boolean variables can be directly used in the condition of if/while/conditional choice.
3 Bugs in simulator are fixed.

Version 2.2.0 Build 7715

1, April, 2009
1 PAT2 Shortcut links are fixed. especially for vista user to get rid of UAC.
2 Simulate Counter Example Button is renamed to Simulate Witness Trace
3 Add UNKNOWN result to LTL assertion and reachability assertion

Version 2.2.0 Build 7688

30, March, 2009
1 What’s new link is added to the GUI and update screen
2 Invisible Events: User can explicitly write invisible event (i.e., t event) by using keyword tau, e.g., tau -> Stop. In the tau event, statement block can still be attached. With the support of tau event, you can avoid using hiding operator to explicitly hide some visible events by name them tau events. The second way to write an invisible event is to skip the event name of a statement block, e.g., {x=x+1;} -> Stop, which is equivalent to tau{x=x+1;} -> Stop.
3 out of memory exception is handled properly
4 Refinement checking for hiding expression’s bug is fixed
5 Simulator window edge tooltip is simplified.
6 Parser for channel input is implemented: no parameter or global variables are allowed in channel input.
7 Added support for parsing “P = ||| x :{1..2} ( a -> Skip {a.x});”
8 User Manual is updated to latest version.

Version 2.2.0 Build 7621

27, March, 2009
27, Mar, 2009: PAT 2.2.0 is released!

Version 2.1.0 Build 7082

9, March, 2009
09, Mar, 2009: PAT 2.1.0 is released!

Version 2.0.0 Build 6360

21, Jan, 2009
1 New examples are added for stablizing leader election protocols
2 Saving Button bugs are fixed.
3 Option form is improved.
4 Allow auto saving when buttons are clicked.
5 Bug fixing for WS module.

Version 2.0.0 Build 6091

9, Jan, 2009
1 Each document tab can be closed/saved by using right mouse click on the tab.
2 UI update to fix some bugs and improve the usability
3 Web Service Module is implemented. Currently, we have finished all functions: verification, simulation, synthesis
But this module still needs more testing.
4 Example updates for lift system, keyless car system and pace maker examples.

Version 2.0.0 Build 5595

5, Jan, 2009
1 Icons added for the CSP and WS files
2 Exception Dialog is added
3 Choregraphy Synthesis in WS module is implemented.
4 Archectecture improvement.
5 Road Assistance Example for WS is added.

Version 1.3.1 Build 5530

28, Dec, 2008
Strong Global Fair algorithm is improved. The performance is improved significantly if the found SCCs are big.

Version 1.3.1 Build 5515

21, Dec, 2008
1 21, Dec, 2008: PAT 1.3.1 is released!
2 Launch PAT after installation option is added.
3 Manual is updated to version 1.3.1.

Version 1.3.0 Build 5478

17, Dec, 2008
1 Manual is updated for the typos in tutorial and language reference. The completed grammar rules are added.
2 Parser supports channel events like “c!1”, “c?3”. ! and ? are special charactors, it is not possible to put them into LTL assertions like normal events eat.0
So we decided to user quotation mark to group them as single event. Hope this is acceptable solution.
3 Upon the request, we changed the parser so that the semi colon of the last expression in event statement block is optional.
e.g., “event{a = a +1} -> Stop” is valid syntax. This will make the modelling easier.

Version 2.0.0 beta

10, Dec, 2008
The Web Service Module is integrated in PAT.

Version 1.3.0 Build 5450

04, Dec, 2008
New Manual is updated.
Parser bug fixed.
Keyless Car System Example is added.

Version 1.3.0 Build 5423

26, Nov, 2008
Display of the current enabled events is fixed.
Unhandled exceptions of PAT is displayed with better details.
Parser typo fixed.

Version 1.3.0 Build 5395

25, Nov, 2008
25, Nov, 2008: PAT 1.3.0 is released!

Version 1.2.9 Build 5202

21, Nov, 2008
init event is added to the system.
UI improvement.

Version 1.2.9 Build 5152

19, Nov, 2008

19, Nov, 2008: PAT 1.2.9 is released! Please re-install PAT!

Version 1.2.8 Build 4917

15, Nov, 2008
15, Nov, 2008: PAT 1.2.8 is released!

Version 1.2.7 Build 4917

11, Nov, 2008
Bug fixed for negative operator.
Parser is improved
csp can be opened by PAT directly now.

Version 1.2.7 Build 4850

06, Nov, 2008
Bug fixed for the exmaple loading.

Version 1.2.7 Build 4848

05, Nov, 2008
Bugs in the limited depth search is fixed.
Partial Order Reduction is disabled for the limited depth search.

Version 1.2.7 Build 4824

04, Nov, 2008
04, Nov, 2008: PAT 1.2.7 is released!

Version 1.2.6 Build 4709

17, Oct, 2008
1 Bugs in generating counter example is fixed.
2 Add multi-threading for the counter example generating prcoess
3 Parser supports variables in alphabets declarations, also, if the variable is not declared in the process definition, the error message will popup.

Version 1.2.6 Build 4680

16, Oct, 2008
Some bug fixing and performance improvement.

Version 1.2.6 Build 4600

13, Oct, 2008
Conditional Choice >> is removed from the syntax.
sdefine and sequal is added
Bug fixing for FD verification
Refinement checking speed improvement.
GUI improvement.

Version 1.2.6 Build 4531

10, Oct, 2008
Bug fix for the Event Prefix class.
The sequence class is optimized using algebra law. Got a big performance improvement.
Linearizability examples are added back.

Version 1.2.6 Build 4401

06, Oct, 2008: PAT 1.2.6 is released!

Version 1.2.5 Build 4268

03, Oct, 2008: PAT 1.2.5 is released!

Version 1.2.4 Build 3140

11, Sep, 2008
The structure is improved.
Bugs in the counter example display are fixed.

Version 1.2.3 Build 2684

8, Aug, 2008
Accept C# code as customized functions
Mailbox problem is built-in.

Version 1.2.2 Build 2566

6, Aug, 2008
Bugs in the LTL model checking is fixed.
User Manual is updated

Version 1.2.2 Build 2512

5, Aug, 2008
Bugs in the LTL model checking is fixed.
Peterson Algorithm is added into the system.

Version 1.2.2 Build 2492

31, July, 2008
MSAGL is integrated into PAT.
Progress bar in the model checking is removed
Bugs in LTL2BA conversion are fixed.
Simulation Direction choice is added: Top-Down or Left-Right.
Auto-update function is added to pat.

Version 1.2.1 Build 2301

23, July, 2008
Performance (both time and memory) for the refinement checking is improved.
Timer is added in the model checking UI.
One Linearizibility example is added in.

Version 1.2.1 Build 2213

22, July, 2008
Linearizibility examples are added in.
One more leader elction protocol is added in.
two puzzle examples are added in.
Bug in refinement check is fix.
The local variable is considered in the partial order reduction of refinement checking.
Syntax color for Skip and Stop is changed to Navy.

Version 1.2.1 Build 1988

16, July, 2008
Simulator’s User interface is improved:
1 Current enabled events are highlighted in blue
2 hidden events are shown as [event].
Two leader election protocol is added as built-in examples.

Version 1.2.1 Build 1952

14, July, 2008
The couter example information is totally redesigned for better speed and code structures.
Counter example generation and simulation’s bugs are fixed.

Version 1.2.0 Build 1812

10, July, 2008
Process level fairness is supported: include global, strong and weak fairness
Leader Election protocol examples are implemented and built-in PAT.
Counter example simulation is improved.
Strongly connected components simulation is improved.
Counter exampple generation bugs fixed.

Version 1.1.5 Build 1566

1, July, 2008
Fairness loop detection bug fixed and performance improved.
Verification details added: Search Depth, States visited, Transitions.
Unary Operator bug fixed.
The process level fairness coding started.

Version 1.1.5 Build 1506

7, June, 2008
Built-in examples are corrected.
Console is updated to latest model checker.

Version 1.1.5 Build 1484

2, June, 2008
Temporal operators are supported in PAT:
G (always)
F (Eventually)
U (until)
V | R (realease)
X (next)
The example creation form is improved to add more explainations.
The error message of wrong LTL properties is improved.

Version 1.1.5 Build 1374

25, May, 2008
Parallel/interleave Parsing Errors are fixed.
Repeated properties can be detacted and reported.
Specification Description panel is added.
The embedded example are completely re-written now, a new example BridgeCrossing Exmaple is added.
GetAlphabet Method and ClearConstant Method. The alphabet of a process is default to be the events constituting the process (all parameter instantiated) expression.
Support constant in declarations definition (and possible elsewhere).
Report error message if an array declaration contains a negative number.
Verification user interface is improved and more meaningful icons are used.

Version 1.1.5 Build 1137

7, May, 2008
The simulation window’ docking display is improved.
The graph states info in the simulation window is added.

Version 1.1.5 Build 1128

5, May, 2008
Build Number is added into the system for better tracking. The build number is auto-increased.
Parser is redesigned using two time AST parsing.
Post to Post Links II error: No post found with slug "add-the-syntax-checking-after-parsing-to-rule-out-invalid-un-declared-variables-usage"
Weak Fair and Strong Fair annotations are supported by PAT now
In the main UI, Output panel display bug is fixed.
StateGuard class is replaced by using IfProcess class.
Unit Testing via NUnit is added, hope later we can add more test cases into the system.
Simulation window is redesigned completely

Version 1.1.5 revision 1

25, April, 2008
User interface of simulation form is improved to allow user adjust the width of the different columsn.
The loops in the counter example is highlighted, and highlighted in simulator.
If process is implemented for the easy handling of multiple external choice operator.
Bug fixing of Bounded Model Checking: the TLS tree tranversal method is wrong.
Bug fixing in if expression evaluation: the else clause null checking is missing in build var method.
Strong fair and weak fair annotations are added in the system, the corresponding model checking algorithms are updated.

Version 1.1.5

25, April, 2008
User interface of model checking form is improved.

The loops in the counter example is highlighted in the output box, and also highlighted in simulator.
If process is implemented for the easy handling of multiple external choice operator.
Bug fixing of Bounded Model Checking: the TLS tree tranversal method is wrong.
Bug fixing in if expression evaluation: the else clause null checking is missing in build var method.
Strong fair and weak fair annotations are added in the system, the corresponding model checking algorithms are updated.

Version 1.1.4 revision 1

23, April, 2008
Allow Constant in the index parallel and interleave processes
Exception handling is added in the Simulation and Model Checking interface so that the application will not crash due to the invalid model.
Various Bug fixing

Version 1.1.4

31, March, 2008
Refinement checking is implemented.
Installation file is created.
Batch Mode Console interface is created for PAT.

Version 1.1.3

20, Feb, 2008
Partial Order reduction is added to bounded model checking.
channel is supported
bug fixed in simulator and model checkers.
Syntax sugar for the Interleave and Parallel Construct is added.

Version 1.1.2

16, Jan, 2008
Libra is renamed to PAT (Process Analysis Toolkit) to avoid the conflict with Microsoft Libra searching system.
Reachbility checking is supported.
Assertions is introduced for various model checking and refinement checking.
Combine the Model Checking and Bounded Model Checking in one Window.
Performance optimizations and bug fixing.
The support of array is added.
Fair events are added to the examples.

Version 1.1.1

09, Jan, 2008
Bug fixed for the model checking algorithms.
Partial Order Reduction option is added in the user interface
SAT model checking can handle Local Parameters.

Version 1.1

03, Jan, 2008
Partial Order Reduction is added, which gives a great performance improvement for some cases.
On-the-fly model checking algorithms are implemented for the specifications with or without fairness. We implemented the improved iterative Tarjan algorithms.
Counter example simulation is added in the model checking windows.
System simulation is improved and simplified.

Version 1.0

28, Nov, 2007
Global variables and functions are introduced into Libra.
Dike is renamed to Libra due to its pronunciation.
More testing are needed.

Version 0.9

10, Nov, 2007
Model Checker based on SAT solvers are added into the system.
System is restructured for extensible design and standard naming convention.

Version 0.8

15, Oct, 2007
Simulator is added into the system.

Version 0.7

02, Oct, 2007
Parser is re-implemented to support all possible definitions specifications.
Verification can be done for user selected Process definitions.
LTL error message reporting function added.
Syntax highlighting is added.

Version 0.6

26, Sep, 2007
More meaning parsing error report for the specification is added.
Full set of editing functions are added.
The tool is named Dike officially.
LTL parser crashing is solved.

Version 0.5

10, Sep, 2007
Comprehensive Multi-tab editing environments are integrated into the Dike.
The implementation is based on FireBall.
LTL parsing options are added.
Peterson’s Algorithm Examples are added.

Version 0.4

23, August, 2007
The Buchi Automata Viewer is integrated.
MC algorithms improved: Finite processes can be checked under fairness conditions

Version 0.3

10, August, 2007
The LTL to BA convector is added.
Dinning Philosophers Examples are added.

Version 0.2

2, August, 2007
The parser of CSP is added, which is based on Antlr 3.0.
Get All traces function is added.
Several bug fixing for the model checking algorithms
The previous closure algorithm is improved for fast feasible and model checking.

Version 0.1

25, July, 2007
The first implementation of the UI is finished.
Feasibility and Model checking algorithms is completed.