Infinite loop

[light-and-salt]

I'm trying to write some ASP to model the relationship between multiple charts in a dashboard... The following ASP leaves clingo hanging forever (looks like an infinite loop to me).

When I try to manually declare the results I want, it's SATISFIABLE:

% inconsistent(Ti) :- inconsistent_qdomain(_, _, _, _, Ti).
inconsistent(0).
consistent(1).

However, whenever I try to infer inconsistent(Ti), I get the infinite loop:

inconsistent(Ti) :- inconsistent_qdomain(_, _, _, _, Ti).
% inconsistent(0).
% consistent(1).

What did I do wrong? Here is the code that hangs...

% INPUT DASHBOARD
dashboard(1, alive, machine, 0). % the first (empty) dashboard was created by the system
dashboard_has_chart(1, ("my chart 1";"my chart 2";"my chart 3"), alive, human, 0). % human added chart 1 - 3 to dashboard 1

chart("my chart 1", alive, machine, 0). % the first (empty) chart was created by the system
channel("my chart 1", x, alive, machine, 0). % double click "Horsepower" and it went to x shelf
field("my chart 1", x, "Horsepower", alive, human, 0).
quantitative_scale_domain("my chart 1", x, (0,100), alive, machine, 0).
scale_range("my chart 1", x, (1,100), alive, machine, 0).
scale_type("my chart 1", x, linear, alive, machine, 0).

chart("my chart 2", alive, human, 0).
channel("my chart 2", x, alive, human, 0). % drag "Horsepower" to x shelf
field("my chart 2", x, "Horsepower", alive, human, 0).
quantitative_scale_domain("my chart 2", x, (0,99), alive, machine, 0).
scale_range("my chart 2", x, (110,210), alive, machine, 0).
scale_type("my chart 2", x, linear, alive, machine, 0).

% define two mixed-initiative parties
is_initiative(human;machine).

% define life and death (e.g., chart removed)
life(alive;removed).

% if there is a partial revision at Ti
% then Ti is a step
is_step(Ti+1) :- inconsistent(Ti).
#show is_step/1.

% 0 is also a step -- the initial step
is_step(0).

% search for 12 steps ahead (at most)
:- is_step(Ti), Ti > 12.

is_final_step(Tmax) :- #max { Ti: is_step(Ti) } = Tmax.
#show is_final_step/1.

% DEFINE CONSISTENCY
consistent(Ti) :- dashboard(_, _, _, Ti), not inconsistent(Ti).

% helper: include field F
quantitative_scale_domain(CH, C, F, D, alive, I, Ti) :-
  field(CH, C, F, alive, _, Ti),
  quantitative_scale_domain(CH, C, D, alive, I, Ti).
#show quantitative_scale_domain/6. % show source
% #show quantitative_scale_domain/7. % hide inference

% INCONSISTENT_Q_DOMAIN: the same field having diff quantitative domains would be inconsistent (regardless of channel)
inconsistent(Ti) :- inconsistent_qdomain(_, _, _, _, Ti).
% inconsistent(0).
% consistent(1).
{
  inconsistent_qdomain(F, CH1, C1, D1, Ti);
  inconsistent_qdomain(F, CH2, C2, D2, Ti)
} = 2 :-
  quantitative_scale_domain(CH1,C1,F,D1,alive,_,Ti),
  quantitative_scale_domain(CH2,C2,F,D2,alive,_,Ti),
  D1 != D2,
  not exception_axes_not_juxtaposed(),
  not exception_too_much_whitespace(),
  not exception_too_much_color_waste().
#show inconsistent_qdomain/5.

% GOAL
% the final step should be consistent
:- is_final_step(Ti), inconsistent(Ti).

% % GENERATE REVISIONS

% limit: 1 revision step at a time
:- {
  rs_union_qdomain(_, _, _, _, _, Ti+1);
  rs_replace_field(_, Ti+1);
  rs_remove_field(_, _, _, _, _, Ti+1);
  rs_replace_color_constant(_, _, _, Ti+1)
} != 1, inconsistent(Ti).

% get the unioned qdomain [MIN, MAX] of all scales enconding F
unioned_qdomain_global(F, GMIN, GMAX, Ti) :-
  inconsistent_qdomain(F, _, _, _, Ti),
  GMIN = #min { MIN: inconsistent_qdomain(F, _, _, (MIN, _), Ti) },
  GMAX = #max { MAX: inconsistent_qdomain(F, _, _, (_, MAX), Ti) }.
#show unioned_qdomain_global/4.

