:- module( _,[stairs/3],[assertions,regtypes,nativeprops]).

% adapted from the `Symmetrical Stairs` example of the Interproc analyzer
%   http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
%
% var x:int,y:int;
%
% begin
%   x = 0;
%   y = 0;
%   while (x<=99) do
%     if x<=49 then
%       x = x+1;
%       y = y+1;
%     else
%       x = x+1;
%       y = y-1;
%     endif;
%   done;
% OLD:  if (y < 0) then fail; endif;
%   assert(y >= 0);
% end

:- entry stairs(X,Y,ResY) : constraint([X >= 0, Y >= 0]).
:- pred stairs(X,Y,ResY) : constraint([X >= 0, Y >= 0]) => constraint([ResY >= 0]).

stairs(X,Y,ResY) :-
% X,Y ascend to 50
        X =< 49,
        X1 is X + 1,
        Y1 is Y + 1,
        stairs(X1,Y1,ResY).
stairs(X,Y,ResY) :-
% X ascends to 100, y descends to 0
        X > 49,
        X =< 99,
        X1 is X + 1,
        Y1 is Y - 1,
        stairs(X1,Y1,ResY).
stairs(X,Y,Y) :- X > 99.
