--------------------------------------------------------------------------------------------------------------------------------------- --------------------------------------------------------------------------------------------------------------------------------------- -- -- COWS interpreter & Model Checker - HELP -- --------------------------------------------------------------------------------------------------------------------------------------- --------------------------------------------------------------------------------------------------------------------------------------- -- -- -- ------------------------------------------------------------ COWS Syntax -------------------------------------------------------------- -- -- -- s ::= (services) -- nil (empty activity) -- | kill(k) (kill) -- | u.u'! (invoke) -- | p.o?.s (receive) -- | s1 + ... + sn (receive-guarded choice) -- s1 ... sn must be receive activities -- | s | s' (parallel composition) -- | {s} (protection) -- | [n#] s (name delimitation) -- | [k] s (kill delimitation) -- | [X] s (variable delimitation) -- | * s (replication) -- | A(fparams) (call) -- | let A(fparams)=s in s' end (let construct) -- -- --------------------------------------------------------------------------------------------------------------------------------------- -- -- -- Killer labels: k,k',... (killer labels start with lower case letters, they can only be used as argument of kill -- activities, i.e. they cannot be exchanged in communication) -- -- Variables: X,Y,... (variables start with capital letters) -- -- Service identifiers: A,A',... (each service identifier has a fixed non-negative arity) -- -- Names: n,m,...,p,p',...,o,o',... (names start with lower case letters; we prefer letters p,p',... when we want to stress the -- use of a name as a partner, o,o',... when we want to stress the use of a name as an operation) -- -- Values: v,v',... ::= integerNumber | boolean | Names -- -- Identifiers: u,u',... ::= Variables | Names -- -- Expressions: e,e',... ::= (at runtime, only closed expressions, i.e. expressions without variables, are evaluated) -- Variables -- | Values -- | e+e' (if both e and e' are evaluated as integer numbers then the evaluation of e+e' -- returns the integer number corresponding to their sum, otherwise it returns -- the name corresponding to their concatenation) -- | e=e' (if both e and e' are evaluated as values then the evaluation of e=e' returns -- the boolean true if these values are the same value, otherwise it returns the boolean false) -- -- Invoke arguments: args ::= e | args,args (variables in the same tuple must be pairwise distinct) -- -- Receive parameters: params ::= Variables | Values | params,params (variables in the same tuple must be pairwise distinct) -- -- Formal parameters: fparams ::= Variables | Names | KillerLabels | fparams,fparams (variables in the same tuple must be -- pairwise distinct) -- -- Actual parameters: aparams ::= Variables | Values | KillerLabels | aparams,aparams (variables in the same tuple must be -- pairwise distinct) -- --------------------------------------------------------------------------------------------------------------------------------------- -- -- -- Operators precedence conventions: monadic operators bind more tightly than parallel composition, and prefixing more tightly -- than choice; parentheses can be used in the conventional way to override operators precedence -- -- Communication endpoints: a communication endpoint p.o is composed of a partner name p and of an operation name o; communication -- endpoints of receive activities are identified statically because their syntax only allows using -- names and not variables -- -- Binding: [n#]s binds n in the scope s, [k]s binds k in the scope s, [X] s binds X in the scope s, and let A(fparams)=s in s' end -- binds params in s and A in s' -- -- Closed services: the tool accepts only closed services, i.e. services without free variables, labels and service identifiers -- -- ------------------------------------------------------- COWS informal semantics ------------------------------------------------------- -- -- nil : the empty activity cannot perform any actions -- -- kill(k) : the kill activity forces termination of all unprotected parallel activities that are inside an -- enclosing [k] (that stops the killing effect); kill activities are executed eagerly (i.e. they -- have higher priority than other activities) -- -- p.o! : the invoke activity permits invoking the operation o provided by the partner p and transmitting -- the data resulting from the evaluation of the expressions in args; a service invocation can -- proceed only if the expressions in the argument can be evaluated -- -- p.o?.s : the receive activity offers the invocable operation o along the partner name p; communication -- with a parallel invoke activity using p.o can take place when params matches the tuple of values -- sent by the invoke, and gives rise to substitutions for replacing the variables argument of the -- receive with the corresponding values; once the communication has taken place, the service -- continues as s -- -- s1 + ... + sn : the receive-guarded choice behaves like one of its alternative branches according to which of -- them executes a receive activity -- -- s | s' : execution of parallel services is interleaved, but when a kill activity or a communication is -- performed; the former must trigger termination of all parallel services (see kill(k)), while the -- latter must ensure that only the matching receive that needs fewer substitutions is selected to -- progress (see p.o?.s) -- -- {s} : protection operator can be used to protect s from the effect of a forced termination (see kill(k)); -- this way, {s} behaves like s -- -- [n#] s : the name delimitation permits to generate a fresh names n with scope s (as the restriction -- operator of the pi-calculus); the scope of a name can be extended provided that name captures -- are avoided -- -- [k] s : the killer label delimitation defines the field of action of a kill activity kill(k) (see kill(k)); -- the scope of a killer label cannot be extended -- -- [X] s : the variable delimitation regulates the range of application of the substitution generated by a -- communication (see p.o?.s); this way, a shared state of concurrent threads within each -- service instance can be modelled and updated; the scope of a variable can be extended provided -- that name captures are avoided -- -- * s : the replication operator permits creating an unbounded number of copies of s, i.e. * s behaves -- like s | (* s); this way, replication can be used to implement persistent services and recursive -- behaviours; -- -- A(fparams/aparams) : a service call occurring in the body s' of a construct let A(fparams)=s in s' end behaves like -- the service obtained from s by substituting the formal parameters fparams with the corresponding -- actual parameters aparams -- -- let A(fparams)=s in s' end : the let construct permits to re-use the same 'service code', thus allowing to define services in -- a modular style; let A(params)=s in s' end behaves like s', where calls to A can occur -- (see A(fparams/aparams)) -- -- --------------------------------------------------------------------------------------------------------------------------------------- -- -- -- References: For motivation, informal and formal account of COWS, we refer to the COWS web site: http://rap.dsi.unifi..it/cows/ -- -- ---------------------------------------------------------------------------------------------------------------------------------------