Mocha

Reactive modules grammar

Table of contents

  1. Syntax
    1. Constants
    2. Types
    3. Expressions
    4. Guarded commands
    5. Atoms
    6. Modules
    7. Module expressions
  2. Semantics
    1. Constants
    2. Types
    3. Expressions
    4. Guarded commands
    5. Atoms
    6. Modules
    7. Module expressions
  3. Preprocessor

3. Syntax

Keywords:

const, type, is, event, bool, bitvector, if, then, else, fi, true, false, inc, dec, by, inv, shiftright, shiftleft, and, or, exor, atom, lazy, controls, reads, awaits, init, update, initupdate, external, interface, private, module, hide, in, array, of, forall, forsome, forindex, max, compose, parameter, nondet, default

Tokens:
id any nonempty, case-sensitive string of letters followed by a possibly empty string of digits, so that 'id' is not a keyword
num any nonempty string of digits
bitstring "#" followed by any nonempty string of "0"s and "1"s 

def-list
  : def-list def 
  | 
  ;

def 
  : const-def 
  | type-def 
  | module-def
  ;

3.1. Constants

const-def 
  : "const" id 
  ;

3.2. Types

type-def 
  : "type" id "is" type-decl 
  ;

type-decl 
  : simp-type-decl 
  | array-type-decl 
  ;

simp-type-decl 
  : event-type-decl 
  | index-type-decl 
  ;

index-type-decl 
  : bool-type-decl 
  | enum-type-decl 
  | range-type-decl
  | bitvector-type-decl 
  ;

event-type-decl 
  : id 
  | "event" 
  ;

bool-type-decl 
  : id 
  | "bool" 
  ;

enum-type-decl 
  : id 
  | "{" nonempty-enum-val-list "}" 
  ;

nonempty-enum-val-list 
  : nonempty-enum-val-list "," enum-val 
  | enum-val 
  ;

enum-val 
  : id 
  | num
  | bitstring 
  ;

range-type-decl 
  : id 
  | "(" "0" ".." num ")" 
  ;

bitvector-type-decl 
  : id 
  | "bitvector" range-type-decl 
  ;

array-type-decl 
  : id
  | "array" index-type-decl "of" simp-type-decl
  ;

3.3. Expressions

bool-exp 
  : paren-bool-exp
  | enum-pred
  | range-pred 
  | bitvector-pred 
  | array-pred
  | "~" paren-bool-exp 
  | and-bool-exp 
  | or-bool-exp 
  | equiv-bool-exp 
  | exor-bool-exp 
  ;

and-bool-exp 
  : and-bool-exp "&" paren-bool-exp 
  | paren-bool-exp "&" paren-bool-exp 
  ;

or-bool-exp 
  : or-bool-exp "|" paren-bool-exp 
  | paren-bool-exp "|" paren-bool-exp 
  ;

equiv-bool-exp 
  : equiv-bool-exp "=" paren-bool-exp 
  | paren-bool-exp "=" paren-bool-exp 
  ;

exor-bool-exp 
  : exor-bool-exp "~=" paren-bool-exp 
  | paren-bool-exp "~=" paren-bool-exp 
  ;

paren-bool-exp 
  : atomic-bool-exp 
  | "(" bool-exp ")" 
  | "if" bool-exp "then" bool-exp "else" bool-exp "fi" 
  ;

atomic-bool-exp 
  : id 
  | id "'" 
  | id "?" 
  | bool-val
  | paren-bitvector-exp "[" range-exp "]" 
  | array-bool-exp 
  ;

array-bool-exp 
  : id "[" index-exp "]"
  | id "'" "[" index-exp "]"
  | id "[" index-exp "]" "?"
  ;

bool-val
  : "true"
  | "false"
  ;

enum-pred 
  : paren-enum-exp "=" 
  | paren-enum-exp "~=" paren-enum-exp 
  ;

enum-exp 
  : paren-enum-exp 
  ;

paren-enum-exp 
  : atomic-enum-exp 
  | "(" enum-exp ")"
  | "if" bool-exp "then" enum-exp "else" enum-exp "fi" 
  ;

atomic-enum-exp 
  : id 
  | id "'" 
  | enum-val 
  | array-enum-exp 
  ;

array-enum-exp 
  : id "[" index-exp "]"
  | id "'" "[" index-exp "]"
  ;

range-pred 
  : paren-range-exp "=" paren-range-exp 
  | paren-range-exp "~=" paren-range-exp 
  | paren-range-exp ">" paren-range-exp 
  | paren-range-exp "<" paren-range-exp 
  | paren-range-exp ">=" paren-range-exp 
  | paren-range-exp "<=" paren-range-exp 
  ;

range-exp 
  : paren-range-exp 
  | "inc" paren-range-exp "by" paren-range-exp 
  | "dec" paren-range-exp "by" paren-range-exp 
  ;

paren-range-exp 
  : atomic-range-exp 
  | "(" range-exp ")"
  | "if" bool-exp "then" range-exp "else" range-exp "fi"
  ;

atomic-range-exp 
  : id 
  | id "'" 
  | range-val
  | array-range-exp 
  ;

array-range-exp 
  : id "[" index-exp "]"
  | id "'" "[" index-exp "]"
  ;

range-val
  : num
  | num "(" "max" num ")"
  ;

bitvector-pred 
  :
  | paren-bitvector-exp "=" paren-bitvector-exp 
  | paren-bitvector-exp "~=" paren-bitvector-exp 
  | paren-bitvector-exp ">" paren-bitvector-exp 
  | paren-bitvector-exp "<" paren-bitvector-exp 
  | paren-bitvector-exp ">=" paren-bitvector-exp 
  | paren-bitvector-exp "<=" paren-bitvector-exp 
  ;

bitvector-exp 
  : paren-bitvector-exp
  | "inv" paren-bitvector-exp 
  | "shiftright" paren-bitvector-exp "by" paren-range-exp 
  | "shiftleft" paren-bitvector-exp "by" paren-range-exp 
  | and-bitvector-exp 
  | or-bitvector-exp 
  | exor-bitvector-exp 
  ;

and-bitvector-exp 
  : and-bitvector-exp "and" paren-bitvector-exp 
  | paren-bitvector-exp "and" paren-bitvector-exp 
  ;

or-bitvector-exp 
  : or-bitvector-exp "or" paren-bitvector-exp 
  | paren-bitvector-exp "or" paren-bitvector-exp 
  ;

exor-bitvector-exp 
  : exor-bitvector-exp "exor" paren-bitvector-exp 
  | paren-bitvector-exp "exor" paren-bitvector-exp 
  ;

paren-bitvector-exp 
  : atomic-bitvector-exp 
  | "(" bitvector-exp ")"
  | "if" bool-exp "then" bitvector-exp "else" bitvector-exp "fi"
  ;

atomic-bitvector-exp 
  : id 
  | id "'" 
  | bitvector-val
  | array-bitvector-exp 
  ;

array-bitvector-exp 
  : id "[" index-exp "]"
  | id "'" "[" index-exp "]"
  ;

bitvector-val
  : bitstring 
  ;

array-pred 
  : array-exp "=" array-exp
  | array-exp "~=" array-exp
  | "{" "forall" id "in" index-type-decl ":" bool-exp "}"
  | "{" "forsome" id "in" index-type-decl ":" bool-exp "}"
  ;

array-exp
  : id
  | id "'"
  ;

index-exp
  : bool-exp
  | enum-exp
  | range-exp
  | bitvector-exp
  ;

3.4. Guarded commands

default-guarded-cmd 
  : guarded-cmd default-assign-list 
  ;

guarded-cmd 
  : guarded-cmd guarded-assign-list 
  | 
  ;

guarded-assign-list 
  : "[]" bool-exp "->" assign-list 
  ;

default-assign-list 
  : "[]" "default" "->" assign-list 
  | 
  ;

assign-list 
  : nonempty-assign-list 
  | nonempty-assign-list ";"
  | 
  ;

nonempty-assign-list 
  : nonempty-assign-list ";" assign 
  | assign 
  ;

assign 
  : event-assign
  | bool-assign 
  | enum-assign 
  | range-assign
  | bitvector-assign 
  | array-event-assign
  | array-assign
  ;

event-assign
  : id "!"
  | id "[" index-exp "]" "!"
  ;

bool-assign 
  : bool-assign-lhs ":=" bool-assign-rhs
  ;

bool-assign-lhs
  : id "'"
  | id "'" "[" index-exp "]"
  ;

bool-assign-rhs
  : bool-exp
  | bool-type-decl
  | "nondet"
  ;

enum-assign 
  : enum-assign-lhs ":=" enum-assign-rhs
  ;

enum-assign-lhs
  : id "'"
  | id "'" "[" index-exp "]"
  ;

enum-assign-rhs
  : enum-exp
  | enum-type-decl
  | "nondet"
  ;

range-assign 
  : range-assign-lhs ":=" range-assign-rhs
  ;

range-assign-lhs
  : id "'"
  | id "'" "[" index-exp "]"
  ;

range-assign-rhs
  : range-exp
  | range-type-decl
  | "nondet"
  ;

