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.
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
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
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}]
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]}
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).
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 ).
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).
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.
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
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 @(A, e) 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.
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.
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.
|