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.