OoasTools

\documentclass[11pt]{scrartcl}

\usepackage{cancel}

\usepackage{listings}

\usepackage{xspace}

\usepackage{longtable}

\usepackage{graphicx}

\usepackage{url}

\newcommand{\doodblock}{{\bf do} {\bf od}-block \xspace}

\newcommand{\doodblocks}{{\bf do} {\bf od}-blocks \xspace}

\lstdefinelanguage{ooa} {

  morekeywords={autocons, types, methods, do, obs, action, end, ctr, requires, od, true, and,

     signal, after, false, actions, var, |[, ]|, [], public, of, len,

     //, hd, tl, system},

   sensitive=true,

   morecomment=[s]{/*}{*/},

   showspaces=false,

   showstringspaces=false,

   numbers=left,

   numbersep=5pt,

   numberstyle=\tiny,

   tabsize=2,

   escapeinside={@}{@},

   framexleftmargin=9pt,

  }

\begin{document}

\begin{titlepage}

\begin{center}

\vspace*{15mm}

{\Large TECHNICAL REPORT}

\vspace{10mm}

{\large IST-MBT-2012-01}

\vspace{15mm}

{\huge \bf The Argos Manual}

\vspace{5mm}

{\Large for Argos version: 0.39}

\vspace{15mm}

{\Large Stefan Tiran}

\vspace{5mm}

{\large stiran@ist.tugraz.at}

\vspace{15mm}

{\large March 2012} % 13.03.2012

\vspace{10mm}

{\large

Institute for Software Technology (IST)\\

Graz University of Technology\\

A-8010 Graz, Austria\\}

\end{center}

\end{titlepage}

%\title{The Argos Manual}

%\author{Stefan Tiran}

%\subtitle{for Argos version: 0.39}

%\maketitle

\newpage

\tableofcontents

\listoffigures

\section{Introduction}

Argos is a compiler for Object-Oriented Action Systems (OOAS). It has been developed

by Willibald Krenn from Graz University of Technology within the MOGENTES project.

Its main target is producing Action Systems in the proprietary format that \emph{Ulysses}

can process. \emph{Ulysses} is an ioco-checker written by Harald Brandl also within the

MOGENTES project.

\section{How To Run Argos}

Argos is a .NET based command line program. To run it you need either

the .NET Framework or mono (\url{http://www.mono-project.com}).

\subsection{Program Invocation}

Since Argos is a command line tool you need to open a command line prompt

(using Windows) resp. a shell (using a UNIX-like system).

When using Windows change to the Argos directory and simply run argos.exe:

\texttt{

c:\textbackslash Argos \textbackslash > argos}

When using a UNIX-like system run mono with argos.exe as parameter:

\texttt{

\$ mono argos.exe}

In both cases one should now see this welcome screen:

\begin{verbatim}

          >> Mogentes OO-Action System Parser <<

          Version: 0.39 (16471)

  Grammar-Version: 0.06

Usage:    argos [options] <oo-actionsystem-file>

Options:

     -o<name>   ... write output to file <name> (overwrites!)

     -n<name>   ... use namespace <name> (default: as)

     -d<depth>  ... set max. search depth (default: 35)

     -q         ... "quiet" mode: doesn't print Warnings to console

     -a         ... create pseudo-action system code

     -p         ... create prolog code

     -c         ... create CADP implicit LTS

\end{verbatim}

\subsection{Options and Arguments}

As can be seen in the welcome screen for translating Action Systems the

last parameter has to be the OOAS-File you want to convert, every other

options has to come before.

If no other option is given, Argos will translate the given OOAS-File to

C\#-Pseudo-Code and print it out on the screen. Since this most probably

won't be something you will find extremely useful, you should at least

specify an output-file and the desired language.

For specifying the output-file use option \texttt{-o} followed by the

file name resp. the relative path of the file you want to create. There

should be NO space between \texttt{-o} and the file name!

For specifying the language include option \texttt{-c} for creating

C-Code for the CADP-Toolbox resp. option \texttt{-p} for creating

Prolog-Code for use with the Ulysses tool.

When creating Prolog-Code the following options are important:

\begin{itemize}

\item[-n] With this option one can specify the namespace within the Prolog-File;

	the only meaningful use of this option is \texttt{-nasm} for letting

	the Ulysses tool know, that this file represents the mutant rather

	then the original file.

\item[-d] With this option one can specify the max. depth, to which the Ulysses

	tool will search for differences. Please note that this option has

	to be followed by a number WITHOUT a space before! The default value

	is 35, so leaving out this option is equivalent to writing

	\texttt{-d35}.

\subsection{Examples}

To illustrate the use of the options, we hereby provide the following examples:

\begin{itemize}

\item Translate an original OOAS specification \texttt{original.ooas} to a Prolog

	file \texttt{original.pl} for the Ulysses tool with max. search depth

	42:

	\begin{verbatim} argos.exe -p -d42 -ooriginal.pl original.ooas \end{verbatim}

\item Translate a mutated OOAS specification \texttt{mutant.ooas} to a Prolog

	file \texttt{mutant.pl} for the Ulysses tool with max. search depth

	42:

	\begin{verbatim} argos.exe -p -d42 -nasm -omutant.pl mutant.ooas \end{verbatim}

\item Translate OOAS specification \texttt{original.ooas} to a C file 

	\texttt{original.c} for the use with the CADP toolbox:

	\begin{verbatim} argos.exe -c -ooriginal.c original.ooas \end{verbatim}

\end{itemize}

\end{itemize} 

\section{OOAS Language}

The Argos tool will only work if the given file is well formed according

to the language that is described in this section. The language is based

on the language proposed in \cite{Bonsangue1998} but only a subset of features

is actually implemented.

\subsection{Base structure}

To illustrate the base structure of an OOAS file let us consider the simple

Hello World program in Figure \ref{HelloWorld}.

\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

  Greeter = autocons system

  |[

  var

        done : bool = false

  actions

        obs HelloWorld = requires done = false :

                done := true

                end

  do

        HelloWorld

  od

  ]|

system

        Greeter

 \end{lstlisting}

\caption{HelloWorld}

\label{HelloWorld}

\end{figure}

Every OOAS consists of two different regions: The type definition block and

the system assembling block. In the HelloWorld system the type definition block

consists of Lines 1 - 13 and the system assembling consists of Lines 14 and 15.

Let us now discuss the system Line by Line:

Line 1 just consists of the keyword \texttt{types} stating that here begins

the type definition block.

In Line 2 a class called \texttt{Greeter} is defined. The keyword

\texttt{autocons} states that one instance of the class will automatically

be created at system start. This instance is called the ``root object''.

The symbols in Line 3 and 13 state the begin and the end of the class

definition.

In Lines 4 and 5 there is  a variable definition

block. Even though this block is not formally necessary for Argos to compile

a file, Argos will not create a valid prolog file if this block is missing.

In Lines 6 - 9 there is the action block consisting of the action

\texttt{HelloWorld}. The keyword \texttt{obs} states that this action is

\emph{observable} rather then \emph{controllable} (keyword: \texttt{ctr}) or

internal (no keyword).

The keyword \texttt{requires} states the beginning of the guard, which enables

the action.

The body of this action consists of Lines 8 and 9. Line 8 contains an

assignment, the keyword \texttt{end} in Line 9 marks the end of the action.

Lines 10 - 12 contains the so-called \doodblock. The \doodblock is

described in Section \ref{dood}.

As already mentioned, Lines 14 + 15 contain the system assembling block. In this

block the system is composed of its classes. Since this example system only

contains of one class, the block is quite simple and needs no further

explanation.

\subsection{The Type Definition Block}

The type definition block has two purposes: As we have already seen it can be

used for defining the classes of which the system consists of. However it

can also be used for creating named types which is similar to the use of

\texttt{type-def} in C.

The latter use is quite important as OOAS has a very strict typing system.

For example if you want to define a variable as integer, you also have to

define the range of the values. This is due to the fact that too wide ranges

can lead to enormous efficiency problems when simulating the model.

\subsubsection{Defining Integer Types}

Integer types can be defined by the lower and upper range.

Consider you want to define a type \texttt{MyInt} that can contain values

between 0 and 31, then you can write

\begin{verbatim}

  MyInt = int [0..31];

\end{verbatim}

Please note that the semicolon has to be placed if and only if this is not

the last definition.

\subsubsection{Defining Enum Types}

Enums can be defined by enumerating the possible values and optionally assigning them

integer values. If integer values are explicitly assigned, enum types can be casted to

integer types.

Consider you want to define an enum type \texttt{Color} that can contain the

values \texttt{red}, \texttt{green}, \texttt{blue}, \texttt{yellow} and \texttt{black},

then you can write:

\begin{verbatim}

  Color = {red, green, blue, yellow, black};

\end{verbatim}

The possibility to explicitly assign integer values is especially useful when

dealing with equivalent classes of integers. Consider you need an integer type

that can only contain small number of different values but these values define

a range with "holes" rather then a complete one.

So in case you need a type that can hold the values 1, 42 and 1337 you can write

\begin{verbatim}

    CoolValueSet = {CoolValue1 = 1, CoolValue2 = 42, CoolValue3 = 1337};

\end{verbatim}

\subsubsection{Defining Complex Types (Lists, Tuples)}

Additional to the former so-called simple types the OOAS language also

supports so-called complex types. These are: lists and tuples.

A list is defined by the number and the type of its elements.

An example for the former variant would be:

\begin{verbatim}

  MyList = list [42] of char;

\end{verbatim}

A tuple is defined by the types of its elements. Unlike a list the types can

differ among the different elements.

An example would be:

\begin{verbatim}

  MyTuple = (MyInt, SmallInt);

\end{verbatim}

Even though maps and qualitative reasoning types would be specified by the

OOAS language, Argos does not support them yet.

\subsubsection{Defining Classes}

In the OOAS language the definition of a class (ooActionSystem) does not differ

from the definition of any other type.

\subsection{Structure of Classes}

\subsubsection{Inheritance}

As common in Object-Oriented languages, classes can be derived from other classes

and inherit their behavior.

A sample class \texttt{Desc} inheriting from a class \texttt{base} could look like this:

\begin{verbatim}

  Desc = system (base)

  |[

  ]|

\end{verbatim}

\subsubsection{Defining Variables (Attributes)}

\label{Variables}

Variables store the information of the state of an object. An alternative name

of variables often used in error messages is ``attributes''. Variables can be

static and have to be initialized with a valid value. For objects there is a

predefined object \texttt{nil}. There is also a self-reference called

\texttt{self}.

The definition of a variable can look like this:

\begin{verbatim}

        done : bool = false;

\end{verbatim}

Please note that the semicolon has to be placed if and only if this is not

the last definition.

\subsubsection{Creating Objects}

The only place where an object can be created is in the variable definition block.

Line 5 in Figure \ref{object} demonstrates how a variable with the name

\texttt{myOtherClassObject} can be initialized with an object with the name

\texttt{OtherClassObject} of a class \texttt{OtherClass}.

For details on the System Assembling Block (Lines 23 and 24) see Section

\ref{SAB}.

\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

  RootClass = autocons system

  |[

  var

        myOtherClassObject : OtherClass = new(OtherClass,"OtherClassObject") ;

        initialized : bool = false

  actions

        obs init = requires initialized = false : initialized := true end

  do

        init ()

  od

  ]| ;

  OtherClass = system

  |[

  var

        initialized : bool = false

  actions

        obs init = requires initialized = false : initialized := true end

  do

        init ()

  od

  ]|

system

        RootClass [] OtherClass

 \end{lstlisting}

\caption{Creating an object}

\label{object}

\end{figure}

\subsubsection{Defining Methods}

Methods can be used for defining subroutines. Methods can have parameters,

variables and a return value. Methods can be called from actions and

from other methods, but not recursively - neither directly nor indirectly.

The body of a method isn't any different from the body of an action

and therefore described in Section \ref{Actions}.

A sample method, that returns the bigger of two values could look like this:

\begin{verbatim}

  maxValue(a : MyInt, b : MyInt) : MyInt =

    result := if (a > b) then a else b end

  end;

\end{verbatim}

Returning a value is done by assigning it to the variable result.

For a list of possible expressions we refer to Section \ref{Expressions}.

One important aspect of methods is their pureness. A method is pure

iff there is no assignment to a variable other than \texttt{result}.

This property is checked on compile

time. Only if a method is pure it can be used in a guard or in a list

comprehension.

\subsubsection{Defining Actions}

\label{Actions}

Named actions consist of an optional parameter list, a variable definition

block and a body but they lack a return value. Named actions can only be

called in the so-called \doodblock.

A named action can be controllable (keyword \texttt{ctr}),

observable (keyword \texttt{obs}) or internal (no keyword). 

The definition of local variables does not differ from any

other variable definition so we refer to Section \ref{Variables}.

The body of a named action can consist of one or more basic actions.

Every action has a guard which ``enables'' it. The general form of a guard

is \texttt{requires p : $S_1$ end} where p is the condition

and $S_1$ is the action. The condition can be any expression that doesn't

involve the calling of a non-pure method or a non-pure assignment.

For further details about expressions see Section \ref{Expressions}!

Basic actions can be the built-in action \texttt{skip},

single or multiple assignment or a sequential composition of two other actions.

For details on the composition we refer to Section \ref{Composition}.

The built-in action \texttt{skip} doesn't do anything at all.

Sometimes this is called \emph{identity assignment}.

Single assignment has the simple form \texttt{v := e} where

v is a variable and e is an expression.

However you can also assign multiple expressions to multiple

variables by separating them with commas.

So if \texttt{done} and \texttt{multi} are both variables of

type \texttt{bool}, then you can write:

\begin{verbatim}

                done, multi := true, true

\end{verbatim}

\subsection{Composition}

\label{Composition}

\subsubsection{Sequential Composition}

The easiest way of composing two actions is the sequential

composition. It has the general form \texttt{A ; B} where

A and B are both actions and has the meaning that iff

A and B are \emph{enabled}, first action A is executed and then

action B is executed. Note that it is not necessary for B

to be enabled before A. It is also possible that B becomes

enabled because of A.

Please note that despite of the

apparent resemblance with the semicolon as marker of the

end of a line in many imperative programming languages

there are two very important differences:

The first difference is that since it is a composition operator,

there must not be a semicolon after the last action. This

difference seems to be more on a syntactical level, but should

also warn about the other very important difference:

The second difference is that since actions have guards, no

action of a sequence block is executed, if a single action is

not enabled. This also means that an action can hinder actions

to be executed, which were called \emph{before}!

\subsubsection{Non-deterministic Choice}

The counterpart of the ``sequential composition'' is the so

called ``non-deterministic choice''.

The general form of a non-deterministic choice is \texttt{ A [] B }

where A and B are both actions and the meaning is that either

A or B is executed. However an action can only be chosen if it

is enabled. According to the theory of action systems an action has to be

chosen if it is aborting. However there is no abort feature implemented yet.

\subsubsection{Prioritizing Composition}

The ``prioritizing composition'' is rather an abbreviation

than an actual new type of composition.

The general form is \texttt{ A // B } and it means that if A

is enabled, it is chosen and otherwise B is chosen.

\subsection{Expressions}

\label{Expressions}

Expressions can be evaluated and their values can be assigned to variables.

\subsubsection{Conditional Assignment}

Conditional Assignments are expressions. They can not be used for branching

the control sequence. Branching the control sequence has to be done by using

guards and non-deterministic choice.

A conditional assignment can look like this:

\begin{verbatim}

  c := if (a > b) then a else b end

\end{verbatim}

\subsubsection{Fold}

For the purpose of iterating through a list in OOAS \emph{fold} is used.

\emph{Fold} is a higher-order function well known from the functional

programming paradigm.

In the OOAS language both \emph{right fold} and \emph{left fold} are

defined. The symbol for the former is \texttt{:>:} whereas the symbol

for the latter is \texttt{:<:}. However in Argos only \emph{right fold} is

implemented.

The general form of a fold expression is \texttt{method :: (init\_expression) :>:  (list\_\\expression)}

where \texttt{method} is the name of the method, \texttt{init\_expression} is the value for the last

parameter of the method for the first call. For any other call the result of the former call is used instead.

Finally \texttt{list\_expression} is the expression that evaluates to the list to be iterated.

Figure \ref{Sum} shows how to define a method \texttt{Sum}

using a method \texttt{Add} and the \emph{fold} operator.

\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

  MyInt = int [0..42];

  SmallInt = int [0..3];

  MyTuple = (MyInt, SmallInt);

  Sum = autocons system

  |[

  var

        my_list : list [4] of SmallInt = [5,5,5,5]

  methods

    add(a: MyInt, b: SmallInt) : MyInt =

        requires true :

          result := a + b

        end

    end ;

    sum(Xs : list [4] of SmallInt) : MyInt =

        requires true  :

          result := add :: (0) :>: (Xs)

        end

    end

  actions

        obs Sum(a: MyInt) =

                requires a = sum(my_list) :

                        skip

                end

  do

        var A : MyInt : Sum(A)

  od

  ]|

system

        Sum

 \end{lstlisting}

\caption{Defining sum of all list elements using the fold meta function}

\label{Sum}

\end{figure}

\subsubsection{Quantifier Expressions}

The OOAS language allows to use the quantifiers \texttt{forall} and

\texttt{exists}. The resulting expressions will evaluate to Boolean

values. The general form is \texttt{(quantifier : Type  : (logical sentence))}.

For example an existential quantification can look like this:

\texttt{(exists i : LengthInt : (primes[i] = a))}.

\subsubsection{List Comprehension}

The OOAS language allows to construct new list expressions based on existing lists

by using the set-builder notation. These expressions can be assigned to list

variables at any time after the initialization, but not in the declaration.

The general form of a list comprehension is:

\texttt{list := [x | var x : Type \& (condition)]}, where \texttt{Type} is the type

of the list elements and \texttt{condition} is a logical sentence which determines

whether a value should be inserted to the list.

The example in Figure \ref{Prime} illustrates both \emph{Quantifier Expressions}

and \emph{List Comprehension} by computing prime numbers.

\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

  MyInt = int [2..100];

  LengthInt = int [0..40];

  Primes = autocons system

  |[

  var

        initialized : bool = false ;

        primes : list [ 40 ] of MyInt = [3]

  actions

    obs init = requires initialized = false :

      primes := [ x | var x: MyInt & (forall tmp : MyInt : 

            (tmp < x => (x mod tmp <> 0 )))  ] ;

      initialized := true end;

    obs Prime(a: MyInt) =

      requires (exists i : LengthInt : (primes[i] = a)) :

        skip

      end

  do

        init() // var A : MyInt : Prime(A)

  od

  ]|

system

        Primes

 \end{lstlisting}

\caption{Prime number calculation}

\label{Prime}

\end{figure}

\subsubsection{Tuple Expressions}

The general form of an expression that evaluates to a tuple is:

\begin{verbatim}

	TupleType(v_1,...,v_n)

\end{verbatim}

where TupleType is the type of the tuple and v\_1,...,v\_n are the values.

An example for using Tuples can be found in Figure \ref{Tuple}

\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

  MyInt = int [0..42] ;

  MyTuple = (MyInt, MyInt) ;

  TupleDemo = autocons system

  |[

  var

        theTuple : MyTuple = MyTuple(1,1)

  actions

        ctr change1 = requires theTuple = MyTuple(1,1) :

                theTuple := MyTuple(1,2)

                end ;

        ctr change2 = requires theTuple[1] = 2 :

                theTuple := MyTuple(1,3)

                end

  do

        change1 [] change2

  od

  ]|

system

        TupleDemo

\end{lstlisting}

\caption{Tuple Example}

\label{Tuple}

\end{figure}

\subsubsection{Access Expressions}

\emph{Access Expression} is the general term for the access of elements

in a list or tuple, call of method or access to an attribute of an object.

Accessing elements of a list is done by using the index operator \texttt{[]}

well known from accessing arrays in imperative languages like C.

The index starts with 0.

The index operator \texttt{[]} can also be used to access a specific element of

a tuple. This feature is illustrated in the guard of action \texttt{change2} in

Figure \ref{Tuple}. However this feature is not implemented in the left hand

side of an assignment, e. g. it is not possible to write \texttt{theTuple[0] := 1}.

\subsubsection{Cast Expressions}

When dealing with a class hierarchy it is possibly to use an object of a

sub class instead of an object of its super class. This is called \emph{upcast}

and done implicitly in most contexts. However, when concatenating two

lists it has to be done explicitly using the operator \texttt{as} as illustrated

in Line 10 in Figure \ref{Cast}.

\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

  Class1 = autocons system

  |[

  var

        O2 : Class2 = new (Class2);

        O3 : Class3 = new (Class3);

        OL : list[2] of Class2 = [nil]

  actions

        ctr fill = requires true :

                OL := [O2]^[O3 as Class2]

                end

  do

        fill

  od

  ]| ;

  Class2 = system

  |[

  ]| ;

  Class3 = system (Class2)

  |[

  ]|

system

        Class1

\end{lstlisting}

\caption{Cast Example}

\label{Cast}

\end{figure}

\subsection{Operators}

\subsubsection{Numeric Operators}

The numeric operators are \texttt{+} for adding two numbers of an integer or

float type, \texttt{-} for subtracting, \texttt{*} for multiplying. The operator

for the division of two numbers of a float type is \texttt{/}. For the division

of two numbers of an integer type there are operators \texttt{div} for the

quotient and \texttt{mod} for the remainder.

\subsubsection{Logical Operators} 

The logical operators are inspired by VDM and written \texttt{and} for logical

and, \texttt{or} for logical or, \texttt{not} for negation, \texttt{=>} for

implication, and \texttt{<=>} for bi-implication.

\subsubsection{Comparison Operators}

For comparing two values of the same type there are \texttt{=} for equality

and \texttt{<>} for inequality.

Values of integer and float types can also be compared with \texttt{>} for

greater, \texttt{>=} for greater or equal, \texttt{<} for less, and \texttt{<=}

for less or equal.

\subsubsection{List Operators (Head, Tail, Length, Concatenation)}

The OOAS language provides several basic list operators that make it

easy to use lists.

The first operator is \texttt{hd} which is short for \emph{head}. This

operator returns the first element of a list. Therefore if \texttt{my\_list}

is a list, then \texttt{hd my\_list} is equivalent to \texttt{my\_list[0]}.

The counterpart to \emph{head} is \emph{tail}, which returns the list without

the first element. In OOAS the operator token is \texttt{tl}. So if you want

to remove the first element from a list \texttt{my\_stack} you can write

\texttt{my\_stack := tl my\_stack}.

The next important operation is determining how many elements are currently

in a list, which is the so-called \emph{length} of a list. In OOAS this

operator is written \texttt{len}. For example if an action should only be

enabled if there are less than 10 elements in the list \texttt{my\_stack} you

can write \texttt{requires len my\_stack < 10}.

The last operation is creating a list that contains all the elements of two

given lists, which is called \emph{concatenation}. The operator is written

\texttt{\^}. If for instance you want to append an element \texttt{a} to

a list \texttt{my\_stack}, you can write

\begin{verbatim}

my_stack := [a] ^ my_stack

\end{verbatim}

The example in Figure \ref{Stack} illustrates how these operators can be used

to build a stack.

\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

  SmallInt = int [0..3];

  Stack = autocons system

  |[

  var

        my_stack : list [10] of SmallInt = [0]

  actions

        obs top (a : SmallInt) = requires (a = hd my_stack) :

                skip

                end ;

        obs pop = requires (len my_stack > 0) :

                my_stack := tl my_stack

                end;

        obs push (a : SmallInt) = requires len my_stack < 10 :

                my_stack := [a] ^ my_stack

                end

  do

        var A : SmallInt : push(A) []  pop() [] var B : SmallInt : top(B)

  od

  ]|

system

  Stack

\end{lstlisting}

\caption{Stack}

\label{Stack}

\end{figure}

\subsection{The Dood Block}

\label{dood}

The actual behavior of an action system is defined in the so-called \doodblock.

The \doodblock was inspired by Dijkstra's guarded iteration statement. The

canonical form of a \doodblock is to list all named actions of the class

and connect them using the \texttt{[]} operator. In this case in each iteration

an action is available iff its guard evaluates to \texttt{true} and the system

terminates iff no action is enabled.

However, in OOAS actions are neither limited to named actions nor is the

non-deterministic choice the only possible operator.

Instead, all operators described in Section \ref{Composition} are available

as well as the built-in action \texttt{skip} and so-called anonymous actions.

An anonymous action is a guard followed by assignments, methods or built-in

action \texttt{skip}. In literature anonymous actions are often referred to

as \emph{guarded commands}.

If (named) actions are parametrized, enumeration can be used as generalization

of the non-deterministic choice over the values of a data type.

For instance given a data type \texttt{SmallInt = int[0..3]} and a named action

\texttt{doSomething ( a : SmallInt )} it is possible to write

\begin{verbatim}

do

	var : A : SmallInt : doSomething(A)

od

\end{verbatim}

as abbreviation for

\begin{verbatim}

do

	doSomething(0) [] doSomething(1) [] doSomething(2) [] doSomething(3)

od

\end{verbatim}

\subsection{The System Assembling Block}

\label{SAB}

In the System Assembling Block the system is assembled by its classes. All

the classes used by the system are connected either by the non-deterministic

choice operator \texttt{[]} or by the prioritized composition operator

\texttt{//}. This feature allows the user to manually set the priority among

the classes.

\clearpage

\subsection{Comments}

The OOAS language supports single line comments. Comments start

with a \texttt{\#} symbol.

\subsection{Formal Syntax}

The following EBNF grammar defines the syntax of an Object-Oriented action

system (OOAS). Features that are not implemented at all are left out. However

there are some features that are not completely implemented and do produce

code that doesn't work. These features are stroked out.

\\

\begin{longtable}[h]{lll}

OOAS &:=& ['\texttt{consts}' ConstList] '\texttt{types}' TypeList '\texttt{system}' ASTypeComp \\

ConstList &:=& NamedConst \{ '\texttt{;}' NamedConst \} \\

NamedConst &:=& Identifier '=' Exp \\

TypeList &:=& NamedType \{ '\texttt{;}' NamedType \} \\

NamedType &:=& Identifier '=' ( ComplexType $\vert$ OOActionSystem ) \\

ComplexType &:=& ( '\texttt{list}' '\texttt{[}'  ( Num $\vert$ Identifier )  '\texttt{]}'  '\texttt{of}' ComplexType ) \\

 & &  $\vert$ ( '\texttt{[}' Identifier \{ '\texttt{,}' Identifier \} '\texttt{]}'  ) \\

 & & $\vert$ ( '\texttt{(}' ComplexType \{ '\texttt{,}' ComplexType \}  '\texttt{)}'  ) \\

 & & $\vert$ SimpleType \\

SimpleType &:=& '\texttt{bool}'\\ 

 & & $\vert$ ( '\texttt{int}' '\texttt{[}' ( Num $\vert$ Identifier ) '\texttt{..}' ( Num $\vert$ Identifier )  '\texttt{]}' )\\

 & & $\vert$ ( '\texttt{float}' '\texttt{[}' ( FloatNum $\vert$ Identifier ) '\texttt{..}' ( FloatNum $\vert$ Identifier )  '\texttt{]}' )\\

 & & $\vert$ '\texttt{char}' \\

 & & $\vert$ '\texttt{\{}' Identifier [ '\texttt{=}' Num] \{ '\texttt{,} Identifier [ '\texttt{=}' Num ] \} '\texttt{\}}' \\

 & & $\vert$ Identifier \\

OOActionSystem &:=& [ '\texttt{autocons}' ] '\texttt{system}' [ Identifier ] \\

 & & '\texttt{|[}'  [ '\texttt{var}' AttrList ] [ '\texttt{methods}' MethodList ] \\

& & [ '\texttt{actions}' NamedActionList ] [ '\texttt{do}' [ActionBlock] '\texttt{od}'] '\texttt{]|}' \\

AttrList &:=& Attr \{ '\texttt{;}' Attr \} \\

Attr &:=& [ '\texttt{static}' ]  [ '\texttt{obs}' $\vert$ '\texttt{ctr}' ] Identifier '\texttt{:}' ComplexType [ '\texttt{=}' Exp ] \\ 

MethodList &:=& Method \{ '\texttt{;}' Method \} \\

Method &:=& Identifier [ '\texttt{(}' MethodParamList '\texttt{)}' ] [ '\texttt{:}' ComplexType ] '\texttt{=}' \\

 & & [ '\texttt{var}' LocalActionVars '\texttt{begin}' ] ActionBody '\texttt{end}' \\

MethodParamList &:=& Identifier '\texttt{:}' ComplexType \{ '\texttt{,}' Identifier '\texttt{:}' ComplexType  \} \\

NamedActionList &:=& NamedAction \{ '\texttt{;}' NamedAction \} \\

NamedAction &:=& [ '\texttt{obs}' $\vert$ '\texttt{ctr}' ]  Identifier [ '\texttt{(}' MethodParamList '\texttt{)}' ] \\

 & &  [ '\texttt{:}' ComplexType ] '\texttt{=}'  [ '\texttt{var}' LocalActionVars ] DiscreteActionBody \\

LocalActionVars &:=& Identifier '\texttt{:}' ComplexType \{ '\texttt{;}' Identifier '\texttt{:}' ComplexType\} \\

DiscreteActionBody &:=& '\texttt{requires}' Exp '\texttt{:}' ActionBody '\texttt{end}'\\

Exp &:=& AtomExpression BinOperator AtomExpression \\

AtomExpression &:=& ( [ OpUn ] ( Reference $\vert$ Constant $\vert$ InitComplexType $\vert$ QuantExp\\

&& $\vert$ '\texttt{(}' Exp '\texttt{)}' \{ '\texttt{.}' Identifier \} [ AccessExp] ) \\

&& [ '\texttt{as}' Identifier ] ) \\

& & $\vert$ ( '\texttt{if}' Exp '\texttt{then}' Exp '\texttt{else}' Exp '\texttt{end}' ) \\

OpUn &:=& '\texttt{-}'  $\vert$ '\texttt{not}' $\vert$ '\texttt{hd}' $\vert$ '\texttt{tl'} $\vert$ '\texttt{len}'\\

Constant &:=& ('\texttt{true}') $\vert$ ('\texttt{false'}) $\vert$ ('\texttt{nil}') $\vert$ ('\texttt{self}') $\vert$ (FloatNum) $\vert$ (Num) $\vert$ \\

&& (\cancel{StringLiteral}) \\

InitComplexType &:=& InitListType $\vert$ ('\texttt{new}' '\texttt{(}' Identifier [ '\texttt{,}' StringLiteral ] '\texttt{)}') \\

InitListType &:=& '\texttt{[}' Exp [ ListComp $\vert$ \{ '\texttt{,} Exp'\} ] '\texttt{]}' \\

ListComp &:=& '\texttt{|}' '\texttt{var}' Identifier '\texttt{:}' ComplexType \{ \texttt{;} Identifier ComplexType \} '\texttt{\&}' Exp \\

QuantExp &:=& ('\texttt{forall}' $\vert$ '\texttt{exists}') Identifier '\texttt{:}' SimpleType \\

&& \{ '\texttt{,}' Identifier '\texttt{:} SimpleType' \}  '\texttt{:}' '\texttt{(}' Exp '\texttt{)}' \\

ActionBody &:=& ActionBodyParallel '\texttt{//}' ActionBodyParallel \\

ActionBodyParallel &:=& ActionBodySeq '\texttt{[]}' ActionBodySeq \\

ActionBodySeq &:=& ActionBodyParen '\texttt{;}' ActionBodyParen \\

ActionBodyParen &:=& ( '\texttt{(}' ActionBody '\texttt{)}' ) $\vert$ ( Statement ) \\

Statement &:=& ( '\texttt{skip'} ) $\vert$ ( Reference \{ '\texttt{,}' Reference  \} '\texttt{:=}' Exp \{ '\texttt{,}' Exp\} ) \\

Reference &:=& QualId [ AccessExp ] [ [ '\texttt{::}' '\texttt{(}' Exp '\texttt{)}' ] '\texttt{:>:}' '\texttt{(}' Exp '\texttt{)}'  ] \\

AccessExp &:=& ( ( '\texttt{[}' Exp '\texttt{]}' )  $\vert$ ( '\texttt{(}' MethodCallParam '\texttt{)}') ) \\

&& \{( ( '\texttt{[}' Exp '\texttt{]}' )  | ( '\texttt{(}' MethodCallParam '\texttt{)}') ) \} \\

&& [ '\texttt{.}' Identifier \{ '\texttt{.}' Identifier\} AccessExp] \\

QualId &:=& [ '\texttt{self}' '\texttt{.}' ] Identifier \{ '\texttt{.} Identifier'\} \\

MethodCallParam &:=&  [ Exp \{ '\texttt{,}' Exp\}]\\

ActionBlock &:=& ActionBlockPar \{ '\texttt{//}' ActionBlockPar\} \\

ActionBlockPar &:=& ActionBlockSeq \{ '\texttt{[]}' ActionBlockSeq\} \\

ActionBlockSeq &:=& [ '\texttt{var}' BlockVarList [\cancel{'\texttt{\&}' Exp} ] '\texttt{:}' ] \\

&&ActionBlockParen  \{ '\texttt{;}' ActionBlockParen\}\\

ActionBlockParen &:=& ('\texttt{(}' ActionBlock '\texttt{)}' ) $\vert$ (AnonOrNamedAct)\\

AnonOrNamedAct &:=&  DiscreteActionBody $\vert$ '\texttt{skip}' $\vert$ \\

&& Identifier [ '\texttt{(}' MethodCallParam '\texttt{)}' ] [ '\texttt{:>:}' '\texttt{(}' Exp '\texttt{)}'  ]  \\

BlockVarList &:=& BlockVar \{ '\texttt{;} BlockVar'\} \\

BlockVar &:=& Identifier '\texttt{:}' ComplexType \\

ASTypeComp &:=& ASTypeCompPar \{ '\texttt{//}' ASTypeCompPar\} \\

ASTypeCompPar &:=& ASTypeCompSeq \{ '\texttt{[]}' ASTypeCompSeq\} \\

ASTypeCompSeq &:=& ASTypeCompBP \\

ASTypeCompBP &:=& ('\texttt{(}' ASTypeComp '\texttt{)}' ) \\

BinOperator &:=& ('\texttt{<=>}') $\vert$ ('\texttt{>}')$\vert$ ('\texttt{>=}')$\vert$ ('\texttt{<}')$\vert$ ('\texttt{<=)}')$\vert$ ('\texttt{=}')$\vert$ ('\texttt{<>}')$\vert$ ('\texttt{=>}') $\vert$ ('\texttt{-}')$\vert$ ('\texttt{+}') \\

&&$\vert$ ('\texttt{or}')$\vert$ ('\texttt{and}')$\vert$ ('\texttt{/}') $\vert$ ('\texttt{div}') $\vert$ ('\texttt{*}') $\vert$ ('\texttt{mod}') $\vert$ ('\texttt{\^}')\\

Identifier &:=& Letter \{Letter $\vert$ Digit\}\\

Num &:=& ['\texttt{+}' $\vert$ '\texttt{-}'] Digit \{ Digit \} \\

FloatNum &:=& ['\texttt{+}' $\vert$ '\texttt{-}'] Digit \{ Digit \} '\texttt{.}' Digit \{Digit\} ['\texttt{e}' $\vert$ '\texttt{E}' ['\texttt{+}' $\vert$ '\texttt{-}' ] Digit \{ Digit \}]\\

Letter &:=& '\texttt{\$}' $\vert$ '\texttt{\_}' $\vert$ '\texttt{A}'..'\texttt{Z}' $\vert$ '\texttt{a}'..'\texttt{z}'\\

Digit &:=& '\texttt{0}'..'\texttt{9}'\\

\end{longtable}

\clearpage

\section{Incomplete Features}

The following features are supported by the grammar, but do not produce

executable or useful code.

\subsection{Sequential Block Expression}

In the \doodblock when calling an action with a variable it is possible

to add an additional guard. However if the guard is true, the produced

Prolog-Code will not work.

Example:

\begin{verbatim}

do

	var A : SmallInt & A < 3 : push(A)

od

\end{verbatim}

\subsection{String}

It is possible to assign a string to a variable of any list type of char.

Example:

\begin{verbatim}

  var

	my_string : list[20] of char = [0] 

  actions

	obs fill = requires true :

		my_string := "Hello World!"

		end

\end{verbatim}

However, in the produced Prolog-Code the characters stored in the list are

not of type char, but instead Prolog atoms. This may lead to strange behaviour.

\section{CADP Target}

\subsection{The Argos CADP-Target}

The CADP-Target is an Add-On for Argos. It produces C files for the use

with the CADP toolbox available at \url{http://www.inrialpes.fr/vasy/cadp/}.

It is deployed as dynamic library

with the file name \texttt{ArgosCadpTarget.dll}. If this file is present

an additional Argos option \texttt{-c} is available.

The invocation of Argos to produce C files for CADP is very similar

to the invocation of Argos to produce prolog files for Ulysses. Instead

of using the option \texttt{-p} one has to use the option \texttt{-c} and

the options \texttt{-n} and \texttt{-d} should be omitted as they are

meaningless in this context.

\subsection{Generating BCG}

The generated C file can be used to produce a graph in CADP's proprietary

BCG format. This is done by compiling the file against CADP's tools using

the \texttt{cadp\_cc} compiler.

Given a shell with the environment variables \texttt{\$CADP} set to the

CADP directory and \texttt{\$ARGOS} set to the Argos directory one

can compile an Argos generated C file \texttt{model.c} into an object

file \texttt{model.o} using the following command:

\begin{verbatim}

$CADP/src/com/cadp_cc -g3 -O0 -I. -I$CADP/incl -I$CADP/src/open_caesar \

-I $ARGOS/trunk/src/cadp/cadpruntime/ -c model.c -o model.o

\end{verbatim}

Now the generator from the CADP toolbox can be compiled using the command:

\begin{verbatim}

$CADP/src/com/cadp_cc  -g3 -O0 -I. -I$CADP/incl -I$CADP/src/open_caesar \

-c $CADP/src/open_caesar/generator.c -o generator.o

\end{verbatim}

Finally the two object files can be linked into an executable using the command:

\begin{verbatim}

$CADP/src/com/cadp_cc generator.o model.o -o generator \

-L${BCG:-$CADP}/bin.`$CADP/com/arch` -lcaesar -lBCG_IO -lBCG -lm

\end{verbatim}

\subsection{Animator}

For debugging purposes Argos provides a so-called Animator that enables

one to walk step wise through a model. The models can be either encoded as

graphs in \texttt{aut} files or as dynamic link library compiled from an Argos

generated C file. The compilation can be done using any C compiler that is

capable of generating dynamic link libraries for 32 bit Windows platforms.

However, compiling the model to a dynamic link library can be a little bit

tricky, so a solution file for Microsoft Visual Studio 2008 can be found

in the argos source directory or to be exact in the sub-directory

\texttt{cadp/model}. Unfortunately some paths in this file are absolute,

so they have to be changed to match the paths that are actually used.

This can be done by a right-click on \emph{model} within the

\emph{Solution Explorer}. Now a \emph{model Property Pages} window

pops up, providing an element \emph{Configuration Properties}. This

element can be expanded, and \emph{C/C++} has to be chosen. The first

entry of this page, called \emph{Additional Include Directories} has

to be changed to fit.

\section{Alarm System}

\subsection{Overview}

In this section a model of a Car Alarm System is presented. The purpose is

to show how Object-Oriented Action Systems can be used to model real world

system in contrast to the examples presented so far. The Car Alarm System

has been a demonstrator in the MOGENTES project. The specifications were

provided by Ford. This demonstrator was also used in \cite{Aichernig2010a}.

\subsection{Requirements}

In \cite{Aichernig2010a} the specification was condensed to the following three

requirements:

\textbf{R1: Arming.} The system is armed 20 seconds

after the vehicle is locked and the bonnet, luggage compartment, and

all doors are closed.

\textbf{R2: Alarm.} The alarm sounds for 30 seconds if

an unauthorized person opens the door, the luggage compartment, or the

bonnet. The hazard flasher lights will flash for five minutes.

\textbf{R3: Deactivation.} The CAS

can be deactivated at any time, even when the alarm is sounding, by

unlocking the vehicle from outside.

\subsection{State Chart}

In \cite{Aichernig2010a} a UML transformation tool was used to generate an

Object-Oriented action system. The paper contains a state chart which is cited

in Figure \ref{statechart}. In contrast the action system presented in this

manual was written by hand but it is somehow based on this State Chart

regarding the interpretation of the requirements.

\begin{figure}[h]

 \includegraphics[width=1\linewidth,keepaspectratio]{figures/SM_AlarmSystem}

\caption{State Chart of Car Alarm System}

\label{statechart}

\end{figure}

\clearpage

\subsection{Object-Oriented Action System}

\subsubsection{Interface}

In the context of generating labeled transition systems for \emph{Ulysses}

the interface of an Object-Oriented action system consists of named actions.

According to the ioco theory, labels have to be marked as either input or

output. In Object-Oriented action systems the corresponding keywords are

\texttt{ctr} resp. \texttt{obs}.

Therefore the interface of the Car Alarm System consists of 4 controllable

actions \texttt{Close}, \texttt{Open}, \texttt{Lock} and \texttt{Unlock}.

In the context of the implementation these actions correspond to the input

coming from various sensors. In the context of a generated test case these

actions correspond to outputs to the System Under Test.

Also there are 6 observable actions \texttt{ArmedOn}, \texttt{ArmedOff},

\texttt{SoundOn}, \texttt{SoundOff}, \texttt{FlashOn}, and \texttt{FlashOff}.

In the context of the implementation these action correspond to output that

triggers the resp. signals to the environment.

In the context of the generated test cases these actions correspond to the

expected inputs coming from the System Under Test.

\subsubsection{Time Handling}

One important aspect of modeling such a system is time handling. In former

models within the MOGENTES project passing of time had been modeled by

introducing an observable action \emph{after}. Later in the project this

caused some problems as some test cases were not generated.

To solve these problems the after action in this model is removed. Instead,

elapsed time is now encoded as first parameter of every remaining action.

\subsubsection{Protocol Layer}

In the context of model-ling an embedded system the \doodblock can be thought

as protocol layer. To keep the model simple, the most canonical form of the

\doodblock has been used. That is, all named actions are connected using

the non-deterministic choice. Since the named actions are parametrized,

enumeration is used. Unfortunately the size of the state space grows

exponentially by number of enumerated values, so it is very important

to keep the resp. ranges as small as possible. In the context of this model,

where the meaning of each action's parameter is the elapsed time, this

means that only ``interesting'' time periods are considered. Actually,

``interesting'' events only happen immediately, 20, 30 or 270 seconds

after the previous event. Exactly these values are contained in the

Enum Type \texttt{TimeSteps}.

\subsubsection{Non-determinism}

This model makes use of non-determinism. That means that there are situations

in which the system can choose how it responses to a certain input.

More technically that means, that there sequences of controllable and

observable actions, after which there is more than one observable action.

In the context of using the model to specify a system that means

underspecification. A system can choose among some possible options how to

react.

In this particular model, non-determinism is used so that the implementation

has some freedom with regards to the exact sequence of observable actions.

For example when an intrusion is detected by the alarm system, then three

events happen immediately: The arming is set off, the sound alarm is set

on and the flash alarm is set on. A deterministic system would specify the

exact order, in which these actions must be triggered. In the context of

test case generation this could lead to some false positives, as the

requirements do not specify a fixed order.

\subsubsection{Code}

%\begin{figure}[h]

 \begin{lstlisting}[language=ooa,linewidth=\textwidth,breaklines,basicstyle=\scriptsize]

types

	TimeSteps = {Int0 = 0 , Int20 = 20, Int30 = 30, Int270 = 270} ;

	Int = int[0..270] ;

	SmallInt = int[0..3] ;

	AlarmSystem = autocons system

	|[

		var

			open : bool = true ;

			locked : bool = false ;

			armed : bool = false ;

			soundAlarm : bool = false ;

			flashAlarm : bool = false ;

			blockingLevel : SmallInt = 0 ;

			armedOnNow : bool = false ;

			armedOnLater : bool = false ;

			armedOff : bool = false ;

			soundOn : bool = false ;

			soundOffNow : bool = false ;

			soundOffLater : bool = false ;

			flashOn : bool = false ;

			flashOffNow : bool = false ;

			flashOffLater : bool = false  ;

			silent : bool = false # true after alarms turned off

		actions

			ctr Close ( waittime : Int) =

				requires not flashAlarm and not soundAlarm :

					requires open and waittime = 0 and blockingLevel = 0 and locked and silent:

						open := false ;

						blockingLevel := 1 ;

						armedOnNow := true ;

						silent := false			

					end []

					requires open and waittime = 0 and blockingLevel = 0 and not locked and silent:

						silent := false ;

						open := false 

					end []

					requires open and waittime = 0 and blockingLevel = 0 and locked and not silent:

						open := false ;

						blockingLevel := 1 ;

						armedOnLater := true

					end []

					requires open and waittime = 0 and blockingLevel = 0 and not locked and not silent:

						open := false 

					end

				end ;

			ctr Open ( waittime : Int) =

				requires true :

					requires not open and waittime = 0 and blockingLevel = 0 and not armed :

						open := true

					end []

					requires not open and waittime = 0 and blockingLevel = 0 and armed :

						open := true ;

						armed := false ;

						blockingLevel := 3 ;

						armedOff := true ;

						soundOn := true ;

						flashOn := true

					end 

				end ;

			ctr Unlock ( waittime : Int) =

				requires true : 

					requires locked and waittime = 0 and blockingLevel = 0 and not flashAlarm and soundAlarm:

						locked := false ;

						silent := false ;

						soundOffLater := false ;

						soundOffNow := true ;

						blockingLevel := 1 

					end []

					requires locked and waittime = 0 and blockingLevel = 0 and flashAlarm and soundAlarm :

						locked := false ;

						flashOffNow := true ;

						blockingLevel := 2 ;

						silent := false ;

						soundOffLater := false ;

						soundOffNow := true

					end []

					requires locked and waittime = 0 and blockingLevel = 0 and not flashAlarm and not soundAlarm:

						locked := false ;

						silent := false ;

						armedOff := true ;

						blockingLevel := 1

					end []

					requires locked and waittime = 0 and blockingLevel = 0 and flashAlarm and not soundAlarm:

						locked := false ;

						flashOffNow := true ;

						flashOffLater := false ;

						blockingLevel := 1 ;

						silent := false

					end

				end;

			ctr Lock ( waittime : Int) =

				requires true :

					requires not locked and waittime = 0 and blockingLevel = 0 and open :

						locked := true

					end []

					requires not locked and waittime = 0 and blockingLevel = 0 and not open :

						locked := true ;

						blockingLevel := 1 ;

						armedOnLater := true

					end 

				end ;

			obs ArmedOn (waittime : Int) =

				requires (armedOnNow or armedOnLater):

					requires (waittime = 20 and armedOnLater) :

						armedOnLater := false ;

						blockingLevel := blockingLevel - 1 ;

						armed := true

					end

					[] requires (waittime = 0 and armedOnNow) :

						armedOnNow := false ;

						blockingLevel := blockingLevel - 1 ;

						armed := true

					end

				end ;

			obs ArmedOff (waittime : Int) =

				requires (waittime = 0 and armedOff) :

					armedOff := false ;

					blockingLevel := blockingLevel - 1 ;

					armed := false

				end ;

			obs SoundOn (waittime : Int) =

				requires true :

					requires (waittime = 0 and soundOn and blockingLevel = 1) :

						soundOn := false ;

						blockingLevel := blockingLevel - 1 ;

						soundAlarm := true ;

						soundOffLater := true 

					end []

					requires (waittime = 0 and soundOn and blockingLevel <> 1) :

						soundOn := false ;

						blockingLevel := blockingLevel - 1 ;

						soundAlarm := true

					end 

				end ;

			obs SoundOff (waittime : Int) =

				requires (soundOffNow or soundOffLater) :

					requires (waittime = 30 and soundOffLater) :

						soundOffLater := false ;

						flashOffLater := true ;

						soundAlarm := false

					end

					[] requires (waittime = 0 and soundOffNow) :

						soundOffNow := false ;

						blockingLevel := blockingLevel - 1 ;

						soundAlarm := false

					end

				end ;

			obs FlashOn (waittime : Int) =

				requires true :

					requires (waittime = 0 and flashOn and blockingLevel = 1) :

						flashOn := false ;

						blockingLevel := blockingLevel - 1 ;

						flashAlarm := true ;

						soundOffLater := true 

					end []

					requires (waittime = 0 and flashOn and blockingLevel <> 1) :

						flashOn := false ;

						blockingLevel := blockingLevel - 1 ;

						flashAlarm := true

				end 

				end ;

			obs FlashOff (waittime : Int) =

				requires (flashOffNow or flashOffLater) :

					requires (waittime = 270 and flashOffLater) :

						flashOffLater := false ;

						flashAlarm := false ;

						silent := true

					end

					[] requires (waittime = 0 and flashOffNow) :

						flashOffNow := false ;

						blockingLevel := blockingLevel - 1 ;

						flashAlarm := false

					end

				end

	do

		var A : TimeSteps : Close (A) [] 

		var B : TimeSteps : Open (B) []

		var C : TimeSteps : Lock (C) []

		var D : TimeSteps : Unlock (D) []

		var E : TimeSteps : ArmedOn (E) []        

		var F : TimeSteps : ArmedOff (F) []        

		var G : TimeSteps : SoundOn (G) []        

		var H : TimeSteps : SoundOff (H) []   

		var I : TimeSteps : FlashOn (I) []        

		var J : TimeSteps : FlashOff (J)    

	od

	]|

system

	AlarmSystem

\end{lstlisting}

%\caption{Car Alarm System in OOAS}

%\label{Stack}

%\end{figure}

\subsection{Labeled Transition System}

In Figure \ref{lts} you can find a graphical representation

of labeled transition system that corresponds to the Object-Oriented

action system. It is a ioco product graph produced by \emph{Ulysses}.

So there is an additional observable action \emph{delta} that denotes

quiescence. Iff in a given state the system has no specified output,

there is a self loop labeled with \emph{delta}.

\begin{figure}[h]

 \includegraphics[angle=90,width=0.42\linewidth,keepaspectratio]{figures/out}

\caption{Labeled Transition System}

\label{lts}

\end{figure}

\section*{Acknowledgements}

%Research herein was 

Funded by the European Artemis Joint Undertaking project

MBAT, Combined Model-based Analysis and Testing of Embedded Systems %.

%ART Call 2010: 269335.

and by the Austrian Research Promotion Agency

(FFG), program line ``Trust in IT Systems'', project number 829583, TRUst via Failed FALsification of Complex

Dependable Systems Using Automated Test Case Generation through Model

Mutation (TRUFAL).

\clearpage

\bibliographystyle{plain}

\bibliography{papers}

\end{document}