is labeled

and goes to the vertex

The modified transition system is nondeterministic, in the sense that it contains a pair of different edges that start at the same vertex and have the same label.

This change can be reflected in the language of CCalc by replacing the proposition

shoot causes -alivein the original formalization of the shooting domain with

shoot may cause -alive.

**Exercise 2.6.**
In the modified domain, the assumptions of the Yale Shooting Problem
(the person is initially alive, then the gun is loaded, then he waits, and
then he is shot) entails neither that the fluent *alive* is true in
the final state nor that it is false. Verify this assertion using CCalc.

In the examples discussed so far in this tutorial we have seen CCalc
propositions of three kinds: `causes` propositions,
`nonexecutable` propositions and `may cause` propositions.
The reader familiar with action language C+ knows
that all these expressions are actually abbreviations for special kinds of
"fluent dynamic laws" (see
NMCT,
Appendix B). The general form of a fluent dynamic law is

where *F*, *G* and *H* are formulas; *F* and *G*
are not allowed to contain symbols for actions. In particular,

is shorthand for

("there is a cause for *F* to hold after the execution of action
*A* in a state satisfying condition *G*"). The proposition

is shorthand for

The proposition

is expanded into

-- if *F* holds after the execution of action *A* in a state
satisfying condition *G* then there is a cause for this. In other
words, *F* is a possible outcome of *A*; *F* is allowed to
become true after executing *A*, but this outcome is not required.

The reader familiar with C+ knows also that there is no syntactic
category of "inertial fluents" in that language. The syntax of C+
distinguishes between two kinds of fluent constants -- simple and
statically determined. If *C* is a simple fluent constant then

is shorthand for the set of fluent dynamic laws

for all possible values *V* of *C*: if *C* has
now the same value *V* that it had before then there
is a cause for this. (Intuitively, inertia is the cause; this is how
fluent dynamic laws solve the frame problem.) These fluent dynamic laws
are similar to those obtained by expanding `may cause` propositions:
they also have the form
`caused` *F* `if` *F* `after` ... .

In accordance with this understanding of inertial fluents, an
`inertialFluent` declaration in CCalc code is an abbreviation for a
`simpleFluent` declaration combined with an `inertial`
proposition. For instance, the declaration

:- constants c :: inertialFluent(0..n).has the same meaning as

:- constants c :: simpleFluent(0..n). inertial c.Forward to Section 2.3: Counting Bullets Back to Section 2.1: Basic Formulation Up to the Table of Contents