\documentclass{article}

\title{CspCASL syntax description}

\author{Christian Maeder}

\begin{document}

\maketitle

CspCASL is designed as CASL extension with additional channel and process

items as parts of basic specifications.

The only support for structural specifications is given by the ``data''

keyword, that can be viewed as a special case for an extended specification

given by the ``then'' keyword.

\begin{verbatim}

logic CASL

spec s = ...

logic CspCSL

spec c = data s

...

\end{verbatim}

can also be written as:

\begin{verbatim}

logic CASL

spec s = ...

logic CspCSL

spec c = s then

...

\end{verbatim}

The missing parts (indicated by the dots above), can be any sequence of basic

CspCASL or CASL items. Sort, operation and predicate items can be freely mixed

with channel or process items.

\section{Basic CspCASL Items}

As in CASL basic items are introduced by a (singular or plural) keyword

followed by list of items of the same kind that are separated by semicolons,

where a final semicolon is optional. A new item keyword, like ``sort'' or

``channel'', starts a new item list. (The plural of ``process'' is currently

not supported as keyword.)

Similar to the CASL grammar, we adopt the following convention:

\begin{itemize}

\item Nonterminal symbols are written as uppercase words, possibly hyphenated,

e.g.~BASIC-ITEMS.

\item Terminal symbols (possibly quoted) are written as either lowercase

words, e.g.~channel; or sequences of special characters that do not clash

with the metasymbols ::=, $|$, or ‘...’.

\item A final optional semicolon is written as ;/

\item Repetitions are indicated by ellipsis ‘...’, e.g. ID ,..., ID indicate

one or more IDs separated by commas in the latter case.

\item Alternative sequences are separated by vertical bars

\item A vertical bar followed by ellipsis hint at alternatives that

are not shown.

\end{itemize}

\subsection{Channel Items}

Channels are associated to sorts to control the communication. Many different

channels may communicate data of the same sort. Channels with the same name

but over a different sort are considered as different. Such channels (within

alphabets or event sets) must be qualified with their sort for

disambiguation.

\begin{verbatim}

BASIC-ITEMS ::= channel CHANNEL-ITEM ;...; CHANNEL-ITEM ;/

| channels CHANNEL-ITEM ;...; CHANNEL-ITEM ;/

| ...

CHANNEL-ITEM ::= CHANNEL ,..., CHANNEL : SORT

CHANNEL ::= SORT-ID

\end{verbatim}

It is also possible to use the same names for channel and sorts. Again

channels must be qualified then, later on. However, in practice, it is not

recommended to exploit overloading extensively.

\subsection{Process Items}

Processes may be declared or defined (or both at the same time) by process items.

\begin{verbatim}

BASIC-ITEMS ::= process PROCESS-ITEM ;...; PROCESS-ITEM ;/

| ...

PROCESS-ITEM ::= PROCESS-NAME PROCESS-PROFILE

| PROCESS-NAME PROCESS-HEAD = PROCESS

| PROCESS-NAME = PROCESS

PROCESS-NAME ::= SORT-ID

PROCESS-PROFILE ::= ( SORT ,..., SORT ) : ALPHABET

| : ALPHABET

PROCESS-HEAD ::= ( VAR ,..., VAR )

| ( ARG-DECL ;...; ARG-DECL) : ALPHABET

| : ALPHABET

ALPHABETT ::= SORT-OR-CHANNEL ,..., SORT-OR-CHANNEL

| { SORT-OR-CHANNEL ,..., SORT-OR-CHANNEL }

| { }

SORT-OR-CHANNEL ::= SORT

| CHANNEL

| CHANNEL : SORT

\end{verbatim}

A mere process declaration introduces a process name, possibly with sorted

arguments, and a communication alphabet (starting with a colon sign).

Process names may be overloaded as long as the argument sorts are sufficiently

different to disambiguate the names later within process expressions.

Proper mixfix identifiers (containing places) are not allowed as process

names, in order to avoid confusion with the CspCASL builtin infix operators.

However, compound identifiers like those for sorts and channel are legal.

A process definition is an equation that defines the process depending on its

input variables (that must all be different).

Such an equation can be seen as a special process formula and just like

operations or predicates in CASL also processes can be declared and defined

simultaneously, if sorted variables (possibly none) and the communication

