FSP Syntax reference
Identifiers starting with a lower case letter are used for action label names and range variables. Identifiers starting with an upper case letter are used for process names, range names, constant names and process parameter names.
upper_identifier ::= uppercase_letter { letter | digit }
lower_identifier ::= lowercase_letter { letter | digit }
Reserved words: const, property, range, if, then, else, forall, when
Predefined local process identifiers: ERROR, STOP
constant_declaration ::= const upper_identifier "=" integer_value
Example: const TRUE = 1
range_declaration ::= range upper_identifier "=" lower_bound_expression ".." upper_bound_expression
Example: range BIT = 0..1, range BOOL = FALSE..TRUE
index ::= "[" expression "]"
range ::= range_declaration_identifier | lower_bound_expression ".." upper_bound_expression
range_declaration_identifier ::= upper_identifier
index_range ::= "[" [ lower_identifier ":" ] range "]"
index_label ::= index | index_range
index_labels::= index_label { index_label }
Examples: [1], [i * 2], [1..2], [i:0..5]
simple_action_label ::= lower_identifier | index_labels
action_label ::= simple_action_label { "." simple_action_label }
action_label_set ::= "{" action_label { "," action_label } "}"
Examples: tick, coord[1][2], buff.out, buff.in[x:0..1], {a,b,c,d}
A label of the form a[0..2]
is exactly equivalent to the label set {a[0], a[1], a[2]}
primitive_process :: = upper_identifier [ "(" parameter_list ")" ] "=" primitive_process_body
primitive_process_body ::= process_body { "," local_process_defn } [alphabet_extension] [relabels] [label_visibility]"."
local_process_name ::= upper_identifier [ index ] | STOP | ERROR
process_body ::= "(" choices ")" | local_process_name | conditional
choices ::= choice { "|" choice }
choice ::= [when boolean_expression ] action_label_part "
->" process_bodyaction_label_part ::= action_label | action_label_set
conditional ::= if boolean_expression then process_body [ else process_body ]
local_process_defn::= upper_identifier ["@"][ index | index_range ] "=" process_body
parameter_list ::= parameter {"," parameter }
parameter ::= upper_identifier "=" integer_value
alphabet_extension ::= "+" action_label_set
label_visibility::= hide_label | expose_label
hide_label ::= "\" action_label_set
relabels::="/" relabel_set
relabel_set ::= "{" relabel { "," relabel } "}"
relabel::= simple_relabel | forall index_range relabel_set
simple_relabel ::= action_label "/" action_label
composite_process ::=
"||" upper_identifier [ "(" parameter_list ")" ] "=" composite_body [relabels] [label_visibility] "."
composite_body ::= process_instance | parallel_list | composite_conditional | composite_replicator
composite_replicator ::= forall index_range composite_body
composite_conditional ::= if boolean_expression then composite_body [ else composite_body]
parallel_list ::= "(" composite_body { "||" composite_body } ")"
process_instance ::= [action_label_set "::"][action_label ":" ] upper_identifier
[ "(" actual_parameter_list ")" ] [relabels]
actual_parameter_list ::= expression { "," expression }
property_automata ::= property primitive_process
specification ::= { constant_declaration | primitive_process | composite_process | property_automata }