Skip to content

Commit

Permalink
Fix a few typos (#1306)
Browse files Browse the repository at this point in the history
  • Loading branch information
lochana-chathura authored Jun 12, 2024
1 parent d686981 commit dae2257
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions lang/spec.html
Original file line number Diff line number Diff line change
Expand Up @@ -8221,7 +8221,7 @@ <h3>Worker message passing</h3>
could be executed more than once.
</p>
<p>
There are three types determined at compile-time for each slot:
There are four types determined at compile-time for each slot:
</p>
<ul>
<li>a message type: if a message v is written to the slot, then v belongs to the
Expand All @@ -8233,15 +8233,15 @@ <h3>Worker message passing</h3>
<li>a send failure type: this is the type of termination failure in the sending
worker that caused the corresponding message not to be sent; more precisely, for
any slot index <var>i</var>, if it is possible for <var>i</var> to be &#x2265;
the value of index <var>w</var> of the queue at the time when the sending worker
the index <var>w</var> of the queue at the time when the sending worker
completes normally with termination value <var>e</var>, then <var>e</var>
belongs to the send failure type of the slot with index <var>i</var>; it is a
compile-time error if the send failure type is not a (possibly empty) subtype of
error;</li>
<li>a receive failure type: this is the type of termination failure in the
receiving worker that caused the corresponding message not to be received; more
precisely, for any slot index <var>i</var>, if it is possible for <var>i</var>
to be &#x2265; the value of index <var>r</var> of the queue at the time when the
to be &#x2265; the index <var>r</var> of the queue at the time when the
receiving worker completes normally with termination value <var>e</var>, then
<var>e</var> belongs to the receive failure type of the slot with index
<var>i</var>; it is a compile-time error if the receive failure type is not a
Expand Down Expand Up @@ -8349,8 +8349,8 @@ <h5>Flush action</h5>
A flush-action with peer-worker R occurring within worker W is associated with the
queue with sending worker W and receiving worker R. Evaluating
the flush-action flushes the queue up to index
<var>i</var> where <var>k</var> is the number of send-actions in W that syntactically
precede the flush-action. More precisely, the evaluation of a flush-action waits until
<var>i</var> where <var>i</var> is the number of send-actions in W that syntactically
precede the flush-action. More precisely, the evaluation of a flush-action waits
until either the index <var>r</var> of the queue is &#x2265;
<var>i</var> or the receiving worker has terminated. It then completes as
follows:
Expand Down

0 comments on commit dae2257

Please sign in to comment.