bitvector-assign 
  : bitvector-assign-lhs ":=" bitvector-assign-rhs
  ;

bitvector-assign-lhs
  : id "'"
  | id "'" "[" index-exp "]"
  ;

bitvector-assign-rhs
  : bitvector-exp
  | bitvector-type-decl
  | "nondet"
  ;

array-event-assign
  : id array-event-assign-rhs "!"
  ;

array-event-assign-rhs
  : 
  | "{" "forindex" id ":" bool-exp "}"
  ;

array-assign 
  : array-assign-lhs ":=" array-assign-rhs
  ;

array-assign-lhs
  : id "'"
  ;

array-assign-rhs
  : array-exp
  | "{" "forindex" id ":" bound-exp "}"
  | array-type-decl
  | "nondet"
  ;

bound-exp
  : bool-exp
  | enum-exp
  | range-exp
  | bitvector-exp
  ;

3.5. Atoms

atom 
  : "atom" atom-name atom-var-decl-list init-update-decl 
  | "lazy" "atom" atom-name atom-var-decl-list init-update-decl 
  ;

atom-name
  : id
  | id "[" const-exp "]"
  ;

const-exp 
  : bool-val
  | enum-val
  | range-val
  | bitvector-val
  ;

atom-var-decl-list 
  : atom-var-decl-list atom-var-decl 
  | 
  ;

atom-var-decl 
  : "controls" atom-var-list 
  | "reads" atom-var-list 
  | "awaits" atom-var-list
  ;

atom-var-list 
  : nonempty-atom-var-list 
  | 
  ;

nonempty-atom-var-list 
  : nonempty-atom-var-list "," atom-var-exp
  | atom-var-exp
  ;

atom-var-exp 
  : id 
  | id "[" const-exp "]"
  ;

init-update-decl 
  : "init" default-guarded-cmd "update" default-guarded-cmd 
  | "initupdate"  default-guarded-cmd 
  ;

3.6. Modules

atomic-module-decl
  : module-name
  | module-var-decl-list atom-list 
  ;

module-name
  : id
  | id "[" const-exp "]"
  ;

module-var-decl-list 
  : module-var-decl-list module-var-decl 
  | 
  ;

module-var-decl 
  : "external" typed-module-var-list 
  | "interface" typed-module-var-list
  | "private" typed-module-var-list 
  ;

typed-module-var-list 
  : nonempty-typed-module-var-list 
  | nonempty-typed-module-var-list ";"
  | 
  ;

nonempty-typed-module-var-list 
  : nonempty-typed-module-var-list ";" typed-module-var-exp
  | typed-module-var-exp
  ;

typed-module-var-exp
  : nonempty-module-var-list ":" type-decl 
  | nonempty-module-array-list ":" type-decl 
  ;

nonempty-module-var-list 
  : nonempty-module-var-list "," module-var-exp
  | module-var-exp
  ;

module-var-exp 
  : id 
  | id "[" const-exp "]"
  ;

nonempty-module-array-list 
  : nonempty-module-array-list "," module-array-exp
  | module-array-exp
  ;

module-array-exp 
  : id 
  ;

atom-list 
  : atom-list atom 
  | 
  ;

3.7. Module expressions

module-def 
  : "module" module-name "is" module-decl 
  ;

module-decl 
  : paren-module-decl
  | hide-module-decl 
  | rename-module-decl
  | comp-module-decl
% | *preprocessor* (see below)
  ;  

paren-module-decl
  : atomic-module-decl
  | "(" module-decl ")"
  ;

hide-module-decl
  : "hide" nonempty-id-list "in" paren-module-decl 
  ;

nonempty-id-list 
  : nonempty-id-list "," id 
  | id 
  ;

rename-module-decl    
  : rename-module-decl "[" rename-lhs ":=" rename-rhs "]"
  | paren-module-decl "[" rename-lhs ":=" rename-rhs "]"
  ;

rename-lhs
  : rename-lhs "," id 
  | id 
  ;

rename-rhs 
  : rename-rhs "," id 
  | id 
  ;

comp-module-decl
  : comp-module-decl "||" paren-module-decl 
  | paren-module-decl "||" paren-module-decl
  ;

4. Semantics

"$"marks input attributes
"&"marks output attributes
"\"is the lambda quantifier for defining functions

The following operations on attributes are used.

On sets and stacks:

EmptySet
SetInsert(elem,set)
SetMember(elem,set)
SetUnion(set1,...,setn)
Intersect(set1,...,setn)
SetDiff(set1,set2) subtract set2 from set1
Subset(set1,set2) set1 is a subset of set2
EmptyStack
Push(elem,stack)
Pop(stack)
StackMember(elem,stack)

On environments and valuations:

An environment is a set of variables, each with an associated type. A valuation is a set of variables, each with an associated value.
EmptyEnv returns the empty environment
EnvInserts(varset,type,env) adds an entry for each variable in 'varset' to the environment 'env', so that added variables have the type 'type'
EnvUnion(env1,env2) merges two environments that agree on all common variables
EnvMember(var,env) checks if the environment 'env' contains an entry for the variable 'var'
Type(var,env) returns the type of the variable 'var' according to the environment 'env'
States(env) returns the set of all valuations for the variables in the environment 'env'
Vltns(varset1,...,varsetn,env) returns the set of all valuations for the variables in the union set of 'varset1,...,varsetn', all of whose types are interpreted according to the environment 'env'
Val(var,vltn)
Ext(bltn,var,val) returns the value of the variable 'var' according to the valuation 'vltn'
Ext(bltn,var,val) returns the valuation that extends the valuation 'valtn' by assigning the value 'val' to the variable 'var'

On symbol tables:

A symbol table is a set of identifiers, each with an associated list of attributes.
EmptyTab returns the empty symbol table
TabInsert(entry,tab) adds the entry 'entry' to the symbol table 'tab'
TabMember(id,tab) checks if the symbol table 'tab' contains an entry for the identifier 'id'
Att(id,tab) returns the list of attributes of the identifier 'id' according to the symbol table 'tab'

Symbol table entries have the following forms:

id.CONST identifier 'id' denotes a constant
id.TYPE.EVENT identifier 'id' denotes the type 'event'
id.TYPE.BOOL identifier 'id' denotes the type 'bool'
id.TYPE.ENUM.set identifier 'id' denotes the enumerative type 'set'
id.TYPE.RANGE.max identifier 'id' denotes the range type '[0..max]'
id.TYPE.BITVECTOR.len identifier 'id' denotes the type of bitvectors with 'len+1' bits
id.TYPE.ARRAY.indextype.valuetype
id.DUMMY identifier 'id' denotes a dummy
id.VAR identifier 'id' denotes a variable
id.ATOM identifier 'id' denotes an atom
id.MODULE.atoms.extl.intf.priv.env.dep.init.trans identifier 'id' denotes a module such that
'atoms' is the set of atom names
'extl' is the set of external variables
'intf' is the set of interface variables
'priv' is the set of private variables
'env' is an environment that gives types to all module variables
'dep' is the await dependency relation on the module variables
'init' is the set of initial states
'trans' is the transition relation 

def-list ( &tab )
  : def-list ( &loctab ) 
    def ( $loctab &tab ) 
  | { tab := EmptyTab }
  ;

def ( $intab &outtab )
  : const-def ( $intab &outtab ) 
  | type-def ( $intab &outtab ) 
  | module-def ( $intab &outtab ) 
  ;

4.1. Constants

const-def ( $intab &outtab )
  : "const" id 
    { not TabMember(id,intab) } 
    { outtab := TabInsert(id.CONST,intab) }
  ;

4.2. Types

type-def ( $intab &outtab )
  : "type" id 
    { not TabMember(id,intab) } 
    "is" type-decl ( $intab &type ) 
    { outtab := TabInsert(id.TYPE.type,intab) }
  ;

type-decl ( $tab &type ) 
  : simp-type-decl ( $tab &type )
  | array-type-decl ( $tab &index &value )
    { type := index.value }
  ;

simp-type-decl ( $tab &type ) 
  : event-type-decl ( $tab ) 
    { type := EVENT }
  | index-type-decl ( $tab &type ) 
  ;

index-type-decl ( $tab &type ) 
  : bool-type-decl ( $tab ) 
    { type := BOOL }
  | enum-type-decl ( $tab &set ) 
    { type := ENUM.set }
  | range-type-decl ( $tab &max ) 
    { type := RANGE.max }
  | bitvector-type-decl ( $tab &len ) 
    { type := BITVECTOR.len }
  ;

event-type-decl ( $tab ) 
  : id 
    { Att(id,tab) = TYPE.EVENT }
  | "event" 
  ;

bool-type-decl ( $tab ) 
  : id 
    { Att(id,tab) = TYPE.BOOL }
  | "bool" 
  ;

enum-type-decl ( $tab &set ) 
  : id 
    { Att(id,tab) = TYPE.ENUM.set }
  | "{" nonempty-enum-val-list ( $tab &set ) 
    "}" 
  ;

