Bug 145

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).