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.may cause propositions, like causes propositions, can be conditional (that is, followed by if...).
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
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