%%%%%%%%%%%%%%%%%%%%%%%%
% Mode declarations

:- modeh(1,state(+qval,+qval,+qval,+qval,+qval))?
:- modeb(1,deriv(+qval,+qval))?
:- modeb(1,add(+qval,+qval,+qval,[]))?
:- modeb(1,mult(+qval,+qval,+qval,[]))?
:- modeb(1,m_plus(+qval,+qval,[]))?
:- modeb(1,m_minus(+qval,+qval,[]))?
:- modeb(1,mA(+qval,+qval,[]))?
:- op(30,xfy,:)?
:- op(10, xfx, ...)?

%%%%%%%%%%%%%%%%%%%%%%%%
% Type declarations

qval(Var:Mag/Der) :-
	not Var = deriv,
	succ(Var,M1,M2),
	(Mag = M1 ; Mag = M1...M2),
	der(Der).

der(dec).
der(std).
der(inc).

%%%%%%%%%%%%%%%%%%%%%%%%
% Positive examples

% Examples for pole and cart with force constant to right

%%%%%%%%%%%%%%%%%%%%%%%%
% State 1 (initial)
%
%	  <--
%	   |
%	  _|_
%	 |___| -->
%	0=o=o=====================================>

state(x:0/inc,dx:0...inf/inc,th:0/dec,dth:minf...0/dec,ddth:minf...0/dec).

state(x:0/inc,dx:0...inf/inc,th:0...th0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:0/inc,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:0/inc,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:minf...0/std).
state(x:x0/std,dx:0/inc,th:th0/std,dth:0/dec,ddth:minf...0/dec).
state(x:0...inf/inc,dx:0...inf/inc,th:0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:0...inf/inc,dx:0...inf/inc,th:0...th0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:0...inf/inc,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:0...inf/inc,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:minf...0/std).
state(x:x0...0/inc,dx:0...inf/inc,th:0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:x0...0/inc,dx:0...inf/inc,th:0...th0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:x0...0/inc,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:minf...0/dec).
state(x:x0...0/inc,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:minf...0/std).

%%%%%%%%%%%%%%%%%%%%%%%%
% Negative examples

:- state(x:0/dec,dx:0...inf/inc,th:0/dec,dth:minf...0/dec,ddth:minf...0/dec).
	% x changed
:- state(x:0/inc,dx:0...inf/inc,th:0/dec,dth:0/inc,ddth:minf...0/dec).
	% dth changed
:- state(x:0/inc,dx:0...inf/inc,th:0/dec,dth:minf...0/dec,ddth:0/dec).
	% ddth changed
:- state(x:x0...0/dec,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:minf...0/std).
	% x changed
:- state(x:x0...0/inc,dx:0...inf/inc,th:minf...0/dec,dth:0/std,
	ddth:minf...0/inc).
	% dth changed
:- state(x:x0...0/inc,dx:0...inf/inc,th:minf...0/dec,dth:minf...0/dec,
	ddth:0/std).
	% ddth changed


% A si2logic model of pole-on-cart

succ(deriv, dec, std).
succ(deriv, std, inc).

succ( x, minf, x0).
succ( x, x0, 0).
succ( x, 0, inf).

succ( dx, minf, 0).
succ( dx, 0, inf).

succ( ddx, minf, 0).
succ( ddx, 0, inf).

succ( th, minf, 0).
succ( th, 0, th0).
succ( th, th0, inf).

succ( dth, minf, 0).
succ( dth, 0, inf).

succ( ddth, minf, 0).
succ( ddth, 0, inf).

succ( f, minf, negf).
succ( f, negf, 0).
succ( f, 0, posf).
succ( f, posf, inf).

% New variable m1th: m_plus( th, m1th)

succ( m1th, minf, 0).
succ( m1th, 0, inf).

% New variable m2th: m_plus( th, m2th)

succ( m2th, minf, 0).
succ( m2th, 0, inf).

% New variable ath: mA( th, ath)

succ( ath, minf, 0).
succ( ath, 0, inf).

% New variable fath: mult( f, ath, fath)

succ( fath, minf, 0).
succ( fath, 0, athmax).
succ( fath, athmax, inf).

% ---------------------------------------------------------------------------
%
%                            .BOF. SI2_LOGIC
%                   Version with Alen's corrections Dec. 1990
% ---------------------------------------------------------------------------


