2021-04-11 10:33:58 (CEST) cTI start

% cTI_lt 0.25 using 23.619 MLIPS SICStus 3.8.5 (x86-linux-glibc2.1): Mon Oct 30 16:34:14 CET 2000.
% cTI: Rt=160ms, Wt=271ms. NTI: Rt=8ms, Wt=10ms at most 95 inferences for useful informations.
% NTI summary: 2 cases unresolved, 0 predicates have been ignored: []

color_map(A,B)terminates_if b(A),b(B).
    % optimal. loops found: [color_map([region(_,_,_)|_],[_|_]),color_map([region(y,y,y)|y],[_|_]),color_map([region(_,y,[y]),region(_,y,[])|_],[y,y|y])]. NTI took    0ms,95i,95i
color_region(A,B)terminates_if b(A),b(B).
    % optimal. loops found: [color_region(region(_,_,_),[_|_]),color_region(region(y,y,y),[_|_]),color_region(region(_,y,[y,y|_]),[y,y|y])]. NTI took    0ms,90i,90i
colors(A,B)terminates_if true.
map(A,B)terminates_if true.
member(A,B)terminates_if b(B).
    % optimal. loops found: [member(x,[_|_])]. NTI took    0ms,72i,72i
members(A,B)terminates_if b(A),b(B).
    % optimal. loops found: [members([_|_],[_|_]),members([y|y],[_|_]),members([y,y|_],[y|y])]. NTI took    0ms,80i,80i
select(A,B,C)terminates_if b(B);b(C).
    % optimal. loops found: [select(x,[A|_],[A|_])]. NTI took    0ms,72i,72i
test_color(A,B)terminates_if b(B).
    % 2 unresolved: [test_color(b,f),test_color(f,f)].
    %  NTI took    0ms, 0i,100i

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 18 proofs the 8 inferred conditions:

color_map(b, b).
    % ==> termination proof established
color_map(b, f).
    % ==> no proof found
color_map(f, b).
    % ==> no proof found
color_region(b, b).
    % ==> termination proof established
color_region(b, f).
    % ==> no proof found
color_region(f, b).
    % ==> no proof found
colors(f, f).
    % ==> termination proof established
map(f, f).
    % ==> termination proof established
member(f, b).
    % ==> termination proof established
member(b, f).
    % ==> no proof found
members(b, b).
    % ==> termination proof established
members(b, f).
    % ==> no proof found
members(f, b).
    % ==> no proof found
select(f, f, b).
    % ==> termination proof established
select(f, b, f).
    % ==> termination proof established
select(b, f, f).
    % ==> no proof found
test_color(f, b).
    % ==> termination proof established
test_color(b, f).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Analyzed program located at URL http://www.complang.tuwien.ac.at/cti/bench/apt/SS_map:

/*
color_map(Map,Colors) :-
	Map is colored with Colors, so that no two neighbors have the same
	color. The map is represented as an adjacency-list of regions
	region(Name,Color,Neighbors), where Name is the name of the
	region, Color is its color, and Neighbors are the colors of the 
	neighbors. 
*/
	color_map([Region|Regions],Colors) :-
		color_region(Region,Colors),
		color_map(Regions,Colors).
	color_map([],Colors).
/*
   color_region(Region,Colors) :-
	Region and its neighbors are colored using Colors so that the
	region's color is different from the color of any of its neighbors.
*/
	color_region(region(Name,Color,Neighbors),Colors) :-
		select(Color,Colors,Colors1),
		members(Neighbors,Colors1).

	select(X,[X|Xs],Xs).
	select(X,[Y|Ys],[Y|Zs]) :- select(X,Ys,Zs).

     members([X|Xs],Ys) :- member(X,Ys), members(Xs,Ys).
     members([],Ys).

%	Program 14.4: Map coloring

member(X,[X|_]).
member(X,[_|T]) :- member(X,T).

	/* Test data */

	test_color(Name,Map) :-
		map(Name,Map),
		colors(Name,Colors),
		color_map(Map,Colors).

	map(test,[region(a,A,[B,C,D]),     region(b,B,[A,C,E]), 
		      region(c,C,[A,B,D,E,F]), region(d,D,[A,C,F]),
			  region(e,E,[B,C,F]),     region(f,F,[C,D,E])]).

	map(west_europe,
		 [	region(portugal,P,[E]),  region(spain,E,[F,P]),
			region(france,F,[E,I,S,B,WG,L]),  region(belgium,B,[F,H,L,WG]),
			region(holland,H,[B,WG]), region(west_germany,WG,[F,A,S,H,B,L]),
			region(luxembourg,L,[F,B,WG]), region(italy,I,[F,A,S]),
			region(switzerland,S,[F,I,A,WG]), region(austria,A,[I,S,WG])]).

	colors(X,[red,yellow,blue,white]).

%	Program 14.5: Test data for map coloring