%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% IMPLEMENTATION OF THE TRANSITION FUNCTION %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- use_module(library(clpfd)).

next(0,(AType,N):T,AMsg,T,N) :- has_type(AMsg, AType), !.
next(M,AType:T1,AMsg,T1,N) :- AType \= (_,_), has_type(AMsg, AType), !, M > 0, N is M - 1.
next(M,T1+_,A,T2,N) :- next(M,T1,A,T2,N). 
next(M,_+T1,A,T2,N) :- !,next(M,T1,A,T2,N).
next(N,T1|T2,A,T3|T2,M) :- next(N,T1,A,T3,M). 
next(N,T1|T2,A,T1|T3,M) :- next(N,T2,A,T3,M).
next(N,T1|T2,A,T3|T4,P) :- next(N,T1,A,T3,M), M > 0, next(M,T2,A,T4,P). 
next(N,T1|T2,A,T4|T3,P) :- !,next(N,T2,A,T3,M), M > 0, next(M,T1,A,T4,P). 
next(M,T1*T2,A,T3*T2,N) :- next(M,T1,A,T3,N).
next(M,T1*T2,A,T3,N) :- !,empty(T1), next(M,T2,A,T3,N).
next(M, attrType(Name, Constr, T1), A, T2, N) :- 
attrType(Name, Constr, T1), !, 
next(M, T1, A, T2, N),
call(Constr).

empty(lambda) :- !.
empty(T1+T2) :- (empty(T1),!;empty(T2)).
empty(T1|T2) :- !,empty(T1),empty(T2).
empty(T1*T2) :- !,empty(T1),empty(T2).

accept(T1,[A|L]) :- next(0,T1,A,T2,0),accept(T2,L).
accept(T,[]) :- empty(T).
accept(N,T,[*]) :- empty(T),N==0,!.
accept(0,_,[]) :- !.
accept(N,T1,[A|L]) :- next(0,T1,A,T2,0), M is N - 1,accept(M,T2,L).

fc(T, T1, C, N) :- N>1, copy_term(T1, Fresh1), 
N1 is N-1, fc(T2, T1, C, N1),  T =.. [C, Fresh1, T2].
fc(Fresh1, T1, _C, 1) :- copy_term(T1, Fresh1).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ITERATIVE CONTRACT NET PROTOCOL %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


/* You may try to call this goal:
cn(1400, 3, 701).
that will generate one trace containing 1400 sending actions, in a simulated setting where there are 701 agents, and the agent that plays the initiator role is the one identified by 3. Please note that it will require some time.*/

has_type(AMsg, AType) :-  AType =.. [F, A1, A2], !, A1 \== A2, AMsg =.. [F, A1, A2].
has_type(cfp(Init, X, DL), cfp(Init, X, DL)) :-  Init \== X. 
has_type(cfp(Init, X, CFPcurr, DL), cfp(Init, X, CFPcurr, DL)) :-  !, Init \== X. 
has_type(propose(X, Init, PROPcurr, noDl), ontime_propose(X, Init, PROPcurr, noDl)) :- !.
has_type(ontime_propose(X, Init, PROPcurr, DL), ontime_propose(X, Init, PROPcurr, DL)):- Init \== X.
has_type(late_propose(DL), late_propose(DL)).
has_type(ontime_refuse(X, Init, DL), ontime_refuse(X, Init, DL)) :- Init \== X.
has_type(late_refuse(DL), late_refuse(DL)).

attrType(ontime, dec_inc(X, Init, _CFPprev, CFPcurr, _PROPprev, PROPcurr, DL), 
(((ontime_refuse(X, Init, DL),0):lambda) + 
 (
  (ontime_propose(X, Init, PROPcurr, DL),0):
   (
    (
     (
      (reject_proposal(Init, X),0):lambda
     ) + 
     (
      (accept_proposal(Init, X),0):
       (
        (
         ((inform(X, Init),0):lambda) + 
         ((failure(X, Init),0):lambda)
        )
       )
      )
     ) + 
    (
     ((cfp(Init, X, CFPcurr),0):attrType(ontime, dec_inc(X, Init, CFPcurr, _, PROPcurr, _, noDl), _))
    )
   )
  )
 )
).