% ---------------------------------------------------------------------------
%
%                         DIRECTIVES AND OPERATORS
%
% ---------------------------------------------------------------------------




% ---------------------------------------------------------------------------
%
%                                TOP LEVEL
%
% ---------------------------------------------------------------------------




oscil:-
  reconsult(oscil),
  write('Depth: '),
  read(N), nl,
  simulate([x:0/inc, v:v0/std, a:0/dec], N).


oscil2:-
  reconsult(oscil),
  write('Depth: '),
  read(N), nl,
  simulate([x:0/inc, v:vmax/std, a:0/dec], N).

% oscil(File): write trace on File

oscil(File) :-
  reconsult(oscil),
  write('Depth: '),
  read(N), nl,
  tell( File),
  simulatetofile([x:0/inc, v:v0/std, a:0/dec], N),
  told.

oscil2(File) :-
  reconsult(oscil),
  write('Depth: '),
  read(N), nl,
  tell( File),
  simulatetofile([x:0/inc, v:vmax/std, a:0/dec], N),
  told.

heat:-
  reconsult(heat),
  write('Depth: '),
  read(N), nl,
  simulate([ts:ts0/std, t:t0/inc, dt:dt0/dec, q:q0/dec], N).

tube:-
  reconsult(tube),
  write('Depth: '),
  read(N), nl,
  simulate([la:la0/dec, lb:lb0/inc, fab:f0/dec, fba: mf0/inc], N).

% tube( TubeModel): consult file with tube model and run it

tube( File) :-
  reconsult(File),
    write('Depth: '),
      read(N), nl,
	simulate([la:la0/dec, lb:lb0/inc, fab:f0/dec, fba: mf0/inc], N).
	 

tube2:-
  reconsult(tube2),
    write('Depth: '),
      read(N), nl,
	simulate([la:la0/dec, lb:lb0/inc, fab:f0/dec, fba: mf0/inc], N).

tube3:-
  reconsult(tube3),
    write('Depth: '),
      read(N), nl,
	simulate([la:la0/inc, lb:lb0/dec, fab:f0/inc, fba: mf0/dec], N).

tube4 :-
  reconsult(tube4),
    write('Depth: '),
      read(N), nl,
	simulate([la:la0/dec, lb:lb0/inc, fab:f0/dec, fba: mf0/inc], N).
	 

tube_all  :-   % Simulation runs from all legal initial states
  u_tube( LA,LB,FAB,FBA),   % A legal u-tube state
  simulate( [LA,LB,FAB,FBA], 6),
  nl, write('End of run'), nl,nl,
  fail
  ;
  write('End of all possible u-tube traces').

leak:-
  reconsult(leak),
  write('Depth: '),
  read(N), nl,
  simulate([la:la0/dec, lb:lb0/inc, dab:dab0/dec,
            fab:fab0/dec, fba:fba0/inc, fxb:fbx0/dec, fbt : fbt0/dec], N).


polepos  :-
  consult( polepos),
  write( 'Depth: '),
  read( N), nl,
  simulate( [
    x:x0/std, dx:0/inc, ddx:0...inf/std,
    th:th0/std, dth:0/dec, ddth:minf...0/dec,
    f:posf/std, m1th:0...inf/std, mf:0...inf/std, ath:0...athmax/std, mfath:0...inf/std], N).

polerightdet  :-              % 'Determinate' pole on cart withf force pushing right
  reconsult( polerightdet),
    write( 'Depth: '),
      read( N), nl,
	simulate( [
	    x:x0/std, dx:0/inc, ddx:0...inf/std,
		th:th0/std, dth:0/dec, ddth:minf...0/dec,
		    m1th:0...inf/std, ath:0...athmax/std], N).
		     

poleright  :-
  reconsult( poleright),   
    write( 'Depth: '), 
      read( N), nl,    
	simulate( [ 
	    x:x0/std, dx:0/inc, th:th0/std, dth:0/dec, ddth:minf...0/dec ], N ) .
		     
polerighttofile  :-
  reconsult( poleright),
  write( 'Depth: '),
  read( N), nl,
  simulatetofile( [
       x:x0/std, dx:0/inc, th:th0/std, dth:0/dec, ddth:minf...0/dec ], N ) .

								     
