proto_seq User's Guide

Table of Contents
  1. proto_seq User's Guide
    1. Starting the Tool
    2. Creating a New Specification
    3. Opening an Old Specification
    4. Saving a Specification
    5. Saving a Specification Under a New Name
    6. Exporting the Specification to HTML
    7. Closing the Specification
    8. Quitting
    9. Tab Contents
      1. Tab Data Table Contents and Functionality
        1. Creation of New Data Items
        2. Editing of Old Data Items
        3. Sorting of the Data Items
        4. Filtering of the Data Items
        5. Cutting of Data Items
        6. Pasting of Data Items
        7. Copying of Data Items
        8. Deleting of Data Items
      2. Tab Editing Area
      3. Tab Filtering Area
    10. Specific Tab Contents
      1. Requirements Tab
      2. System Boundary Tab
      3. Stimuli Tab
      4. Outputs Tab
      5. Named Responses Tab
      6. Predicates Tab
      7. Sequence Enumeration Tab
      8. State Variable Definition Tab
      9. Canonical Sequence Analysis Tab
    11. Copyright
This document provides some brief instructions on using the prototype sequence enumeration tool. The tool runs under Linux, Solaris, and Windows XP.

Starting the Tool

Under Linx/Solaris, enter the command proto_seq from the shell prompt.
Under Windows XP, double click on the proto_seq_win32 icon.
After starting the tool you will be presented with the tool's GUI with no specification loaded. At this point you may create a new specification or load a previously created specification.

Creating a New Specification

To create a new specification, select the File::New menu item. This will cause a file browser dialog to be displayed in which you must select the name of the file in which to save the specification. After selecting a file in which to save the specification, the GUI will display a set of empty tabs. The tab contents will be discussed later in this document.

Opening an Old Specification

To open a previously created specification, select the File::Open menu item. This will cause a file browser dialog to be displayed in which you must select the name of the file to open. After selecting the file to open, the GUI will display a set of tabs containing the contents of the opened specification. The tab contents will be discussed later in this document.

Saving a Specification

To save the current specification, select the File::Save menu item.

Saving a Specification Under a New Name

To save the current specification in a new file, select the File::SaveAs menu item. You will be presented with a file dialog in which you may select the new file in which to save the specification.

Exporting the Specification to HTML

To export the specification to HTML, select the File::Export menu item. Given a specification saved in file X.pse, the HTML will be exported to file X.pse.html.

Closing the Specification

To close the current specification, select the File::Close menu item.

Quitting

To exit the tool, select the File::Exit menu item.

Tab Contents

The proto_seq tool uses a tabbed interface, where each tab is used to display and edit the different pieces of information that make up a specification. Currently there are seven different tabs. The contents of the tabs are as follows:
Tab Name
 Description
Requirements
 The system requirements are defined on this tab.
System Boundary
 The interfaces to which outputs may be sent and from which stimuli may be received are defined on this tab.
Stimuli
 The system stimuli are defined on this tab.
Outputs
 The system outputs (which will be used to create the responses in the enumeration) are defined on this tab.
Named Responses
 Groupings of outputs that are used several times as responses can be referenced as a common named response. These named responses are defined on this tab.
Predicates
 Boolean predicate functions of the form S*->{true, false} may be defined on this tab. The defined predicates may be used when performing the sequence enumeration.
Sequence Enumeration
 The actual sequence enumeration is performed on this tab.
State Variable Definition
 The state variables and their possible values are defined on this tab.
Canonical Sequence Analysis
 Using the state variables defined on the state variable definition tab, the canonical sequence analysis is performed on this tab.

Each tab has the same basic structure, with basic functionality common to each tab. Each tab is composed of three different components.

Tab Data Table Contents and Functionality

The particular data being displayed and edited on a tab is displayed in a table.  The various fields of  the data items being edited are displayed in different columns of the table. The data table supports several different operations:

Creation of New Data Items

To add a new data item to the specification, double click on the blank row at the bottom of the table. This will shift the interface focus down to the editing area at the bottom of the tab. A new data item may then be defined in the editing area. The editing area will be discussed later. After completing the creation of a new data item in the editing area, the editing area will be cleared, allowing a new item to be defined.

Editing of Old Data Items

To edit a previously created item in the specification, double click on the row containing the data item to be edited. This will shift the interface focus down to the editing area at the bottom of the tab. The old data item may then be edited in the editing area. The editing area will be discussed later. Focus will return to the data item table after editing an item.

Sorting of the Data Items

The table may be sorted based on the contents of the fields of the data items. To sort the table in ascending order based on the contents of a field of interest, single click on the column header containing the field of interest. To sort the table in descending order based on the contents of that same field of interest single click on the same column header a second time.

