Specification (4): Slime

Abstract: The document describes the requirement specification for the Java-Fortgeschrittenenpraktikum in the summer term 2002. It is available also as postscript or pdf. The requirement specification is being updated und refined during the semester according the the project's progress and the decisions taken.

1 Introduction

The document describes informally the functionality of Slime, a graphical tool for editing and analyzing SFCs (Sequential function charts modeling environment).

One crucial part of the implementation, around which most of the rest has been arranged, is the abstract syntax (cf. Section A).

The rest of the documents sketches the parts of the project, each implemented by one package of the project. Especially, we describe in first approximation

the functionality offered by each package, and
the functionality expected from other packages.

As we intend to start early with the integration, the required methods should be provided rather quickly without being (fully) implemented (i.e., as stubs). See also the time-line of the project.

We provide as starting point a first implementation of the abstract syntax (cf. Section A) and a small textual printer in the utilities package.

If from the perspective of a package, changes or extensions seem necessary or desirable as far as the abstract syntax is concerned, the wish should be uttered and justified as early as possible to all participants (and then potentially implemented by us or the requester, if everyone agrees).

2 Graphical user interface (Gui)

Responsible: Norbert Boeck

Slime is built from various components interacting with the user. There's an integrating top-level packages responsible for the following tasks:

Start: When invoking a Slime-session, a ``window'' appears which allows to activate the various sub-components of the system.
Dependency: Not all interactions are sensible all situations, for instance: a simulation can be started only on a syntactically correct program. The task is, to define the dependencies between the packages and implement them in the tool.
Session management: (2nd priority) It should be possible to save a session (opened windows, loaded files, chosen options ...). It should be possible to reload a saved session.

The user interface integrates all other packages. Thus, the one responsible for the GUI should be especially aware of inconsistencies between the packages and react upon detected violations.

Interfaces

With all other packages, cf. the corresponding description there.

3 Editor

Responsible: Andreas Niemann

The graphical editor for SFC's should support the following features:

construction: The editor must be able to build-up a SFC |perhaps using some templates. A proposal how an SFC could look like is shown in Figure 1.
save and load: It must be able to store and reload programs
select: Parts of an SFC must be selectable; this is needed for other actions
delete and copy: selected parts can be deleted and copied.
highlight: parts of the displayed SFC, especially steps and transitions, can be marked as highlighted.

Interfaces

With the Gui (Section 2), where the division of work between gui and editor should be discussed. Furthermore with the simulator (Section 5), concerning the highlighting.

An important interface (as for all other packages) is with the abstract syntax package. To support the graphical representation, the abstract syntax classes are equipped with coordinates, the meaning and the representation is to be discussed among editor and the graphical-placement-package.

4 Checks

Responsible: Thomas Richter, Karsten Stahl, Martin Steffen, all others too

Only syntactically correct systems can be meaningfully processed, in our case simulated. The task of this package is to check syntactical consistency. The task comprises the definition of what syntactical correctness means, i.e., what is guaranteed/checked by this group upon which the others can rely on.

Interface

With the gui. The gui has to take care that the packages for graph-placement, simulation, model-checking, code-generation ...are handed over only checked syntax. What needs not to be checked are ``graphical lapses'', e.g., whether the nodes are placed one over the other or similar things.

Contract

The checker assures well-typedness of expressions. The languages is rather simple and the abstract syntax of Section A only features integers and booleans and no scopes. We assume that the language is well-typed. The types of the operators is shown in Table 1.

operator/constant type(s)

true,false Bool

0,1,... Int

+,*,/ Int × Int ® Int

- Int × Int ® Int, Int®Int

<,>,£,³ Int ×Int ® Bool

=, ¹ Int×Int ® Bool, Bool×Bool®Bool

¬ Bool® Bool

Table 1: Types

Besides (and prior to) type-checking, the checker detects also various situations, when the programs is considered to be ill-formed. The checker guarantees, that

the sfc is non-null,
the (unique) initial step is contained in the set of steps,
all steps and transitions are non-null,
no step occurs twice (by name), and
no transition has a non-existing step as source or target (by name)