poletofile  :-
  reconsult( polepos),
    write( 'Depth: '),
      read( N), nl,
	simulatetofile( [
	    x:x0/std, dx:0/inc, ddx:0...inf/std,
		th:th0/std, dth:0/dec, ddth:minf...0/dec,
		    f:posf/std, m1th:0...inf/std, mf:0...inf/std, ath:0...athmax/std, mfath:0...inf/std], N).



% ---------------------------------------------------------------------------
%
%                                SIMULATOR
%
% ---------------------------------------------------------------------------

% simulate(InitialState, Depth)

simulate(S, N):-
  write(point:S), nl,
  simulate(point:S, 1, N).

simulate(_, _).



simulate(S, M, N):-
  M =< N,
  noninfinity(S),
  M1 is M+1,
  transition(S, S1),
  tab(M), write(S1), nl,
  simulate(S1, M1, N).


simulatetofile(S, N):-
  nl, reformat( S, SS), write_canonical( SS), write(.),
  simulatetofile(point:S, 1, N).

simulatetofile(_, _).



simulatetofile(S, M, N):-
  M =< N,
  noninfinity(S),
  M1 is M+1,
  transition(S, S1),
  S1 = _:SS1, reformat( SS1, SSS1),
  tab(M), write_canonical(SSS1), write(.), nl,
  simulatetofile(S1, M1, N).

reformat( VarList, StateTerm)  :-
  StateTerm =.. [state | VarList].


% ---------------------------------------------------------------------------
%
%                                KERNEL
%
% ---------------------------------------------------------------------------

%  Constraints
%
%    range( Func:Mag/Der, RangeMag/RangeDer) :
%      Mag is inside RangeMag, Der is inside RangeDer,
%      where RangeMag = LowestMag...HighestMag,
%            Der = LowestDer...HighestDer
%      Eg:  range( x:Mag/Der, x0...x0/std...std)   x is constant x0
%
%
%    deriv( F1:M1/D1, F2:M2/D2) :
%      d/dt(F1) =q F2
%
%
%    add( F1:M1/D1, F2:M2/D2, F3:M3/D3, CorrespValList) :
%      F1 + F2 =q F3  with corr. values in CorrValList
%      CorrValList = [ c(Val1,Val2,Val3), c(...), ...]
%
%
%    mult( F1:M1/D1, F2:M2/D2, F3:M3/D3, CorrValList)
%      F1 * F2 =q F3  with corr values in CorrValList
%
%
%    minus( F1:M1/D1, F2:M2/D2, CorrList)
%      F1 =q -F2  with corr. values in CorrList
%      CorrList  =  [ c(Val1, Val2), c(...), ...]
%
%
%   m_plus( F1:M1/D1, F2:M2/D2, CorrList) :
%      F1 is monotonically inc. function of F2 with corr. values in CorrList
%
%
%    m_minus( F1:M1/D1, F2:M2/D2, CorrList) :
%      F1 is monotonically dec. function of F2 with corr. values in CorrList
%
%
%    mA( F1:M1/D1, F2:M2/D2, CorrList) :
%      F2 is an A-monotonic inc. - dec. function of F1 with CorrList
%
%
%    mV( F1:M1/D1, F2:M2/D2, CorrList) :
%      F2 is a V-monotonic dec. - inc. function of F1 with CorrList


range(F:M/D, Rm/Rd):-
  inside_closed(F, M, Rm),
  inside_closed(deriv, D, Rd).

deriv(_:_/D1, F2:M2/_):-
  verify_range_deriv(D1, F2, M2).

add(F1:M1/D1, F2:M2/D2, F3:M3/D3, C):-
  verify_add_inf_consistence(M1, M2, M3),
  verify_add_mag(F1, F2, F3, M1, M2, M3, C),
  verify_add_der(D1, D2, D3).

mult(F1:M1/D1, F2:M2/D2, F3:M3/D3, C):-
  verify_mult_zeroinf_consistence(M1, M2, M3),
  norm_mag(F1, M1, 0, X1),
  norm_mag(F2, M2, 0, X2),
  norm_mag(F3, M3, 0, X3),
  lookup_mult_sign_table(X1, X2, X3),
  verify_mult_mag_and_der(F1, F2, F3, M1, M2, M3, D1, D2, D3, C).

