<b>t</b>.  In terms of the transition system, this modification means that
one more edge is added to the graph.  The edge starts at the vertex<p>

<center>
<i>alive</i>=<b>t</b>,&nbsp;<i>loaded</i>=<b>t</b>,
</center>

<p>is labeled<p>

<center>
<i>load</i>=<b>f</b>,&nbsp;<i>shoot</i>=<b>t</b>
</center>

<p>and goes to the vertex<p>

<center>
<i>alive</i>=<b>t</b>,&nbsp;<i>loaded</i>=<b>f</b>.
</center>

<p>The modified transition system is nondeterministic, in the sense that it
contains a pair of different