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.


       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        


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  














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.














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 Letter

       UpperCaseIdentifier Digit



       LowerCaseIdentifier Letter

       LowerCaseIdentifier Digit




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

       [ Expression ]

       ActionLabel [ Expression ]


       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).




       [ 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.




       Variable : Range

       Variable : Set



       Expression .. Expression



       { SetElements }



       SetElements , ActionLabels



       {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.


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


1.3const, range, set

Named constants, ranges and sets are defined as follows:


       const ConstantIdent = SimpleExpression


       range RangeIdent = SimpleExpression.. SimpleExpression


       set SetIdent   = { setElements }




       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.


       ProcessIdent  Paramopt = ProcessBody

AlphabetExtensionopt  Relabelopt  Hidingopt .



       LocalProcess , LocalProcessDefs



       LocalProcessDefs, LocalProcessDef


       ProcessIdent IndexRangesopt = LocalProcess


       + 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.




       if Expression then LocalProcess

       if Expression then LocalProcess else LocalProcess

       (  Choice )





       ProcessIdent  Indicesopt




       Choice | ActionPrefix


       Guardopt PrefixActions -> LocalProcess

PrefixActions :


       PrefixActions -> ActionsLabels


       when Expression



       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.


       [ Expression ]

       Indices[ Expression ]


       [ Expression ]

       [ ActionRange ]

       IndexRanges[ Expression ]

       IndexRanges[ ActionRange ]



       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.


       SeqProcessList ; BaseLocalProcess



       SeqProcessList ; ProcessRef



       ProcessIdent Argumentopt


       (  ArgumentList )



       ArgumentList , Expression




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.


       ||ProcessIdent Paramopt =  CompositeBody

                                                                    Priorityopt Hidingopt .


       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    


       >> Set

       << Set


       [ ActionRange ]

       Ranges[ ActionRange ]





       ||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.



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

        if (i<=2)then

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


          (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




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.


       ( ParameterList )        





       ParameterIdent = Expression




       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.


       /{ RelabelDefs }



       RelabelDefs , 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.



       /* 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).


       \ 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.


       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.


       progress ProgressIdent Rangesopt = Set

       progress ProgressIdent Rangesopt = if Set then Set


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



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


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


       menu MenuIdent = Set



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.







       OrExpr || AndExpr



       AndExpr && BitOrExpr



       BitOrExpr | BitExclOrExpr



       BitExclOrExpr ^ BitAndExpr



       BitAndExpr & EqualityExpr



       EqualityExpr == RelationalExpr

       EqualityExpr != RelationalExpr



       RelationalExpr < ShiftExpr

       RelationalExpr <= ShiftExpr

       RelationalExpr > ShiftExpr

       RelationalExpr >= ShiftExpr



       ShiftExpr >> AdditiveExpr

       ShiftExpr << AdditiveExpr



       AdditiveExpr + MultiplicativeExpr

       AdditiveExpr MultiplicativeExpr






       MultiplicativeExpr * UnaryExpr

       MultiplicativeExpr / UnaryExpr

       MultiplicativeExpr % UnaryExpr



       + BaseExpr

       - BaseExpr

       ! BaseExpr






       # 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:


       BProcessBody  AlphabetExtensionopt  Relabelopt  Hidingopt .

BProcessBody :

       ProcessIdent = BLocalProcess

       BProcessBody , ProcessIdent = BLocalProcess



       ( BChoice )






ProcessIdent ; BBaseProcess


       ActionLabel -> BLocalProcess

       BChoice | ActionLabel -> BLocalProcess



       ||ProcessIdent =  BCompositeBody Priorityopt Hidingopt .


       ProcessIdent Relabelopt

       ( BParallelComposition ) Relabelopt



       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.


               fluent FluentIdent IndexRangesopt

= < ActionLabels , ActionLabels > Initiallyopt


       initially SimpleExpression




       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.


       assert AssertIdent Paramopt = FLTLUnaryExpression





       FLTLOrExpr ||  FLTLBinaryExpr



       FLTLBinaryExpr U     FLTLAndExpr                  -- until

       FLTLBinaryExpr W   FLTLAndExpr                -- weak until

       FLTLBinaryExpr ->   FLTLAndExpr                -- implication

FLTLBinaryExpr <-> FLTLAndExpr                -- equivalence



       FLTLAndExpr && FLTLUnaryExpr



       ! FLTLUnaryExpr        -- negation

X FLTLUnaryExpr        -- next time

<> FLTLUnaryExpr        -- eventually

[] FLTLUnaryExpr        -- always

forall Ranges FLTLUnaryExpr        

exists Ranges FLTLUnaryExpr


FluentIdent Rangesopt


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.