minus(F1:M1/D1, F2:M2/D2, C):-
  verify_minus_zeroinf_consistence(M1, M2),
  norm_mag(F1, M1, 0, X1),
  norm_mag(F2, M2, 0, X2),
  lookup_minus_sign_table(X1, X2),
  verify_minus_mag(F1, F2, M1, M2, C),
  verify_minus_der(D1, D2).

m_plus(F1:Mag1/Der1, F2:Mag2/Der2, C):-
  verify_m_plus_limit( F1, F2, Mag1, Mag2, C),
  m_plus_deriv(Der1, Der2),
  !.

m_minus(F1:Mag1/Der1, F2:Mag2/Der2, C):-
  verify_m_minus_limit(F1,F2,Mag1, Mag2, C),
  m_minus_deriv(Der1, Der2),
  !.

% mA( F1:Mag1/Der1, F2:Mag2/Der2, Corr) :
%   the A-monotonic constr, that is:
%   if Mag1 < 0 then m_plus else m_minus

mA( F1:Mag1/Der1, FQ2, Corr)  :-
  conc( CorrNeg, [ c(0,M) | CorrPos], Corr),     % Divide corr. vals. in neg. and pos.
  (
  less_than( F1, Mag1, 0),       % F1 negative
  m_plus( F1:Mag1/Der1, FQ2, [ c(0,M) | CorrNeg])
  ;
  leseq_than( F1, 0, Mag1),        % F1 positive
  m_minus( F1:Mag1/Der1, FQ2, [ c(0,M) | CorrPos])
  ).


% mV( F1:Mag1/Der1, F2:Mag2/Der2, Corr) :
%   the V-monotonic constr., that is:
%   if Mag1 < 0 then m_minus else m_plus

mV( F1:Mag1/Der1, FQ2, Corr)  :- 
 conc( CorrNeg, [ c(0,M) | CorrPos], Corr),     % Divide corr. vals. in neg. and pos. 
 (
 less_than( F1, Mag1, 0),         % F1 negative
 m_minus( F1:Mag1/Der1, FQ2, CorrNeg)
 ;
 leseq_than( F1, 0, Mag1),        % F1 positive
 m_plus( F1:Mag1/Der1, FQ2, [ c(0,M) | CorrPos])
 ).
	      

% time_descriptor(Old_Td, New_Td)

time_descriptor(point, interval).
time_descriptor(interval, point).



% single_transition(Td, F:M0/D0, TransitionId, F:M/D)

single_transition(point, F:Mag/std,         p1,  F:Mag/std):-
  not Mag = _..._ .

single_transition(point, F:Mag/std,         p2,  F:Mag...Mag1/inc):-
  succ(F, Mag, Mag1).

single_transition(point, F:Mag/std,         p3,  F:Mag1...Mag/dec):-
  succ(F, Mag1, Mag).

single_transition(point, F:Mag/inc,         p4,  F:Mag...Mag1/inc):-
  succ(F, Mag, Mag1).

single_transition(point, F:Mag1...Mag2/inc, p5,  F:Mag1...Mag2/inc).

single_transition(point, F:Mag/dec,         p6,  F:Mag1...Mag/dec):-
  succ(F, Mag1, Mag).

single_transition(point, F:Mag1...Mag2/dec, p7,  F:Mag1...Mag2/dec).

single_transition(point, F:Mag1...Mag2/std, p8,  F:Mag1...Mag2/dec).

single_transition(point, F:Mag1...Mag2/std, p9,  F:Mag1...Mag2/std).

single_transition(point, F:Mag1...Mag2/std, p10, F:Mag1...Mag2/inc).


single_transition(interval, F:Mag/std,         i1, F:Mag/std).

single_transition(interval, F:_...Mag2/inc,    i2, F:Mag2/std).

single_transition(interval, F:_...Mag2/inc,    i3, F:Mag2/inc).

single_transition(interval, F:Mag1...Mag2/inc, i4, F:Mag1...Mag2/inc).

single_transition(interval, F:Mag1..._/dec,    i5, F:Mag1/std).

single_transition(interval, F:Mag1..._/dec,    i6, F:Mag1/dec).

single_transition(interval, F:Mag1...Mag2/dec, i7, F:Mag1...Mag2/dec).

single_transition(interval, F:Mag1...Mag2/inc, i8, F:Mag1...Mag2/std).

