Monkey Banana - Test case

[zhangyuanlin]

Test is waiting for resolvent of using attribute for constants with parameters (#10). There may be more bugs for the alm program. Here is the latest I used in my test. Future test should continue from this one.

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

            climb :: move
            attributes
            elevation : elevations

        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
                % top(E) is the destination of climbing an elevation E
                dest(A) = C if elevation(A) = E, C = top(E).

                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 main depends on moving
        sort declarations
            floor_points, ceiling_points, movable_points :: points
        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).
                        % 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).
                        % 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)

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

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

        climb(box) in climb
            actor = monkey
            elevation = box
            dest = top(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).
    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).

[Topology]

In this program, 'top' is not a constant.

        %  top = top(box)
        % top(elevations): movable_points

I think there are some issues.

    box in elevations
        top = top(box)
        % top = t(box)

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

There is a circularity involved in these declarations. This is their likely translation:

   is_a(box, elevations) :- instance(top(box), points)
   is_a(top(X), movable_points) :- instance(X, elevations). 

The rules are satisfied by box not being in elevations.

I think we need to take a step back and ask what we are trying to model. Part of the complication is the name collision between the attribute function 'top' and the attempt at creating object constants 'top'.

If we used different names for things, is there a problem? If so, let's get a minimal program that demonstrates the problem to isolate it from any other concerns.

If the problem is related to name collision, then lets continue that discussion on the namespace issue. I'm beginning to think that even in the ALM program we should be scoping attribute functions to be preceded by the sort names they are available for.

[zhangyuanlin]

This is thread for testing use, not a bug report. Sorry it confuses. The bug is reported in #10.