Changes between Version 3 and Version 4 of Language

Timestamp:

05/17/23 21:22:41 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -244 +244 @@
 == Statements
 
-=== `$atomic`
+=== Atomic blocks: `$atomic`
 
 An ''atomic block'' is a statement of the form
@@ -279 +279 @@
 Execution of a `$yield` does not change the multiplicity; the process releases the lock but maintains the multiplicity, so that when the lock is re-obtained, the original multiplicity is still in place.
 
-=== `$choose`
+=== Nondeterministic selection statement `$choose`
+
+A `$choose` statement has the form
+{{{
+$choose {
+  stmt1;
+  stmt2;
+  ...
+  default: stmt
+}
+}}}
+The default clause is optional.
+The guards of the statements are evaluated and among those that are true, one is chosen nondeterministically and executed.
+If none are true and the default clause is present, it is chosen.
+The default clause will only be selected if all guards are false.
+If no default clause is present and all guards are false, the statement blocks.
+Hence the implicit guard of the `$choose` statement without a default clause is the disjunction of the guards of its sub-statements.
+The implicit guard of the `$choose` statement with a default clause is ''true''.
+
+Example: this shows how to encode a “low-level” guarded transition system:
+{{{
+l1:
+$choose {
+  $when (x>0) {x--; goto l2;}
+  $when (x==0) {y=1; goto l3;}
+  default: {z=1; goto l4;}
+}
+l2:
+$choose {
+  ...
+}
+l3:
+$choose {
+  ...
+}
+}}}
 
 === `$for`