%------------------------------------------------------------------------
% Program that is dynamically stratified but not dynamically stratified
% from left-to-right.  It shows that delay is necessary for the correct
% evaluation of dynamically stratified programs (the negation suspension
% transformation is not enough).
%
% Model = {s, ~p, ~q, ~r}
%------------------------------------------------------------------------

:- table s/0, p/0, q/0, r/0.

s :- tnot(p), tnot(q), tnot(r).
p :- tnot(q), r.
q :- tnot(r), p.
r :- tnot(p), q.

%------------------------------------------------------------------------

test_p :- abolish_all_tables, p, fail.
test_p :-
	( p -> writeln('p. p is true') ; writeln('p. p is false (OK)') ),
	( q -> writeln('p. q is true') ; writeln('p. q is false (OK)') ),
	( r -> writeln('p. r is true') ; writeln('p. r is false (OK)') ),
	( s ->
	    ( tnot(s) -> writeln('p. s is undefined')
	    ; writeln('p. s is true (OK)') )
	; writeln('p. s is false') ).
test_s :- abolish_all_tables, s, fail.
test_s :-
	( p -> writeln('s. p is true') ; writeln('s. p is false (OK)') ),
	( q -> writeln('s. q is true') ; writeln('s. q is false (OK)') ),
	( r -> writeln('s. r is true') ; writeln('s. r is false (OK)') ),
	( s ->
	    ( tnot(s) -> writeln('s. s is undefined')
	    ; writeln('s. s is true (OK)') )
	; writeln('s. s is false') ).

test :- test_p, fail.
test :- test_s.