= `$choose` statement =

== current syntax ==
{{{
$choose{
  S1
  S2
  ...
  default: Sn
}
}}}
`Sk` (`k=1..n`) could be any statement: a compound statement, any kind of atomic statement, a guarded statement, any other statement (if-else, while, for, ...).


=== example ===

{{{
$choose{
  $when(x<0){$when(y>0){int k; k=x+y;}}
  $when(1){ 
    $comm_enqueue(comm, out);
    in = $comm_dequeue(comm, source, recvtag);
  }
  $when(1){
    in = $comm_dequeue(comm, source, recvtag);
    $comm_enqueue(comm, out);
  }
}
}}}

=== the result of the current translation would be ===

`TRANS1`:

{{{
LOC0:
[x<0 && y>0] k=x+y -> LOC3
[true] $comm_enqueue(...) -> LOC1
[comm_probe()] $comm_dequeue(...) -> LOC2

LOC1:
[$comm_probe()] $comm_dequeue(...) -> LOC3

LOC2:
[true] $comm_enqueue(...) -> LOC3

LOC3:
...  
}}}

=== problem of current translation (`TRANS1`) ===
1. when there are new scope introduced by the any clause, the clauses can't share the same source location in the model, because a location is associated with a unique scope; for example, at `LOC0` in `TRANS1`, the first statement accesses `k` but `k` isn't visible in the scope associated to `LOC0` (`LOC0` is corresponding to the scope at `$choose`)
2. a quick solution for 1 is introduce a noop at the beginning of each clause, and move the guard of the first statement of the clause to the noop; this would translate the example into `TRANS2`:

`TRANS2`:
{{{
LOC0:
[x<0 && y>0] noop -> LOC1
[true] noop -> LOC2
[comm_probe()] noop  -> LOC3

LOC1:
[true] k=x+y; -> LOC

LOC2:
[true] $comm_enqueue(...) -> LOC4

LOC3:
[true] $comm_dequeue(...) -> LOC5

LOC4:
[$comm_probe()] $comm_dequeue(...) -> LOC6

LOC5:
[true] $comm_enqueue(...) -> LOC6

LOC6:
...  
}}}

=== problem of `TRANS2` ===
There are still a few problems in the above translation (`TRANS2`):

1. it breaks the checking of potential deadlock. CIVL will report a false alarm of a potential deadlock.
2. the extra noop changes the semantics slightly: for example, if at LOC0, the first noop is chosen to executed, i.e., `x<0 && y>0` is evaluated to be true; and then another process updates the value of `x` or `y` and then `x<0 && y>0` is no longer true, but since the process is now at LOC1, so the statement `k=x+y` will still be executed. This conflicts with the semantics of the guarded statement `$when(x<0){$when(y>0){int k; k=x+y;}}`.

== new solutions ==

=== new syntax ===

- requires curly braces in each clause of `$choose` , not allowing clauses to introduce new scopes
{{{
choose_stmt: ‘$choose’ ‘{‘  choose_clause+ ‘}’;

choose_clause: 
      ‘{‘ block_item* ‘}’      
    | when_stmt   
    | labeled_stmt 
}}}

- uses labels
{{{
$choose {

  LABEL0:  stmt*;

  LABEL1:  stmt*;


}
}}}

=== translation notes ===

- inside a compound statement that is the body of a `$when`/`$atomic`/`$atom` or a clause in a `$choose`, if the first item is a declaration a no-op is inserted before it in translation.  Then you are guaranteed that the guard will never involve a new variable. 

example:

{{{
$when (e) {int x; blah}  translated to:   
    LOC0 -e:noop-> LOC1(int x)
$when (e) {$when (f) S} translated to: (let So the first atomic statement in S)
    LOC0 -e&&f:S0-> LOC1  if S0 is not a variable declaration
or otherwise
    LOC0 -e&&f:noop-> LOC1(variable declared by S0) 
$when (e) {$comm_dequeue; …} translated to: 
    LOC0 -e&&$comm_probe(…):$comm_dequeue()-> LOC1
}}}