ProTL provides a graphical user interface, which can be separated into two parts, i.e., Translator and Verifier.

Translator

Translator provides the service for users to edit textural encodings of PrCCSL specifications and automatically translate PrCCSL encodings/specifications into corresponding Uppaal-SMC models. In addition, Translator provide the option for users to import the behavioral models in Uppaal-SMC ( .xml ) file and combine the generated Uppaal-SMC model of PrCCSL specification and the imported file into an ( .xml ) file.

As shown in Figure 1, Translator of ProTL consists of five parts:

1. Tool Bar (on the top): provides basic functions that enable user to import and save files;

2. Setting (on the upper left corner): allows users to configure the parameters for translation, i.e., simulation bound;

3. Keyword (below the Setting): offers the textural keywords in PrCCSL to facilitate users edit the PrCCSL encodings/specifications;

4. Editor (on the right): allows users to edit encodings in PrCCSL format;

5. Console (on the bottom): shows the errors/warnings information of the input PrCCSL encodings/ specifications to help users to refine/fix the encodings.

Verifier

Verifier offers the support of automatic generation of probabilistic queries that can be recognized in Uppaal-SMC and performs verification and simulations on the generated Uppaal-SMC models and queries. Figure 2 pictures the Verifier of ProTL consisting of three parts (from top to bottom): Query Configuration, Query List and Console.

Query Configuration enables specification of parameters for generation of five types queries, which consists of six sections: Hypothesis Testing, Probability Estimation, Probability Comparison, Simulations, Expected Value and Generate Query button.

Query List exhibits the set of generated queries and performs verification/simulation based on queries. Users can select (multiple) queries in Query List for verification/simulation. The verification/simulation of the selected queries can be started by clicking the Verify button. After the verification/simulation is completed, the verification results, along with the verification performance (analysis time, CPU, memory consumption, etc.), are displayed in the Query List table. Queries can be selected or de-selected using the left-button of mouse or clicking with Shift or Contrl key pressed (press the Shift key to (de-)select multiple queries and the Contrl key to (de-)select a single query).