Extensible Data Type and Library

For simplicity, existing modules in PAT only support integer variables, Boolean variables and (multi-directional) arrays of integer or Boolean. However, sometimes user defined data type is necessary and can simplify the model substantially. In the Common project, PAT defines the interface for variable valuations, which includes methods for hashing (or encoding) the value for state representation, a to-string method for simulator display and deep-clone method for duplicating the values. PAT provides the functionality to create arbitrary data type by simply creating a C# class inheriting the Value interface. These classes can be imported into the model (based on the reflection mechanism in .NET) and used as normal variables. We demonstrate the idea by creating a Set data type using the code in the following Listing.

• 1       public class Set:HashSet < int >, Value {
• 2                public override string ExpressionID {
• 3                      get {
• 4                             String id = " " ;
• 5                             foreach ( int element in set ) {
• 6                                     id += element + " , " ;
• 7                             }
• 8                             return id.TrimEnd ( ' , ' ) ;
• 9                      }
• 10                }
• 11                public override string ToString( ) {
• 12                      return " { " + ExpressionID + " } " ;
• 13                }
• 14                 public override Value GetClone( ) {
• 15                      return new Set ( this ) ;
• 16                }
• 17                 public bool IsDisjoint( Set set ) {
• 18                      foreach ( int i in this ) {
• 19                             foreach ( int j in set ) {
• 20                                      if ( i == j ) {
• 21                                           return false ;
• 22                                      }
• 23                             }
• 24                      }
• 25                      return true ;
• 26                 }
• 27       }

First, Set class implements the Value interface in order to be used in PAT. ExpressionID property returns the unique string representation of the data type at any time. ToString method produces the pretty print of the set elements, which can be used in the simulator. GetClone method implements the PROTOTYPE design pattern. To implement the operations of a set, Set class inherits the generic HashSet class in the .NET framework. Therefore existing methods in HashSet like Add, Remove are inherited automatically. New methods can also be created easily, for example IsDisjoint method. Compared with Bogor's set extension, our approach is much simpler. To use the Set class, users only need to import the compiled DLL and declare the variable of Set type. The variable can be initialized using new keyword and methods of Set class can be invoked as in traditional OO program. The syntax of using the user defined data type can be found in section 2.5 Using C# Code as Libraries.

Another benefit of the extensible data type design is that users can control the data hashing function, which may reduce the state space significantly. For example, a check board can be presented by the position of pieces only without including the empties spaces. Therefore, the ExpressionID property can be defined to contain only positions of pieces to speedup the verification.

Language Syntax Extension

In general, the input language of a model checker must be carefully designed, with preciseness, intuitiveness and efficiency in mind. A minor syntax extension or modification may require re-examination of the whole system. PAT facilitates such extensions with the following design supports.

• All the parsers in PAT are developed using ANTLR parser generator with clearly documented grammars rules. New language syntax can be easily added by changing the grammar rules and generating the code automatically.
• Each language syntax is implemented in a single class (refer to PAT.CSP package in the class diagram), which implements its semantics. To support new language syntax, only one class needs to be implemented by following the syntax class interface (e.g., the Process class in the class diagram). PAT's layered design requires minimum change in the system and all model checking algorithm developed can be reused.

Taking the probabilistic module PCSP as an example, it extends the concurrent system modling language CSP# with one additional language feature, i.e., probabilistic choices. Knowledge about existing modules is required and a new parser is created for the extended language features.