missionaryCannibal - integer/interval sorts

[zhangyuanlin]

1) there seem to be issues on integers in type checking 2) sort [0..3] is not allowed yet. if allowed, consequence to type checking.

Should this be of high priority? If decided to work on it, do we need to discuss first?

=== source code and error message for missionaryCannibal % Errors (semantic) % Message: Sort mismatch in expression [TN-N at (66:19)]. Sort [any type] was expected but a term of sort [integers] occurred. % Message: Sort mismatch in expression [TN-N at (66:19)]. Sort [integers] was expected but a term of sort [integers] occurred. % Message: Sort mismatch in expression [n_m(X,c)+n_m(X,m) at (93:12)]. Sort [any type] was expected but a term of sort [integers] occurred. % Bug/missing functionality: sort [0..3] is not allowed yet. if allowed, consequence to type checking. % This is a reified version of the system description % for missionaries and cannibals problem. % -- YL, Aug 2018 system description missionariesAndCannibals theory missionariesAndCannibals module missionariesAndCannibals sort declarations % sort for banks of the river. bank :: universe % sort of all thing type in the problem % we have people type (missionary, cannibal) and equipment type (boat) things :: universe equipment, people :: things % Action move(NC, NM, Dest) - % move NC canabals and NM missionaries % to bank Dest move :: actions attributes % n_m(X) - number of people type X (cannibal or missionary) to move % [0..3] is an integer range % ?? do we allow anonymous sort, {m, c} n_m: things -> integers % dest - the destination dest: bank

constant declarations
    % m: missinory; c: cannibal, b: boat
    c, m : people
    b: equipment

function declarations
    statics
      basic
        % opposite(X) - the opposite bank of bank X.
        opposite: bank -> bank
        % totalNumber(T) - the total number of type T (b, m or c)
        totalNumber: things -> integers
    fluents
      basic
        % n(T, B) - the number of type T at bank B
        n: things * bank -> integers
      defined
        % casualties - true if cannibals outnumber missionaries
        casualties: booleans

axioms
    dynamic causal laws
      % move(NC, NM, Dest) will increase the number of
      % missionaries/cannibals/boat at bank Dest by NM/NC/1.
      occurs(X) causes n(T, Dbank) = N+NT if
        instance(X, move),
        n_m(X, T) = NT,
        dest(X) = Dbank,
        n(T, Dbank) = N.
    state constraints
      % the things at one bank is the total number
      % minus those at the opposite bank
      n(T, opposite(B)) = NewN if
        n(T, B) = N,
        % NewN = totalNumber(T) - N, % bug
        NewN = TN - N,
        TN = totalNumber(T).
      % Do we need extra state constraint to make sure
      % n(b, bank1) != n(b,bank2)? (This should be implied by above law)

      % casualties should be avoided in every state.
      false if casualties.

    function definitions
      % casualties - true if cannibals outnumber missionaries
      casualties if
        n(c,B) > n(m,B),
        n(m,B) > 0. % make sure we have a missionary
    executability conditions
      % move(NC, NM, Dest) not possible if boat capacity is exceeded.
      impossible occurs(X) if
        instance(X, move),
        n_m(X,c) = NC,
        n_m(X,m) = NM,
        NC + NM > 2.

      % move(NC, NM, Dest) not possible if no one is on boat.
      impossible occurs(X) if
        instance(X, move),
        % n(X,c) = NC,
        % n(X,m) = NM,
        % NC + NM = 0.
        n_m(X, c) + n_m(X, m) = 0.

      % move(NC, NM, Dest) not possible if boat is not at source bank
      % this is covered by the next executibility condition
      %impossible occurs(X) if
      %  instance(X, move),
      %  dest(X) = Dbank,
      %  n(b, opposite(Dbank)) = 0. % this n is not attribute n for move action

      % move(NC, NM, Dest) not possible if number of things
      % (cannibals/missionaries/boat) to move is smaller that their
      % number at the source bank.
      impossible occurs(X) if
        instance(X, move),
        n_m(X,T) = NT,
        n(T, opposite(dest(X))) < NT.

    %% A struct to simplify the two rules above may be:
    %% X: move
    %% NC = n(X, c). NM = n(X, m). Dbank = dest(X).
    %% impossible occurs(X) if NC + NM = 0.
    %% impossible occurs(X) if NC + NM > 2.
    %% impossible occurs(X) if
    %%      n(T, opposite(Dbank)) < n(X,T).

