Appendix B - FSP Language Specification

Top  Previous 

FSP stands for Finite State Processes.

This appendix contains a comprehensive specification of the syntax of FSP together with a commentary on features such as variable scope that are not treated explicitly in the body of the book.

In specifying the syntax of FSP, we have followed the approach used in the Java Language Specification. In particular, the syntax is specified using a context-free grammar that consists of a number of productions. Each production is defined by a non-terminal symbol as its left-hand side and a sequence of one or more terminal and non-terminal symbols as its right-hand side. In the following, non-terminal symbols are shown in italic type and terminal symbols in a fixed width bolded type. The definition of a non-terminal is introduced by its name followed by a colon. One or more alternative right-hand sides for the non-terminal then follow on succeeding lines. For example, the following production specifies the syntax for an FSP constant definition.

ConstantDef:

       const ConstantIdent = Expression

 

The production below specifies an argument list as consisting of either a single expression or a list of expressions separated by commas:

ArgumentList:

       Expression

       ArgumentList , Expression        

 

The subscripted suffix "opt", which may appear after a terminal or non-terminal, indicates an optional symbol.

1.FSP description

In addition to definitions for processes and compositions of processes, an FSP model description consists of definitions for constants, ranges of integers, sets of action labels, safety properties, progress properties,  animation menus, fluents and assertions.

FSPdescription:

       FSPdefinition

       FSPdescription FSPdefinition  

FSPdefinition:

       ConstantDef

       RangeDef

       SetDef

       ProcessDef

       CompositeDef

       PropertyDef

       ProgressDef

       MenuDef

       FluentDef

       AssertDef

 

1.1Identifiers

FSP definitions and process parameters are named by identifiers beginning with an uppercase letter. Action label and variable identifiers begin with a lower case letter.

ConstantIdent:

RangeIdent:

SetIdent:

ParameterIdent:

ProcessIdent:

PropertyIdent:

ProgressIdent:

MenuIdent:

FluentIdent:

AssertIdent:

       UpperCaseIdentifier

Variable:

       LowerCaseIdentifier

Upper and lower case identifiers are specified by the following productions in which UpperCaseLetter denotes one of the uppercase alphabetical characters and LowerCaseLetter denotes one of the lower case alphabetical characters or underscore “_”. Digit denotes one of the decimal digits.

UpperCaseIdentifier:

       UpperCaseLetter

       UpperCaseIdentifier Letter

       UpperCaseIdentifier Digit

LowerCaseIdentifier:

       LowerCaseLetter

       LowerCaseIdentifier Letter

       LowerCaseIdentifier Digit

Letter:

       UpperCaseLetter

       LowerCaseLetter

1.2Action Labels

Actions in FSP can be labeled either by a lowercase identifier or by a value computed from an expression enclosed by square brackets. Action labels are also formed by concatenating simpler labels with a dot.

ActionLabel:

       LowerCaseIdentifier

       ActionLabel . LowerCaseIdentifier

       [ Expression ]

       ActionLabel [ Expression ]

Examples

       in   [43]   in[12]   in[2][i*2]   x[1].y[3]

 

Wherever a single action label can be used in FSP, a set of action labels can also be used. The exception is where label values are used in expressions (see B.10).

ActionLabels:

       ActionLabel

       Set

       [ ActionRange ]

       ActionLabels. ActionLabel

       ActionLabels. Set

       ActionLabels [  ActionRange ]

       ActionLabels [  Expression ]

Sets of action labels are defined explicitly by a set or by a range of integer values.

ActionRange:

       Range

       Set

       Variable : Range

       Variable : Set

Range:

       RangeIdent

       Expression .. Expression

Set:

       SetIdent

       { SetElements }

SetElements:

       ActionLabels

       SetElements , ActionLabels

 

Examples

       {a,b,c}  X.a   in[x:1..3]   in[x:T]   a.{x,y,z}

Variables can be associated with a set or a range in an ActionRange. The variable successively takes on each of the values of the set or range. The scope of variables is discussed in the following with respect to their use in processes, composite processes and re-labeling definitions.

Examples

       a[i:1..3]   x[v:{a,b,c}]

 

1.3const, range, set

Named constants, ranges and sets are defined as follows:

ConstantDef:

       const ConstantIdent = SimpleExpression