alphabet is supplied.

An alphabet or possible event sets are just comma separated sets of sorts or

channels, that may even be empty.

It remains to describe the process expression that may occur on the left hand

side of a process equation.

\subsection{Processes}

Processes are basically composed of more primitive processes. The most

primitive processes are:

\begin{verbatim}

PROCESS ::= "SKIP"

| "STOP"

| "DIV"

| "RUN" ( EVENT-SET )

| "CHAOS" ( EVENT-SET )

| ...

EVENT-SET ::= ALPHABET

\end{verbatim}

Then, it is possible to invoke a process (declared earlier) with concrete

argument terms.

\begin{verbatim}

PROCESS ::= PROCESS-CALL

| ...

PROCESS-CALL ::= PROCESS-QUAL

| PROCESS-QUAL ( TERM ,..., TERM )

PROCESS-QUAL ::= PROCESS-NAME

| ( process PROCESS-NAME PROCESS-PROFILE )

\end{verbatim}

Processes can be slightly modified by hiding (wrt to an event set) or by

renaming.

\begin{verbatim}

PROCESS ::= PROCESS \ EVENT-SET

| PROCESS [[ RENAMING ]]

| ...

RENAMING ::= ID ,..., ID

\end{verbatim}

Processes can be invoked depending on conditions or events.

\begin{verbatim}

PROCESS ::= if FORMULA then PROCESS else PROCESS

| EVENT -> PROCESS

| TERM -> PROCESS

| ...

EVENT ::= CHANNEL ? VAR :: SORT

| CHANNEL ! VAR :: SORT

| CHANNEL ! TERM

\end{verbatim}

Two processes can be invoked sequentially. (Instead of a single semicolon also

a double semicolon ;; may be used as alternative operator to avoid possible

conflicts wrt basic items.)

\begin{verbatim}

PROCESS ::= PROCESS ; PROCESS

| ...

\end{verbatim}

Next, we have the external and internal choice between two processes.

\begin{verbatim}

PROCESS ::= PROCESS [] PROCESS

| PROCESS |~| PROCESS

| ...

\end{verbatim}

There are also two corresponding prefix choice operators.

\begin{verbatim}

PROCESS ::= [] VAR :: SORT -> PROCESS

| |~| VAR :: SORT -> PROCESS

| ...

\end{verbatim}

Finally, there are four kinds for parallel invocations of two processes,

attributed with generalized, alphabetized, synchronous and interleaved,

respectively.

\begin{verbatim}

PROCESS ::= PROCESS [| EVENT-SET |] PROCESS

| PROCESS [ EVENT-SET || EVENT-SET ] PROCESS

| PROCESS || PROCESS

| PROCESS ||| PROCESS

| ...

\end{verbatim}

Generalized and alphabetized parallel are regarded as (just larger) infix

operators, that also may be written using $|[$ and $]|$ as brackets. (The

double bar between the two event sets within alphabetized parallel may also be

a single bar.)

The grammar given above is quite ambigouos, therefore some precedence rules

and associativities for infix operators will follow. For explicit grouping

parentheses may be used.

\begin{verbatim}

PROCESS ::= ( PROCESS )

| ...

\end{verbatim}

The four parallel infix operators bind weakest, followed by the two infix

choice operators, followed by sequential composition. All infix operators

associate to the right.

\begin{verbatim}

p1 ; p2 ; p3 [] p4 |~| p5 || p6 [] p7 ; p8 ||| p9

\end{verbatim}

is parsed as:

\begin{verbatim}

((p1 ; (p2 ; p3)) [] (p4 |~| p5)) || ((p6 [] (p7 ; p8)) ||| p9)

\end{verbatim}

Prefix operators like the prefix choices or the event processes (using \verb|->|)

bind stronger than infixes and yet stronger bind the postfix operators for

hiding and renaming.

\begin{verbatim}

t -> [] v :: s -> p \ s [[ r ]]

\end{verbatim}

is parsed as:

\begin{verbatim}

t -> ([] v :: s -> ((p \ s) [[ r ]]))

\end{verbatim}

Strongest binding are the primitive processes and process calls.

For conditional if-then-else processes the keywords serve as brackets and the

final process (following else) extends as far to the right as possible.

\section{Concrete Syntax}

\input{concrete_syntax.tex}

\end{document}