module storing_and_withdrawing
  depends on entity_event_and_action

  sort declarations
    store :: actions
    withdraw :: actions
  
  function declarations
    fluents
      basic
        is_stored : entity -> booleans
        stored_in : entity * tangible_entity -> booleans

        content :  tangible_entity * entity -> booleans


  axioms
    is_stored(O) if stored_in(O, B).
    -stored_in(O, B) if -is_stored(O).

    false if instance(X, store),
             -defined_object(X).

    false if instance(X, store),
             -defined_base(X).

    false if instance(X, store),
             base(X, B),
             -instance(B, tangible_entity).

    false if instance(X, store),
             base(X, B1),
             base(X, B2),
             instance(B1, tangible_entity),
             instance(B2, tangible_entity),
             B1 != B2.

    occurs(X) causes stored_in(O, B) if instance(X, store),
                                        object(X, O),
                                        base(X, B).

    occurs(X) causes content(B, O) if instance(X, store),
                                      object(X, O),
                                      base(X, B).

    impossible occurs(X) if instance(X, store),
                            object(X, O),
                            base(X, B),
                            stored_in(O, B).


    false if instance(X, withdraw),
             -defined_object(X).

    false if instance(X, withdraw),
             -defined_base(X).

    false if instance(X, withdraw),
             base(X, B),
             -instance(B, tangible_entity).

    false if instance(X, withdraw),
             base(X, B1),
             base(X, B2),
             instance(B1, tangible_entity),
             instance(B2, tangible_entity),
             B1 != B2.

    occurs(X) causes -stored_in(O, B) if instance(X, withdraw),
                                         object(X, O),
                                         base(X, B).

    occurs(X) causes -content(B, O) if instance(X, withdraw),
                                       object(X, O),
                                       base(X, B).

    impossible occurs(X) if instance(X, withdraw),
                            object(X, O),
                            base(X, B),
                            -stored_in(O, B).