RangeDef:

       range RangeIdent = SimpleExpression.. SimpleExpression

SetDef:

       set SetIdent   = { setElements }

 

 

Examples

       const N = 3

       range R = 0..N

       set   S = {a,b,c,d[R]}

 

1.4Process Definition

A process is defined by one or more local processes. A process can optionally be parameterized and have re-labeling, hiding and alphabet extension parts.

ProcessDef:

       ProcessIdent  Paramopt = ProcessBody

AlphabetExtensionopt  Relabelopt  Hidingopt .

ProcessBody:

       LocalProcess

       LocalProcess , LocalProcessDefs

LocalProcessDefs:

       LocalProcessDef

       LocalProcessDefs, LocalProcessDef

LocalProcessDef:

       ProcessIdent IndexRangesopt = LocalProcess

AlphabetExtension:

       + Set

 

The scope of the name for a local process definition is the process in which it is contained. A local process is END, STOP, ERROR, a reference to another local process, a sequential composition, a conditional process or is defined using action prefix and choice.

LocalProcess:

       BaseLocalProcess

SequentialComposition

       if Expression then LocalProcess

       if Expression then LocalProcess else LocalProcess

       (  Choice )

BaseLocalProcess:

       END

       STOP

       ERROR

       ProcessIdent  Indicesopt

 

Choice:

ActionPrefix

       Choice | ActionPrefix

ActionPrefix:

       Guardopt PrefixActions -> LocalProcess

PrefixActions :

       ActionsLabels

       PrefixActions -> ActionsLabels

Guard:

       when Expression

 

Examples

       TIME = (tick -> TIME).

S = STOP + {a,b,c}.

 

       R = (a -> R | b -> Q),

       Q = STOP.

 

       P = (a[i:1..3] ->

      if i==1 then STOP else P).

 

The scope of a variable defined in an action label is the rest of the local process in which it is defined. However, the scope of a variable defined inside a set does not extend beyond that set e.g. {a, b, c[i:0..2]}. Note that variables are a syntactic convenience to permit concise definitions. The example process P above can be expanded to an equivalent definition without variables and conditionals:

P = (a[1] -> STOP | a[2] -> P | a[3] -> P).

 

In a similar way, processes with guards can be expressed by explicitly enumerating the choices that an action label set represents. For example, the process:

P = (a[i:0..3] ->

     ( when i==0 x -> STOP

     | when i!=0 y -> P

     )

   ).

 

 

is equivalent to:

P = (a[0] -> x -> STOP

   |a[1] -> y -> P

   |a[2] -> y -> P

   |a[3] -> y -> P

   ).

 

Index ranges for local processes are also a syntactic convenience. They define a set of local processes.

Indices:

       [ Expression ]

       Indices[ Expression ]

IndexRanges:

       [ Expression ]

       [ ActionRange ]

       IndexRanges[ Expression ]

       IndexRanges[ ActionRange ]

 

Example

       P         = S[0],

S[i:0..2] = (when i<3 a -> S[i+1]),

S[3]      = STOP.

 

The scope of a variable used in a local process definition is the local process i.e. it extends to the comma that terminates the definition. The example above could be defined without a variable as:

P    = S[0],

S[0] = (a -> S[1]),

S[1] = (a -> S[2]),

S[2] = (a -> S[3]),

S[3] = STOP.

 

The reference to a local process can be replaced by substituting its definition giving:

P = (a -> (a -> (a -> STOP))).

 

This is exactly equivalent to:

       P = (a -> a -> a -> STOP).

 

Variables in FSP definitions can always be removed by syntactic transformation. Consequently, in Appendix C, which presents the semantics of FSP, variables are not considered.

A sequential composition is always defined within a process. The last process in the sequential composition must be END, STOP, ERROR, or a reference to a local process. The composition essentially concatenates processes with the last (i.e. END ) state of a sequential process replaced with the first state of the subsequent process in the composition list.

SequentialComposition:

       SeqProcessList ; BaseLocalProcess

SeqProcessList:

       ProcessRef

       SeqProcessList ; ProcessRef

 

ProcessRef:

       ProcessIdent Argumentopt

Argument:

       (  ArgumentList )

ArgumentList:

       Expression

       ArgumentList , Expression

 

Examples

 

P(I=1) = (a[I]-> b[I] -> END).

 

