The modeling language should be extended with value passing over channels. Such an extension of the language was designed a year or two ago. Plans for an implementation should be made. I assign this to Marius, as he was involved in the initial design.

Yes, I will allocate some of my freetime to this after hard-deadline has passed.

SYNTAX: VALUE PASSING DECLARATIONS I propose to extend the syntax for (channel) variable initializer to include the type of values to be passed through channel: Initializer: Expression /* ordinary variable initializer */ | '{' FieldInitList '}' /* struct variable initializer */ | '{' TypeList '}' ArrayDecl /* value types and size of channel queue */ | '{' TypeList '}' ; /* just value types, assume size=0, i.e. handshake */ ArrayDecl: '[' Expression ']' ; The above yelds the following backward compatible sentences: chan a = { int, int[5,10] } [5]; chan b = { int, int[5,10] }; // assume default [0] for handshake chan c[4] = { int, int[5,10] } [5]; // array of channels Now, if you are C-person it looks OK, but if you are Promela-person you would expect some more syntactical sugar like: chan a = [5] of { int, int[5,10] }; I can massage the bison grammar for one of those forms, please make up your mind here (are we C or Promela oriented?). SYNTAX: VALUE PASSING EXPRESSIONS I propose to extend syntax for synchronization expressions to the following: SyncExpr: Expression '!' ArgList | Expression '?' Arglist ; ArgList: /* empty */ | Expression /* single value */ | ArgList ',' Expression ; /* several values */ Which would yeld the following sentenced on edge synchronization: a ! x, y a ? i, j where x, y, i and j are expressions of compatible types with a initializer. SEMANTICS OF VALUE PASSING Expressions on sending and receiving transitions should be side-effect-free. Upon synchronization(s) of "a!x,y" and "a?i,j" the following should happen: 1) Evaluate the sending expressions (x,y) and the receiving expressions (i,j). 2) the receiving expressions may yeld either right-value (reference to variable) or left-value (constant or reference to expression computed value): 2.1) check the types of corresponding expressions 2.2) compare all receiving lvalue expressions with corresponding shouting values like guards (i==x && j==y in case i and j are lvalue expressions) and discard the receiving transition if this "guard" is not satisfied. 2.3) execute assignments on rvalue expressions to corresponding sending expressions (i=x, j=y in case i and j are rvalue expressions). Similarly to Promela, I propose to have a default function "template" for converting rvalue expression to lvalue which is defined for all available types, in C++ I would express this as: template <type EXPR> EXPR lval(EXPR value) { return value; }; Note that it is not necessary as we may require user to use his own defined function to do the same thing. QUEUED SYNCHRONIZATION SEMANTICS This is future work. I guess queueing will contribute to the size of symbolic state and to the whole state space as it becomes asynchronous. Although, it is good to have syntax denoting queue size for later use when it is implemented in engine if at all. NOTES I already have pretty-printer working to the syntax above, will commit changes when type-checker is done, so please send your comments.

Gerd (and Kim?) asked to have conditions on receiving synchronization, hence some ideas on that: 1) sending part: a ! x, y, z receiving part: a ? #1>5, i==#2, j=#3, k=#1+#3 where #1 denotes the first variable value in structure that is passed via channel, i.e. x, #2 means value of y and #3 is z. semantics of such synchronization would be: synchronize only if (x>5) and (i==y) then execute j=z, k=x+z perhaps it makes sense to separate conditions from assignments by ";", or require conditions not to be mixed with This would allow conditions to be added to existing guards (transition filter) and assignments to updates (expensive successor filter), hence simpler(?) and more efficient(?) implementation. 2) sending part: a ! x, y, z receiving part: a ? f where f is a function with a signature: boolean f(typeof(x), typeof(y), typeof(z)) semantics would be: execute f with x,y,z as parameters and fire the transition only if function returns true. it looks more powerfull but could probably be executed only in successor filter with additional (expensive) state-copy. There seems to be a potential problem with side-effects in broadcast synchronizations where reveiver could potentially modify the value that is being sent (like a!x,y with a?x=#2,y=#1). Additional static analysis on variables would be needed or we could allow only local values to be transmitted or reveived. any comments?

From interview with Alexandre ;-) Parenthesis around parameters are wanted, and (optionally) conditions could be placed after assignment, like in Ruby. Syntax: sending part: a! (x, y) receiving part: a? (&i, &j) if (i>5 && i+j+k<10) Semantics: i=x, j=y, and synchronization is taken only if (i>5 && i+j+k<10) is true. Implementation: 1) during parsing (or just before model-checking) rewrite the receiving part to the following: a? (&i, &j) if (#1 > 5 && #1 + #2 + k < 10) where #1 and #2 are the references to the first and the second value sent (to be received), k is just another variable. 2) now the conditional part can be checked (in transition filter) just after guard evaluation: if true proceed with successor computation, otherwise discard. 3) value assignments executed in successor filter before assignment. Benefits: cosier syntax, memory save on state size (due to removed reduntant global communication variables) and increased performance (due to avoiding redundant expensive state copy).