begin_problem(PDL_vacuum_cleaner_example).
list_of_descriptions.
  name({* PDL vacuum cleaner example 2 *}).
  author({* anon *}).
  status(unknown).
  description({* A formula which says that if the vacuum cleaner agent
        starts in room 1 with charged battery and its goal is to clean
	room 1 and room 2, then it will achive its goals.
        *}).
end_of_list.


list_of_symbols.
% Rr - moveRight, Rl - moveLeft, Rs - suck, Rc - charge,
% br1 - believes that in room1, br2 - in room2, bb - battery charged,
% bc1 - believes room1 clean, bc2 - room2 clean, 
% gc1 - goal to clean room1, gc2 - clean room2.
predicates[ (Rr,2), (r,0), (Rl,2), (l,0), (Rs,2), (s,0), (Rc,2), (c,0), (br1,0), 
	    (br2,0), (bb,0), (bc1,0), (bc2,0), (gc1,0), (gc2,0) ].
% The following interprets dia(r,...) as accessible by Rr,
% dia(l,...) as accessible by Rl, etc.
translpairs[ (r,Rr), (l,Rl), (s, Rs), (c,Rc) ].
end_of_list.

list_of_special_formulae(axioms, eml).
% instances of A2
prop_formula(
  not(and(gc1,bc1))
).
prop_formula(
  not(and(gc2,bc2))
).
% instances of A3 
prop_formula(
  implies(and(gc1, gc2, br1, bb), box(s, and(bc1, gc2, br1, not(bb))))
).
prop_formula(
  implies(and(bc1, gc2, br1, not(bb)), box(r, and(bc1, gc2, br2, not(bb))))
).
prop_formula(
  implies(and(bc1, gc2, br2, not(bb)), box(c, and(bc1, gc2, br2, bb)))
).
prop_formula(
  implies(and(bc1, gc2, br2, bb), box(s, and(bc1, bc2, br2, not(bb))))
).
prop_formula(
  implies(and(gc1, gc2, br1, bb), box(r, and(gc1, gc2, br2, bb)))
).
prop_formula(
  implies(and(gc1, gc2, br2, bb), box(s, and(gc1, bc2, br2, not(bb))))
).
prop_formula(
  implies(and(gc1, bc2, br2, not(bb)), box(c, and(gc1, bc2, br2, bb)))
).
prop_formula(
  implies(and(gc1, bc2, br2, bb), box(l, and(gc1, bc2, br1, bb)))
).
prop_formula(
  implies(and(gc1, bc2, br1, bb), box(s, and(bc1, bc2, br1, not(bb))))
).

% instances of A4
prop_formula(
  implies(not(bb), not(dia(s, true)))
).
prop_formula(
  implies(not(br1), not(dia(r, true)))
).
prop_formula(
  implies(not(br2), not(dia(l, true)))
).
prop_formula(
  implies(not(and(br2, not(bb))), not(dia(c, true)))
).

% instances of A5
prop_formula(
  implies(bb, dia(s, true))
).
prop_formula(
  implies(br1, dia(r, true))
).
prop_formula(
  implies(br2, dia(l, true))
).
prop_formula(
  implies(and(br2, not(bb)), dia(c, true))
).
end_of_list.

% The formula we want to prove below is
% gc1 & gc2 & br1 & bb -> [vac][vac][vac] (bc1 & bc2)
% where vac is the vacuum cleaner's program:
% (gc1?; bb?; (br1?;s) U ((not br1)?;l;s)) U 
% (gc2?; bb?; (br2?;s) U ((not br2)?;r;s)) U
% ( (not bb)?; (br2?;c) U ((not br2)?;r;c)))
                                                                                
list_of_special_formulae(conjectures, EML).
prop_formula(
  implies(
    and (gc1, gc2, br1, bb), 
    box(
      or(
        % rule1 
        comp(test(gc1),
             comp(test(bb),
                  or(comp(test(br1), s),
                     comp(test(not (br1)), comp(l,s))))), 
        % rule2
        comp(test(gc2),
             comp(test(bb),
                  or(comp(test(br2), s),
                     comp(test(not (br2)), comp(r,s))))), 
        % rule 3
        comp(test(not(bb)),
             or(comp(test(br2), c),
                comp(test(not(br2)), comp(r, c))))
      ), % end first vac or
      box(
        or(
          % rule1 
          comp(test(gc1),
               comp(test(bb),
                    or(comp(test(br1), s),
                       comp(test(not (br1)), comp(l,s))))), 
          % rule2
          comp(test(gc2),
               comp(test(bb),
                    or(comp(test(br2), s),
                       comp(test(not (br2)), comp(r,s))))), 
          % rule 3
          comp(test(not(bb)),
               or(comp(test(br2), c),
                  comp(test(not(br2)), comp(r, c))))
  	 ), % end second vac or
         box(
           or(
             % rule1 
             comp(test(gc1),
                  comp(test(bb),
                       or(comp(test(br1), s),
                          comp(test(not (br1)), comp(l,s))))), 
             % rule2
             comp(test(gc2),
                  comp(test(bb),
                       or(comp(test(br2), s),
                          comp(test(not (br2)), comp(r,s))))), 
             % rule 3
             comp(test(not(bb)),
                  or(comp(test(br2), c),
                     comp(test(not(br2)), comp(r, c))))
	   ), % end third vac or
           and(bc1, bc2))))
  ) % end implies
).
end_of_list.
                                                                                
end_problem.