SC = P(1);P(2);SC.

 

The process SC above is defined below without sequential composition and has exactly the same behavior.

SC = (a[1] -> b[1] -> a[2] -> b[2] -> SC).

 

1.5Composite Process

A composite process is distinguished from a primitive process by prefixing its definition with ||.  Composite processes are constructed using parallel composition, re-labeling, priority and hiding. Process labeling and sharing are specialized forms of re-labeling. The replication and conditional constructs are purely syntactic conveniences.

CompositeDef:

       ||ProcessIdent Paramopt =  CompositeBody

                                                                    Priorityopt Hidingopt .

CompositeBody:

       PrefixLabelopt ProcessRef Relabelopt

       PrefixLabelopt ( ParallelComposition ) Relabelopt

       forall Ranges CompositeBody                --replication

       if Expression then CompositeBody        --conditional

       if Expression then CompositeBody else CompositeBody

PrefixLabel :

       ActionLabels :                                  --process labeling

       ActionLabels ::                            --process sharing

       ActionLabels :: ActionLabels :

ParallelComposition:

       CompositeBody

       ParallelComposition || CompositeBody    

Priority:

       >> Set

       << Set

Ranges:

       [ ActionRange ]

       Ranges[ ActionRange ]

 

 

Examples

 

       ||S = a[1..3]:P.

       ||S = {a[1],a[2],a[3]}:P.

||S = forall[i:1..3] a[i]:P.

||S = forall[i:1..3] a:P/{a[i]/a}.

||S = (a[1]:P || a[2]:P || a[3]:P).

 

The composite process definitions above are exactly equivalent and define the same composite process. The syntax for re-labeling is described in section B.8.  The scope of a variable in a composite process is the CompositeBody in which it is defined together with any other CompositeBody contained within that CompositeBody definition.

Example

 

||S = forall[i:1..4]

        if (i<=2)then

          (forall[j:1..2] a[i][j]:P)

        else

          (forall[j:1..2] b[i][j]:P).

 

The definitions of the two occurrences of the variable j do not conflict in the above example since they are each defined in a different CompositeBody. Neither CompositeBody is contained within the other. The replication can be unfolded to give the equivalent definition for S shown below.

||S =

 ( a[1][1]:P || a[1][2]:P || a[2][1]:P || a[2][2]:P

 ||b[3][1]:P || b[3][2]:P || b[4][1]:P || b[4][2]:P

 ).

 

1.6Parameters

Process and Composite Process parameters must always have a default value. This means that a process can always be compiled into a finite Labeled Transition System (LTS). The default parameter value may be changed by an argument when the process, whether composite or primitive, forms part of a another composite process.

Param:

       ( ParameterList )        

ParameterList:

       Parameter

       ParameterList,Parameter

Parameter:

       ParameterIdent = Expression

 

Example

 

       P(X=1)   = (a[X] -> STOP).

||S(Y=2) = (P(Y+1) || P(Y+2)).

 

The scope of a parameter is the process or composite in which it is defined. Parameter substitution creates a new process with each occurrence of the parameter replaced by the argument value. This is simply macro expansion. Substituting the parameters in the example results in the following equivalent definition.

P3   = (a[3] -> STOP).

P4   = (a[4] -> STOP).

||S2 = (P3 || P4).

 

1.7Re-labeling and Hiding

The re-labeling and hiding operators can be applied to both processes and composite processes.

Relabel:

       /{ RelabelDefs }

RelabelDefs:

       RelabelDef

       RelabelDefs , RelabelDef

RelabelDef:

       ActionLabels / ActionLabels

       forall IndexRanges { RelabelDefs }

 

FSP supports relational re-labeling. The re-labeling operator applies a relation to a process, which can result in replacing many labels with a single label and replacing one label with multiple labels. The re-labeling relation is defined by a set of pairs. Each pair takes the form newlabel/oldlabel. Sets of labels and the replication construct permit the concise definition of the re-labeling relation. In each of the examples below, both the concise form and the equivalent expanded form of the relation are given.

