LTSA-Eclipse Preview

Tutorial 1

Building Process Specifications

The LTSA-Eclipse plug-in is an extension to core LTSA tool that allows the creation of models of processes, driven by a formal behaviour model. 

The home of the original LTSA plug-in is here.

This tutorial contains:

• Overview of the views in the plug-in.
• An example of writing Finite State Processes (FSPs) in the LTSA Editor (for Eclipse).
• Compiling, Composing and performing Safety/Progress verification checks on processes. 
• Viewing processes as a Labelled Transition System in a Graphical Draw view.

Prerequisites

The following plug-in requirements are necessary to carry out this tutorial:

• An installation of Eclipse 3.1.0 (tested on build id: 200409240800) 
• Downloaded the preview plug-in build - click here to download. 

Installing the plug-in

Locate the installation directory of Eclipse.  Unzip the plug-in to the \eclipse\plugins directory.  After this has completed, browse to the plugins directory and verify that the directory now contains a ltsaeclipse_1.0.0 sub-directory.

Starting the environment

Start Eclipse using your normal start up routine.

Switching to the LTSA Perspective

1. From the Eclipse menu bar, select Window -> Open Perspective -> Other -> LTSA Perspective. If this menu item is not present, then the plug-in has not been successfully installed.
2. Notice the layout of views/windows will be similar to that illustrated in Figure 1.

Figure 1 LTSA Perspective in Eclipse

Creating a new LTSA project 

3. From the Eclipse menu bar, select File -> New -> Project.
4. Select the Simple -> Project as the type you wish to create and select Next.
5. Enter the name of the new project as LTSA and select Next.

Creating a new LTS container file

1. From the Eclipse menu bar, select File -> New -> File.
2. Select the LTSA project folder and enter the name testLTS.lts in the File name text box.
3. Click Finish to create this file, which will open the file as a new LTSA Editor type.

Writing a sample sequence process in the LTSA Editor view

1. Select the LTSA Editor window for the testLTS.lts file.
2. Enter the following process statements. Return on each new line as it appears in Figure 2.

Figure 2 LTSA Editor View for new LTS

3. Select File -> Save.
4. Notice the Outline View is updated with the new processes defined. If the Outline View is not visible, enable it through the Window -> Show View -> Other -> Basic -> Outline menu command. The Outline View is illustrated in Figure 3.

Figure 3 Outline View for new LTS

5. Select different processes in the Outline View and note how the focus of view changes to the process definition in the LTSA Editor view.

Compiling the sequence process and examining the Output View

1. Select the “SEQUENCE” process in the Outline View.
2. Right-click the SEQUENCE process in the Outline View, Figure 4 (left), and select the Compile item from the popup menu list.
3. Switch to the Output View. If this view is not visible, enable it by Window -> Show View -> Other -> LTSA -> Output.
4. Note the compilation result messages, as illustrated in Figure 4 (right).

Figure 4 Compile action (left) and Output View of compiled processes (right)

View the process in the Graphical LTS Process Draw view

1. Select the “SEQUENCE” process in the Outline View.
2. Right-click the SEQUENCE process in the Outline View and select the View Process item from the popup menu list.
3. Switch to the LTS Process view. If this view is not visible, enable it by Window -> Show View -> Other -> LTSA -> LTS Process.
4. Select the SEQUENCE process (from the left hand pane listing the processes compiled).
5. Use the Expand/Reduce Height/Width view toolbar to expand or reduce the drawing canvas.

Figure 5 LTS Process view as Graphical LTS Draw

Creating a parallel composition process in the LTSA Editor view

1. Select the LTSA Editor window for the testLTS.lts file.
2. Add the composition process (FLOW line 4.) definition after the SEQUENCE process definition, as shown in Figure 6.

Figure 6 LTSA Editor View for new LTS with parallel composition definition

3. Select File -> Save.
4. Notice the Outline View is updated with the new composition defined. If the Outline View is not visible, enable it through the Window -> Show View -> Other -> Basic -> Outline menu command. The Outline View is illustrated in Figure 3.

Figure 7 Outline View for new LTS with FLOW composition defined

5. Select the “FLOW” process in the Outline View under Compositions.
6. Right-click the FLOW process in the Outline View and select the Compose item from the popup menu list.
7. Switch to the Output View. If this view is not visible, enable it by Window -> Show View -> Other -> LTSA -> Output.
8. Note the compilation result messages.
9. Switch to the LTS Process view. If this view is not visible, enable it by Window -> Show View -> Other -> LTSA -> LTS Process.
10. Select the FLOW process (from the left hand pane listing the processes compiled).
11. Use the Expand/Reduce Height/Width view toolbar to expand or reduce the drawing canvas.

Figure 8 LTS Draw view of composed FLOW process

END OF TUTORIAL