Filtering of the Data Items

The contents of the table may be filtered based on the contents of the fields of the data items. The filtering area is used to control the filtering of the table. The filtering area will be discussed later.

Cutting of Data Items

A data item may be cut from the specification. To cut a data item from the specification and store the data item in the paste buffer, select the data item to be cut in the table, and select the Edit::Cut menu choice. The item will be removed from the table and placed in the paste buffer.

Pasting of Data Items

A data item may be pasted into the specification by selecting the Edit::Paste menu choice. The edit area will be populated with the item in the paste buffer and interface focus will be shifted down to the editing area, allowing the user to edit the pasted item prior to its inclusion in the specification.

Copying of Data Items

To add an item to the paste buffer without removing it from the table, select the item to copy in the table and then choose the Edit::Copy menu item. The selected item will be added to the paste buffer.

Deleting of Data Items

To remove an item from the specification without adding it to the paste buffer. select the item to be deleted in the table and then choose the Edit::Delete menu item. The selected item will be removed from the table.

Tab Editing Area

The tab editing area is used to create new data items and edit old data items. The editing area is only enabled when editing an old data item or creating a new data item. Note that when an item is being edited on a tab no edits are allowed on other tabs, i.e., only one editing session is allowed at a time. An editing field is displayed for each field in the data item.

To edit the contents of a field in a data item, simply type in its edit field.

To cancel out of the current edit, hit the Cancel button in the editing area (or type the escape key).

To commit the current edit to the specification, hit the Finish button in the editing area.

The tab key transfers focus between items in the editing area.

The space bar may be used to press a button (when the button has focus).

Tab Filtering Area

The tab filtering area is used to specify the criteria for filtering the contents of the data table. Only rows in the table that match the filtering criteria will be displayed. Each field in a data item has a corresponding entry in the filtering area. The filtering criteria for a data item field are entered in its corresponding filtering area entry. The filtering criteria that must be matched by a field are specified with Perl-style regular expressions. At its simplest, you may filter the table so that all displayed rows must have a field matching some specific content X by simply typing in X as the filter criteria for the field of interest. If a filter criteria field is blank that table will not be filtered based on the contents of that field.

To filter the table based on the current filtering criteria, check the Filtering On/Off checkbox.

To stop filtering the table based on the current filtering criteria, uncheck the Filtering On/Off checkbox.

To clear out the current filtering criteria entries, hit the Clear button.

Specific Tab Contents

The specific contents of the different tabs are listed in the following sections.

Requirements Tab

The fields of a requirement are:

System Boundary Tab

The fields of an interface are:

Stimuli Tab

The fields of a stimulus are:

Outputs Tab

The fields of an output are:

Named Responses Tab

The fields of a named response are:

Predicates Tab

The fields of a predicate are:

Sequence Enumeration Tab

The fields of a sequence enumeration are:
To extend the unextended canonical sequences in the enumeration, selected the Enumeration::Extend menu item.

To display only the canonical sequences, set the filtering criteria to:
This will display only the legal sequences that have no equivalence, i.e., the canonical sequences.

State Variable Definition Tab

The fields of the state variable definition tab are:
The state variables defined on the state variable definition tab are used to perform the canonical sequence mapping on the canonical sequence analysis tab. The canonical sequence mapping tab is updated accordingly as state variables are added, changed, or deleted.

Every state variable will contain by default the value "-----", which corresponds to a wild-card, or "don't care" value. Setting a variable to this value in the state data vector mapped to a canonical sequence indicates that the state variable will be ignored when deciding whether the system is in the state corresponding to the canonical sequence of interest.

Canonical Sequence Analysis Tab

The fields of the canonical sequence analysis tab are:
. . .
Once the sequence enumeration has been completed the canonical sequences will be used to populate the table on the canonical sequence analysis tab. Note that changes to the sequence enumeration that cause the enumeration to no longer be complete will cause the canonical sequence analysis (CSA) to be destroyed. Each row in the CSA table contains the state data vector mapped to a corresponding canonical sequence. There will be one column in the table for each state variable defined on the state variable definition tab. Initially every state variable value cell will contain a value of "Not Set" indicating that the state data vector for the corrresponding canonical sequence has not yet been defined.

On the bottom of the CSA tab are two check boxes that indicate the status of the CSA.

Once the CSA is fully defined, i.e., there are no more "Not Set" values in the table, it may be checked. The CSA is checked by selecting the Enumeration::Check Canonical Sequence Analysis menu item. The tool will check the CSA for:

Copyright

Copyright (c) 2005
Software Quality Research Laboratory
University of Tennessee
All rights reserved.

http://www.cs.utk.edu/sqrl