This package implements main graphical user interfaces and the plug-in architecture. GUI package loads the syntax files of different modules during the system initialization, which stores the syntax information (e.g., keywords, folding, and auto-completion) and module information. When users want to perform syntax checking, simulation or verification of an input model, the linked module is loaded into the system dynamically using reflection technique and then the corresponding interface method is invoked.

PAT.Common package

As shown in the Class Digram prevously, PAT.Common package consists of three parts which are module interfaces, common GUI and shared libraries.

Module Interfaces
      The module interface adopts ABSTRACT FACTORY pattern, where ModuleFacadeBase is the abstract factory, and ModuleFacade classes in each module are concrete factories. The product is Specification interface, and the concrete products are the actual Specification implementations in modules. The clients of using the products are the GUI classes. This pattern separates the details of different modules from their general usage.

• Abstract class ModuleFacadeBase in PAT.Common package defines the module interface. It behaves as the central gate communicating with the GUI package by adopting the FACADE design pattern, i.e., check the syntax, show simulator window and model checker window. Note: All modules must implement this interface in order to be recognized by the plug-in framework.
• Specification is the interface class for the internal representation of system models. It also uses FACADE pattern to communicate with SimulatorGUI and ModelCheckerGUI which are the common GUIs, to provide the information of the user input model. Specification is composed by system model and properties (named Assertions in the class diagram) which are to be verified. Since system model information is module dependent, Specification is only associated with Assertions in the common package.

Shared Library
      The Expression and Value classes define the interfaces for a simple but general WHILE language with variables and some primitive values. Though these classes should be implemented in the actual module, we move them to the common library so that they can be shared by all modules. Variable values need to be cloned if one state has more than two outgoing transitions. To systematically implement the clone process for all values, we adopt the PROTOTYPE pattern for Value class and its subclasses, where the Clone method creates new objects by copying the existing ones.

Besides the module interfaces and shared library, PAT.Common package contains the intermediate layer and verification algorithms in the analysis layer.

The LTSState Class
      Since we take CSP module for the running example, the intermediate representation layer here is just one abstract class LTSState, which implements a single transition with a target state in LTS definition. The transition's label is stored in the Label property, and target state information (e.g., variable valuation, channel buffer, program counter and so on) shall be realized in the actual module since it is module related. MoveOneStep method generates all the possible transitions starting from the target state. GetID method returns the unique hashed string representation of the label and target state.  The two abstract methods shall be realized in the actual modules and will be used by the verification algorithms. It is clear that starting from an initial state, these methods are sufficient to generate the complete state space.
      Note: If symbolic model checking is used, the EncodeProcess abstract method should be realized in actual module to encode the target state and outgoing transitions to Boolean formulae that can be used by the symbolic model checker or SAT solvers.

The Assertion Class
      Assertion class defines the interface for properties. It has one initial state, from where it explores the system state space and produces a counterexample if the property is not satisfied. Because verification algorithms need to keep track of visited states or have a scheduler if the concurrent processes have different priorities, a StateManager and a SchedulingManager are linked with the Assertion for verification algorithm to use them to store the states and perform process scheduling without worrying about the actual implementation. These two classes also adopt the STRATEGY pattern since a number of state hashing and scheduling strategies are possible.
      Currently, for LTS verification, four categories of assertions are supported as shown in Class Diagram. For example, for safety properties (e.g., DeadlockAssertion, RefinementAssertion and ReachabilityAssertion), three searching strategies are possible: depth-first-search (DFS), breadth-first-search (BFS) and symbolic verification algorithm using greatest fixed point method. For liveness properties (i.e., LTLAssertion), two searching strategies are possible: nested DFS [GJH97] or Tarjan's strongly-connected components searching algorithm [Tarjan72]. These strategies are selected according to users' choice during the run-time.

Note: To increase the reusability of the code, we create the generic version of popular algorithms using TEMPLATE pattern. For example, DFS and BFS are searching algorithms used in all safety property verification.
                  To have a reusable implementation, we create a generic DFS (BFS) algorithm with an abstract early termination condition. Different algorithms implement the early termination condition differently. For instance, DeadlockAssertion's early termination condition is that the current state is a deadlock state. ReachabilityAssertion's early termination condition is that the current state satisfies the desired condition.