total function

[zhangyuanlin]

holding is defined as a basic total function (fluent). In a program given later, it is value is not defined for step 0 to 2. Not sure if this is a bug.

The full program:

% holding is a total function. But it is not defined
% in steps 0 to 2. Is it a bug?

system description monkeyBanana
    theory basic_motion
      module moving
        sort declarations
            points, things :: universe
            agents :: things

            carriables :: things

            elevations :: things
              attributes
                top: points

            move :: actions
                attributes
                    actor : agents
                    origin : points
                    dest : points

        function declarations
            statics
                basic
                    symmetric_connectivity : booleans
                    transitive_connectivity : booleans
            fluents
                basic
                    % connnected(P1, P2) - true if P1 and P2 are connected
                    connected : points * points -> booleans
                    % loca_in(T) - the point where thing T is at
                    total loc_in : things -> points
        axioms
            dynamic causal laws
                % move action causes its actor to be at its destination
                occurs(X) causes loc_in(A) = D if
                    instance(X, move),
                    actor(X) = A,
                    dest(X) = D.
            state constraints
                connected(X, X).
                connected(X, Y) if connected(Y, X),symmetric_connectivity.
                -connected(X, Y) if -connected(Y, X),symmetric_connectivity.
                connected(X, Z) if
                    connected(X, Y),connected(Y, Z),transitive_connectivity.
                % NEW bug?

            executability conditions
                % move is not possible if its actor is not at its origin.
                % NEW - what if the origin of actor unknown?
                impossible occurs(X) if
                    instance(X, move),actor(X) = A,loc_in(A) != origin(X).
                    % instance(X, move), loc_in(actor(X)) != origin(X).

                % move is not possible if its actor is at its dest.
                impossible occurs(X) if
                    instance(X, move),actor(X) = A,loc_in(A) = dest(X).
                    % instance(X, move), loc_in(actor(X)) = dest(X).

                % move is not possible if the location of its actor is not
                % connected to its dest.
                impossible occurs(X) if
                    instance(X, move),
                    actor(X) = A,
                    loc_in(A) = O,
                    dest(X) = D,
                    -connected(O, D).

    module carrying_things depends on moving
        sort declarations
            carriables :: things
            % carry <actor, origin, dest, carried_obj>
            %   actor carries carried_obj from origin to dest.
            carry :: move
                attributes
                    carried_object : carriables
            % grasp <grasper, grasped_thing> - rasper grasps grasped_thing
            grasp :: actions
                attributes
                    grasper : agents
                    grasped_thing : things
            % release <releaser, released_thing> -
            %   releaser releases released_thing
            release :: actions
                attributes
                    releaser : agents
                    released_thing : things
        function declarations
            fluents
                basic
                    % holding(A, T) - agent A holds thing T.
                    total holding : agents * things -> booleans
                defined
                    % is_held(T) - thign T is held (by some agent)
                    is_held : things -> booleans
                    % can_reach(A, T) - agent A can reach thing T
                    can_reach : agents * things -> booleans
        axioms
            dynamic causal laws
                % grasp causes its grasper to hold its grasped_thing
                occurs(A) causes holding(X,Y) if
                    instance(A,grasp), grasper(A) = X, grasped_thing(A) = Y.
                % release causes its releaser not to hold its grasped_thing.
                occurs(A) causes -holding(X,Y) if
                    instance(A,release), releaser(A) = X, released_thing(A) = Y.
            state constraints
                % If A holds T, then they have the same location.
                loc_in(T) = P if holding(A,T), loc_in(A) = P.
                loc_in(A) = P if holding(A,T), loc_in(T) = P.
                % An agent can hold only one thing
                -holding(X,Y2) if holding(X,Y1), Y1 != Y2.
                % NEW on default values of carry:
                %   its origin is where the agent is
                % general question - principles of where to
                % "set" values of attributes structure or state constraits?
                % there is a bug below: using fluent (loc_in/1) define attribute
                % origin(C) = P if
                %    instance(C, carry),
                %    loc_in(actor(C)) = P.
            function definitions
                is_held(X) if holding(T,X).
                % Agent M can reach O if they are in the same location
                can_reach(M,O) if loc_in(M) = loc_in(O).
            executability conditions
                % grasp is not possible if its grasper already holds its grasped
                impossible occurs(A) if instance(A,grasp), grasper(A) = X, grasped_thing(A) = Y, holding(X,Y).
                % grasp is not possible if its grasper cannot reach its grasped
                impossible occurs(A) if
                    instance(A,grasp), grasper(A) = X,
                    grasped_thing(A) = Y, -can_reach(X,Y).
                % release is not possible if its releaser does not hold its grasped
                impossible occurs(A) if
                    instance(A,release), releaser(A) = X,
                    released_thing(A) = Y, -holding(X,Y).
                % move is not possible if its actor is held.
                impossible occurs(X) if
                    instance(X,move), actor(X) = A, is_held(A).
                % carry is not possible if its actor does not hold its carried
                impossible occurs(X) if
                    instance(X,carry), actor(X) = A,
                    carried_object(X) = C, -holding(A,C).

    %module main depends on moving
    module main depends on carrying_things
        sort declarations
            floor_points, ceiling_points, movable_points :: points

            climb :: move
              attributes
                elevation : elevations

        constant declarations
            monkey : agents
            box :  elevations
            %  top = top(box)
            % top(elevations): movable_points
            box, banana : carriables
        function declarations
            statics
                basic
                    % under(P, T) - point P is under thing T
                    under : floor_points * things -> booleans
            axioms
                function definitions
                    % monkey can reach the banana if it is on top of the box
                    % which under the banana
                    can_reach(monkey, banana) if
                      loc_in(box) = P, under(P,banana),loc_in(monkey) = top(box).
                state constraints
                    % top(E) is the destination of climbing an elevation E
                    % NEW ??
                    %dest(A) = C if instance(A, climb), elevation(A) = E, C = top(E).
                    % top(E) is the destination of climbing an elevation E
                    dest(A) = C if elevation(A) = E, C = top(E).
                    % The location of the box is connected to the top of the box
                    connected(T,P) if
                        loc_in(box) = P, T= top(box), instance(P, floor_points).
                    % top of box is not connected to
                    % any points other than the box's location.
                    %-connected(top(box),P) if
                    %   loc_in(box) != P, instance(P,floor_points).
                    % workaround of the above
                    -connected(TE,P) if
                      loc_in(box) != P, instance(P,floor_points), TE = top(box).
                    % any two points on floor are connected
                    connected(P1,P2) if
                        instance(P1,floor_points), instance(P2, floor_points).
                    % any ceiling point is not connected to any other point
                    -connected(P1, P2) if
                        instance(P1, ceiling_points),
                        instance(P2,points), P1 != P2.
                executability conditions

    structure monkey_and_banana
    instances
        under_banana, initial_monkey, initial_box in floor_points
        initial_banana in ceiling_points
        box in elevations
            % top = top(box)
            top = t(box)

        t(X) in movable_points where instance(X, elevations)

        move(P) in move where instance(P, points)
            actor = monkey
            dest = P

        carry(box, P) in carry where instance(P, floor_points)
            actor = monkey
            carried_object = box
            dest = P
        grasp(C) in grasp where instance(C, carriables)
            grasper = monkey
            grasped_thing = C
        release(C) in release where instance(C, carriables)
            releaser = monkey
            released_thing = C

        climb(box) in climb
            actor = monkey
            elevation = box
            dest = t(box)

    value of statics
        under(under_banana, banana).
        symmetric_connectivity.
        -transitive_connectivity.

temporal projection
max steps 7
history

    observed(loc_in(box), initial_box, 0).
    observed(loc_in(monkey), initial_monkey, 0).
%% Plan 1:
%    happened(move(initial_box), 0).
%    happened(grasp(box), 1).
%    happened(carry(box, under_banana), 2).
%    happened(release(box), 3).
%    happened(climb(box), 4).
%    happened(grasp(banana), 5).

%% Plan 2:
happened(    carry(box,under_banana)    , 2    )    .
happened(    move(t(box))    , 3    )    .
happened(    move(initial_box)    , 1    )    .
happened(    grasp(banana)    , 4    )    .
happened(    release(box)    , 3    )    .
happened(    grasp(box)    , 2    )    .

% display (usable only in SPARC program to control answer sets display)
%   observed.
%   happened.
%   loc_in.
%   loc_in.
%   move_origin.
%   can_reach.
%   -can_reach.
%   #floor_points.
%   under.
%   elevations_top.
%   holding.
%   occurs.

[Topology]

related to #23

[zhangyuanlin]

noted. thanks.