SpecList := Spec | SpecList Spec;

Spec := Configuration | Style;

Style := "Style" SimpleName

            [ “Import Lattice” LatticeName LatticeFileName ]

                        [ TypeList ]

         [ "Constraints"

                    [ ConstraintExpression ] ]

         "End Style";

LatticeFileName := AFilePath;

TypeList := Type | TypeList Type ;

Type := Component | Connector | InterfaceType | GeneralProcess;

Component := "Component" SimpleName [ '(' FormalCCParams ')' ]

                         [ PortList ]

                         "Computation" BehaviorDescription;

Connector := "Connector" SimpleName [ '(' FormalCCParams ')' ]

                         [ RoleList ]

                         "Glue" BehaviorDescription;

PortList := Port | PortList Port;

Port := "Port" FormalPRName '=' ProcessExpression;

RoleList := Role | RoleList Role;

Role := "Role" FormalPRName '=' ProcessExpression;

Configuration := "Configuration" SimpleName

                                [ “Import Lattice” LatticeName LatticeFileName ]

                         [ "Style" SimpleName ]

                         [ TypeList ]

                         "Instances"

                                 [ InstanceList ]

                                  [   “Clearances”

                                     [ClearanceLists]   ]

                         "Attachments"

                                 [ AttachmentList ]

                         "End Configuration";

InstanceList := Instance | InstanceList Instance;

Instance := InstanceNameList ':' TypeUse;

InstanceNameList := InstanceName | InstanceNameList ‘,’ InstanceName;

InstanceName := SimpleName [ “_{“ FiniteRangeExpression ‘}’ ];

TypeUse := SimpleName [ '(' ActualCCParams ')' ];

ClearanceLists := ClearanceList | ClearanceLists ClearanceList;

ClearanceList := SubjectList ‘:’ Clearance;

SubjectList := aSubject | SubjectList ‘,’ aSubject;

aSubject := ComponentConnectorName | PortRoleName ;

FiniteRangeExpressionOrIndex := FiniteRangeExpression | IntegerExpression;

ComponentConnectorName := SimpleName [ "_{" FiniteRangeExpressionOrIndex "_}" ];

PortRoleName := ComponentConnectorName '.' SimpleName [ "_{" FiniteRangeExpressionOrIndex "_}" ];

Clearance := SimpleName;

AttachmentList := Attachment | AttachmentList Attachment;

Attachment : Interface "As" Interface;

Interface : SimpleName [ "_{" IntegerExpression '}' ] '.' ActualPRName;

InterfaceType := "Interface Type" ProcessName  '='  ProcessExpression;

GeneralProcess := "Process" ProcessName '=' ProcessExpression;

--

-- Names and Lists

--

-- IDENTIFIER is a terminal representing an arbitrary name.  Such names can contain

--   an combination of letters and digits, but must begin with a letter.  Spaces

--   underscores are not permitted in names.

--

SimpleName := IDENTIFIER;

ProcessName := SimpleName [ "_{" ProcessParams '}' ]

AlphabetName := "ALPHA" SimpleName;

DefnName := ProcessName | AlphabetName;

NameList := SimpleName | NameList ',' SimpleName;

ElementList := DataExpression | ElementList ',' DataExpression;

FormalPRName := SimpleName [ "_{" FiniteRangeExpression  '}' ];

ActualPRName := SimpleName [ "_{" IntegerExpression '}' ];

EventName := [ ActualPRName '.' ] SimpleName

BehaviorDescription :=   '=' ProcessExpression

                                   | Subconfiguration;

Subconfiguration := Configuration

                    "Bindings"

                          [ BindingList ]

                    "End Bindings"

BindingList := Binding | BindingList Binding;

Binding := Interface '=' ActualPRName;

DeclList := Declaration | DeclList Declaration;

Declaration :=

              DefnName '=' AnyExpression

            | DefnName '=' "Cond" '{' ConditionalDefinitions '}'

ConditionalDefinitions =

              ConditionalDefinition

            | ConditionalDefinitions ConditionalDefinition

ConditionalDefinition =

              ProcessExpression "When" '{' LogicalExpression '}'

            | ProcessExpression "Otherwise"

--

-- types of parameters (formal and actual for use in various rules)

--   The NL variant of ForamlParams allows lists of parameters, but each parameter

--   of the same type must be specified separately instead of in a list of the same

--   type (eg, "i,j:X" is not permitted; instead "i:X; j:X" would have to be used).

--

FormalParams := FormalParam | FormalParams ';' FormalParam;

FormalParam  := NameList ':' SetExpression;

FormalParamsNL := FormalParamNL | FormalParamsNL ';' FormalParamNL;

FormalParamNL  := SimpleName ':' SetExpression;

ProcessParams :=  AnyExpression | ProcessParams ',' AnyExpression;

FormalCCParams := FormalCCParam | FormalCCParams ';' FormalCCParam;

FormalCCParam  := NameList ':' ProcessType | NameList ':' FiniteRangeExpression                

                  | NameList ‘:’ “Security Label”;

