% Compulsory fixed declaration
:- multifile r/5,implicit_updates/0,var2names/2,preds/2,trans_preds/3,cube_size/1.
:- multifile start/1,error/1,refinement/1,cutpoint/1,invgen_template/2,invgen_template/1.
:- multifile cfg_exit_relation/1,stmtsrc/2,strengthening/2.

% data(V1,..,Vn) represents the program variables.
preds(p(_, data(V1, V2)), []).
trans_preds(p(_, data(V1, V2)), p(_, data(V1p, V2p)), []).

% Physical name map.
var2names(p(pc(_), data(V1, V2)), [(V1, 'x'), (V2, 'n')]).

% start location:
start(pc(init)).

% error location:
error(pc(err)).

% cutpoint locations:
cutpoint(pc(loop)).

% template Shape(optional)
% following template is disjunctive template. It represents
% disjunction of conjunction of one linear inequalities.
invgen_template((1;1)).

% More Examples:
%         invgen_template(2).         -> (a/\b)
%         invgen_template((2;2)).     -> (a/\b)\/(c/\d)
%         invgen_template((1;2)).     ->  a \/ ( b/\c )
%         invgen_template([(1;1),1]). -> ( a\/b ) /\ c


% 3 transitions

% x=0;
r(p(pc(init), data(V1, V2)), p(pc(loop), data(V1p, V2p)), [], [V1p = 0, V2p = V2], 1).

% assume(x<n);x++;
r(p(pc(loop), data(V1, V2)), p(pc(loop), data(V1p, V2p)), [(V1 +1 =< V2)], [V1p = V1 + 1, V2p = V2], 2).

% assume(n > 1); assume(x > n);
r(p(pc(loop), data(V1, V2)), p(pc(err), data(V1p, V2p)), [(V1 >= 1+ V2) , ( V2 >= 1)], [V1p = V1, V2p = V2], 3). 


% Result of abstract interpreter(optional)
strengthening(p(pc(loop), data(V1, V2)), [ V1 >= 0 ]). % x >= 0