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