ActualCCParams := ActualCCParam | ActualCCParams ',' ActualCCParam;

ActualCCParam  := ProcessExpression | IntegerExpression | LatticeFunction;

LatticeFunction := LatticeName ‘.’ FunctionName ;

FunctionName := “meet” ‘(‘ SetOfNodes ‘)’ | “join” ‘(‘ SetOfNodes ‘)’ | “max()” | “min()”;

SetOfNodes := NodeName ‘,’ NodeList;

NodeList := NodeName | NodeList ‘,’ NodeName;

NodeName :=IDENTIFIER;

LatticeName := SimpleName;

--

-- types of expresssions

--

ProcessType :=

      "Interface Type"

    | "Process"

    | "Port"

    | "Role"

    | "Computation"

    | "Glue";

ProcessExpression :=       ProcessExpression ';' ProcessExpression

                                                | ProcessExpression "/\" ProcessExpression

                         | EventExpression "->" ProcessExpression

                         | ProcessExpression "||" ProcessExpression

                                                | ProcessExpression "|||" ProcessExpression

                         | ProcessExpression "[]" ProcessExpression

                         | ProcessExpression "|~|" ProcessExpression

                         | "[]" FormalParams  '@' ProcessExpression

                         | "|~|" FormalParams '@' ProcessExpression

                         | ';' FormalParams   '@' ProcessExpression

                         | "||" FormalParams  '@' ProcessExpression

                                                | "|||" FormalParams '@' ProcessExpression

                                                | ToolAnnotation

                         | ProcessName

                         | "Computation"

                         | "Glue"

                                                | "Success"

                                                | "Skip"

                                                | "Stop"

                         | ProcessExpression "Where" '{' DeclList '}'

                         | '(' ProcessExpression ')';

ToolAnnotation :=

              "diamond" '(' ProcessExpression ')'

            | "normalise" '(' ProcessExpression ')';

EventExpression :=  '_' EventName [ EventDataList ]

                           | EventName [ EventDataList ];

EventDataList :=  EventDataList '?' NonEventDataExpression

                        | EventDataList '!' NonEventDataExpression

                        | '?' NonEventDataExpression

                        | '!' NonEventDataExpression;

LogicalExpression :=       "not" LogicalExpression

                         | LogicalExpression "or" LogicalExpression

                         | LogicalExpression "and" LogicalExpression

                         | "forall" FormalParams '@' LogicalExpression

                         | "forall" FormalParams '|' LogicalExpression '@' LogicalExpression

                         | "exists" FormalParams '@' LogicalExpression

                         | "exists" FormalParams '|' LogicalExpression '@' LogicalExpression

                                                | NonEventDataExpression "==" NonEventDataExpression

                                                | NonEventDataExpression "!=" NonEventDataExpression

                         | IntegerExpression '<' IntegerExpression

                         | IntegerExpression '>' IntegerExpression

                         | IntegerExpression "<=" IntegerExpression

                         | IntegerExpression ">=" IntegerExpression

                         | DataExpression "in" SetExpression

                         | DataExpression "notin" SetExpression

                                                | "true"

                                                | "false"

                         | LogicalExpression "Where" '{' DeclList '}'

                         | '(' LogicalExpression ')';

-- This introduces a lot of new possibilities and needs extensive work.

ConstraintExpression := LogicalExpression;

SetExpression :=           SetExpression "union" SetExpression

                         | SetExpression "intersection" SetExpression

                         | SetExpression "setminus" SetExpression

                         | SetExpression "cross" SetExpression

                         | "power" SetExpression

                                                | "sequence" SetExpression

                         | '{' ElementList '}'

                         | '{' FormalParamsNL [ '|'  LogicalExpression ] [ '@' DataExpression]  '}'

                                                | RangeExpression

                                                | SimpleName

                                                | AlphabetName

                                                | "Integer"

                                                | "{}"

                         | SetExpression "Where" '{' DeclList '}'

                                                | '(' SetExpression ')';

SequenceExpression :=

                                      '<' ElementList '>'

                                    | SequenceExpression '^' SequenceExpression

                                    | SimpleName

                                    | "<>"

                   | SequenceExpression "Where" '{' DeclList '}'

                                    | '(' SequenceExpression ')';

IntegerExpression :=       IntegerExpression '+' IntegerExpression

                         | IntegerExpression '-' IntegerExpression

                         | SimpleName

                         | INTEGER

                         | IntegerExpression "Where" '{' DeclList '}'

                         | '(' IntegerExpression ')';

RangeExpression :=         IntegerExpression ".." IntegerExpression

                         | IntegerExpression ".."

                         | ".." IntegerExpression;

FiniteRangeExpression := IntegerExpression ".." IntegerExpression

TupleExpression :=  '(' DataExpression ',' DataExpression ')';

NonEventDataExpression :=

              SetExpression

            | IntegerExpression

            | SequenceExpression

            | LogicalExpresssion

            | TupleExpression;

DataExpression := EventExpression | NonEventDataExpression;

AnyExpression :=  ProcessExpression | DataExpresssion;