structure missionariesAndCannibals instances bank1, bank2 in bank % the two banks of the river % Action move(NC, NM, Dest) - % move NC canabals and NM missionaries % to bank Dest move(NC, NM, Dest) in move n(c) = NC % the number of cannibals to Dest is NC n(m) = NM % the number of cannibals to Dest is NM n(b) = 1 % one boat moves to Dest dest = Dest value of statics % totalNumber: things -> integers totalNumber(m) = 3. totalNumber(c) = 3. totalNumber(b) = 1.

planning problem max steps 12

history % initially all cannibals and missionaries at bank1. observed(n(m,bank1), 3, 0). observed(n(c,bank1), 3, 0). observed(n(b,bank1), 1, 0).

% Our goal is to have all people on bank2 without ever casualties. goal = {n(m, bank2) = 3, n(c, bank2) = 3}

%End of File

[Topology]

These are the items we need decisions on to implement range sorts:

1. name of the sort in the hierarchy? [n..m] --> range_n_to_m
2. Parent sorts in the hierarchy? range_n_to_m :: integers
3. (The integers sort is no longer a predefined sort , it is the finite subset of mathematical Integers that occur in the program)
4. Do we need to automatically detect non-empty intersections of ranges so that there exists a sort that is the intersection for type checking? (If so, I think the shared instances would need to be added in the intersection instead of in the separate ranges.)

It would take about 8 hours of work.

[zhangyuanlin]

name of the sort in the hierarchy? [n..m] --> range_n_to_m

syntax like n..m seems to be generally used. (SPARC also uses n..m). Do you mean to create a sort name range_n_to_m?

Parent sorts in the hierarchy? range_n_to_m :: integers (The integers sort is no longer a predefined sort , it is the finite subset of mathematical Integers that > occur in the program)

maybe we don't need parent sort range_n_to_m/integers. In type checking, it may be easier to use special treatment for intervals/integers (see below).

Do we need to automatically detect non-empty intersections of ranges so that there exists a sort that is the intersection for type checking? (If so, I think the shared instances would need to be added in the intersection instead of in the separate ranges.)

I think we have two options:

1. a set of sorts is integer-compatible if all of them are either interval or integer. A set of sorts is compatible if they are compatible by our earlier definition (when there are no intervals) or they are integer compatible.
   2. For integer compatible sorts, further check if the intersection is empty. (We can put off this for now.)

[Topology]

Right now there is no special semantic treatment of integers. I have not tested any kind of numeric relations: >, <, <=, >=, etc. My thought was to simply treat a finite set of integers as any other finite domain sort, enumerate the instances in the sort and let SPARC or ASP solvers interpret the symbols in the expected domain. Which is why I suggested populating any non-empty intersections of ranges.

If someone declares functions and an axiom:

f: sort1 -> 1..9 h: sort2 -> 5..15 defined g: 1..15 -> booleans

g(A) :- f(X) =A, A = h(Y), instance(X, sort1), instance(Y, sort2).

Minimal effort is to detect intersection and create inferred subsort, populating instances of each sort.

5..9 :: 1..9, 5..15

This would work in the current type checking algorithm, no additional testing required. Changing the type checking algorithm means the changes need to thought about and tested thoroughly. I can do either. But the above is the quickest way of getting to a passable solution that doesn't require theoretical review.

[zhangyuanlin]

That's fine as long as you are sure it is "correct" and done quicker. We can discuss it later.

[Topology]

The below program now has answersets with respect to integer range sorts. (run program in calm.jar to see products)

Work Completed:

1. Integer range sorts are comparable.
2. each range sort has is_a(x, range_low_high) added as a fact where low <= x <= high