attrType(late, dl(DL), 
(
  ((late_refuse(DL),0):lambda) + 
  ((late_propose(DL),0):lambda)
)).
    

attrType(icnp, allDiff(DL, Init, Current, List, X), 
(((cfp(Init, X, DL),0):
(attrType(ontime, dec_inc(X, Init, 11, _, 2, _, DL), _) + attrType(late, dl(DL), _)))|
attrType(icnp, allDiff(DL, Init, NewCurrent, [X|List], _), _))
) :- Current > 0, NewCurrent is Current-1.

attrType(icnp, allDiff(_DL, _Init, 0, _List, _X), lambda).

cn(N, Init, Participants):-
retractall(participants(_)),
DL = 3500,
open('logICNP.txt',write,Str),
P is Participants-1, assert(participants(Participants)),
T = attrType(icnp, allDiff(DL, Init, P, [], _), _),
get_time(Time1), 
accept(N,T,IL),
get_time(Time2),
print_list(Str,IL),write(Str,'\n'),flush_output(Str),
TotTime is Time2-Time1,
write('\nThe total execution time was '), write(TotTime), write('\n'),
close(Str). 
 
dl(_).
dec_inc(_X, _Init, Cp, Cc, Pp, Pc, _) :- Cc is Cp-1, Pc is Pp+1, Cc > Pc.
 

allDiff(_DL, Init, _Num, [], X) :- participants(P), X in 1..P, label([X]), Init #\= X.
allDiff(_DL, Init, _Num, [H|T], X) :- participants(P), X in 1..P, label([X]), Init #\= X, all_different([X|[H|T]]).


%%%%%%%%%%%%%%%%%%
% PARAMETRIC ABP %
%%%%%%%%%%%%%%%%%%


/* You may try to call this goal:
abp(100, 15). 
to generate the Alternating Bit Protocol traces long 100, involving 15 participants. Please note that it will require some time.  */

% has_type(T, T). /* UNCOMMENT THIS FACT WHEN YOU WANT TO EXPERIMENT THE ABP, AND COMMENT IT AGAIN WHEN YOU EXPERIMENT THE ICNP: THIS FACT MAY RAISE PROBLEMS IF USED WHEN EXPERIMENTING THE ICNP, AND LEADS TO A FAILURE IF NOT USED WHEN EXPERIMENTING THE ABP. */

attrType(abpMainThread, c([X]),(msg(X),1):(ack(X),0):attrType(abpMainThread, c([X]), _T2)). 

attrType(abpSynchSeq, modulo(Mod, _, Y), (lambda + (msg(Y):attrType(abpSynchSeq, modulo(Mod, Y, _), _)))).


abp(N, NumOfParticipants):-
open('logABP.txt',write,Str),
fc(TF, attrType(abpMainThread, c([_]), _), |, NumOfParticipants),
TS = attrType(abpSynchSeq, modulo(NumOfParticipants, -1, _), _),
T = (TF|TS),
write(Str,'/*** ABP with '), write(Str, NumOfParticipants), write(Str,' agents and traces long '),write(Str, N),  write(Str, ' ***/\n\n'), flush_output(Str),
setof(IL,T^(get_time(Time1), accept(N,T,IL), get_time(Time2), DiffTime is Time2-Time1,  write(Str,IL),write(Str,' generated after '), write(Str, DiffTime), write(Str, ' seconds from the beginning of the execution.\n\n'), flush_output(Str)),OL), 
print_list(OL), 
print_list(Str,OL),
close(Str). 

c(_).

modulo(Mod, X, Y) :- M1 is Mod-1, X < M1, !, Y is X+1.
modulo(_Mod, _X, 0).


/* UTILITIES */

print_list(_,[]).
print_list(S,[X|L]) :- write(S,X),write(S,'\n'),print_list(S,L).

print_list_of_lists(_,[]).
print_list_of_lists(S,[X|L]) :- print_list(S,X),write(S,'\n'),print_list_of_lists(S,L).

print_list([]).
print_list([X|L]) :- write(X),write('\n'),print_list(L).


