PAT: Process Analysis Toolkit

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

25, Sep, 2009: PAT supports user defined data structures


PAT only
supports integer, Boolean and
integer arrays for the purpose of efficient verification.
However, advanced data structures (e.g., stack, queue, hashtable and so
on) are necessary for some models. To support arbitary data structures, PAT
provides an interface to create user defined data type by inheriting an
abstract classes
ExpressionValue.

The
following is one simple example showing how to create a hashtable
in C#.


using System.Collections;
using
PAT.Common.Classes.Expressions.ExpressionClass;

//the namespace must be PAT.Lib, the class and method names can
be arbitrary
namespace PAT.Lib {
    public class
HashTable : ExpressionValue
{
        public Hashtable
table;

        /// Default
constructor without any parameter must be
implemented
        public HashTable()
{
           
table = new Hashtable();
       
}

        public
HashTable(Hashtable newTable)
{
           
table = newTable;
       
}

        public void Add(int
key, int value)
{
           
if(!table.ContainsKey(key))
{
               
table.Add(key,
value);
           
}
       
}
       

        public bool ContainsKey(int
key)
{
           
return
table.ContainsKey(key);
       
}

        public int
GetValue(int key)
{
           
return (int)table[key];
       
}

        /// Return the
string representation of the hash
table.
        /// This method must
be overriden
        public override
string ToString()
{
           
string returnString =
“”;
           
foreach (DictionaryEntry entry in table)
{
               
returnString += entry.Key + “=” + entry.Value +
“,”;
           
}

           
return returnString;
       
}

        /// Return a deep
clone of the hash table
        ///
This method must be
overriden
        public override
ExpressionValue GetClone()
{
           
return new HashTable(new
Hashtable(table));
       
}

        /// Return the
compact string representation of the hash
table.
        /// This method must
be overriden
        /// Smart
implementation of this method can reduce the state space and speedup
verification
        public
override string GetID()
{
           
string returnString =
“”;
           
foreach (DictionaryEntry entry in table)
{
               
returnString += entry.Key + “=” + entry.Value +
“,”;
           
}

           
return returnString;
       
}
   
}
}

 Note the
following requirements when you create your own data structure
objects:

  • The
    namespace must be “PAT.Lib”, otherwise it will not be recognized. There is no
    restriction for class names and method
    names.
  • Importing the PAT Expression name
    space using “
    using
    PAT.Common.Classes.Expressions.ExpressionClass;
    “.
  • Only
    public methods can be used in PAT models
  • The
    parameters must be of type “bool”, “int”, “int[]”  (int array) or object
    (object type allow user to pass user defined data type as
    parameter)
    .
  • The
    number of parameters can be 0 or many.
  • The
    return type must be of type “void”, “bool”, “int”, “int[]” (int
    array) or user defined data type
    .
  • The
    method names are case sensitive.
  • Put
    the compiled dlls in “Lib” folder of the PAT installation directory to make
    the linking easy by using #import
    “DLL_Name”;

if your
methods need to handle exceptional cases, you can throw PAT runtime
exceptions as illustrated as the following example.


public static int StackPeek(int[] array)
{
    if (array.Length >
0)
           return
array[array.Length – 1];

    //throw PAT Runtime
exception
    throw new
PAT.Common.Classes.Expressions.ExpressionClass.RuntimeException(“Access an
empty
stack!”);
}

To
import the libraries in your model, users can using following
syntax:

#import “PAT.Lib.Hashtable”; //to import a library under
Lib folder of PAT installation path

#import
“C:Program FilesIntelHashtable.dll”; //to import a library using absolute
path

To
declar the user defined types in your models, please use the following

syntax:

var<HashTable> table; //use the class name here
as the type of the varaible.

To
invoke the public methods in your models, please use the
following syntax
:

  • table.Add(10, 2);
  • if(table.ContainsKey(10))…


 


Copyright © 2007-2009 School of Computing, National University of
Singapore