Copper Specification Grammar
- Comments are C/C++ style
- Basics
- Expressions
- Additional Information About C Procedures
- FSP Productions
- LTL Productions
- Top-Level Specification Productions
Comments are C/C++ style
comment : /* ... */ | // ...Basics
identifier : lower_id | upper_id | dummy_varint_constant : integer constant
string_literal : string literal
lower_id : identifier beginning with lower-case letter
upper_id : identifier beginning with upper-case letter
dummy_var : dummy variable beginning with a "$"
Back To Top
Expressions
primary_expression: identifier
| int_constant
| string_literal
| "(" expression ")"
postfix_expression
: primary_expression
| postfix_expression "[" expression "]"
| postfix_expression "(" ")"
| postfix_expression "(" argument_expression_list ")"
| postfix_expression "." identifier
| postfix_expression "->" identifier
| postfix_expression "++"
| postfix_expression "--"
argument_expression_list
: assignment_expression
| argument_expression_list "," assignment_expression
unary_expression
: postfix_expression
| "++" unary_expression
| "--" unary_expression
| unary_operator cast_expression
| "sizeof" unary_expression
| "sizeof" "(" type_name ")"
unary_operator : "&" | "*" | "+" | "-" | "~" | "!"
cast_expression
: unary_expression
| "(" type_name ")" cast_expression
| "(" type_name ")" list_initializer
multiplicative_expression
: cast_expression
| multiplicative_expression "*" cast_expression
| multiplicative_expression "/" cast_expression
| multiplicative_expression "%" cast_expression
additive_expression
: multiplicative_expression
| additive_expression "+" multiplicative_expression
| additive_expression "-" multiplicative_expression
shift_expression
: additive_expression
| shift_expression "<<" additive_expression
| shift_expression ">>" additive_expression
relational_expression
: shift_expression { $$ = $1; }
| relational_expression "<" shift_expression
| relational_expression ">" shift_expression
| relational_expression "<=" shift_expression
| relational_expression ">=" shift_expression
equality_expression
: relational_expression
| equality_expression "==" relational_expression
| equality_expression "!=" relational_expression
and_expression
: equality_expression
| and_expression "&" equality_expression
exclusive_or_expression
: and_expression
| exclusive_or_expression "^" and_expression
inclusive_or_expression
: exclusive_or_expression
| inclusive_or_expression "|" exclusive_or_expression
logical_and_expression
: inclusive_or_expression
| logical_and_expression "&&" inclusive_or_expression
logical_or_expression
: logical_and_expression
| logical_or_expression "||" logical_and_expression
conditional_expression
: logical_or_expression
| logical_or_expression "?" ":" conditional_expression
| logical_or_expression "?" expression ":" conditional_expression
assignment_expression
: conditional_expression
| unary_expression assignment_operator assignment_expression
assignment_operator : "=" | "*=" | "/=" | "%=" | "+=" | "-=" | "<<=" | ">>=" | "&=" | "^=" | "|="
expression
: assignment_expression
| expression "," assignment_expression
constant_expression : conditional_expression
Back To Top
Additional Information About C Procedures
procedure_name : postfix_expressioncomponent
/*single name*/
: procedure_name
/*two names - second name to be substituted - ignore this for now*/
| procedure_name "|" procedure_name
component_list
/*name*/
: component
/*list*/
| component_list "," component
inline_list
/*name*/
: procedure_name
/*list*/
| inline_list "," procedure_name
program_info
: "program" component_list "{" program_decls "}"
| "program" component_list "{" "}"
program_decls
: program_decl
| program_decls program_decl
program_decl
: "specification" identifier "," "{" argument_expression_list "}" "," process_id ";"
| "specification" identifier "," "{" argument_expression_list "}" "," ltl_formula_name ";"
procedure_info
: "procedure" procedure_name "{" procedure_decls "}"
| "procedure" procedure_name "{" "}"
procedure_decls
/*pred*/
: predicate_decl
/*pred_list*/
| procedure_decls predicate_decl
/*fair_loop*/
| fair_loop_decl
/*fair_loop_list*/
| procedure_decls fair_loop_decl
/*aux*/
| auxiliary_decl
/*aux_list*/
| procedure_decls auxiliary_decl
/*inline*/
| inline_decl
/*inline_list*/
| procedure_decls inline_decl
/*alias*/
| alias_decl
/*alias_list*/
| procedure_decls alias_decl
/*abstract*/
| abstract_decl
/*abstract_list*/
| procedure_decls abstract_decl
/*context*/
| context_decl
/*context_list*/
| procedure_decls context_decl
predicate_decl : "predicate" predicate_list ";"
fair_loop_decl : "fair_loop" predicate_list ";"
auxiliary_decl : "auxiliary" predicate_list ";"
predicate_list
/*pred*/
: conditional_expression
/*list*/
| predicate_list "," conditional_expression
inline_decl : "inline" inline_list ";"
alias_decl : "alias" alias_item_list ";"
alias_item_list
: alias_item
| alias_item_list "," alias_item
alias_item
: "{" conditional_expression "," points_to_list "}"
points_to_list
/*name*/
: conditional_expression
/*list*/
| points_to_list "," conditional_expression
abstract_decl
: "abstract" abstract_item_list ";"
abstract_item_list
: abstract_item
| abstract_item_list "," abstract_item
abstract_item
: "{" conditional_expression "," process_id "}"
context_decl : "context" int_constant ";"
Back To Top
FSP Productions
process_id : upper_idaction_label
/*id*/
: lower_id
/*normal return*/
| "return" "{" conditional_expression "}"
/*void return*/
| "return" "{" "}"
/*assign*/
| "{" conditional_expression "=" "[" conditional_expression "]" "}"
/*broadcast*/
| lower_id "!!" "[" predicate_list "]"
/*void send*/
| lower_id "!" "[" "]"
/*send*/
| lower_id "!" "[" predicate_list "]"
/*void receive*/
| lower_id "?" "[" "]"
/*receive*/
| lower_id "?" "[" predicate_list "]"
action_label_list
: action_label
| action_label_list "," action_label
action_labels
/*action*/
: action_label
process_definition
: process_id "=" process_body "."
| process_id "=" process_body "+" "{" action_label_list "}" "."
process_body
/*local*/
: local_process
/*list*/
| local_process "," local_process_defs
local_process_defs
/*local*/
: local_process_def
/*list*/
| local_process_defs "," local_process_def
local_process_def : process_id "=" local_process
local_process
/*stop*/
: "STOP"
/*id*/
| process_id
/*choice*/
| "(" process_choice ")"
process_choice
/*action*/
: action_prefix
/*choice*/
| process_choice "|" action_prefix
action_prefix : prefix_actions PTR_OP local_process
prefix_actions
/*action*/
: action_labels
/*prefix*/
| prefix_actions "->" action_labels
prop_label
: process_id "=" "{" predicate_list "}" "{" predicate_list "}" ";"
| process_id "=" "{" predicate_list "}" "{" "}" ";"
| process_id "=" "{" "}" "{" predicate_list "}" ";"
fsp_definition
/*process*/
: process_definition
/*propositional_labeling*/
| prop_label
Back To Top
LTL Productions
ltl_formula_name : upper_id primary_ltl_formula: "[" conditional_expression "]"
| action_label
| "(" ltl_formula ")"
unary_ltl_formula
: primary_ltl_formula
| "!" unary_ltl_formula
| "#X" unary_ltl_formula
| "#G" unary_ltl_formula
| "#F" unary_ltl_formula
and_ltl_formula
: unary_ltl_formula
| and_ltl_formula "&" unary_ltl_formula
or_ltl_formula
: and_ltl_formula
| or_ltl_formula "|" and_ltl_formula
until_ltl_formula
: or_ltl_formula
| until_ltl_formula "#U" or_ltl_formula
release_ltl_formula
: until_ltl_formula
| release_ltl_formula "#R" until_ltl_formula
implies_ltl_formula
: release_ltl_formula
| release_ltl_formula "=>" implies_ltl_formula
ltl_formula : implies_ltl_formula
ltl_formula_def : "ltl" ltl_formula_name "{" ltl_formula ";" "}"
Back To Top
Top-Level Specification Productions
ext_def_list/*fsp*/
: fsp_definition
/*list_fsp*/
| ext_def_list fsp_definition
/*ltl*/
| ltl_formula_def
/*list_ltl*/
| ext_def_list ltl_formula_def
/*program*/
| program_info
/*list_program*/
| ext_def_list program_info
/*procedure*/
| procedure_info
/*list_procedure*/
| ext_def_list procedure_info
spec_translation_unit : ext_def_list
Back To Top