Examples

 

       /* one to one re-labeling */

       P/{ forall[i:1..3] {a[i]/x[i]}}

       /* equivalent */

       P/{ a[1]/x[1], a[2]/x[2], a[3]/x[3] }

 

 

       /* one to many re-labeling */

       P/{ {x,y,z}/a }

       /* equivalent */

       P/{ x/a, y/a, z/a }

 

 

       /* many to one re-labeling */

       P/{ a/{x,y,z} }

       /* equivalent */

       P/{ a/x, a/y, a/z }

 

       /* many to many re-labeling */

       P/{ {a,b}/{x,y} }

       /* equivalent */

       P/{ a/x, a/y, b/x , b/y }

 

If the old label does not appear in the alphabet of P, then the re-labeling pair newlabel/oldlabel has no effect. Re-labeling in FSP is always applied before parallel composition such that for a re-labeling relation R, (P||Q)/R is equivalent to(P/R||Q/R).

Hiding:

       \ Set

       @ Set

 

There are two forms of the hiding operator: \ applies a set of labels to a process such that the labels that occur in both the alphabet of the process and the set are hidden, @ applies a set of labels to a process such that every label in the alphabet is hidden except those that occur in the set.

Prefix Matching

Actions labels in hiding sets, priority sets and on the right-hand side of a re-labeling pair match prefixes of labels in the alphabet of the process to which they are applied. For example, an action label a in a hiding set will hide all labels prefixed by a e.g. a.b, a[1], a.x.y.  Similarly, the re-labeling pair x/a would replace these labels with x.b, x[1], x.x.y.  Prefix matching permits label details to be ignored when processes are composed.

1.8Property, Progress and Menu

A safety property is defined by a process prefixed by the keyword property.

PropertyDef:

       property ProcessDef

 

There are two forms of progress property, though we have used only the simpler form in the main text of this book. The first form asserts that at least one action in a set S must occur infinitely often. The second form is conditional progress, which takes the form if C then S. This asserts that if one of the actions in the set C occurs infinitely often then so must one of the actions in the set S.

ProgressDef:

       progress ProgressIdent Rangesopt = Set

       progress ProgressIdent Rangesopt = if Set then Set

 

A set of progress properties may be declared using an index range.

Example

 

       progress G[i:1..3] = {{a,b}[i]}

 

A menu definition specifies the set of actions that the user can control in an animation.

MenuDef:

       menu MenuIdent = Set

 

1.9Expression

Expressions in FSP are a subset of expressions in Java. This has the advantage of familiarity, however it has the disadvantage that some of the FSP process operators have a different meaning when used in the context of an expression.  In particular, the priority operators << and >> mean shift left and shift right when used in an expression, the parallel composition operator || means logical or when used in an expression, the choice operator | means bit-wise or in an expression and the re-label operator / means division. Where confusion might arise, namely in constant and range definitions, expressions with the logical and shift operators must be bracketed. This is the reason why constant and range definitions are defined using SimpleExpression rather than Expression. The syntax of expressions used in FSP is specified by the following expressions.

SimpleExpression:

       AdditiveExpr

Expression:

       OrExpr

OrExpr:

       AndExpr

       OrExpr || AndExpr

AndExpr:

       BitOrExpr

       AndExpr && BitOrExpr

BitOrExpr:

       BitExclOrExpr

       BitOrExpr | BitExclOrExpr

BitExclOrExpr:

       BitAndExpr

       BitExclOrExpr ^ BitAndExpr

BitAndExpr:

       EqualityExpr

       BitAndExpr & EqualityExpr

EqualityExpr:

       RelationalExpr

       EqualityExpr == RelationalExpr

       EqualityExpr != RelationalExpr

RelationalExpr:

       ShiftExpr

       RelationalExpr < ShiftExpr

       RelationalExpr <= ShiftExpr

       RelationalExpr > ShiftExpr

       RelationalExpr >= ShiftExpr

ShiftExpr:

       AdditiveExpr

       ShiftExpr >> AdditiveExpr

       ShiftExpr << AdditiveExpr

AdditiveExpr:

       MultiplicativeExpr

       AdditiveExpr + MultiplicativeExpr

       AdditiveExpr MultiplicativeExpr

 

 

 

MultiplicativeExpr:

       unaryExpr

       MultiplicativeExpr * UnaryExpr

       MultiplicativeExpr / UnaryExpr

       MultiplicativeExpr % UnaryExpr

UnaryExpr:

       BaseExpr

       + BaseExpr

       - BaseExpr

       ! BaseExpr

