The compiler uses a regular action representation with explanatory frame axioms and conflict exclusion [Ernst et al.1997]. We adopt a standard fluent model in which time takes nonnegative integer values. State-fluents occur at even-numbered times and actions at odd times. The initial state is completely specified at time zero, including all properties presumed false by the closed-world assumption.
Each test, set, and influence statement compiles to a propositional variable that triggers the associated constraint. Just as logical preconditions and effects are implied by their associated actions, the triggers for metric preconditions and effects are implied by their actions.
The compiler must generate frame axioms for constraint variables as well as for propositional variables, but the axiomatizations are very different. Explanatory frames are used for boolean variables, while for real variables, compilation proceeds in two steps. First, we create a constraint which, if activated, will set the value of the variable at the next step equal to its current value plus all the influences that might act on it (untriggered influences are set to zero). Next, we construct a clause which activates this constraint unless some action actually sets the variable's value.
For a parallel encoding, the compiler must consider certain set and influence statements to be mutually exclusive. For simplicity, we adopt the following convention: two actions are mutually exclusive if and only if at least one sets a variable which the other either influences or sets.
This exclusivity policy results in a plan which is correct if actions at each step are executed strictly in parallel; however, the actions may not be serializable, as demonstrated in Figure 6. In order to make parallel actions arbitrarily serializable, we would have to adopt more restrictive exclusivity conditions and a less expressive format for our test statements.
