% ------------------------------------------------------------------------------------------------------
% Test the Prova Rule Implementation
% ------------------------------------------------------------------------------------------------------

% include basic predicates
:-eval(consult('ContractLog/math.prova')).
:-eval(consult('ContractLog/datetime.prova')).
:-eval(consult('ContractLog/ec.prova')).
:-eval(consult('ContractLog/list.prova')).
:-eval(consult('ContractLog/list_math.prova')).
:-eval(consult('ContractLog/utils.prova')).






% ------------------------------------------------------------------------ 
%
% Some test events / test data


initiallyTrue(serverIsDown).


setUpTest(Start,Number,T):-
	addTestPair(Start,T,Count,T2),
	lessequ(Count,Number),
	datetime_epoch(T2,E1),
	timespan_epoch(timespan(0,0,0,1),T3),	
	math_add(E1,T3,TE), 
	datetime_epoch(T4,TE),	
	setUpTest(Count,Number,T4).
	
addTestPair(Start,T,Count,T2):-
	datetime_epoch(T,E1),
	timespan_epoch(timespan(0,0,0,1),T1),	
	math_add(E1,T1,TE), 
	datetime_epoch(T2,TE),	
	assert(happens(serverAwakes, T)),
	assert(happens(serverGoesDown, T2)),
	math_add(Start,1,Count).



% ------------------------------------------------------------------------ 
%
% Some test rules

initiates(serverGoesDown, serverIsDown, T).
terminates(serverAwakes, serverIsDown, T).


% ------------------------------------------------------------------------ 
%
% Tests


%Test 1: holdsAt-Test

testHoldsAt() :-
sysTime(T),
println(["Test 1: holdsAt"]),
println(["-----------------------"]),
C1=rbsla.utils.WebsiteAvailable.getDate(),
T1=C1.getTimeInMillis(),

holdsAt(serverIsDown,T),

C2=rbsla.utils.WebsiteAvailable.getDate(),
T2=C2.getTimeInMillis(),
math_sub(T2,T1,DIF),
println(["Duration:",DIF]),
println(["-----------------------"]).




%Test 1.1: not holdsAt-Test

testnotHoldsAt() :-
happens(serverGoesDown, T),
!,
println(["Test 1.1: not holdsAt"]),
println(["-----------------------"]),
C1=rbsla.utils.WebsiteAvailable.getDate(),
T1=C1.getTimeInMillis(),

neg(holdsAt(serverIsDown,T)),

C2=rbsla.utils.WebsiteAvailable.getDate(),
T2=C2.getTimeInMillis(),
math_sub(T2,T1,DIF),
println(["Duration:",DIF]),
println(["-----------------------"]).




%Test 2: valueAt-Test




trajectory(serverIsDown, Before, serverDownDuration, After, X):-
	math_sub(After,Before,X).
	
antitrajectories(serverIsDown, Before, serverDownDuration, Tdelta, X):-
	valueAt(serverDownDuration, Before, X).


testValueAt(Name) :-
sysTime(TX),
println(["Test 2: ",Name]),
println(["-----------------------"]),
C1=rbsla.utils.WebsiteAvailable.getDate(),
T1=C1.getTimeInMillis(),

valueAt(serverDownDuration,TX,T),

println(["Server Downtime: ",T]),
C2=rbsla.utils.WebsiteAvailable.getDate(),
T2=C2.getTimeInMillis(),
math_sub(T2,T1,DIF),
println(["Duration:",DIF]),
println(["-----------------------"]).



startTest(Size,DT):-
	setUpTest(0,Size,datetime(2006,1,1,0,0,0)).

:- solve(startTest(1000,DT)).  % Set up 500 happens facts

:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt
:- solve(testHoldsAt()). % normal holdsAt


:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt
:- solve(testnotHoldsAt()). % normal notholdsAt

:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
:- solve(testValueAt("valueAt")). %normal valueAt