single_transition(interval, F:Mag1...Mag2/dec, i9, F:Mag1...Mag2/std).



% verify_range_deriv(QDer, Func, Mag):-

verify_range_deriv(dec, F, M):-
  less_than(F, M, 0).
verify_range_deriv(std, _, 0).
verify_range_deriv(inc, F, M):-
  less_than(F, 0, M).



% verify_add_inf_consistence(Mag1, Mag2, Mag3)

verify_add_inf_consistence(minf, inf, _).
verify_add_inf_consistence(inf, minf, _).
verify_add_inf_consistence(A, inf, X):-
  not A = minf,
  X = inf.
verify_add_inf_consistence(A, minf, X):-
  not A = inf,
  X = minf.
verify_add_inf_consistence(inf, A, X):-
  not A = minf,
  X = inf.
verify_add_inf_consistence(minf, A, X):-
  not A = inf,
  X = minf.
verify_add_inf_consistence(A, B, C):-
  not A = inf,
  not A = minf,
  not B = inf,
  not B = minf,
  not C = inf,
  not C = minf.



% verify_add_mag(Func1, Func2, Func3, Mag1, Mag2, Mag3, Corr)
%   - check add-magnitude consistency.

verify_add_mag(F1, F2, F3, M1, M2, M3, []):-
  norm_mag(F1, M1, 0, A1),
  norm_mag(F2, M2, 0, A2),
  norm_mag(F3, M3, 0, A3),
  lookup_consist_table(A1, A2, A3).

verify_add_mag(F1, F2, F3, M1, M2, M3, [c(C1,C2,C3) |Corr]):-
  norm_mag(F1, M1, C1, A1),
  norm_mag(F2, M2, C2, A2),
  norm_mag(F3, M3, C3, A3),
  lookup_consist_table(A1, A2, A3),
  verify_add_mag(F1, F2, F3, M1, M2, M3, Corr).



% norm_mag(Func, Val1, Val2, Norm_val)  - Norm_val = sgn(Val1-Val2).

norm_mag(_, V, V, zero).

norm_mag(F, V1, V2, neg):-
  not V1 = V2,
  less_than(F, V1, V2).

norm_mag(F, V1, V2, pos):-
  not V1 = V2,
  less_than(F, V2, V1).



% lookup_consist_table(A1, A2, A3)  - add/mult-value-consistency table.

lookup_consist_table(neg,  neg,  neg ).
lookup_consist_table(neg,  zero, neg ).
lookup_consist_table(neg,  pos,  neg ).
lookup_consist_table(neg,  pos,  zero).
lookup_consist_table(neg,  pos,  pos ).
lookup_consist_table(zero, neg,  neg ).
lookup_consist_table(zero, zero, zero).
lookup_consist_table(zero, pos,  pos ).
lookup_consist_table(pos,  neg,  neg ).
lookup_consist_table(pos,  neg,  zero).
lookup_consist_table(pos,  neg,  pos ).
lookup_consist_table(pos,  zero, pos ).
lookup_consist_table(pos,  pos,  pos ).



% verify_add_der(Der1, Der2, Der3)  - chech add-deriv consistency.

verify_add_der(Der1, Der2, Der3):-
  norm_deriv(Der1, D1),
  norm_deriv(Der2, D2),
  norm_deriv(Der3, D3),
  lookup_consist_table(D1, D2, D3).



% norm_deriv(Deriv, Norm_deriv)  - normalise deriv.

norm_deriv(inc, pos ).
norm_deriv(std, zero).
norm_deriv(dec, neg ).



% verify_mult_mag_and_der(Func1, Func2, Func3,
%                         Mag1, Mag2, Mag3, Der1, Der2, Der3, Corr)
%   - check mult-magnitude/derivate consistency.

verify_mult_mag_and_der(F1, F2, _, M1, M2, _, D1, D2, D3, []):-
  norm_deriv(D1, Nd1),
  norm_deriv(D2, Nd2),
  norm_deriv(D3, Nd3),
  norm_mag(F1, M1, 0, Nm1),
  norm_mag(F2, M2, 0, Nm2),
  lookup_mult_sign_table(Nd1, Nm2, X1),
  lookup_mult_sign_table(Nd2, Nm1, X2),
  lookup_consist_table(X1, X2, Nd3).

