% ------------------------------------------------------------------------------------------------------
% Event Calculus Demonstration
% 
% Defined EC rules
%
% initiates(serverGoesDown, serverIsDown, T).
% terminates(serverAwakes, serverIsDown, T).
% 
% ------------------------------------------------------------------------------------------------------

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


% ------------------------------------------------------------------------ 
%
% Some events for a webserver


happens(serverGoesDown, datetime(2006,1,1,13,30,0)).

happens(serverAwakes, datetime(2006,1,1,13,35,0)).

happens(serverGoesDown, datetime(2006,1,1,13,40,0)).
happens(serverAwakes, datetime(2006,1,1,13,45,0)).

initiallyTrue(serverIsDown).

happens(serverAwakes, datetime(2006,1,1,0,0,0)).

happens(serverGoesDown, datetime(2006,1,1,13,22,0)).

happens(serverAwakes, datetime(2006,1,1,13,24,20)).





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


% ------------------------------------------------------------------------ 
%
% calculate the serverDownTime

%valueAt(serverDownDuration, datetime(2006,1,1,0,0,0),X).


constant(serverIsDown).

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


% holdsAt
:- solve(holdsAt(serverIsDown,datetime(2006,1,1,13,34,10))).
%valueAt
:- solve(valueAt(serverDownDuration,datetime(2006,1,1,13,34,10),T)).
% number of MVIs
:- solve(countMVIs(serverIsDown,Number)).
% list all MVIs
:- solve(mvi(serverIsDown,MVI)).
% compute overall MVI
:- solve(overallMVI(serverIsDown,OVERALL)).