nonempty-enum-val-list ( $tab &set ) 
  : nonempty-enum-val-list ( $tab &set )
    "," enum-val ( $tab &name ) 
    { not SetMember(name,set) }
    { set := SetInsert(name,set) }
  | enum-val ( $tab &name ) 
    { set := SetInsert(name,EmptySet) }
  ;

enum-val ( $tab &val )
  : id 
    { Att(id,tab) = CONST } 
    { val := id }
  | num 
    { val := num }
  | bitstring 
    { val := bitstring }
  ;

range-type-decl ( $tab &max ) 
  : id 
    { Att(id,tab) = TYPE.RANGE.max }
  | "(" "0" ".." num ")" 
    { max := num }
  ;

bitvector-type-decl ( $tab &len ) 
  : id 
    { Att(id,tab) = TYPE.BITVECTOR.len }
  | "bitvector" range-type-decl ( $tab &max ) 
    { len := max }
  ;

array-type-decl ( $tab &index &value )
  : id
    { Att(id,tab) = TYPE.ARRAY.index.value }
  | "array" index-type-decl ( $tab &index ) 
    "of" simp-type-decl ( $tab &value )
  ;

4.3. Expressions

bool-exp ( $tab $env $dom &const &fun )   
  : paren-bool-exp ( $tab $env $dom &const &fun ) 
  | enum-pred ( $tab $env $dom &const &fun)
  | range-pred ( $tab $env $dom &const &fun )
  | bitvector-pred ( $tab $env $dom &const &fun )
  | array-pred ( $tab $env $dom &const &fun )
  | "~" paren-bool-exp ( $tab $env $dom &const &fun ) 
    { fun := \s in Vltns(dom,env). not fun(s) }
  | and-bool-exp ( $tab $env $dom &const &fun ) 
  | or-bool-exp ( $tab $env $dom &const &fun )
  | equiv-bool-exp ( $tab $env $dom &const &fun )
  | exor-bool-exp ( $tab $env $dom &const &fun )
  ;

and-bool-exp ( $tab $env $dom &const &fun )
  : and-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "&" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) and fun2(s) }
  | paren-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "&" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) and fun2(s) }
  ;

or-bool-exp ( $tab $env $dom &const &fun )
  : or-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "|" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) or fun2(s) }
  | paren-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "|" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) or fun2(s) }
  ;

equiv-bool-exp ( $tab $env $dom &const &fun )
  : equiv-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "=" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) = fun2(s) }
  | paren-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "=" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) = fun2(s) }
  ;

exor-bool-exp ( $tab $env $dom &const &fun )
  : exor-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "~=" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). not fun1(s) = fun2(s) }
  | paren-bool-exp ( $tab $env $dom &const1 &fun1 ) 
    "~=" paren-bool-exp ( $tab $env $dom &const2 &fun2 ) 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). not fun1(s) = fun2(s) }
  ;

paren-bool-exp ( $tab $env $dom &const &fun )
  : atomic-bool-exp ( $tab $env $dom &const &fun )
  | "(" bool-exp ( $tab $env $dom &const &fun ) 
    ")" 
  | "if" bool-exp ( $tab $env $dom &const1 &fun1 )
    "then" bool-exp ( $tab $env $dom &const2 &fun2 )
    "else" bool-exp ( $tab $env $dom &const3 &fun3 )
    "fi" 
    { const := const1 and const2 and const3,
      fun := \s in Vltns(dom,env). if fun1(s) then fun2(s) else fun3(s) }
  ;

atomic-bool-exp ( $tab $env $dom &const &fun )
  : id 
    { Att(id,tab) = DUMMY and Type(id,env) = BOOL }
    { const := true, fun := \s in Vltns(dom,env). Val(id,s) }
  | id
    { Att(id,tab) = VAR and Type(id,env) = BOOL and SetMember(id,dom) }
    { const := false, fun := \s in Vltns(dom,env). Val(id,s) }
  | id "'" 
    { Type(id,env) = BOOL and SetMember(id',dom) }
    { const := false, fun := \s in Vltns(dom,env). Val(id',s) }
  | id "?"
    { Type(id,env) = EVENT and SetMember(id,dom) and SetMember(id',dom) }
    { const := false, fun := \s in Vltns(dom,env). not Val(id,s) = Val(id',s) }
  | bool-val ( $tab &val )
    { const := true, fun := \s in Vltns(dom,env). val }
  | paren-bitvector-exp ( $tab $env $dom &len &const1 &fun1 ) 
    "[" range-exp ( $tab $env $dom &max &undefmax &const2 &fun2 ) 
    { max <= len }
    "]" 
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). bit fun2(s) of fun1(s) }
  | array-bool-exp ( $tab $env $dom &fun )
    { const := false }
  ;

array-bool-exp ( $tab $env $dom &fun )
  : id
    { Type(id,env) = ARRAY.index.value and value = BOOL }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val,dom) }
    { if const then SetMember(id.fun(s),dom) for any s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s),s) }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = BOOL }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val',dom) }
    { if const then SetMember(id.fun(s)',dom) for any s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s)',s) }
  | id 
    { Type(id,env) = ARRAY.index.value and value = EVENT }
    "[" index-exp ( $tab $env $dom $index &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val,dom) and SetMember(id.val',dom) }
    { if const then SetMember(id.fun(s),dom) and SetMember(id.fun(s)',s)
                    for any s in Vltns(dom,env) }
    "]" "?"
    { fun := \s in Vltns(dom,env). not Val(id.fun(s),s) = Val(id.fun(s)',s) }
  ;

bool-val ( $tab &val )
  : "true" 
    { val := true }
  | "false" 
    { val := false }
  ;

enum-pred ( $tab $env $dom &const &fun )
  : paren-enum-exp ( $tab $env $dom &set1 &const1 &fun1 ) 
    "=" paren-enum-exp ( $tab $env $dom &set2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) = fun2(s) }
  | paren-enum-exp ( $tab $env $dom &set1 &const1 &fun1 ) 
    "~=" paren-enum-exp ( $tab $env $dom &set2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). not fun1(s) = fun2(s) }
  ;

enum-exp ( $tab $env $dom &set &const &fun )
  : paren-enum-exp ( $tab $env $dom &set &const &fun )
  ;

paren-enum-exp ( $tab $env $dom &set &const &fun )
  : atomic-enum-exp ( $tab $env $dom &set &const &fun )
  | "(" enum-exp ( $tab $env $dom &set &const &fun ) 
    ")"
  | "if" bool-exp ( $tab $env $dom &const1 &fun1 )
    "then" enum-exp ( $tab $env $dom &set1 &const2 &fun2 )
    "else" enum-exp ( $tab $env $dom &set2 &const3 &fun3 )
    "fi" 
    { set := SetUnion(set1,set2),
      const := const1 and const2 and const3,
      fun := \s in Vltns(dom,env). if fun1(s) then fun2(s) else fun3(s) }
  ;

atomic-enum-exp ( $tab $env $dom &set &const &fun )
  : id 
    { Att(id,tab) = DUMMY and Type(id,env) = ENUM.set }
    { const := true, fun := \s in Vltns(dom,env). Val(id,s) }
  | id
    { Att(id,tab) = VAR and Type(id,env) = ENUM.set and SetMember(id,dom) }
    { const := false, fun := \s in Vltns(dom,env). Val(id,s) }
  | id "'" 
    { Type(id,env) = ENUM.set and SetMember(id',dom) }
    { const := false, fun := \s in Vltns(dom,env). Val(id',s) }
  | enum-val ( $tab &name ) 
    { set := SetInsert(name,EmptySet),
      const := true,
      fun := \s in Vltns(dom,env). name }
  | array-enum-exp ( $tab $env $dom &set &fun )
    { const := false }
  ;

array-enum-exp ( $tab $env $dom &set &fun )
  : id
    { Type(id,env) = ARRAY.index.value and value = ENUM.set }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val,dom) }
    { if const then SetMember(id.fun(s),dom) for any s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s),s) }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = ENUM.set }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val',dom) }
    { if const then SetMember(id.fun(s)',dom) for any s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s)',s) }
  ;

range-pred ( $tab $env $dom &const &fun )
  : paren-range-exp ( $tab $env $dom &max1 &undefmax1 &const1 &fun1 ) 
    "=" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) = fun2(s) }
  | paren-range-exp ( $tab $env $dom &max1 &undefmax1 &const1 &fun1 ) 
    "~=" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). not fun1(s) = fun2(s) }
  | paren-range-exp ( $tab $env $dom &max1 &undefmax1 &const1 &fun1 ) 
    ">" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) > fun2(s) }
  | paren-range-exp ( $tab $env $dom &max1 &undefmax1 &const1 &fun1 ) 
    "<" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) < fun2(s) }
  | paren-range-exp ( $tab $env $dom &max1 &undefmax1 &const1 &fun1 ) 
    ">=" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) >= fun2(s) }
  | paren-range-exp ( $tab $env $dom &max1 &undefmax1 &const1 &fun1 ) 
    "<=" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2 )
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) <= fun2(s) }
  ;

