Blocks world assured




fluents: on(B,L) requires block(B), location(L).
occupied(B) requires location(B).

supported(B) requires block(B).
actions: move(B,L) requires block(B), location(L).

always: executable move(B,L) if not occupied(B), not occupied(L), B <> L.
inertial on(B,L).

caused occupied(B) if on(B1,B), block(B).

caused on(B,L) after move(B,L).

caused -on(B,L1) after move(B,L), on(B,L1), L <> L1.
noConcurrency.

initially: caused false if on(B,L), on(B,L1), L<>L1.

always: executable move(B,L) if not occupied(B), not occupied(L), B <> L.
caused false if on(B1,B), on(B2,B), block(B), B1<>B2.

caused supported(B) if on(B,table).

caused supported(B) if on(B,B1), supported(B1).

caused false if not supported(B).