Consider the problem of turning on the engines in order to reach a desired total power starting from 0, and to keep it. A possible requirement would be to always have the engines "balanced": at any step of the plan execution, the maximum difference between the power of any engine with that of any other must be at most 1 (see picture, right part). This can be expressed as an extended goal.
(define (domain saturation_balancing)
(:types engine_no power_range total_power_range)
(:functions
(engine_power
?e - engine_no) - power_range
(desired_power)
- total_power_range)
(:action increase_power
:parameters (?e - engine_no)
:precondition (not (= (engine_power
?e) (sup power_range)))
:effect
(assign (engine_power ?e) (+ (engine_power ?e) 1)))
(:action decrease_power
:parameters (?e - engine_no)
:precondition (not (= (engine_power
?e) (inf power_range)))
:effect
(assign (engine_power ?e) (- (engine_power ?e) 1)))
(:action nop)
)
The following problem describes the goal of reaching and keeping full
power from 0 keeping balancing of the powers provided by the engines (see
picture, right part). Intuitively, the CTL goal expresses (a) that maximum
power must be reached (the "AF" clause), and (b) that for
every pair of engines, the maximum allowed power difference is always
1 (the "forall... AG" clause).
Notice that :
(define (problem satbal_pb)
(:domain
saturation_balancing)
(:typedef
engine_no - (range 1 3)
total_power_range - (range 0 6)
power_range - (range 0 2))
(:init
(forall (?e - engine_no)
(= (engine_power ?e) (inf power_range))))
(:ctlgoal
(and
(af (= 6
(sum (?e - engine_no) (engine_power ?e))))
(forall (?e1 - engine_no)
(forall (?e2 - engine_no)
(ag (not (> (engine_power ?e1) (+ (engine_power ?e2) 1)))))))))
To solve the problem, run
MBP-solve -plan_output - <domain> <problem>
where <domain> and <problem> are the domain
and problem above.