% Modified Dong Jin Song's worker example
% by Andrew E. Santosa
% To run: ?- run(X). where X = 0 (no noise), 1 (display states visited),
% 2 (display states visited, and stop for input at each state).

% Number of processes
processnum(1).

% 1 more than the biggest program point
saved_base(3).

% No symmetry for this problem
have_symmetry(0).

% Leave as is.
which_table([X|_], X).

% Free variable for each program variable
genvars([_, _, _]).

% Invariant: Note that invariants are only checked, not
% adding constraints.
invariant([X, _Y, Z]) :-
	X >= 0, Z >= 0.

% Initial State
start_labels([0]).
start_mem([_X, Y, _Z]) :- Y = 0.

% Transitions
trans([0], [1], [_X, Y, Z], [X1, Y1, Z1]) :-
	E >= 0, X1 = E, Y1 = 0, Z1 = Z + E, X1 - Y <= 10.
trans([1], [2], [X, Y, _Z], [X1, Y1, Z1]) :-
	E >= 0, X1 = X + E, Y1 = Y, Z1 = E, Y < 4, X - Y <= 10, Z1 < 2.
trans([2], [1], [X, Y, Z], [X1, Y1, Z1]) :-
	E >= 0, X1 = X + E, Y1 = Y + Z, Z1 = Z + E, Z < 2, X1 - Y1 <= 10.
trans([1], [0], [X, Y, Z], [X1, Y1, Z1]) :-
	E >= 0, X1 = X + E, Y1 = X, Z1 = Z + E, 8 < X - Y, X - Y <= 10.


% Wrapper, containing the question on whether the worker
% can possibly stay out of his house for 15 hours or more
% In fact she can, and the run will show a counterexample
%
% But she actually can't stay out of house for more than 16
% hours, so you can try with Y >= 16 instead.

run(_) :-
	ztime, fail.
run(Noise) :-
	Y >= 15, cs(0, Noise, [x, y, z], [0], [_X, Y, _Z]).
run(_) :-
	ctime(T),
	counter_value(attempted_node, Anode),
	counter_value(unsubsumed_node, Unode),
	printf("Time % seconds, Stored % nodes, Redundant % nodes\n", [T, Unode, Anode]).

:- consult('u28b.clpr').