% ccs.syn
% 2-12-96
% This file contains a PAC specification for CCS.
%
ALGEBRA ccs
sorts
id, act , rename , relabeling , id_set, restriction,
automaton, state, trans, int,
agent, binding, ('a frame), ('a env), spec
cons
Res_set : id_set -> restriction
Res_var : id -> restriction
Rename : id * id -> rename
Nil : unit -> agent
Bottom : unit -> agent
Ag_var : id -> agent
Prefix : act * agent -> agent
Plus : agent * agent -> agent
Par : agent * agent -> agent
Res : agent * restriction -> agent
Rel : agent * relabeling -> agent
Aut : automaton -> agent
Fix : agent * (agent frame) -> agent
Ag_bind : id * agent -> binding
Set_bind : id * id_set -> binding
Spec : (binding list) -> spec
funs
tau : unit -> act
input : id -> act
output : id -> act
id_parse : string -> id
label_of : act -> id
inverse : act -> act
inverses : act * act -> bool
mk_relabeling : (rename list) -> relabeling
apply : relabeling * act -> act
compose : relabeling * relabeling -> relabeling
mk_set : (id list) -> id_set
member : id * id_set -> bool
insert : id * id_set -> id_set
id_set_union : id_set * id_set -> id_set
empty_set_binding_list : unit -> (binding list)
mk_ag_frame : (binding list) -> (agent frame)
mk_set_frame : (binding list) -> (id_set frame)
empty : unit -> ('a env)
push_frame : ('a frame) * ('a env) -> ('a env)
lookup : id * ('a env) -> 'a
atoi : string -> int
mk_automaton : int * (state list) -> automaton
State : int * (trans list) -> state
Trans : act * (int list) -> trans
rels
transitions : (agent env) * (id_set env) * agent * act * agent -> bool
diverges : (agent env) * (id_set env) * agent -> bool
aut_trans : automaton * act * automaton -> bool
inputs
transitions is [1,2,3]
diverges is [1,2,3]
aut_trans is [1]
pragmas
CWB "user files: ccs_user_decls.sml, ccs_user_lib.sml,
ccs_act.sml, ccs_agent.sml"
CWB "parser entries: act, agent, spec, id_set"
CWB "unparser entries: act, agent, id_set"
CWB "unparser info:
space(1) PLUS space(1),
space(1) PAR space(1),
PREFIX no_break,
space(1) END space(1),
space(1) WHERE space(1),
space(1) AND space(1),
break LBRACE no_break,
space(1) EQUALS space(1) no_break,
ID no_break,
space(1) LCBRACE,
RCBRACE space(1),
COLON space(1)
"
CWB "sharing constraints:
user_decls_sig {
where type int = int
where type id_set = Id.Set.set
where type id = Id.id
where type 'a frame = 'a F.frame
where type 'a env = 'a E.env
where type relabeling = Relabeling.relabeling
where type act = CcsBasicAct.act
where type automaton = CcsAut.automaton
where type trans = CcsAut.trans
where type state = CcsAut.state
}
"
CWB "comments: eoln {\*}"
CWB "cache transitions: parallel_1,parallel_2,parallel_3"
SYNTAX
tokens
"t" => TAU
"'" => PRIME
":" => COLON
"\/" => SLASH
"nil" => NIL
"@" => BOTTOM
"\." => PREFIX
"\+" => PLUS
"\|" => PAR
"\[" => LBRACE
"]" => RBRACE
"where" => WHERE
"and" => AND
"end" => END
"proc" => PROC
"set" => SET
"\{" => LCBRACE
"}" => RCBRACE
"\(" => LPAREN
"\)" => RPAREN
"," => COMMA
"\=" => EQUALS
"\\" => BACKSLASH
"Aut" => AUT
"start" => START
"[a-zA-Z][a-zA-Z0-9'_-]*" => ID of String
"[1-9][0-9]{0,8} | 0" => INT of String
priorities
noassoc 40 WHERE
right 50 PLUS
right 60 PAR
noassoc 70 BACKSLASH
noassoc 80 PREFIX
noassoc 85 LBRACE
noassoc 90 NIL BOTTOM
nonterminals
spec of spec
binding_list of (binding list)
binding of binding
agent of agent
act of act
restriction of restriction
relabeling of relabeling
rename of rename
id_set of id_set
id of id
rename_list of (rename list)
id_list of (id list)
agent_frame of (agent frame)
agent_binding of binding
agent_binding_list of (binding list)
automaton of automaton
state of state
state_list of (state list)
trans of trans
trans_list of (trans list)
int of int
int_list of (int list)
grammar
spec : binding_list (Spec(binding_list))
binding : PROC id EQUALS agent (Ag_bind(id,agent))
| SET id EQUALS id_set (Set_bind(id,id_set))
agent : NIL (Nil())
| BOTTOM (Bottom())
| id (Ag_var(id))
| act PREFIX agent (Prefix(act,agent))
| agent PLUS agent (Plus(agent1,agent2))
| agent PAR agent (Par(agent1,agent2))
| agent BACKSLASH restriction (Res(agent,restriction))
| agent LBRACE relabeling RBRACE (Rel(agent,relabeling))
| agent WHERE agent_frame END (Fix(agent,agent_frame))
| automaton (Aut(automaton))
| LPAREN agent RPAREN (agent)
act : TAU (tau())
| id (input(id))
| PRIME id (output(id))
restriction : id_set (Res_set(id_set))
| id (Res_var(id))
id_set : LCBRACE id_list RCBRACE (mk_set(id_list))
relabeling : rename_list (mk_relabeling(rename_list))
rename : id SLASH id (Rename(id1,id2))
agent_frame : agent_binding_list (mk_ag_frame(agent_binding_list))
agent_binding : id EQUALS agent (Ag_bind(id,agent))
automaton : AUT LPAREN START EQUALS int COMMA state_list RPAREN
(mk_automaton(int,state_list))
state : int COLON trans_list (State(int,trans_list))
trans : act int_list (Trans(act,int_list))
id : ID (id_parse(ID))
int : INT (atoi(INT))
lists
% for top-level bindings
binding_list is non_empty_list EMPTY_STR EMPTY_STR EMPTY_STR of binding
% for fixpoint operator
agent_binding_list is non_empty_list EMPTY_STR AND EMPTY_STR of
agent_binding
rename_list is non_empty_list EMPTY_STR COMMA EMPTY_STR of rename
id_list is non_empty_list EMPTY_STR COMMA EMPTY_STR of id
% for automata
state_list is non_empty_list EMPTY_STR EMPTY_STR EMPTY_STR of state
trans_list is empty_list EMPTY_STR EMPTY_STR EMPTY_STR of trans
int_list is empty_list LCBRACE COMMA RCBRACE of int
RULES SYNTAX
tokens
"labelof" => LABELOF
"inverses" => INVERSES
"apply" => APPLY
"compose" => COMPOSE
"same" => SAME
"mkRelabeling" => MKRELABELING
"id_set_union" => UNION
"in" => IN
"insert" => INSERT
"mkSet" => MKSET
"mkenv" => MKENV
"\=\=\>" => BIGARROW
"--" => DASHDASH
"--\>" => ARROW
"-" => DASH
"-\>" => SHORTARROW
"""^""" => HAT
"insort" => INSORT
"lookup" => LOOKUP
"push_frame" => PUSH_FRAME
"Diverges" => DIVERGES
priorities
left 110 SLASH
left 120 DASH
nonterminals
agent_env of (agent env)
id_set_env of (id_set env)
ag_lookup of agent
id_set_frame of (id_set frame)
id_set_eqn of binding
id_set_eqn_list of (binding list)
grammar
id : LABELOF LPAREN act RPAREN (label_of(act))
bool : INVERSES LPAREN act COMMA act RPAREN (inverses(act1,act2))
| id IN id_set (member(id,id_set))
| DIVERGES LPAREN agent_env COMMA id_set_env COMMA agent RPAREN
(diverges(agent_env,id_set_env,agent))
| act EQUALS act (act_eq(act1,act2))
relation : agent_env COMMA id_set_env COLON agent DASHDASH act ARROW agent
(transitions(agent_env,id_set_env,agent1,act,agent2))
| agent_env COMMA id_set_env COLON agent HAT
(diverges(agent_env,id_set_env,agent))
| automaton DASH act SHORTARROW automaton
(aut_trans(automaton1,act,automaton2))
agent_env : LBRACE agent_frame RBRACE
(push_frame(agent_frame,empty()))
| PUSH_FRAME LPAREN agent_frame COMMA agent_env RPAREN
(push_frame(agent_frame,agent_env))
id_set_eqn : id EQUALS id_set (Set_bind(id,id_set))
id_set_frame : id_set_eqn_list (mk_set_frame(id_set_eqn_list))
id_set_env : LBRACE id_set_frame RBRACE
(push_frame(id_set_frame,empty()))
agent : LOOKUP LPAREN id COMMA agent_env RPAREN (lookup(id,agent_env))
act : APPLY LPAREN act COMMA relabeling RPAREN (apply(relabeling,act))
relabeling : COMPOSE LPAREN relabeling COLON relabeling RPAREN
(compose(relabeling1,
relabeling2))
| MKRELABELING LPAREN rename_list RPAREN
(mk_relabeling(rename_list))
id_set : LOOKUP LPAREN id COMMA id_set_env RPAREN (lookup(id,id_set_env))
| INSERT LPAREN id COMMA id_set RPAREN (insert(id,id_set))
| UNION LPAREN id_set COMMA id_set RPAREN
(id_set_union(id_set1,id_set2))
lists
id_set_eqn_list is non_empty_list EMPTY_STR EMPTY_STR EMPTY_STR of id_set_eqn
end % ALGEBRA CCS