Introduction

SMILEstands for ybolic nteractive OTOS xecution. It is a tool that allows one to execute a LOTOS specification, and to analyse the state/event space denoted by that specification. It offers a number of functionalities:

• Execution of arbitrary parts of the specification
• Single stepping
• Automatic symbolic execution
• Analysis of the abstract data type part of a specification
• Reports on executability of the abstract data type part
• Translation of behaviour expressions into finite state machines
• Execution towards a user-defined state
• Ignoring certain components of the specification while executing
• Verification of certain properties
• Programmable evaluation strategies and analysis techniques

This manual applies to SMILEversion 4.0. It is organized as follows: first, some terminology is introduced by describing a simple SMILE-session. Then the algorithms used in SMILEare explained in more detail in chapter 3. This allows the user to understand why certain operations take more time than others, and how (s)he may be able to change the specification such that execution is more efficient. Chapter 4 can be used as a reference manual, all commands are explained there. In chapter 5 we will describe how SMILEcan be programmed, and how new commands can be added to the tool. Finally, in chapter 6 it is shown how the tool can be customized for particular specifications or displays.

Throughout this manual, the following example specification will be used:

specification test[g] : noexit
library naturalnumber, boolean
endlib

type my_nat is naturalnumber
opns
  _-_                         : nat, nat                    -> nat
  1, 2, 3                     :                             -> nat
eqns ofsort nat
  forall  x, y : nat
  x - 0 = x;
  0 - x = 0;
  succ(x) - succ(y) = x - y;
  1 = succ(0);
  2 = succ(1);
  3 = succ(2);
endtype (* my_nat *)

behaviour 
count_to_3 [g] (0)
where
  process count_to_3[g](x : nat) : noexit:=
       [x lt 3] -> g!x ; count_to_3 [g] (x + 1) 
   []  [x gt 3] -> g!x ; count_to_3 [g] (x - 1)
   []  [x eq 3] -> g!x ; count_to_3 [g] (x)
  endproc (* count_to_3 *)
endspec (* test *)

This specification contains one process, which counts down (or up, depending on the value of the parameter) to 3, and, when it reaches 3, continues to output 3. It is clear that the transition system of this process consists of only one state (parameterised with the free variable ) and three transitions. This specification is available in the SMILE distribution, as file demo-smile.lot and demo-smile.cr. The .lot-file is the (human-readable) LOTOS file (displayed above), whereas the .cr-file is the pre-processed file that is generated by the static semantics checker, and read by SMILE.

In this manual teletype font is used for user input and tool output, and bold font is used for the names of commands (cf. the titles on the buttons or in the pulldown menus of the user interface).