% can generate a union_scale_domains revision step
% union all
% union by channel
% replace_scale_domain(F, CH, C, MIN, MAX, Ti+1)
% In [all charts, CH1, CH2, ...] and [all encodings, XY, COLOR, ...], change F start and end values to [MIN, MAX]
%     union(F,
%           (CH1, C1, MIN, MAX),
%           (CH1, C2, MIN, MAX),
%           (CH2, C2, MIN, MAX),
%           ...
%           Ti)
0 { rs_union_qdomain(F, CH, C, (MIN, MAX), machine, Ti+1) } 1 :-
  inconsistent(Ti),
  inconsistent_qdomain(F, CH, C, D, Ti),
  unioned_qdomain_global(F, MIN, MAX, Ti),
  D != (MIN, MAX).
#show rs_union_qdomain/6.

% the effect of union_scale_domains
quantitative_scale_domain(CH, C, (MIN, MAX), alive, machine, Ti+1) :-
  rs_union_qdomain(F, CH, C, (MIN, MAX), machine, Ti+1).

% INERTIA

% can inherit field type from previous step
0 { field_type(F, T, I, Ti+1) } 1 :- inconsistent(Ti), field_type(F, T, I, Ti).
% there must be 1 type, per field, per step
:- { field_type(F, _, _, Ti) } != 1, is_field(F), is_step(Ti).

% can inherit dashboard from previous step
0 { dashboard(D, L, I, Ti+1) } 1:- inconsistent(Ti), dashboard(D, L, I, Ti).
% there must be 1 dashboard definition, per step, from its creation till the final step
:- { dashboard(D, _, _, Ti+1) } != 1, dashboard(D, _, _, Ti), is_step(Ti), not is_final_step(Ti).

% can inherit dashboard_has_chart from previous step
0 { dashboard_has_chart(D, CH, L, I, Ti+1) } 1:- inconsistent(Ti), dashboard_has_chart(D, CH, L, I, Ti).
% there must be 1 dashboard_has_chart definition, per step, from its addition to the dashboard till the final step
:- { dashboard_has_chart(D, CH, _, _, Ti+1) } != 1, dashboard_has_chart(D, CH, _, _, Ti), is_step(Ti), not is_final_step(Ti).

% can inherit chart from previous step
0 { chart(CH, L, I, Ti+1) } 1 :- inconsistent(Ti), chart(CH, L, I, Ti).
% there must be 1 chart definition, per step, from its creation till the final step
:- { chart(CH, _, _, Ti+1) } != 1, chart(CH, _, _, Ti), is_step(Ti), not is_final_step(Ti).

% can inherit channel from previous step
0 { channel(CH, C, L, I, Ti+1) } 1:- inconsistent(Ti), channel(CH, C, L, I, Ti).
% there must be 1 channel definition, per chart, per step, from its beginning till the final step
:- { channel(CH, C, _, _, Ti+1) } != 1, channel(CH, C, _, _, Ti), is_step(Ti), not is_final_step(Ti).

% can inherit field from previous step
0 { field(CH, C, F, L, I, Ti+1) } 1 :- inconsistent(Ti), field(CH, C, F, L, I, Ti).
% there must be 1 field definition per step, from its beginning occupation of a channel till the final step
:- { field(CH, C, F, _, _, Ti+1) } != 1, field(CH, C, F, _, _, Ti), is_step(Ti), not is_final_step(Ti).

% can inherit quantitative_scale_domain from previous step
0 { quantitative_scale_domain(CH, C, (MIN, MAX), L, I, Ti+1) } 1 :- inconsistent(Ti),
  quantitative_scale_domain(CH, C, (MIN, MAX), L, I, Ti).
% there must be 1 quantitative_scale_domain definition per step, from its beginning till the final step
:- { quantitative_scale_domain(CH, C, _, _, _, Ti+1) } != 1, quantitative_scale_domain(CH, C, _, _, _, Ti), is_step(Ti), not is_final_step(Ti).

[rkaminsk]

clingo first grounds a program by replacing all variables with variable-free terms. This means you have to limit the maximum number of steps by some finite bound.

If you add something like

inconsistent(Ti) :- inconsistent_qdomain(_, _, _, _, Ti), Ti<42.

then the problem should have a finite grounding.

[light-and-salt]

Wow, this works! Thank you, @rkaminsk for the timely reply! It solves my problem!

inconsistent(Ti) :- inconsistent_qdomain(_, _, _, _, Ti), Ti<42.

This is the culprit in my original non-working code... I thought the following lines would bound Ti, but :- is_step(Ti), Ti > 12. depends on inconsistent(Ti) in the first place... 😅

% if there is a partial revision at Ti
% then Ti is a step
is_step(Ti+1) :- inconsistent(Ti).

% search for 12 steps ahead (at most)
:- is_step(Ti), Ti > 12.

Many thanks! 🙏