BaseExpr:        

       IntegerLiteral

       Variable

       ConstantIdent

       'ActionLabel

       # SetIdent

       @( SetIdent , Expression )

       (Expression )

 

FSP supports only integer and label expressions. Variables may take either an integer value or a label value. Label literals are formed by preceding an action label with a quote – this distinguishes a label value from a variable. The only valid operators on label values are equality and inequality.

The expression @(Ae) returns a label value which is the eth element of the set identified by A.

The expression # A, returns as an integer value the cardinality of the set identified by A.

As in the programming language C, the results of boolean expressions in FSP are integer values. A false expression has the value 0 and a true expression the value 1.

 

1.10Basic FSP

In the previous sections, we have indicated that constructs such as guards, replicators, conditionals, variables and index ranges are syntactic conveniences to permit concise descriptions. Models described using these constructs can be syntactically transformed into a more basic form of FSP. This basic form of FSP uses only the process operators and the primitive local processes END, STOP and ERROR. The syntax of basic FSP is described by the following productions:

BProcessDef:

       BProcessBody  AlphabetExtensionopt  Relabelopt  Hidingopt .

BProcessBody :

       ProcessIdent = BLocalProcess

       BProcessBody , ProcessIdent = BLocalProcess

BLocalProcess:

               BBaseProcess

       ( BChoice )

BBaseProcess:

END

STOP

       ERROR

       ProcessIdent

ProcessIdent ; BBaseProcess

BChoice:

       ActionLabel -> BLocalProcess

       BChoice | ActionLabel -> BLocalProcess

 

BCompositeDef:

       ||ProcessIdent =  BCompositeBody Priorityopt Hidingopt .

BCompositeBody:

       ProcessIdent Relabelopt

       ( BParallelComposition ) Relabelopt

BParallelComposition:

       BCompositeBody

       BParallelComposition || BCompositeBody    

 

A formal semantics for basic FSP is presented in Appendix C.

 

1.11fluent and assert

Fluents used in linear temporal logic expressions are defined by two sets of action labels and an optional initialization expression that determines whether the fluent is initially true or false. The sets may be singletons, in which case a single action label may be defined. If initialization is omitted, by default, the fluent is initially false. A set of fluents may be declared using an index range.

FluentDef:

               fluent FluentIdent IndexRangesopt

= < ActionLabels , ActionLabels > Initiallyopt

Initially:

       initially SimpleExpression

 

Example

 

       fluent Simple        = <a,b>

       fluent Sets        = <{start,begin},{end,finish}>

       fluent Indexed[i:1..8]

                         = <a[i],b[i]> initially (i%2==0)

 

Assertions define properties expressed in Fluent Linear Temporal Logic (FLTL). Assertions are named FLTL formulae and they may be parameterized and used in the definition of more complex properties.

AssertDef:

       assert AssertIdent Paramopt = FLTLUnaryExpression

 

 

FLTLOrExpr:

       FLTLBinaryExpr

       FLTLOrExpr ||  FLTLBinaryExpr

FLTLBinaryExpr:

       FLTLAndExpr

       FLTLBinaryExpr U     FLTLAndExpr                  -- until

       FLTLBinaryExpr W   FLTLAndExpr                -- weak until

       FLTLBinaryExpr ->   FLTLAndExpr                -- implication

FLTLBinaryExpr <-> FLTLAndExpr                -- equivalence

FLTLAndExpr:

       FLTLUnaryExpr

       FLTLAndExpr && FLTLUnaryExpr

FLTLUnaryExpr:

       FLTLBaseExpr

       ! FLTLUnaryExpr        -- negation

X FLTLUnaryExpr        -- next time

<> FLTLUnaryExpr        -- eventually

[] FLTLUnaryExpr        -- always

forall Ranges FLTLUnaryExpr        

exists Ranges FLTLUnaryExpr

FLTLBaseExpr:

FluentIdent Rangesopt

       ActionLabels

AssertIdent Argumentopt

       rigid SimpleExpression

       ( FLTLOrExpr )                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    

 

Uppercase identifiers in FLTL expressions refer either to fluent or assertion definitions. Lower case identifiers refer to action labels. Where a set of action labels is used, this means the disjunction of the fluents representing each individual action. The simple expression introduced by the keyword rigid is a Boolean expression that must evaluate to either 0 false or 1 true.