%% Contract(3k)_byA(0120)H

/*
Ａが作成した知識ベースをHが改訂したもの。
今回は、事例3kも解けるようにした。
*/

/*
【時間指示変数の整理】
T1=offerが到達するとき
T2=withdrawlが到達するとき
T3=acceptanceが到達するとき
T4=revocationが到達するとき
T5=acceptanceが発信されるとき
*/

%rule
:-unknown(P,fail).

%23

is_concluded(contract(A,B,C),T3):-
	become_effective(offer(A,B,C),T1),become_effective(acceptance(B,A, offer(A,B,C)),T3).



%15(1) 
become_effective(offer(A,B,C),T1):-
	reach(offer(A,B,C),B,T1),
	\+(become_effective(withdrawl(A,B,offer(A,B,C),T2))).

%15(2)
become_effective(withdrawl(A,B,offer(A,B,C),T2)):-
        reach(withdrawl(A,B,offer(A,B,C)),B,T2),
        \+((reach(offer(A,B,C),B,T1),T1@<T2)).


%18(2)

become_effective(acceptance(B,A,offer(A,B,C)),T3):-
	reach(acceptance(B,A,offer(A,B,C)),A,T3),
	\+(become_effective(withdrawl(B,A,acceptance(B,A,offer(A,B,C))),T8)),
	\+((become_null(offer(A,B,C),T4),T4@<T3)).

%22
become_effective(withdrawl(B,A,acceptance(B,A,offer(A,B,C))),T8):-
	reach(withdrawl(B,A,acceptance(B,A,offer(A,B,C))),A,T8),
	\+((reach(acceptance(B,A,offer(A,B,C)),A,T3),T8@<T3)).



become_null(offer(A,B,C),T4):-
	become_effective(revocation(A,B,offer(A,B,C),T4)).

%16(1)
become_effective(revocation(A,B,offer(A,B,C),T4)):-
	reach(revocation(A,B,offer(A,B,C)),B,T4),
	\+(((dispatch(acceptance(B,A,offer(A,B,C)),A,T5)),T5@=<T4)).

%17
become_null(offer(A,B,C),T4):-
	become_effectuve(rejection(B,A,offer(A,B,C)),T4).

become_effectuve(rejection(B,A,offer(A,B,C)),T4):-
	reach(rejection(B,A,offer(A,B,C)),A,T4),
	\+((reach(acceptance(B,A,offer(A,B,C)),A,T3),T3@<T4)).



%fact
%case3k
reach(offer(anzai,bernard,sale(agriculture_machine,'$10000')),bernard,t0408).
reach(withdrawl(bernard,anzai,acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000')))),anzai,t0411).
reach(rejection(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0411).
reach(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0416).


dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0416).