verify_mult_mag_and_der(F1, F2, F3, M1, M2, M3,
                        D1, D2, D3, [c(C1,C2,C3) |Corr]):-
        norm_mag(F1, C1, 0, Nc1),
        norm_mag(F1, M1, C1, A1),
        norm_mag_sign_correction(A1, Nc1, Cnc1),
        norm_mag(F2, C2, 0, Nc2),
        norm_mag(F2, M2, C2, A2),
        norm_mag_sign_correction(A2, Nc2, Cnc2),
        norm_mag(F3, C3, 0, Nc3),
        norm_mag(F3, M3, C3, A3),
        norm_mag_sign_correction(A3, Nc3, Cnc3),
        lookup_consist_table(Cnc1, Cnc2, Cnc3),
        verify_mult_mag_and_der(F1, F2, F3, M1, M2, M3, D1, D2, D3, Corr).



% norm_mag_sign_correction(A, B, New_a)
%   - sign correction for mult-mag-normalisation.

norm_mag_sign_correction(pos, neg, neg).
norm_mag_sign_correction(neg, neg, pos).
norm_mag_sign_correction(A,   B,   A  ):-
  not B = neg.



% verify_mult_zeroinf_consistence(Mag1, Mag2, Mag3)

verify_mult_zeroinf_consistence(inf, inf, inf).
verify_mult_zeroinf_consistence(inf, minf, minf).
verify_mult_zeroinf_consistence(minf, inf, minf).
verify_mult_zeroinf_consistence(minf, minf, inf).

verify_mult_zeroinf_consistence(0, inf, _).
verify_mult_zeroinf_consistence(0, minf, _).
verify_mult_zeroinf_consistence(inf, 0, _).
verify_mult_zeroinf_consistence(minf, 0, _).

verify_mult_zeroinf_consistence(minf, A, X):-
  not A = inf,
  not A = 0,
  not A = minf,
  (
    X=minf
    ;
    X = inf
  ).
verify_mult_zeroinf_consistence(inf, A, X):-
  not A = inf,
  not A = 0,
  not A = minf,
  (
    X=minf
    ;
    X = inf
  ).
verify_mult_zeroinf_consistence(A, minf, X):-
  not A = inf,
  not A = 0,
  not A = minf,
  (
    X=minf
    ;
    X = inf
  ).
verify_mult_zeroinf_consistence(A, inf, X):-
  not A = inf,
  not A = 0,
  not A = minf,
  (
    X=minf
    ;
    X = inf
  ).

verify_mult_zeroinf_consistence(0, A, 0):-
  not A = inf,
  not A = minf.
verify_mult_zeroinf_consistence(A, 0, 0):-
  not A = inf,
  not A = 0,
  not A = minf.

verify_mult_zeroinf_consistence(A, B, C):-
  not A = inf,
  not A = 0,
  not A = minf,
  not B = inf,
  not B = 0,
  not B = minf,
  not C = inf,
  not C = 0,
  not C = minf.



% lookup_mult_sign_table(V1, V2, V3)  - mult-sign-consistency.

lookup_mult_sign_table(zero, _  ,  zero).
lookup_mult_sign_table(X   , zero, zero):-
  not X = zero.
lookup_mult_sign_table(pos,  pos,  pos ).
lookup_mult_sign_table(pos,  neg,  neg ).
lookup_mult_sign_table(neg,  pos,  neg ).
lookup_mult_sign_table(neg,  neg,  pos ).



% verify_minus_zeroinf_consistence(Mag1, Mag2)

verify_minus_zeroinf_consistence(0, 0).
verify_minus_zeroinf_consistence(inf, minf).
verify_minus_zeroinf_consistence(minf, inf).
verify_minus_zeroinf_consistence(A, B):-
  not A = inf,
  not A = 0,
  not A = minf,
  not B = inf,
  not B = 0,
  not B = minf.



% verify_minus_mag(Func1, Func2, Mag1, Mag2, Corr)
%   - check minus-magnitude consistency.

verify_minus_mag(_, _, _, _, []).

verify_minus_mag(F1, F2, M1, M2, [c(C1,C2) |Corr]):-
  norm_mag(F1, M1, C1, Norm),
  norm_mag(F2, C2, M2, Norm),
  verify_minus_mag(F1, F2, M1, M2, Corr).