range-exp ( $tab $env $dom &max &undefmax &const &fun )
  : paren-range-exp ( $tab $env $dom &max &undefmax &const &fun )
  | "inc" paren-range-exp ( $tab $env $dom &max &undefmax &const &fun1) 
    { not undefmax }
    "by" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2) 
    { max2 <= max }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s)+fun2(s) mod max+1 }
  | "dec" paren-range-exp ( $tab $env $dom &max &undefmax &const &fun1) 
    { not max = UNDEF }
    "by" paren-range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2) 
    { max2 <= max }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s)-fun2(s) mod max+1 }
  ;

paren-range-exp ( $tab $env $dom &max &undefmax &const &fun )
  : atomic-range-exp ( $tab $env $dom &max &undefmax &const &fun )
  | "(" range-exp ( $tab $env $dom &max &undefmax &const &fun ) 
    ")"
  | "if" bool-exp ( $tab $env $dom &const1 &fun1 )
    "then" range-exp ( $tab $env $dom &max2 &undefmax2 &const2 &fun2 )
    "else" range-exp ( $tab $env $dom &max3 &undefmax3 &const3 &fun3 ) 
     { if max2 > max3 then undefmax3 }
     { if max3 > max2 then undefmax2 }
    "fi" 
    { max := Max(max2,max3),
      undefmax := undefmax2 and undefmax3,
      const := const1 and const2 and const3,
      fun := \s in Vltns(dom,env). if fun1(s) then fun2(s) else fun3(s) }
  ;

atomic-range-exp ( $tab $env $dom &max &undefmax &const &fun )
  : id 
    { Att(id,tab) = DUMMY and Type(id,env) = RANGE.max }
    { undefmax := false, const := true, 
      fun := \s in Vltns(dom,env). Val(id,s) }
  | id
    { Att(id,tab) = VAR and Type(id,env) = RANGE.max and SetMember(id,dom) }
    { undefmax := false, const := false, 
      fun := \s in Vltns(dom,env). Val(id,s) }
  | id "'" 
    { Type(id,env) = RANGE.max and SetMember(id',dom) }
    { undefmax := false, const := false, 
      fun := \s in Vltns(dom,env). Val(id',s) }
  | range-val ( $tab &val &max &undefmax )
    { const := true, fun := \s in Vltns(dom,env). val }
  | array-range-exp ( $tab $env $dom &max &fun )
    { undefmax := false, const := false }
  ;

array-range-exp ( $tab $env $dom &max &fun )
  : id
    { Type(id,env) = ARRAY.index.value and value = RANGE.max }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val,dom) }
    { if const then SetMember(id.fun(s),dom) for some s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s),s) }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = RANGE.max }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val',dom) }
    { if const then SetMember(id.fun(s)',dom) for some s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s)',s) }
  ;

range-val ( $tab &val &max &undefmax )
  : num 
    { val := num, max := num, undefmax := true }
  | num 
    { val := num }
    "(" "max" num 
    ")"
    { max := num, undefmax := false }
  ;

bitvector-pred ( $tab $env $dom &const &fun )
  : paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    "=" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) = fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    "~=" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). not fun1(s) = fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    ">" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) > fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    "<" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) < fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    ">=" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) >= fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    "<=" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). fun1(s) <= fun2(s) }
  ;

bitvector-exp ( $tab $env $dom &len &const &fun )
  : paren-bitvector-exp ( $tab $env $dom &len &const &fun )
  | "inv" paren-bitvector-exp ( $tab $env $dom &len &const &fun )
    { fun := \s in Vltns(dom,env). bitwise complement of fun(s) }
  | "shiftright" paren-bitvector-exp ( $tab $env $dom &len &const1 &fun1) 
    "by" paren-range-exp ( $tab $env $dom &max &undefmax &const2 &fun2) 
    { max <= len }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). rotate fun1(s) right by fun2(s) bits }
  | "shiftleft" paren-bitvector-exp ( $tab $env $dom &len &const1 &fun1) 
    "by" paren-range-exp ( $tab $env $dom &max &undefmax &const2 &fun2) 
    { max <= len }
    { const := const1 and const2,
      fun := \s in Vltns(dom,env). rotate fun1(s) left by fun2(s) bits }
  | and-bitvector-exp ( $tab $env $dom &len &const &fun )
  | or-bitvector-exp ( $tab $env $dom &len &const &fun )
  | exor-bitvector-exp ( $tab $env $dom &len &const &fun )
  ;

and-bitvector-exp ( $tab $env $dom &len &const &fun )
  : and-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    "and" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { len := len1,
      const := const1 and const2,
      fun := \s in Vltns(dom,env). bitwise and of fun1(s) and fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 )
    "and" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { len := len1,
      const := const1 and const2,
      fun := \s in Vltns(dom,env). bitwise and of fun1(s) and fun2(s) }
  ;

or-bitvector-exp ( $tab $env $dom &len &const &fun )
  : or-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    "or" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { len := len1, 
      const := const1 and const2,
      fun := \s in Vltns(dom,env). bitwise or of fun1(s) and fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 )
    "or" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { len := len1, 
      const := const1 and const2,
      fun := \s in Vltns(dom,env). bitwise or of fun1(s) and fun2(s) }
  ;

exor-bitvector-exp ( $tab $env $dom &len &const &fun )
  : exor-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 ) 
    "exor" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { len := len1, 
      const := const1 and const2,
      fun := \s in Vltns(dom,env). bitwise exor of fun1(s) and fun2(s) }
  | paren-bitvector-exp ( $tab $env $dom &len1 &const1 &fun1 )
    "exor" paren-bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 ) 
    { len1 = len2 }
    { len := len1, 
      const := const1 and const2,
      fun := \s in Vltns(dom,env). bitwise exor of fun1(s) and fun2(s) }
  ;

paren-bitvector-exp ( $tab $env $dom &len &const &fun )
  : atomic-bitvector-exp ( $tab $env $dom &len &const &fun )
  | "(" bitvector-exp ( $tab $env $dom &len &const &fun ) 
    ")"
  | "if" bool-exp ( $tab $env $dom &const1 &fun1 )
    "then" bitvector-exp ( $tab $env $dom &len2 &const2 &fun2 )
    "else" bitvector-exp ( $tab $env $dom &len3 &const3 &fun3 ) 
    { len2 = len3 }
    "fi" 
    { len := len2,
      const := const1 and const2 and const3,
      fun := \s in Vltns(dom,env). if fun1(s) then fun2(s) else fun3(s) }
  ;

