2.3. Counting Bullets

In the original formalization of the Yale Shooting Problem (Section 2.1) the gun is assumed to hold at most one bullet--it becomes unloaded after shooting. Let us consider a more general case when the number of bullets in the gun is an integer between 0 and a fixed upper bound. This number goes up by 1 after loading, and goes down by 1 after shooting.

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 loaded as a macro, rather than an action constant. (The two macro definitions are combined here under one :- macros heading, separated from each other by a semicolon.) In the presence of this definition, CCalc expands the line
nonexecutable shoot if -loaded
into
nonexecutable shoot if -(numberOfBullets>0).
Then it eliminates the symbol > from this proposition. This is done in two steps. First, the proposition is rewritten as the schematic proposition

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<capacity
appended to the schematic proposition
load causes numberOfBullets=I+1 if numberOfBullets=I
tells CCalc that the value capacity should not be substituted for I when that proposition is grounded. Similarly, the clause
where I>0
tells CCalc not to use the value 0.

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