% This is an alternative ASP encoding of the domain 
% independent axioms of the Functional Event Calculus (FEC)
% See http://www.ucl.ac.uk/infostudies/efec/

% Last update: 16 May 2013

% -- List of domain predicates --
%
% fluent(F).
% possVal(F, V).
% action(A).
%
% causesValue(A,F,V,T).
% possVal(F,v).

% -- Domain independent rules --

time(0..maxtime).
lessThanEqualTo(T1, T2) :-
	time(T1), time(T2),
	T1 <= T2.
lessThan(T1, T2) :-
	lessThanEqualTo(T1, T2),
	T1 != T2.

% FEC1

valueCaused(F, V, T) :-
	happens(A, T), 
	causesValue(A, F, V, T).

hasPossCausedValue(F, T) :-
	valueCaused(F, V, T).

% the below two rules are implementing the follow:
%
% 1 { valueChangedTo(F, V, T) : valueCaused(F, V, T) } 1 :-
% 	hasPossCausedValue(F, T).
%
% Since ASP does not allow non-domain predicate 'possCausedValue' to be used as a 
% condition inside an aggregation literal (i.e., the head of the rule in this case), 
% we have to use the domain predicate 'possValue' as the condition and break the axiom 
% down into two rules.
1 { valueChangedTo(F, V, T) : possVal(F, V) } 1 :-
	hasPossCausedValue(F, T).
:- valueChangedTo(F, V, T), not valueCaused(F, V, T).

-valueChangedTo(F, V, T) :-
	possVal(F, V), time(T),
	not valueChangedTo(F, V, T).

% FEC2
otherValCausedBetween(F, V, T1, T2) :- 
	possVal(F, V),
	valueChangedTo(F, Vp, T),
	lessThanEqualTo(T1, T),
	lessThan(T, T2),
	V != Vp.
-otherValCausedBetween(F, V, T1, T2) :-
	possVal(F, V),
	lessThan(T1, T2),
	not otherValCausedBetween(F, V, T1, T2).

% FEC3
valueOf(F, T2, V) :-
	valueOf(F, T1, V),
	lessThan(T1, T2), 
	not otherValCausedBetween(F, V, T1, T2).
valueOf(F, T2, V) :-
	valueChangedTo(F, V, T1),
	lessThan(T1, T2),
	not otherValCausedBetween(F, V, T1, T2).

% FEC4
valueCausedBetween(F, V, T1, T2) :-
	valueChangedTo(F, V, T),
	lessThanEqualTo(T1, T),
	lessThan(T, T2).
-valueCausedBetween(F, V, T1, T2) :-
	lessThan(T1, T2),
	possVal(F, V),
	not valueCausedBetween(F, V, T1, T2).

-valueOf(F, T2, V) :-
	possVal(F, V),
	lessThan(T1, T2),
	valueChangedTo(F, Vp, T1),
	Vp != V,
	not valueCausedBetween(F, V, T1, T2).

% FEC5
% ic(fec5) 
:- 
	valueOf(F, T, V), not possVal(F, V).

% AUX1
% initially in any world every fluent must have one but only one value
1 { valueOf(F, 0, V) : possVal(F, V) } 1 :-
	fluent(F).
% AUX2
% make sure valueOf is a function.
:-
	fluent(F), time(T), not 1 { valueOf(F, T, V) : possVal(F, V) } 1.