Btuc




fluents:
clogged.

armed(P) requires package(P).

unsafe.
actions:
dunk(P) requires package(P).

flush.
always:
inertial armed(P).

inertial clogged.

caused -clogged after flush.

caused -armed(P) after dunk(P).

total clogged after dunk(P).

caused unsafe if armed(P).

executable flush.

executable dunk(P) if not clogged.
initially:
total armed(P).

caused false if armed(P), armed(P1), P <> P1.

caused false if not unsafe.
securePlan.

noConcurrency.

goal: not unsafe?