atomic-bitvector-exp ( $tab $env $dom &len &const &fun )
  : id 
    { Att(id,tab) = DUMMY and Type(id,env) = BITVECTOR.len }
    { const := true, fun := \s in Vltns(dom,env). Val(id,s) }
  | id
    { Att(id,tab) = VAR and Type(id,env) = BITVECTOR.len and 
      SetMember(id,dom) }
    { const := false, fun := \s in Vltns(dom,env). Val(id,s) }
  | id "'" 
    { Type(id,env) = BITVECTOR.len and SetMember(id',dom) }
    { const := false, fun := \s in Vltns(dom,env). Val(id',s) }
  | bitvector-val ( $tab &val )
    { len := number of bits in bitstring, 
      const := true,
      fun := \s in Vltns(dom,env). bitstring }
  | array-bitvector-exp ( $tab $env $dom &len &fun )
    { const := false }
  ;

array-bitvector-exp ( $tab $env $dom &len &fun )
  : id
    { Type(id,env) = ARRAY.index.value and value = BITVECTOR.len }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val,dom) }
    { if const then SetMember(id.fun(s),dom) for any s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s),s) }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = BITVECTOR.len }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { if not const then forall val in ValsOfType(index). 
                        SetMember(id.val',dom) }
    { if const then SetMember(id.fun(s)',dom) for any s in Vltns(dom,env) }
    "]"
    { fun := \s in Vltns(dom,env). Val(id.fun(s)',s) }
  ;

bitvector-val ( $tab &val )
  : bitstring
    { val := bitstring }
  ;

array-pred ( $tab $env $dom &const &fun )
  : array-exp ( $tab $env $dom &index1 &value1 &fun1 ) 
    "=" array-exp ( $tab $env $dom &index2 &value2 &fun2 )
    { index1 = index2 and value1 = value2 }
    { const := false, fun := \s in Vltns(dom,env). fun1(s) = fun2(s) }
  | array-exp ( $tab $env $dom &index1 &value1 &fun1 ) 
    "~=" array-exp ( $tab $env $dom &index2 &value2 &fun2 )
    { index1 = index2 and value1 = value2 }
    { const := false, fun := \s in Vltns(dom,env). not fun1(s) = fun2(s) }
  | "{" "forall" id 
    { not TabMember(id,tab) }
    "in" index-type-decl ( $tab &index )
    { exttab := TabInsert(id.DUMMY,tab), 
      extenv := EnvInserts(SetInsert(id,EmptySet),index,env),
      extdom := SetInsert(id,dom) }
    ":" bool-exp ( $exttab $extenv $extdom &const &extfun )
    "}"
    { fun := \s in Vltns(dom,env). forall val in ValsOfType(index).
                                   extfun(Ext(s,id,val)) }
  | "{" "forsome" id 
    { not TabMember(id,tab) }
    "in" index-type-decl ( $tab &index )
    { exttab := TabInsert(id.DUMMY,tab), 
      extenv := EnvInserts(SetInsert(id,EmptySet),index,env),
      extdom := SetInsert(id,dom) }
    ":" bool-exp ( $exttab $extenv $extdom &const &extfun )
    "}"
    { fun := \s in Vltns(dom,env). forsome val in ValsOfType(index).
                                   extfun(Ext(s,id,val)) }
  ;

array-exp ( $tab $env $dom &index &value &fun )
  : id
    { Att(id,tab) = VAR and Type(id,env) = ARRAY.index.value and 
      forall val in ValsOfType(index). SetMember(id.val,dom) }
    { fun := \s in Vltns(dom,env). \val in ValsOfType(index). Val(id.val,s) }
  | id "'" 
    { Att(id,tab) = VAR and Type(id,env) = ARRAY.index.value and 
      forall val in ValsOfType(index). SetMember(id.val',dom) }
    { fun := \s in Vltns(dom,env). \val in ValsOfType(index). Val(id.val',s) }
  ;

index-exp ( $tab $env $dom $index &const &fun ) 
  : { index = BOOL }
    bool-exp ( $tab $env $dom &const &fun ) 
  | { index = ENUM.set1 }
    enum-exp ( $tab $env $dom &set2 &const &fun ) 
    { Subset(set2,set1) }
  | { index = RANGE.max1 }
    range-exp ( $tab $env $dom &max2 &undefmax &const &fun ) 
    { max2 <= max1 }
  | { index = BITVECTOR.len1 }
    bitvector-exp ( $tab $env $dom &len2 &const &fun ) 
    { len1 = len2 }
  ;

4.4. Guarded commands

default-guarded-cmd ( $tab $env $ctr $todo $dom &vltns )
  : guarded-cmd ( $tab $env $ctr $todo $dom &guard &vltns1 )
    default-assign-list ( $tab $env $ctr $todo $dom $guard &vltns2 )
   { vltns := SetUnion(vltns1,vltns2) }
  ;

guarded-cmd ( $tab $env $ctr $todo $dom &guard &vltns )
  : guarded-cmd ( $tab $env $ctr $todo $dom &guard1 &vltns1 )
    guarded-assign-list ( $tab $env $ctr $todo $dom &guard2 &vltns2 )
    { guard := SetUnion(guard1,guard2), vltns := SetUnion(vltns1,vltns2) }
  | { guard := EmptySet, vltns := EmptySet }
  ;

guarded-assign-list ( $tab $env $ctr $todo $dom &guard &vltns )
  : "[]" bool-exp ( $tab $env $dom &const &fun )
    { guard := setof s in Vltns(dom,ctr',env). fun(s) }
    "->" assign-list ( $tab $env $ctr $dom &done &maybedone &vltns )
    { Subset(todo,done) }
    { vltns := setof s in Intersect(guard,vltns). 
               forall loc in SetDiff(Intersect(ctr,dom),maybedone). 
               Val(loc,s) = Val(loc',s) }
  ;

default-assign-list ( $tab $env $ctr $todo $dom $guard &vltns )
  : "[]" "default" "->" 
    assign-list ( $tab $env $ctr $dom &done &maybedone &vltns )
    { Subset(todo,done) }
    { vltns := setof s in SetDiff(vltns,guard). 
               forall loc in SetDiff(Intersect(ctr,dom),maybedone). 
               Val(loc,s) = Val(loc',s) }
  | { vltns := SetDiff(Vltns(dom,ctr',env),guard) }
  ;

assign-list ( $tab $env $ctr $dom &done &maybedone &vltns )
  : nonempty-assign-list ( $tab $env $ctr $dom &done &maybedone &vltns )
  | nonempty-assign-list ( $tab $env $ctr $dom &done &maybedone &vltns ) 
    ";"
  | { done := EmptySet, maybedone := EmptySet, vltns := Vltns(dom,ctr',env) }
  ;

nonempty-assign-list ( $tab $env $ctr $dom &done &maybedone &vltns )
  : nonempty-assign-list ( $tab $env $ctr $dom &done1 &maybedone1 &vltns1 )
    ";" assign ( $tab $env $ctr $dom &done2 &maybedone2 &vltns2 )
    { Subset(maybedone2,ctr) and Intersect(maybedone1,maybedone2) = EmptySet }
    { done := SetUnion(done1,done2), 
      maybedone := SetUnion(maybedone1,maybedone2),
      vltns := Intersect(vltns1,vltns2) }
  | assign ( $tab $env $ctr $dom &done &maybedone &vltns ) 
    { Subset(maybedone,ctr) }
  ;

assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : event-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  | bool-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  | enum-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  | range-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  | bitvector-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  | array-event-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  | array-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  ;

event-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : id "!" 
    { Type(id,env) = EVENT and SetMember(id,dom) }
    { done := SetInsert(id,EmptySet), 
      maybedone := SetInsert(id,EmptySet), 
      vltns := setof s in Vltns(dom,ctr',env). not Val(id',s) = Val(id,s) }
  | id 
    { Type(id,env) = ARRAY.index.value and value = EVENT }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { const }
    "]" "!"
    { val := fun(s) for any s in Vltns(dom,env) }
    { SetMember(id.val,dom) }
    { done := SetInsert(id.val,EmptySet),
      maybedone := SetInsert(id.val,EmptySet), 
      vltns := setof s in Vltns(dom,ctr',env). 
               not Val(id.val',s) = Val(id.val,s) }
  | id 
    { Type(id,env) = ARRAY.index.value and value = EVENT }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { not const }
    "]" "!"
    { forall val in ValsOfType(index). SetMember(id.val,dom) }
    { done := EmptySet,
      maybedone := setof id.val with val in ValsOfType(index),
      vltns := setof s in vltns. forall loc in maybedone.
               Val(loc,s) = Val(loc',s) iff not loc = lhs(s) }
  ;

bool-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : bool-assign-lhs ( $tab $env $dom &done &maybedone &lhs )
    ":=" bool-assign-rhs ( $tab $env $ctr $dom $lhs &vltns )
    { vltns := setof s in vltns. forall loc in maybedone.
               if not loc = lhs(s) then Val(loc,s) = Val(loc',s) }
  ;

bool-assign-lhs ( $tab $env $dom &done &maybedone &lhs )
  : id "'" 
    { Att(id,tab) = VAR and Type(id,env) = BOOL }
    { done := SetInsert(id,EmptySet), 
      maybedone := SetInsert(id,EmptySet), 
      lhs := \s in Vltns(dom,env). id }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = BOOL }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { const }
    "]"
    { val := fun(s) for any s in Vltns(dom,env),
      done := SetInsert(id.val,EmptySet),
      maybedone := SetInsert(id.val,EmptySet), 
      lhs := \s in Vltns(dom,env). id.val }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = BOOL }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { not const }
    "]"
    { done := EmptySet,
      maybedone := setof id.val with val in ValsOfType(index),
      lhs := \s in Vltns(dom,env). id.fun(s) }
  ;

bool-assign-rhs ( $tab $env $ctr $dom $lhs &vltns )
  : bool-exp ( $tab $env $dom &const &fun )
    { vltns := setof s in Vltns(dom,ctr',env). Val(lhs(s)',s) = fun(s) }
  | bool-type-decl ( $tab ) 
    { vltns := Vltns(dom,ctr',env) }
  | "nondet"
    { vltns := Vltns(dom,ctr',env) }
  ;

enum-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : enum-assign-lhs ( $tab $env $dom &done &maybedone &lhs &set )
    ":=" enum-assign-rhs ( $tab $env $ctr $dom $lhs $set &vltns )
    { vltns := setof s in vltns. forall loc in maybedone.
               if not loc = lhs(s) then Val(loc,s) = Val(loc',s) }
  ;

enum-assign-lhs ( $tab $env $dom &done &maybedone &lhs &set )
  : id "'" 
    { Att(id,tab) = VAR and Type(id,env) = ENUM.set }
    { done := SetInsert(id,EmptySet), 
      maybedone := SetInsert(id,EmptySet), 
      lhs := \s in Vltns(dom,env). id }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = ENUM.set }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { const } 
    "]"
    { val := fun(s) for any s in Vltns(dom,env),
      done := SetInsert(id.val,EmptySet),
      maybedone := SetInsert(id.val,EmptySet), 
      lhs := \s in Vltns(dom,env). id.val }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = ENUM.set }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { not const }
    "]"
    { done := EmptySet,
      maybedone := setof id.val with val in ValsOfType(index),
      lhs := \s in Vltns(dom,env). id.fun(s) }
  ;

enum-assign-rhs ( $tab $env $ctr $dom $lhs $set1 &vltns )
  : enum-exp ( $tab $env $dom &set2 &const &fun )
    { Subset(set2,set1) }
    { vltns := setof s in Vltns(dom,ctr',env). Val(lhs(s)',s) = fun(s) }
  | enum-type-decl ( $tab &set2 ) 
    { Subset(set2,set1) }
    { vltns := setof s in Vltns(dom,ctr',env). SetMember(Val(lhs(s)',s),set2) }
  | "nondet"
    { vltns := Vltns(dom,ctr',env) }
  ;

range-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : range-assign-lhs ( $tab $env $dom &done &maybedone &lhs &max )
    ":=" range-assign-rhs ( $tab $env $ctr $dom $lhs $max &vltns )
    { vltns := setof s in vltns. forall loc in maybedone.
               if not loc = lhs(s) then Val(loc,s) = Val(loc',s) }
  ;

range-assign-lhs ( $tab $env $dom &done &maybedone &lhs &max )
  : id "'" 
    { Att(id,tab) = VAR and Type(id,env) = RANGE.max }
    { done := SetInsert(id,EmptySet), 
      maybedone := SetInsert(id,EmptySet), 
      lhs := \s in Vltns(dom,env). id }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = RANGE.max }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { const }
    "]"
    { val := fun(s) for any s in Vltns(dom,env),
      done := SetInsert(id.val,EmptySet),
      maybedone := SetInsert(id.val,EmptySet), 
      lhs := \s in Vltns(dom,env). id.val }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = RANGE.max }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { not const }
    "]"
    { done := EmptySet,
      maybedone := setof id.val with val in ValsOfType(index),
      lhs := \s in Vltns(dom,env). id.fun(s) }
  ;

range-assign-rhs ( $tab $env $ctr $dom $lhs $max1 &vltns )
  : range-exp ( $tab $env $dom &max2 &undefmax &const &fun )
    { max2 <= max1 }
    { vltns := setof s in Vltns(dom,ctr',env). Val(lhs(s)',s) = fun(s) }
  | range-type-decl ( $tab &max2 ) 
    { max2 <= max1 }
    { vltns := setof s in Vltns(dom,ctr',env). Val(lhs(s)',s) <= max2 }
  | "nondet"
    { vltns := Vltns(dom,ctr',env) }
  ;

bitvector-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : bitvector-assign-lhs ( $tab $env $dom &done &maybedone &lhs &len )
    ":=" bitvector-assign-rhs ( $tab $env $ctr $dom $lhs $len &vltns )
    { vltns := setof s in vltns. forall loc in maybedone.
               if not loc = lhs(s) then Val(loc,s) = Val(loc',s) }
  ;

bitvector-assign-lhs ( $tab $env $dom &done &maybedone &lhs &len )
  : id "'" 
    { Att(id,tab) = VAR and Type(id,env) = BITVECTOR.len }
    { done := SetInsert(id,EmptySet), 
      maybedone := SetInsert(id,EmptySet), 
      lhs := \s in Vltns(dom,env). id }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = BITVECTOR.len }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { const }
    "]"
    { val := fun(s) for any s in Vltns(dom,env),
      done := SetInsert(id.val,EmptySet),
      maybedone := SetInsert(id.val,EmptySet), 
      lhs := \s in Vltns(dom,env). id.val }
  | id "'"
    { Type(id,env) = ARRAY.index.value and value = BITVECTOR.len }
    "[" index-exp ( $tab $env $dom $index &const &fun ) 
    { not const }
    "]"
    { done := EmptySet,
      maybedone := setof id.val with val in ValsOfType(index),
      lhs := \s in Vltns(dom,env). id.fun(s) }
  ;

bitvector-assign-rhs ( $tab $env $ctr $dom $lhs $len1 &vltns )
  : bitvector-exp ( $tab $env $dom &len2 &const &fun )
    { len2 = len1 }
    { vltns := setof s in Vltns(dom,ctr',env). Val(lhs(s)',s) = fun(s) }
  | bitvector-type-decl ( $tab &len2 ) 
    { len2 = len1 }
    { vltns := Vltns(dom,ctr',env) }
  | "nondet"
    { vltns := Vltns(dom,ctr',env) }
  ;

array-event-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : array-assign-lhs ( $tab $env &done &maybedone &arrayid &index &value )
    { value = EVENT }
    array-event-assign-rhs ( $tab $env $ctr $dom $arrayid $index &vltns )
    "!"
  ;

array-event-assign-rhs ( $tab $env $ctr $dom $arrayid $index &vltns )
  : { vltns := setof s in Vltns(dom,ctr',env). forall val in ValsOfType(index).
               not Val(id.val',s) = Val(id.val,s) }
  | "{" "forindex" id 
    { not TabMember(id,tab) }
    { exttab := TabInsert(id.DUMMY,tab), 
      extenv := EnvInserts(SetInsert(id,EmptySet),index,env),
      extdom := SetInsert(id,dom) }
    ":" bool-exp ( $exttab $extenv $extdom &const &extfun )
    "}" 
    { vltns := setof s in Vltns(dom,ctr',env). forall val in ValsOfType(index).
               Val(arrayid.val,s) = Val(arrayid.val',s) iff 
               not extfun(Ext(s,id2,val)) }
  ;

array-assign ( $tab $env $ctr $dom &done &maybedone &vltns )
  : array-assign-lhs ( $tab $env &done &maybedone &arrayid &index &value )
    { not value = EVENT }
    ":=" 
    array-assign-rhs ( $tab $env $ctr $dom $arrayid $index $value &vltns )
  ;

array-assign-lhs ( $tab $env &done &maybedone &id &index &value )
  : id "'"
    { Type(id,env) = ARRAY.index.value }
    { done := setof id.val with val in ValsOfType(index),
      maybedone := setof id.val with val in ValsOfType(index) }
  ;

array-assign-rhs ( $tab $env $ctr $dom $arrayid $index1 $value1 &vltns )
  : array-exp ( $tab $env $dom &index2 &value2 &fun )
    { index1 = index2 and value1 = value2 }
    { vltns := setof s in Vltns(dom,ctr',env). 
               forall val in ValsOfType(index1).
               Val(arrayid.val',s) = fun(s)(arrayid.val) }
  | "{" "forindex" id 
    { not TabMember(id,tab) }
    { exttab := TabInsert(id.DUMMY,tab), 
      extenv := EnvInserts(SetInsert(id,EmptySet),index1,env),
      extdom := SetInsert(id,dom) }
    ":" bound-exp ( $exttab $extenv $extdom $value1 &extfun )
    "}"
    { vltns := setof s in Vltns(dom,ctr',env). 
               forall val in ValsOfType(index1).
               Val(arrayid.val',s) = extfun(Ext(s,id,val)) }
  | array-type-decl ( $tab &index &value )
    { index1 = index2 and value1 = value2 }
    { vltns := Vltns(dom,ctr',env) }
  | "nondet"
    { vltns := Vltns(dom,ctr',env) }
  ;

bound-exp ( $tab $env $dom $type &fun )
  : { type = BOOL }
    bool-exp ( $tab $env $dom &const &fun )
  | { type = ENUM.set1 }
    enum-exp ( $tab $env $dom &set2 &const &fun )
    { Subset(set2,set1) }
  | { type = RANGE.max1 }
    range-exp ( $tab $env $dom &max2 &undefmax &const &fun )
    { max2 <= max1 }
  | { type = BITVECTOR.len1 }
    bitvector-exp ( $tab $env $dom &len &const &fun )
    { len1 = len2 }
  ;

4.5. Atoms

atom ( $tab $env &name &id &ctr &read &await &initvltns &updvltns )
  : "atom" atom-name ( $tab &name &id )
    atom-var-decl-list ( $tab $env &ctr &read &await ) 
    init-update-decl ( $tab $env $ctr $read $await &initvltns &updvltns )
  | "lazy" "atom" atom-name ( $tab &name )
    atom-var-decl-list ( $tab $env &ctr &read &await ) 
    { Subset(ctr,read) }
    init-update-decl ( $tab $env $ctr $read $await &initvltns &updvltns )
    { updvltns := setof s in Vltns(read,await',ctr',env). 
                  SetMember(s,updvltns) or
                  forall loc in ctr. Val(loc,s) = Val(loc',s) }
  ;

atom-name ( $tab &name &id )
  : id 
    { name := id }
  | id "[" const-exp ( $tab $env $dom &val ) 
    "]"
    { name := id.val }
  ;

atom-var-decl-list ( $tab $env &ctr &read &await )
  : atom-var-decl-list ( $tab $env &ctr1 &read1 &await1 ) 
    { used := SetUnion(ctr1,read1,await1) }
    atom-var-decl ( $tab $env $used &ctr2 &read2 &await2 )
    { ctr := SetUnion(ctr1,ctr2), 
      read := SetUnion(read1,read2), 
      await := SetUnion(await1,await2) }
  | { ctr := EmptySet, read := EmptySet, await := EmptySet }
  ;

atom-var-decl ( $tab $env $used &ctr &read &await ) 
  : "controls" atom-var-list ( $tab $env $used &ctr )  
    { read := EmptySet, await := EmptySet }
  | "reads" atom-var-list ( $tab $env $used &read )  
    { ctr := EmptySet, await := EmptySet }
  | "awaits" atom-var-list ( $tab $env $used &await )  
    { ctr := EmptySet, read := EmptySet }
  ;

atom-var-list ( $tab $env $used &set )
  : nonempty-atom-var-list ( $tab $env $used &set )
  | { set := EmptySet }
  ;

nonempty-atom-var-list ( $tab $env $used &set )
  : nonempty-atom-var-list ( $tab $env $used &locset )
    "," atom-var-exp ( $tab $env $used $locset &set )
  | atom-var-exp ( $tab $env $used $EmptySet &set )
  ;

atom-var-exp ( $tab $env $used $inset &outset )
  : id 
    { EnvMember(id,env) and not Type(id,env) = ARRAY.index.value }
    { not SetMember(id,used) and not SetMember(id,inset) } 
    { outset := SetInsert(id,inset) }
  | id
    { Type(id,env) = ARRAY.index.value }
    { not SetMember(id.val,used) and not SetMember(id.val,inset) for any val }
    { outset := SetUnion((setof id.val with val in ValsOfType(index)),inset) }
  | id 
    "[" const-exp ( $tab $env $dom &val )
    "]"
    { EnvMember(id.val,env) }
    { not SetMember(id.val,used) and not SetMember(id.val,inset) } 
    { outset := SetInsert(id.val,inset) }
  | id 
    "[" const-exp ( $tab $env $dom &val )
    "]"
    { Type(id,env) = ARRAY.index.value and val in ValsOfType(index) }
    { not SetMember(id.val,used) and not SetMember(id.val,inset) } 
    { outset := SetInsert(id.val,inset) }
  ;

const-exp ( $tab $env $dom &val )
  : bool-exp ( $tab $env $dom &const &fun )
    { const }
    { val := fun(s) for any s in Vltns(dom,env) }
  | enum-exp ( $tab $env $dom &set &const &fun )
    { const }
    { val := fun(s) for any s in Vltns(dom,env) }
  | range-exp ( $tab $env $dom &max &undefmax &const &fun )
    { const }
    { val := fun(s) for any s in Vltns(dom,env) }
  | bitvector-exp ( $tab $env $dom &len &const &fun )
    { const }
    { val := fun(s) for any s in Vltns(dom,env) }
  ;

init-update-decl ( $tab $env $ctr $read $await &initvltns &updvltns )
  : "init" 
    { todo := EmptySet, dom := await' }
    default-guarded-cmd ( $tab $env $ctr $todo $dom &initvltns )
    "update" 
    { todo := SetDiff(ctr,read), dom := SetUnion(read,await') }
    default-guarded-cmd ( $tab $env $ctr $todo $dom &updvltns )
  | "initupdate"  
    { read = EmptySet } 
    { todo := ctr, dom := await' }
    default-guarded-cmd ( $tab $env $ctr $todo $dom &initupdvltns )
    { initvltns := initupdvltns, updvltns := initupdvltns }
  ;

4.6. Modules

atomic-module-decl 
  ( $intab $modid &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  : module-name ( $tab &name &id )
    { Att(name,intab) = MODULE.atoms.extl.intf.priv.env.dep.init.trans }
  | module-var-decl-list ( $intab $modid &loctab &env &extl &intf &priv )
    { forall id1.val1 in SetUnion(extl,intf).
      forall id2.val2 in priv. not id1 = id2 }
    atom-list ( $loctab $modid $env &outtab &atoms &ctr &dep &init &trans )
    { ctr = SetUnion(intf,priv) }
    { transitive closure of dep is asymmetric }
    { dep := setof (loc1,loc2) in transitive closure of dep.
             SetMember(loc1,SetUnion(extl,intf)) and SetMember(loc2,intf)}
  ;

module-name ( $tab &name &id )
  : id 
    { name := id }
  | id "[" const-exp ( $tab $env $dom &val ) 
    "]"
    { name := id.val }
  ;

module-var-decl-list ( $intab $modid &outtab &env &extl &intf &priv )
  : module-var-decl-list 
      ( $intab $modid &loctab &locenv &extl1 &intf1 &priv1 )
    module-var-decl 
      ( $loctab $modid $locenv &outtab &outenv &extl2 &intf2 &priv2 )
    { extl := SetUnion(extl1,extl2),
      intf := SetUnion(intf1,intf2),
      priv := SetUnion(priv1,priv2) }
  | { outtab := intab, env := EmptyEnv, 
      extl := EmptySet, intf := EmptySet, priv := EmptySet }
  ;

module-var-decl ( $intab $modid $inenv &outtab &outenv &extl &intf &priv )
  : "external" 
    typed-module-var-list ( $intab $modid $inenv &outtab &outenv &extl ) 
    { intf := EmptySet, priv := EmptySet }
  | "interface" 
    typed-module-var-list ( $intab $modid $inenv &outtab &outenv &intf ) 
    { extl := EmptySet, priv := EmptySet }
  | "private" 
    typed-module-var-list ( $intab $modid $inenv &outtab &outenv &priv ) 
    { extl := EmptySet, intf := EmptySet }
  ;

typed-module-var-list ( $intab $modid $inenv &outtab &outenv &set ) 
  : nonempty-typed-module-var-list 
      ( $intab $modid $inenv &outtab &outenv &set ) 
  | nonempty-typed-module-var-list 
      ( $intab $modid $inenv &outtab &outenv &set )
    ";"
  | { outtab := intab, outenv := inenv, set := EmptySet }
  ;

nonempty-typed-module-var-list ( $intab $modid $inenv &outtab &outenv &set ) 
  : nonempty-typed-module-var-list 
      ( $intab $modid $inenv &loctab &locenv &set1 ) 
    ";" 
    typed-module-var-exp 
      ( $loctab $modid $locenv &outtab &outenv &set2 &type ) 
    { set := SetUnion(set1,set2) }
  | typed-module-var-exp 
      ( $intab $modid $inenv &outtab &outenv &set &type ) 
  ;

typed-module-var ( $intab $modid $inenv &outtab &outenv &set &type ) 
  : nonempty-module-var-list ( $intab $modid $inenv &outtab &set ) 
    ":" type-decl ( $outtab &type )
    { not type = ARRAY.index.value }
    { outenv := EnvInserts(set,type,inenv) }
  | nonempty-module-array-list ( $intab $modid $inenv &outtab &set ) 
    ":" type-decl ( $outtab &type )
    { type = ARRAY.index.value }
    { outenv := EnvInserts(set,type,inenv),
      set := setof id.val with SetMember(id,set) and val in ValsOfType(index) }
  ;

nonempty-module-var-list ( $intab $modid $usedenv &outtab &set ) 
  : nonempty-module-var-list ( $intab $modid $usedenv &outtab &locset ) 
    "," module-var-exp ( $intab $modid $usedenv $locset &outtab &set ) 
  | module-var-exp ( $intab $modid $usedenv $EmptySet &outtab &set ) 
  ;

module-var-exp ( $intab $modid $usedenv $inset &outtab &outset ) 
  : id 
    { not TabMember(id,intab) or Att(id,intab) = VAR }
    { not id = modid }
    { not EnvMember(id,usedenv) and not EnvMember(id.val,usedenv) for any val }
    { not SetMember(id,inset) and not SetMember(id.val,inset) for any val }
    { outtab := TabInsert(id.VAR,intab), outset := SetInsert(id,inset) }
  | id 
    { not TabMember(id,intab) or Att(id,intab) = VAR }
    { not id = modid }
    "[" const-exp ( $intab &val ) 
    "]"
    { not EnvMember(id,usedenv) and not EnvMember(id.val,usedenv) }
    { not SetMember(id,inset) and not SetMember(id.val,inset) }
    { outtab := TabInsert(id.VAR,intab), outset := SetInsert(id.val,inset) }
  ;

nonempty-module-array-list ( $intab $modid $usedenv &outtab &set ) 
  : nonempty-module-array-list ( $intab $modid $usedenv &outtab &locset ) 
    "," module-array-exp ( $intab $modid $usedenv $locset &outtab &set ) 
  | module-array-exp ( $intab $modid $usedenv $EmptySet &outtab &set ) 
  ;

module-array-exp ( $intab $modid $usedenv $inset &outtab &outset ) 
  : id 
    { not TabMember(id,intab) or Att(id,intab) = VAR }
    { not id = modid }
    { not EnvMember(id,usedenv) and not EnvMember(id.val,usedenv) for any val }
    { not SetMember(id,inset) }
    { outtab := TabInsert(id.VAR,intab), outset := SetInsert(id,inset) }
  ;

atom-list ( $intab $modid $env &outtab &atoms &ctr &dep &init &trans )
  : atom-list ( $intab $modid $env &loctab &atoms &dep &ctr1 &init &trans )
    atom ( $loctab $env &name &id &ctr2 &read &await &initvltns &updvltns )
    { not TabMember(id,intab) or Att(id,intab) = ATOM }
    { not id = modid and not SetMember(name,atoms) }
    { Intersect(ctr1,ctr2) = EmptySet }
    { outtab := TabInsert(id.ATOM,loctab), 
      atoms := SetInsert(name,atoms), 
      ctr := SetUnion(ctr1,ctr2), 
      dep := SetUnion(dep, setof (loc1,loc2). 
                           SetMember(loc1,await) and SetMember(loc2,ctr2)),
      init := setof s in init. restriction of s' is in initvltns,
      trans := setof (s1,s2) in trans. restriction of (s1,s2') is in updvltns }
  | { outtab := intab, atoms := EmptySet, ctr := EmptySet, dep := EmptySet, 
      init := States(env), trans := States(env)^2 }
  ;

4.7. Module expressions

module-def ( $intab &outtab )
  : "module" module-name ( $intab &name &id )
    { not TabMember(name,intab) and not TabMember(id,intab) }
    { if TabMember(id.val,intab) for any val then Att(id.val,intab) = MODULE }
    "is" 
    module-decl 
      ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
    { outtab := TabInsert(name.MODULE.atoms.extl.intf.priv.env.dep.init.trans,
                outtab) }
  ;

module-decl 
  ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  : paren-module-decl
      ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  | hide-module-decl 
      ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  | rename-module-decl
      ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  | comp-module-decl
      ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
% | *preprocessor* (see below)
  ;  

paren-module-decl
  ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  : { modid := if name = id.val then id else name }
    atomic-module-decl
      ( $intab $modid &outtab &atoms &extl &intf &priv &env &dep &init &trans )
    { atoms := prefix every element of atoms by 'name/',
      priv := prefix every element of priv by 'name/',
      update env, init, and trans consistent with the prefixing of priv }
  | "(" 
    module-decl 
      ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
    ")"
  ;

hide-module-decl
  ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  : "hide" 
    { modid := if name = id.val then id else name }
    nonempty-id-list ( $intab $modid &loctab &set ) 
    "in" 
    paren-module-decl 
      ( $loctab $name 
        &outtab &atoms &extl &intf &priv &env &dep &init &trans )
    { forall id in set.
      EnvMember(id,env) or EnvMember(id.val,env) for some val }
    { eset := setof id and id.val in extl. SetMember(id,set),
      iset := setof id and id.val in intf. SetMember(id,set),
      extl := SetDiff(extl,eset), 
      intf := SetDiff(intf,iset), 
      dep := remove from dep all pairs containing id or id.val for some val
             with SetMember(id,set),
      eset := prefix every element of eset by 'name/',
      iset := prefix every element of iset by 'name/',
      priv := SetUnion(eset,iset,priv);
      update env, init, and trans consistent with the prefixing of eset and 
        iset }
  ;

nonempty-id-list ( $intab $modid &outtab &set ) 
  : nonempty-id-list ( $intab $modid &outtab &set ) 
    "," id 
    { not TabMember(id,intab) or Att(id,intab) = VAR }
    { not id = modid and not SetMember(id,set) }
    { outtab := TabInsert(id.VAR,intab), set := SetInsert(id,set) }
  | id 
    { not TabMember(id,intab) or Att(id,intab) = VAR }
    { not id = modid }
    { outtab := TabInsert(id.VAR,intab), set := SetInsert(id,EmptySet) }
  ;

rename-module-decl    
  ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  : rename-module-decl 
      ( $intab $name &loctab &atoms &extl &intf &priv &env &dep &init &trans )
    { dom := setof id with id or id.val for some val in SetUnion(extl,intf) }
    "[" rename-lhs ( $dom &stack )
    ":=" 
    { modid := if name = id.val then id else name }
    rename-rhs ( $loctab $modid $dom $stack &outtab &used &renaming )
    "]"
    { extl := apply renaming to extl, 
      intf := apply renaming to intf,
      env := apply renaming to env, 
      dep := apply renaming to dep,
      init := apply renaming to init, 
      trans := apply renaming to trans }
  | paren-module-decl 
      ( $intab $name &loctab &atoms &extl &intf &priv &env &dep &init &trans )
    { dom := setof id with id or id.val for some val in SetUnion(extl,intf) }
    "[" rename-lhs ( $dom &stack )
    ":=" 
    { modid := if name = id.val then id else name }
    rename-rhs ( $loctab $modid $dom $stack &outtab &used &renaming )
    "]"
    { extl := apply renaming to extl, 
      intf := apply renaming to intf,
      env := apply renaming to env, 
      dep := apply renaming to dep,
      init := apply renaming to init, 
      trans := apply renaming to trans }
  ;

rename-lhs ( $dom &stack )
  : rename-lhs ( $dom &stack )
    "," id 
    { SetMember(id,dom) and not StackMember(id,stack) }
    { stack := Push(id,stack) }
  | id 
    { stack := Push(id,EmptyStack) }
  ;

rename-rhs ( $intab $modid $dom $stack &outtab &used &renaming )
  : { (renamedid,stack) := Pop(stack) }
    rename-rhs ( $intab $modid $dom $stack &outtab &used &renaming )
    "," id 
    { not TabMember(id,intab) or TabMember(id,intab) = VAR }
    { not id = modid and not SetMember(id,used) }
    { not SetMember(id,dom) or StackMember(id,stack) }
    { outtab := TabInsert(id.VAR,intab),
      renaming := SetInsert((renamedid,id),renaming),
      used := SetInsert(id,used) }
  | { (renamedid,stack) := Pop(stack) } 
    { stack = EmptyStack }
    id 
    { not TabMember(id,intab) or TabMember(id,intab) = VAR }
    { not id = modid }
    { not SetMember(id,dom) or StackMember(id,stack) }
    { outtab := TabInsert(id.VAR,intab),
      renaming := SetInsert((renamedid,id),EmptySet),
      used := SetInsert(id,EmptySet) }
  ;

comp-module-decl
  ( $intab $name &outtab &atoms &extl &intf &priv &env &dep &init &trans )
  : comp-module-decl 
      ( $intab $name 
        &loctab &atoms1 &extl1 &intf1 &priv1 &env1 &dep1 &init1 &trans1 )
    "||"
    paren-module-decl 
      ( $loctab $name 
        &outtab &atoms2 &extl2 &intf2 &priv2 &env2 &dep2 &init2 &trans2 )
    { Intersect(atoms1,atoms2) = EmptySet }
    { Intersect(intf1,intf2) = EmptySet }
    { forall id in intf1. not id.val in intf2 for any val }
    { forall id in intf2. not id.val in intf1 for any val }
    { forall loc with EnvMember(loc,env1) and EnvMember(loc,env2).
      Type(loc,env1) = Type(loc,env2) }
    { transitive closure of SetUnion(dep1,dep2) is asymmetric }
    { atoms := SetUnion(atoms1,atoms2),
      extl := SetDiff(SetUnion(extl1,extl2),SetUnion(intf1,intf2)),
      intf := SetUnion(intf1,intf2),
      priv := SetUnion(priv1,priv2),
      env := EnvUnion(env1,env2),
      dep := transitive closure of SetUnion(dep1,dep2),
      init := setof s in States(env). 
              restrictions of s are in init1 and init2,
      trans := setof t in States(env)^2.
               restrictions of t are in trans1 and trans2 }
  | paren-module-decl 
      ( $intab $name 
        &loctab &atoms1 &extl1 &intf1 &priv1 &env1 &dep1 &init1 &trans1 )
    "||"
    paren-module-decl
      ( $loctab $name 
        &outtab &atoms2 &extl2 &intf2 &priv2 &env2 &dep2 &init2 &trans2 ) 
    { Intersect(atoms1,atoms2) = EmptySet }
    { Intersect(intf1,intf2) = EmptySet }
    { forall id in intf1. not id.val in intf2 for any val }
    { forall id in intf2. not id.val in intf1 for any val }
    { forall loc with EnvMember(loc,env1) and EnvMember(loc,env2).
      Type(loc,env1) = Type(loc,env2) }
    { transitive closure of SetUnion(dep1,dep2) is asymmetric }
    { atoms := SetUnion(atoms1,atoms2),
      extl := SetDiff(SetUnion(extl1,extl2),SetUnion(intf1,intf2)),
      intf := SetUnion(intf1,intf2),
      priv := SetUnion(priv1,priv2),
      env := EnvUnion(env1,env2),
      dep := transitive closure of SetUnion(dep1,dep2),
      init := setof s in States(env). 
              restrictions of s are in init1 and init2,
      trans := setof t in States(env)^2.
               restrictions of t are in trans1 and trans2 }
  ;

5. Preprocessor

The preprocessor replaces every text of the form 

"{" "compose" id { not TabMember(id,tab) } 
{ tab := TabInsert(id.PARM,tab) }
"in" index-type-decl ( $tab &index ) 
":" module-decl "}"
by 
"(" Macro(text,id,val1) ")" "||" ... "||" "(" Macro(text,id,valn) ")"
where Macro(text,id,val) replaces all occurrences of the identifier 'id' in 'text' by 'val', and {val1,...,valn} is the set of values of type index so that if index = RANGE.max, then the values have the form 'num (of max)'.

Similarly, the preprocessor replaces every text of the form 

"{" "parameter" id { not TabMember(id,tab) } 
{ tab := TabInsert(id.PARM,tab) }
"in" index-type-decl ( $tab &index ) 
":" module-decl "}"
by 
Macro(text,id,val1) ... Macro(text,id,valn)

You are not logged in 
©2002-2009 U.C. Regents