% verify_minus_der(Der1, Der2)
%   - check minus-derivative consistency.

verify_minus_der(D1, D2):-
  lookup_minus_der_table(D1, D2).



% lookup_minus_sign_table(X1, X2)  - minus-sign consistency.

lookup_minus_sign_table(pos,  neg).
lookup_minus_sign_table(zero, zero).
lookup_minus_sign_table(neg,  pos).



% lookup_minus_der_table(X1, X2)  - minus-der consistency.

lookup_minus_der_table(dec, inc).
lookup_minus_der_table(std, std).
lookup_minus_der_table(inc, dec).



% verify_m_plus_limit(Func1, Func2, Mag1, Mag2, Corr_list)  - 
%   check monotone increasing limit approach.

verify_m_plus_limit(_, _, _, _, []).

verify_m_plus_limit( F1, F2,M1, M2, [c(A,B) |Corr]):-
  norm_mag( F1, M1, A, Nm),
  norm_mag( F2, M2, B, Nm),
  verify_m_plus_limit( F1, F2, M1, M2, Corr).

% verify_m_minus_limit( Func1, Func2, Mag1, Mag2, CorrList)
%   check monotone decreasing approach

verify_m_minus_limit(_, _, _, _, []).

verify_m_minus_limit( F1, F2, M1, M2, [c(A,B) |Corr]):-
  norm_mag( F1, M1, A, Nm), 
  norm_mag( F2, B, M2, Nm), 
  verify_m_minus_limit( F1, F2, M1, M2, Corr).
       

% The following (verify_m_limit) is probabbly no longer needed!!!

verify_m_limit(M1, M2, [c(A,B) |Corr]):-
  not M1 = A,
  not M2 = B,
  verify_m_limit(M1, M2, Corr).



% m_plus_deriv(Mag1, Mag2)
%   - verify m_plus deriv condition

m_plus_deriv(D, D).


% m_minus_deriv(Mag1, Mag2)
%   - verify m_minus deriv condition

m_minus_deriv(D1, D2):-
  lookup_minus_der_table(D1, D2).



% less_than(Func, Val1, Val2)  - Val1 < Val2 for Functionn.

less_than(_, _...A, A..._).
less_than(F, _...A2, B1..._):-
  less_than(F, A2, B1).

less_than(_, A, A..._):-
  not A = _..._.
less_than(F, A, B1..._):-
  not A = _..._,
  less_than(F, A, B1).

less_than(_, _...B, B):-
  not B = _..._.
less_than(F, _...A2, B):-
  not B = _..._,
  less_than(F, A2, B).

less_than(F, A, B):-
  not A = _..._,
  not B = _..._,
  succ(F, A, B).
less_than(F, A, B):-
  not A = _..._,
  not B = _..._,
  succ(F, A, C),
  less_than(F, C, B).



leseq_than(_, A, A).

leseq_than(F, A, B):-
  less_than(F, A, B).



% inside _closed(Func, Val, Range)
%   - is Val in the closed interval Range for Function.

inside_closed(F, V1...V2, R1...R2):-
  leseq_than(F, R1, V1),
  less_than(F, V1, V2),
  leseq_than(F, V2, R2).

inside_closed(_, V, R...R):-
  not V = _..._,
  V = R.

inside_closed(F, V, R1...R2):-
  not V = _..._,
  not R1 = R2,
  leseq_than(F, R1, V),
  leseq_than(F, V, R2).

inside_closed(_, V, V):-
  not V = _..._.



noninfinity(_:S):-
  finite_values(S).



finite_values([]).

finite_values([_:A/_ |S]):-
  not A = inf,
  not A = minf,
  finite_values(S).



global(_:S):-
  changed_state(S).



changed_state([i1:_ |S]):-
  changed_state(S).

changed_state([i4:_ |S]):-
  changed_state(S).

changed_state([i7:_ |S]):-
  changed_state(S).

changed_state([Id:_ |_]):-
  not Id = i1,
  not Id = i4,
  not Id = i7.

conc( [], L, L).

conc( [X | L1], L2, [X | L3])  :-
  conc( L1, L2, L3).



% ---------------------------------------------------------------------------
%
%                          .EOF. SI2_LOGIC
%
% ---------------------------------------------------------------------------
