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 -alive

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).

:- constants
 c :: simpleFluent(0..n).

inertial c.