Changes between Version 37 and Version 38 of Language

Timestamp:

05/21/23 10:26:43 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -341 +341 @@
 
 A `$choose` statement has the form
+  `$choose` `{` ''stmt''+ ( `default` `:` ''stmt'' )? `}`
+For example,
+
 {{{
 $choose {
-  stmt1;
-  stmt2;
-  ...
-  default: stmt
+  $when (x<n) x++;
+  $when (s>0) s--;
+  $default: c++;
 }
 }}}
 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.
@@ -417 +420 @@
 
 A guarded command is encoded in CIVL-C using a `$when` statement:
-{{{
-$when (expr) stmt;
-}}}
-All statements have a guard, either implicit or explicit. For most statements, the guard is ''true''.
+  `$when` `(` ''expr'' `)` ''stmt''
+
+Semantics: all CIVL-C statements have a guard, either implicit or explicit, which specifies when the statement is enabled.
+For most statements (e.g., assignments), the guard is implicitly ''true''.
 The `$when` statement allows one to attach an explicit guard to a statement.
 
-When `expr` is ''true'', the statement is enabled, otherwise it is disabled.
+At a state in which the guard evaluates to ''true'', the statement is enabled, otherwise it is disabled.
 A disabled statement is blocked—it will not be scheduled for execution.
-When it is enabled, it may execute by moving control to the `stmt` and executing the first atomic action in the `stmt`.
-If `stmt` itself has a non-trivial guard, the guard of the `$when` statement is the conjunction of the `expr` and the guard of `stmt`.
-
-The evaluation of `expr` and the first atomic action of `stmt` occur as a single atomic action.
-There is no guarantee that execution of `stmt` will continue atomically if it contains more than one atomic action, i.e., other processes may be scheduled.
+When a `$when` statement is enabled and scheduled for execution, it executes by moving control to ''stmt'' and executing the first atomic action in ''stmt''.
+
+If ''stmt'' itself has a non-trivial guard, the guard of the `$when` statement is the conjunction of ''expr'' and the guard of ''stmt''.
+
+The evaluation of ''expr'' and the first atomic action of ''stmt'' occur as a single atomic action.
+There is no guarantee that execution of ''stmt'' will continue atomically if it contains more than one atomic action, i.e., other processes may be scheduled.
 
 ==== Example