Work TBD

1. intersection checking is not completed. It would take some thinking and work to complete specification of intersections properly.

Let me know if there are any problems or changes required.

system description test
        theory test
      module test
        sort declarations
            coordinates :: universe
            points :: universe
               attributes
                  x : coordinates
                  y : coordinates
            1..10 :: coordinates

        constant declarations
            p1 : points
              x = 1
              y = 2

        function declarations
            statics
             basic
                number : 0..10
              defined 
                intersect: booleans

        axioms
            function definitions
            intersect if instance(X, 0..30), X = x(p1). 

[zhangyuanlin]

Great! You might have some "implementation" issue in your mind. That's seems to be alright although I am curious about some details. We can discuss that later. Things seem good and I don't have anything to discuss.

When assign 12 to p1.y, there is no complaint from CALM. I am fine with it for now ...

Just FYI. A more interesting program (likely simpler than what your implementation can allow) below, seems to work well under your new implementation (except no output as reported in #21).

system description test
    theory test
      module test
        sort declarations
            coordinates :: universe
            points :: universe
               attributes
                  x : 1..10
                  y : 1..10

        constant declarations
            p1 : points
              x = 1
              y = 2

        function declarations
            statics
             basic
                number : 0..10
              defined
                intersect: booleans

        axioms
            function definitions
            intersect if instance(X, 0..30), X = x(p1).

[Topology]

I will need to investigate. Type checking should catch that in the end. On a semi-related note, I am having to cheat when it comes to type checking right now. I add a single subsort of all ranges called comparable_integer_sort so that the type checker does not create an empty-type where intersections are expected. when translating I turn the comparable integer sort back into the integers type so that the SPARC program doesn't give it the empty set for instances.

The correct way to do this is to create integer ranges for intersections and populate them. This is more complicated that I was expecting to do and will take some thinking. But once I do that, this error and others should be caught.

For now, I can check that integer occurrences occur as instances within the expected range sorts.

[zhangyuanlin]

I think this bug can be tabled unless you can solve it "by the way". Of course, after the system is stable and we move to the next stage (dissertation/conference paper), I'd like to see a clear mathematical description of how integer/ interval is "processed" as what we've done in NMR paper. - proposal- [a keyword for search for my own use]

[Topology]

Can I have an updated missionary-cannibals program that isolates the missing arithmetic expressions? The one that I have has other issues related to it (ambiguous function definitions):

% This is a reified version of the system description
% for missionaries and cannibals problem. 
% -- YL, Aug 2018
system description missionariesAndCannibals
theory missionariesAndCannibals
module missionariesAndCannibals
        sort declarations
        % sort for banks of the river.
                bank :: universe
        % sort of all thing type in the problem
        % we have people type (missionary, cannibal) and equipment type (boat)
        things :: universe
        equipment, people :: things
        % Action move(NC, NM, Dest) -
        % move NC canabals and NM missionaries
        % to bank Dest
        move :: actions
          attributes
            % n(X) - number of people type X (cannibal or missionary) to move
            % [0..3] is an integer range
            % ?? do we allow anonymous sort, {m, c}
            n: things -> [0..3]
            % dest - the destination
            dest: bank

        constant declarations
        % m: missinory; c: cannibal, b: boat
                c, m : people
        b: equipment

        function declarations
        statics
          basic
            % opposite(X) - the opposite bank of bank X.
            opposite: bank -> bank
            % totalNumber(T) - the total number of type T (b, m or c)
            totalNumber: things -> [0..3]
                fluents
          basic
            % n(T, B) - the number of type T at bank B
            n: things * bank -> [0..3]
          defined
            % casualties - true if cannibals outnumber missionaries
            casualties: booleans

        axioms
                dynamic causal laws
          % move(NC, NM, Dest) will increase the number of
          % missionaries/cannibals/boat at bank Dest by NM/NC/1.
          occurs(X) causes n(P, Dbank) = N+NT if
            instance(X, move),
            n(X, T) = NT,
            dest(X) = Dbank,
            n(T, Dbank) = N.
        state constraints
          % the things at one bank is the total number
          % minus those at the opposite bank
          n(T, opposite(B)) = totalNumber(P) - N if
            n(T, B) = N.
          % Do we need extra state constraint to make sure
          % n(b, bank1) != n(b,bank2)? (This should be implied by above law)

          % casualties should be avoided in every state.
          false if casualties.

        function definitions
          % casualties - true if cannibals outnumber missionaries
          casualties if
            n(c,B) > n(m,B),
            n(m,B) > 0. % make sure we have a missionary
        executability conditions
          % move(NC, NM, Dest) not possible if boat capacity is exceeded.
          impossible occurs(X) if
            instance(X, move),
            n(X,c) = NC,
            n(X,m) = NM,
            NC + NM > 2.

          % move(NC, NM, Dest) not possible if no one is on boat.
          impossible occurs(X) if
            instance(X, move),
            % n(X,c) = NC,
            % n(X,m) = NM,
            % NC + NM = 0.
            n(X, c) + n(X, m) = 0.

          % move(NC, NM, Dest) not possible if boat is not at source bank
          % this is covered by the next executibility condition
          %impossible occurs(X) if
          %  instance(X, move),
          %  dest(X) = Dbank,
          %  n(b, opposite(Dbank)) = 0. % this n is not attribute n for move action

          % move(NC, NM, Dest) not possible if number of things
          % (cannibals/missionaries/boat) to move is smaller that their
          % number at the source bank.
          impossible occurs(X) if
            instance(X, move),
            n(X,T) = NT,
            n(T, opposite(dest(X))) < NT.

        %% A struct to simplify the two rules above may be:
        %% X: move
        %% NC = n(X, c). NM = n(X, m). Dbank = dest(X).
        %% impossible occurs(X) if NC + NM = 0.
        %% impossible occurs(X) if NC + NM > 2.
        %% impossible occurs(X) if
        %%      n(T, opposite(Dbank)) < n(X,T).

structure missionariesAndCannibals
        instances
                bank1, bank2 in bank % the two banks of the river
        % Action move(NC, NM, Dest) -
        % move NC canabals and NM missionaries
        % to bank Dest
        move(NC, NM, Dest) in move
            n(c) = NC % the number of cannibals to Dest is NC
            n(m) = NM % the number of cannibals to Dest is NM
            n(b) = 1  % one boat moves to Dest
            dest = Dest
    value of statics
        % totalNumber: things -> [0..3]
        totalNumber(m) = 3.
        totalNumber(c) = 3.
        totalNumber(b) = 1.

planning problem
max steps 12

history
% initially all cannibals and missionaries at bank1.
observed(n(m,bank1), 3, 0).
observed(n(c,bank1), 3, 0).
observed(n(b,bank1), 1, 0).

% Our goal is to have all people on bank2 without ever casualties.
goal = {n(m, bank2) = 3, n(c, bank2) = 3}

%End of File

Other semantic errors:

--------------------------
---- NO SYNTAX ERRORS ----
--------------------------

-------------------------
---- SEMANTIC ERRORS ----
-------------------------

ErrorID: FND009
Message: Function usage [n(P,Dbank) at (test.alm:50:27)] is ambiguous and matches more than one function declaration: [n:things*bank->0..3 at (test.alm:41:12)] and [n:things->0..3 at (test.alm:22:12)].
Explanation: Ambiguous function usage is not supported in this version of ALM.
Recommendation: Either add instance(X,sort) literals to disambiguate the arguments signature or remove one of the function declarations.

ErrorID: FND003
Message: Function [n(P,Dbank)=N+NT at (test.alm:50:27)] has not been declared prior to use.
Explanation: All functions must be declared prior to use.
Recommendation: Either create a function declaration for the function to change it to the correct function name.

ErrorID: FND009
Message: Function usage [n(T,opposite(B)) at (test.alm:58:10)] is ambiguous and matches more than one function declaration: [n:things*bank->0..3 at (test.alm:41:12)] and [n:things->0..3 at (test.alm:22:12)].
Explanation: Ambiguous function usage is not supported in this version of ALM.
Recommendation: Either add instance(X,sort) literals to disambiguate the arguments signature or remove one of the function declarations.

ErrorID: FND003
Message: Function [n(T,opposite(B)) at (test.alm:58:10)] has not been declared prior to use.
Explanation: All functions must be declared prior to use.
Recommendation: Either create a function declaration for the function to change it to the correct function name.

ErrorID: CND008
Message: Term  [0 at (test.alm:70:21)] has not been declared as a function term or a constant for any sort.
Explanation: Non pre-defined and non-variable terms must be declared before they are used.
Recommendation: Either add a function definition or a constant definition for the term, or replace it with a declared term.

ErrorID: CND008
Message: Term  [2 at (test.alm:77:22)] has not been declared as a function term or a constant for any sort.
Explanation: Non pre-defined and non-variable terms must be declared before they are used.
Recommendation: Either add a function definition or a constant definition for the term, or replace it with a declared term.

ErrorID: CND008
Message: Term  [0 at (test.alm:85:32)] has not been declared as a function term or a constant for any sort.
Explanation: Non pre-defined and non-variable terms must be declared before they are used.
Recommendation: Either add a function definition or a constant definition for the term, or replace it with a declared term.

The ambiguity of the function definition may be causing other errors in type checking.

[zhangyuanlin]

See below for a version (missionary-reified.tp) with the ambiguity removed.

% This is a reified version of the system description
% for missionaries and cannibals problem. 
% -- YL, Aug 2018
system description missionariesAndCannibals
theory missionariesAndCannibals
module missionariesAndCannibals
    sort declarations
        % sort for banks of the river.
        bank :: universe
        % sort of all thing type in the problem
        % we have people type (missionary, cannibal) and equipment type (boat)
        things :: universe
        equipment, people :: things
        % Action move(NC, NM, Dest) -
        % move NC canabals and NM missionaries
        % to bank Dest
        move :: actions
          attributes
            % n_m(X) - number of people type X (cannibal or missionary) to move
            % [0..3] is an integer range
            % ?? do we allow anonymous sort, {m, c}
            n_m: things -> 0..3
            % dest - the destination
            dest: bank

    constant declarations
        % m: missinory; c: cannibal, b: boat
        c, m : people
        b: equipment

    function declarations
        statics
          basic
            % opposite(X) - the opposite bank of bank X.
            opposite: bank -> bank
            % totalNumber(T) - the total number of type T (b, m or c)
            totalNumber: things -> 0..3
        fluents
          basic
            % n(T, B) - the number of type T at bank B
            n: things * bank -> 0..3
          defined
            % casualties - true if cannibals outnumber missionaries
            casualties: booleans

    axioms
        dynamic causal laws
          % move(NC, NM, Dest) will increase the number of
          % missionaries/cannibals/boat at bank Dest by NM/NC/1.
          occurs(X) causes n(T, Dbank) = N+NT if
            instance(X, move),
            n_m(X, T) = NT,
            dest(X) = Dbank,
            n(T, Dbank) = N.
        state constraints
          % the things at one bank is the total number
          % minus those at the opposite bank
          n(T, opposite(B)) = NAtOpposite if
            n(T, B) = N,
            % NewN = totalNumber(T) - N, % bug
            TN = totalNumber(T),
            NAtOpposite = TN - N.
          % Do we need extra state constraint to make sure
          % n(b, bank1) != n(b,bank2)? (This should be implied by above law)

          % casualties should be avoided in every state.
          false if casualties.

        function definitions
          % casualties - true if cannibals outnumber missionaries
          casualties if
            n(c,B) > n(m,B),
            n(m,B) > 0. % make sure we have a missionary
        executability conditions
          % move(NC, NM, Dest) not possible if boat capacity is exceeded.
          impossible occurs(X) if
            instance(X, move),
            n_m(X,c) = NC,
            n_m(X,m) = NM,
            NC + NM > 2.

          % move(NC, NM, Dest) not possible if no one is on boat.
          impossible occurs(X) if
            instance(X, move),
            % n(X,c) = NC,
            % n(X,m) = NM,
            % NC + NM = 0.
            n_m(X, c) + n_m(X, m) = 0.

          % move(NC, NM, Dest) not possible if boat is not at source bank
          % this is covered by the next executibility condition
          %impossible occurs(X) if
          %  instance(X, move),
          %  dest(X) = Dbank,
          %  n(b, opposite(Dbank)) = 0. % this n is not attribute n for move action

          % move(NC, NM, Dest) not possible if number of things
          % (cannibals/missionaries/boat) to move is smaller that their
          % number at the source bank.
          impossible occurs(X) if
            instance(X, move),
            n_m(X,T) = NT,
            n(T, opposite(dest(X))) < NT.

        %% A struct to simplify the two rules above may be:
        %% X: move
        %% NC = n(X, c). NM = n(X, m). Dbank = dest(X).
        %% impossible occurs(X) if NC + NM = 0.
        %% impossible occurs(X) if NC + NM > 2.
        %% impossible occurs(X) if
        %%      n(T, opposite(Dbank)) < n(X,T).

structure missionariesAndCannibals
    instances
        bank1, bank2 in bank % the two banks of the river
        % Action move(NC, NM, Dest) -
        % move NC canabals and NM missionaries
        % to bank Dest
        move(NC, NM, Dest) in move
            n(c) = NC % the number of cannibals to Dest is NC
            n(m) = NM % the number of missionaries to Dest is NM
            n(b) = 1  % one boat moves to Dest
            dest = Dest
    value of statics
        % totalNumber: things -> integers
        totalNumber(m) = 3.
        totalNumber(c) = 3.
        totalNumber(b) = 1.

temporal projection
max steps 12

history
% initially all cannibals and missionaries at bank1.
observed(n(m,bank1), 3, 0).
observed(n(c,bank1), 3, 0).
observed(n(b,bank1), 1, 0).

happened(move(1,1,bank2), 0).
%happened(move(0,1,bank1), 1).
%happened(move(2,0,bank2), 2).
%happened(move(1,0,bank1), 3).
%happened(move(0,2,bank2), 4).
%happened(move(1,1,bank1), 5).
%happened(move(0,2,bank2), 6).
%happened(move(1,0,bank1), 7).
%happened(move(2,0,bank2), 8).
%happened(move(0,1,bank1), 9).
%happened(move(1,1,bank2), 10).

%End of File

[Topology]

check the latest calm.jar with this program. (not the tar.gz file) I am no longer getting math related exceptions.

--------------------------
---- NO SYNTAX ERRORS ----
--------------------------

-------------------------
---- SEMANTIC ERRORS ----
-------------------------

ErrorID: TYP003
Message: Sort mismatch in expression [c at (test.alm:120:14)].  Sort [bank] was expected but a term of sort [people] occurred.
Explanation: The occurring term must belong to a subsort of the expected sort.
Recommendation: Determine if the factors that contribute to the expected sort need to change or if the term must change.

ErrorID: TYP003
Message: Sort mismatch in expression [m at (test.alm:121:14)].  Sort [bank] was expected but a term of sort [people] occurred.
Explanation: The occurring term must belong to a subsort of the expected sort.
Recommendation: Determine if the factors that contribute to the expected sort need to change or if the term must change.

ErrorID: TYP003
Message: Sort mismatch in expression [b at (test.alm:122:14)].  Sort [bank] was expected but a term of sort [equipment] occurred.
Explanation: The occurring term must belong to a subsort of the expected sort.
Recommendation: Determine if the factors that contribute to the expected sort need to change or if the term must change.

[zhangyuanlin]

There is some bug in alm program above. after fixing the bug, it works. I've sent you the alm for p and tp for distribution.

[Topology]

I am closing this issue. The bug reported was not handling the subtract symbol for simple arithmetic expressions. Range expressions are now supported. Any further arithmetic support will fall under support for complex (nested) arithmetic expressions in issue #17.