Note that test of non-nullness is not done for parts other than mentioned (for instance sap's etc.)

5 Simulator

Responsible: Immo Grabe

(Interactive) simulation of a programs is its step-wise execution such that the user can initate steps, choose among different alternatives ...and can follow the execution on the editor. The simulator realizes the semantics from Section B. The following points should be implemented

computation of a successor state
display of the taken step in the editor, using the highlight-function of the editor.

For an extended functionality, one could think of

interactive simulation, non-deterministic simulation
back-stepping
recording, storing, and replay of the taken steps

Interface

With the editor (highlighting).

6 Graphical layout

Responsible: Andreas Niemann

The editor allows to draw SFC's free-handedly. Besides that it should be possible to calculate coordinates of the transition system automatically. To this end, a graphical layout algorithm must be implemented, that takes care of displaying the SFC in a readable manner.

Interface

Gui and editor. The layouter may assume checked syntax. What the meaning of the coordinates is concerned, this must be agreed upon with the editor

7 Parser

Responsible: Marco Wendel

The tool should support a simple, non-graphical input language, to allow a textual program specification. The textual specification is without graphical information; this information can be calculated by the layout package.

This module parses the textual input and generates an abstract syntax tree. The implementation uses JLex und CUP.

The language is a simple C-oid language.

Interface

With the gui (Section 2), providing a method parse_file.

8 Utilities

Different pieces of code, not specifically attributed to any other package, but useful for more than one other package.

8.1 Pretty-Printer

Responsible: Karsten Stahl, Martin Steffen

A simple pretty-printer with tabulated ascii-output, primarily intended for diagnosis. It should be used for testing and debugging the other parts already during development.

Interface

The pretty-printer can used (and is supposed to be used) by everyone for debugging. The only interface that counts is the abstract syntax, which must be printable. The interface is partially implemented, for the usage, see utils.PpExample. Besides the print-for whole programs, the same methods is provided publicly also for other syntactic constructs to make them printable for diagnosis.

A Abstract syntax

Responsible: Karsten Stahl, Martin Steffen, and all others

The following extended BNF-notation specifies the abstract syntax as common intermediate data represenation for the project. Modulo some naming conventions (capitalization), the Java-implementation is straightforward. Each non-terminal is represented as a separate class. Alternatives, specified by |, are subclasses of the abstract class, to which they build the alternative. The entries of the middle collum constitute the fields of the classes. The constructors of the classes are conventionally fixed by the fields of the class (up to the order of the arguments.¹ The lists of the EBNF are implemented as java.lang.LinkedList. Graphical position information, relevant only for the editor and the layout group, is omitted in the EBNF.

                  SFC ::=  istep      : step
                           steps      : step list
                           transs     : transition list
                           actions    : action list
                           declist    : declaration list
                 step ::=  name       : string
                           actions    : stepaction list
           stepaction ::=  qualifier  : action_qualifier
                           a_name     : string
               action ::=  a_name     : string
                           sap        : stmt list  (* simple assignment program *)
                stmt  ::=               skip
                       |                assign
               assign ::=  var        : variable
                           val        : expr
             variable ::=  name       : string
                    isinput    : boolean
      isoutput   : boolean
                           type       : type
     action_qualifier ::=  Nqual                    (* may be extended *)

           transition ::=  source     : step list
                           guard      : expr
                           target     : step list

          declaration ::=  var        : variable
                           type       : type
                           val        : constval

           expr       ::=               b_expr
                       |                u_expr
                       |                constval
                       |                variable
         b_expr       ::=  left_expr  : expr
                           right_expr : expr
                           op         : operand
                           type       : type
         u_expr       ::=  sub_expr   : expr
                           op         : operand             
                           type       : type
           operand    ::=               PLUS | MINUS | TIMES | DIV  (* operand as *)
                       |                AND | OR | NEG              (* const. in expr *)
                       |                LESS | GREATER | LEQ | GEQ | EQ | NEQ
            constval  ::=               ...| -2 | -1 | 0 | 1 | ... | true | false
            type      ::=               inttype
                       |                booltype

B Semantics

The section describes the semantics of Sequential Function Charts (SFC's), as (to be) realized in the tool Slime. The semantics is defined for successfully checked SFC's (cf. Section 4); unchecked SFC's don't have a meaning. Especially, the simulator, which realizes the semantics, can assume checked syntax.

B.1 Informal semantics

We start informally and explain the semantics with the help of the example from Figure 1.

Figure 1: SFC

The SFC's consist of nodes, called steps, to which actions are associated, and transitions between steps, decorated with boolean guards. Always, one ore more of the steps are active and the actions associate with this active steps are executed within one cycle. The transition from s₁ to both s₂ and s₃ (with double horizontal line) is a parallel branching: if this transition is taken, s₁ is deactivated and both s₂ and s₃ get activated. Since this is one transition, and each transition has exactly one guard, the guard is labeled on the upper part of the transition.

In contrast, the ``branching'' from s₃ to s₅ and s₆ is no real branching, it is just an abbreviation for two different transitions: one leading from s₃ to s₅, the other leading from s₃ to s₆. Therefore, the guards are labeled to the lower parts, since each transition has exactly one guard.

The topmost step (marked specifically) is initial. The ''N'' on the left-hand side of the actions is a qualifier, stating that the action is to be executed in each cycle in which the step is active. There are other qualifiers, too, but we will neglect them unless we find good reasons for taking them into account.

The behavior of an SFC during one cycle is as follows.

Reading inputs from the environment.
Executing the actions from the active steps. This is done in two steps as follows:
1. Assemble all active actions (as a set, so each action appears at most one time).
2. Execute the assembled actions in an arbitrary order.
Evaluate the guards.²
Take transition(s) (if possible).
Write outputs.

Each transition is equipped by a guard, i.e., a boolean expression. A transition can be taken only if the guard evaluates to true, and, if all the source steps of the transition are active. We do not enforce the target steps to be disabled.³

If more than one step is active in a parallel branch, the execution of the corresponding action is chosen non-deterministically. This means, they can be executed in an arbitrary order (interleaving semantics).

There is a second source of non-determinism, namely the set of actions associated to the active steps. These actions will be first assembled, and then non-deterministically executed. Each action will only be executed once, even if an action is associated to two different active steps.

Consequently, a program may have a number of different execution runs. The simulator could realize the different runs in that it asks the user, in which order the actions should be performed, and which transition should be taken if several are possible. An alternative is, to determine the order by a random generator.

The transition from s₄ and s₇ to s₈ closes the parallel branch again. Such a transition can be taken only, if all source steps are active. In other words, this transition can be taken if it's guard evaluates to true and furthermore both s₄ and s₇ are active.

1: There are exceptions to this rule, notably for the (Slime-)types in the expressions. The type-fields are not included in the constructors. The corresponding fields will be set later.
2: If one does not allow propositions like step_1_is_active, taking a transition can only disable another transition by deactivating its source steps, the guards will remain true.
3: If during a run a transition is taking which enters an already active step, the SFC is either built using a strange programming style or there is a mistake. But in principle, there seems to be no reason to enforce target steps to be inactive.

This document was translated from L^AT_EX by H^EV^EA.