Here is a possible formalization of the modified domain:

:- macros capacity -> 6; loaded -> (numberOfBullets>0). :- constants alive :: inertialFluent; numberOfBullets :: inertialFluent(0..capacity); load, shoot :: exogenousAction. :- variables I :: 0..capacity. load causes numberOfBullets=I+1 if numberOfBullets=I where I<capacity. nonexecutable load if numberOfBullets=capacity. shoot causes -alive. shoot causes numberOfBullets=I-1 if numberOfBullets=I where I>0. nonexecutable shoot if -loaded. nonexecutable load & shoot.In the new formalization, we defined

nonexecutable shoot if -loadedinto

nonexecutable shoot if -(numberOfBullets>0).Then it eliminates the symbol

`nonexecutable shoot
if numberOfBullets=`*var* `& -(`*var*>0)

where *var* is a variable ranging over the domain `0..capacity`
of the constant `numberOfBullets`. Then this schematic proposition is
grounded and, in every ground instance, *var*>0 is replaced
by `true` or by `false` depending on the value of *var*.

Note the `where` clauses appended to two schematic propositions in the
example above. In the proposition describing the effect of `load` on
`numberOfBullets`
we would like `I` to range over `0..capacity-1`; in the
proposition describing the effect of `shoot` on this fluent, we would
like `I` to range over `1..capacity`. Instead of using two
different variables, we declared `I` to be a variable for all numbers
in the interval `0..capacity`, but instructed CCalc not to use the
"bad" values of `I` in the process of grounding the schematic
propositions containing that variable. The clause

where I<capacityappended to the schematic proposition

load causes numberOfBullets=I+1 if numberOfBullets=Itells CCalc that the value

where I>0tells CCalc not to use the value

**Exercise 2.7.**
What do you think will happen if you remove one of the `where` clauses
from the formalization of the shooting domain above and then instruct CCalc to
`loadf` the modified version? Check that your conjecture is correct.

**Exercise 2.8.**
Recall that file `coins` describes the action
of putting a coin in the box. That action is not executable if the box is
full. Consider the extension of that domain that includes also a second
action -- putting two coins in the box. That action is not executable if the
box is full or "nearly full." Represent this extension in the language of
CCalc using only one variable.

The conditions on the values of variables used in `where` clauses are
called *tests*. In a test, variables ranging over subsets of integers
and their values (such as `0` and `capacity`) can be combined
using symbols for arithmetical operations

(the last is integer division). Atomic tests can be formed from arithmetical expressions using equality and the negation of equality

and order relations

Atomic tests can be further combined into complex tests using propositional connectives

(the last two are material implication and equivalence).
Tests are a special case of formulas of the kind
that we see, for instance, after `if` in propositions. What is special
about tests is that they do not contain fluent symbols, so that they can be
evaluated in the process of grounding.

Forward to Section 3.1: Objects and Sorts Back to Section 2.2: Nondeterministic Shooting Up to the Table of Contents