/*
The copyright of this code belongs to Davide Ancona, Daniela Briola, Angelo Ferrando, and Viviana Mascardi

**** PLEASE NOTE THAT THIS CODE IS JUST A PROOF OF CONCEPT. IT IS RELEASED AS IT IS, WITH NO WARRANTIES ON ITS FUNCTIONING **** 

HOW TO USE THE GRAPH PARTITIONING PROGRAM

-- requires SWI Prolog installed
-- requires the metis software installed and accessible from the command line (it must be in the path)
-- tested on Mageia Linux only
-- given ID the identifier of the protocol to be partitioned (which must be defined in this file following the trace expressions syntax), just call the goal partition(ID, NumPart, OutputFile) where NumPart is the number of partitions and OutputFile is the name of the file where the results will be logged. 

Examples of goals:
partition(abp3, 2, './abp3Out.txt').
partition(socks, 2, './socksOut.txt').
partition(double_abp3, 2, './double_abp3Out.txt').
partition(triple_abp3, 3, './triple_abp3Out.txt').
*/


:- use_module(library(assoc)).
:- use_module(library(clpfd)).
:- dynamic node/2, node/3, edge/3, edge/4, pnode/3, pedge/3, metis_node/4.

debug(on).

/*******************************************************************************************/
/*     					TRACE EXPRESSIONS	   		           */
/*******************************************************************************************/
  
/* Transition rules */

%%% compositional trace expressions with conjunction and implication
new_next(ET:T,E,T) :- has_type(E,ET).
new_next(T1\/_,E,T2) :- new_next(T1,E,T2). 
new_next(_\/T1,E,T2) :- !,new_next(T1,E,T2).
new_next(T1|T2,E,T) :- new_next(T1,E,T3), fork(T3,T2,T). 
new_next(T1|T2,E,T) :- !,new_next(T2,E,T4), fork(T1,T4,T). 
new_next(T1*T2,E,T) :- new_next(T1,E,T3), concat(T3,T2,T).
new_next(T1*T2,E,T3) :- !,new_may_halt(T1), new_next(T2,E,T3).
new_next(T1 /\ T2,E,T) :- new_next(T1,E,T3), new_next(T2,E,T4), conj(T3,T4,T).  %%% conjunction
new_next(ET >> T1, E, ET >> T2)  :- event(E),(has_type(E,ET) *-> new_next(T1,E,T2); T2=T1). 

new_may_halt(lambda) :- !.
new_may_halt(T1\/T2) :- (new_may_halt(T1),!;new_may_halt(T2)).
new_may_halt(T1|T2) :- !,new_may_halt(T1),new_may_halt(T2).
new_may_halt(T1*T2) :- !,new_may_halt(T1),new_may_halt(T2).
new_may_halt(T1/\T2) :- !,new_may_halt(T1),new_may_halt(T2).
new_may_halt(_>>T) :- !,new_may_halt(T).

new_does_not_halt(_:_).
new_does_not_halt(T1\/T2) :- !,new_does_not_halt(T1),new_does_not_halt(T2).
new_does_not_halt(T1|T2) :- (new_does_not_halt(T1),!;new_does_not_halt(T2)).
new_does_not_halt(T1*T2) :- (new_does_not_halt(T1),!;new_does_not_halt(T2)).
new_does_not_halt(T1/\T2) :- (new_does_not_halt(T1),!;new_does_not_halt(T2)).
new_does_not_halt(_>>T) :- !,new_does_not_halt(T).

new_accept(T,[]) :- !,new_may_halt(T).
new_accept(T1,[E|L]) :- !, new_next(T1,E,T2),!,new_accept(T2,L).

new_accept(_,T,[*]) :- new_may_halt(T).
new_accept(0,T,[]) :- !,new_does_not_halt(T).
new_accept(N,T1,[E|L]) :- !, new_next(T1,E,T2), M is N - 1,new_accept(M,T2,L).

% one more argument: the residual term

new_accept(_,T,[*],T) :- new_may_halt(T).
new_accept(0,T,[],T) :- !,new_does_not_halt(T).
new_accept(N,T1,[E|L],T3) :- !, new_next(T1,E,T2), M is N - 1,new_accept(M,T2,L,T3).

%%% used for statistics
:- dynamic counter/1.

new_stat_accept(0,_,[]) :- !.
new_stat_accept(TraceLength,SourceType,[Event|Trace]) :- !, new_next(SourceType,Event,DestType), DecTraceLength is TraceLength - 1,new_stat_accept(DecTraceLength,DestType,Trace).

new_stat_accept_prefix(_,[]) :- !.
new_stat_accept_prefix(SourceType,[Event|Trace]) :- !, new_next(SourceType,Event,DestType),!,new_stat_accept_prefix(DestType,Trace).

new_stat_accept_prefix(0,_,_) :- !.
new_stat_accept_prefix(Times,SourceType,Trace) :- new_stat_accept_prefix(SourceType,Trace),DecTimes is Times -1,new_stat_accept_prefix(DecTimes,SourceType,Trace).

%%% empirical projectability test

test_accept(0,_,[*]) :- !.
test_accept(0,_,[]) :- !.
test_accept(N,T1,[A|L]) :- new_next(T1,A,T2), M is N - 1, test_accept(M,T2,L).

%%% optimization

fork(lambda,T,T) :- !.
fork(T,lambda,T) :- !.
fork((T1l|T1r),T2,(T1l|(T1r|T2))) :- !.
fork(T1,T2,(T1|T2)).

concat(lambda,T,T) :- !.
concat(T,lambda,T) :- !.
concat((T1l*T1r),T2,T1l*(T1r*T2)) :- !.
concat(T1,T2,T1*T2).

conj(lambda/\lambda,lambda) :- !.
conj((T1l/\T1r),T2,T1l/\(T1r/\T2)) :- !.
conj(T1,T2,T1/\T2).


/****************************************************************************/
/* 	          	PROJECTION ALGORITHM (BRUTE FORCE)                  */
/****************************************************************************/

bf_project_by_id(ID, ProjectedAgents, ProjectedType) :- 
type(ID, T), 
bf_project(T, ProjectedAgents, ProjectedType).

/* 0 is depth of the root of T,-1 is the level of the deepest seq operator in the current path */   

bf_project(T, ProjectedAgents, ProjectedType) :- write('\nPROJECTING 1'),
empty_assoc(A), bf_project(A, 0, -1, T, ProjectedAgents, ProjectedType).
                                                                       
bf_project(_Assoc, Depth, _DeepestSeq, lambda, _ProjectedAgents, lambda):- !, write('\nPROJECTING 2: ' , Depth, ' ', lambda). 

bf_project(Assoc, Depth, DeepestSeq, Type, _ProjectedAgents, ProjectedType) :-
get_assoc(Type,Assoc,(AssocProjType,LoopDepth)),!,(LoopDepth =< DeepestSeq -> write('\nPROJECTING 3: ' , Depth, ' ', Type), ProjectedType=AssocProjType; write('\nPROJECTING 4: ' , Depth, ' ', Type), ProjectedType=lambda). 

bf_project(Assoc, Depth, DeepestSeq, (IntType:Type1), ProjectedAgents, ProjectedType) :-
put_assoc((IntType:Type1),Assoc,(ProjectedType,Depth),NewAssoc),
(involves(IntType, ProjectedAgents) -> 
    write('\nPROJECTING 5: ' , Depth, ' ', (IntType:Type1)), IncDepth is Depth+1,bf_project(NewAssoc,IncDepth,Depth,Type1,ProjectedAgents,ProjectedType1),ProjectedType=(IntType:ProjectedType1);
     write('\nPROJECTING 6: ' , Depth, ' ', (IntType:Type1)), bf_project(NewAssoc,Depth,DeepestSeq,Type1,ProjectedAgents,ProjectedType)).  

bf_project(Assoc, Depth, DeepestSeq, (Type1|Type2), ProjectedAgents, ProjectedType) :-
!,
put_assoc((Type1|Type2),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 9: ' , Depth, ' ', (Type1|Type2)), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type1, ProjectedAgents, ProjectedType1), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type2, ProjectedAgents, ProjectedType2), 
ProjectedType=(ProjectedType1|ProjectedType2).

bf_project(Assoc, Depth, DeepestSeq, (Type1\/Type2), ProjectedAgents, ProjectedType) :-
!,
put_assoc((Type1\/Type2),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 10: ' , Depth, ' ', (Type1\/Type2)), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type1, ProjectedAgents, ProjectedType1), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type2, ProjectedAgents, ProjectedType2), 
ProjectedType=(ProjectedType1\/ProjectedType2).

bf_project(Assoc, Depth, DeepestSeq, (Type1*Type2), ProjectedAgents, ProjectedType) :-
!,
put_assoc((Type1*Type2),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 11: ' , Depth, ' ', (Type1*Type2)), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type1, ProjectedAgents, ProjectedType1), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type2, ProjectedAgents, ProjectedType2), 
ProjectedType=(ProjectedType1*ProjectedType2).

bf_project(Assoc, Depth, DeepestSeq, (ET >> T1), ProjectedAgents, ProjectedType) :-
!,
put_assoc((ET >> T1),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 12: ' , Depth, ' ', (ET >> T1)), 
bf_project(NewAssoc, IncDepth, DeepestSeq, T1, ProjectedAgents, ProjectedT1),  
ProjectedType = (ET >> ProjectedT1).

bf_project(Assoc, Depth, DeepestSeq, (Type1/\Type2), ProjectedAgents, ProjectedType) :-
!,
put_assoc((Type1/\Type2),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 13: ' , Depth, ' ', (Type1/\Type2)), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type1, ProjectedAgents, ProjectedType1), 
bf_project(NewAssoc, IncDepth, DeepestSeq, Type2, ProjectedAgents, ProjectedType2), 
ProjectedType=(ProjectedType1/\ProjectedType2). 




/****************************************************************************/
/*   PROJECTION ALGORITHM (CAUTIOUS: DOES NOT PROJECT INTERSECTIONS)        */
/****************************************************************************/

project_by_id(ID, ProjectedAgents, ProjectedType) :- 
type(ID, T), 
project(T, ProjectedAgents, ProjectedType).

/* 0 is depth of the root of T,-1 is the level of the deepest seq operator in the current path */   

project(T, ProjectedAgents, ProjectedType) :- write('\nPROJECTING 1'),
empty_assoc(A), project(A, 0, -1, T, ProjectedAgents, ProjectedType).
                                                                       
project(_Assoc, Depth, _DeepestSeq, lambda, _ProjectedAgents, lambda):- !, write('\nPROJECTING 2: ' , Depth, ' ', lambda). 

project(Assoc, Depth, DeepestSeq, Type, _ProjectedAgents, ProjectedType) :-
get_assoc(Type,Assoc,(AssocProjType,LoopDepth)),!,(LoopDepth =< DeepestSeq -> write('\nPROJECTING 3: ' , Depth, ' ', Type), ProjectedType=AssocProjType; write('\nPROJECTING 4: ' , Depth, ' ', Type), ProjectedType=lambda). 

project(Assoc, Depth, DeepestSeq, (IntType:Type1), ProjectedAgents, ProjectedType) :-
put_assoc((IntType:Type1),Assoc,(ProjectedType,Depth),NewAssoc),
(involves(IntType, ProjectedAgents) -> 
    write('\nPROJECTING 5: ' , Depth, ' ', (IntType:Type1)), IncDepth is Depth+1,project(NewAssoc,IncDepth,Depth,Type1,ProjectedAgents,ProjectedType1),ProjectedType=(IntType:ProjectedType1);
     write('\nPROJECTING 6: ' , Depth, ' ', (IntType:Type1)), project(NewAssoc,Depth,DeepestSeq,Type1,ProjectedAgents,ProjectedType)).  

project(Assoc, Depth, DeepestSeq, (Type1|Type2), ProjectedAgents, ProjectedType) :-
!,
put_assoc((Type1|Type2),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 9: ' , Depth, ' ', (Type1|Type2)), 
project(NewAssoc, IncDepth, DeepestSeq, Type1, ProjectedAgents, ProjectedType1), 
project(NewAssoc, IncDepth, DeepestSeq, Type2, ProjectedAgents, ProjectedType2), 
ProjectedType=(ProjectedType1|ProjectedType2).

project(Assoc, Depth, DeepestSeq, (Type1\/Type2), ProjectedAgents, ProjectedType) :-
!,
put_assoc((Type1\/Type2),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 10: ' , Depth, ' ', (Type1\/Type2)), 
project(NewAssoc, IncDepth, DeepestSeq, Type1, ProjectedAgents, ProjectedType1), 
project(NewAssoc, IncDepth, DeepestSeq, Type2, ProjectedAgents, ProjectedType2), 
ProjectedType=(ProjectedType1\/ProjectedType2).

project(Assoc, Depth, DeepestSeq, (Type1*Type2), ProjectedAgents, ProjectedType) :-
!,
put_assoc((Type1*Type2),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 11: ' , Depth, ' ', (Type1*Type2)), 
project(NewAssoc, IncDepth, DeepestSeq, Type1, ProjectedAgents, ProjectedType1), 
project(NewAssoc, IncDepth, DeepestSeq, Type2, ProjectedAgents, ProjectedType2), 
ProjectedType=(ProjectedType1*ProjectedType2).

project(Assoc, Depth, DeepestSeq, (ET >> T1), ProjectedAgents, ProjectedType) :-
!,
put_assoc((ET >> T1),Assoc,(ProjectedType,Depth),NewAssoc),
IncDepth is Depth+1, write('\nPROJECTING 12: ' , Depth, ' ', (ET >> T1)), 
project(NewAssoc, IncDepth, DeepestSeq, T1, ProjectedAgents, ProjectedT1),  
ProjectedType = (ET >> ProjectedT1).

project(_Assoc, Depth, _DeepestSeq, (Type1/\Type2), _ProjectedAgents, (Type1/\Type2)) :-
write('\nIntersection: ' , Depth, ' ', (Type1/\Type2)). 





/****************************************************************************/
/* 	    		PLAIN GRAPH EXTRACTION   	                    */
/****************************************************************************/

graph_extraction(ID) :- 
findall(X, retract(node(ID, X)), _), 
findall((Y, Z), retract(edge(ID, Y, Z)), _), 
type(ID, Type),
graph_extraction(ID, [], Type).


graph_extraction(_ID, AlreadyMetTypes, Type) :-
member(Type, AlreadyMetTypes), !.

graph_extraction(_ID, _AlreadyMetTypes, lambda).

graph_extraction(ID, AlreadyMetTypes, Type) :-
not(member(Type, AlreadyMetTypes)),
int_type_op(Type, IntType, Type2),

findall(node(ID, S), 
       (has_type(msg(S, _, _, _), IntType),
        not(node(ID, S))), 
SenderList),
findall(node(ID, R), 
       (has_type(msg(_, R, _, _), IntType),
        not(node(ID, R))), 
ReceiverList),
append(SenderList, ReceiverList, NodeList),
assert_list(NodeList),
findall(edge(ID, S, R),
       (has_type(msg(S, R, _, _), IntType),
        not(edge(ID, S, R)),
        not(edge(ID, R, S))), 
EdgeList),
assert_list(EdgeList),
graph_extraction(ID, [Type | AlreadyMetTypes], Type2).


graph_extraction(ID, AlreadyMetTypes, Type) :-
not(member(Type, AlreadyMetTypes)),
binary_op(Type, Type1, Type2),
graph_extraction(ID, [Type | AlreadyMetTypes], Type1),
graph_extraction(ID, [Type | AlreadyMetTypes], Type2).


binary_op(Type, Type1, Type2) :-
Type =.. [F, Type1, Type2],
allowed_trace_expression_op(F).

int_type_op(Type, IntType, Type2):-
Type =.. [F, IntType, Type2],
allowed_int_type_op(F).

% allowed_trace_expression_op(/\).
allowed_trace_expression_op(\/).
allowed_trace_expression_op('|').
allowed_trace_expression_op(*).

allowed_int_type_op(:).
allowed_int_type_op(>>). 

assert_list([]).

assert_list([H|T]) :-
not(H), !, 
assert(H), 
assert_list(T).

assert_list([H|T]) :-
H, !, 
assert_list(T).




/****************************************************************************/
/* 	    		GRAPH EXTRACTION WITH STRUCTURE                     */
/****************************************************************************/

adv_graph_extraction(ID) :- 
findall((X, E1), retract(node(ID, X, E1)), _), 
findall((Y, Z, E2), retract(edge(ID, Y, Z, E2)), _), 
type(ID, Type),
adv_graph_extraction(ID, [], [], 1, Type).


adv_graph_extraction(_ID, AlreadyMetTypes, _Expr, _Level, Type) :-
member(Type, AlreadyMetTypes), !.

adv_graph_extraction(_ID, _AlreadyMetTypes, _Expr, _Level, lambda).

adv_graph_extraction(ID, AlreadyMetTypes, ExprStructure, Level, Type) :-
not(member(Type, AlreadyMetTypes)),
int_type_op(NewOp, Type, IntType, Type2),
NewLevel is Level+1,
append(ExprStructure, [(NewOp, NewLevel)], NewExprStructure),
findall(node(ID, S), 
       (has_type(msg(S, _, _, _), IntType),
        not(node(ID, S))), 
SenderList),
findall(node(ID, R), 
       (has_type(msg(_, R, _, _), IntType),
        not(node(ID, R))), 
ReceiverList),
append(SenderList, ReceiverList, NodeList),
assert_list(NodeList),
findall(edge(ID, S, R, NewExprStructure),
       (has_type(msg(S, R, _, _), IntType),
        not(edge(ID, S, R, NewExprStructure)),
        not(edge(ID, R, S, NewExprStructure))), 
EdgeList),
assert_list(EdgeList),
adv_graph_extraction(ID, [Type | AlreadyMetTypes], NewExprStructure, NewLevel, Type2).


adv_graph_extraction(ID, AlreadyMetTypes, ExprStructure, Level, (Type1 /\ Type2)) :-
not(member((Type1/\Type2), AlreadyMetTypes)),
NewLevel is Level+1,
append(ExprStructure, [(/\, NewLevel)], NewExprStructure),
adv_graph_extraction(ID, [(Type1 /\ Type2) | AlreadyMetTypes], NewExprStructure, NewLevel, Type1),
adv_graph_extraction(ID, [(Type1 /\ Type2) | AlreadyMetTypes], NewExprStructure, NewLevel, Type2).


adv_graph_extraction(ID, AlreadyMetTypes, ExprStructure, Level, Type) :-
not(member(Type, AlreadyMetTypes)),
binary_op(NewOp, Type, Type1, Type2),
NewLevel1 is Level+1,
NewLevel2 is 2*Level+1,
append(ExprStructure, [(NewOp, NewLevel1)], NewExprStructure1),
append(ExprStructure, [(NewOp, NewLevel2)], NewExprStructure2),
adv_graph_extraction(ID, [Type | AlreadyMetTypes], NewExprStructure1, NewLevel1, Type1),
adv_graph_extraction(ID, [Type | AlreadyMetTypes], NewExprStructure2, NewLevel2, Type2).

binary_op(F, Type, Type1, Type2) :-
Type =.. [F, Type1, Type2],
allowed_trace_expression_op(F).

int_type_op(F, Type, IntType, Type2):-
Type =.. [F, IntType, Type2],
allowed_int_type_op(F).


/****************************************************************************/
/* 	  	  UNSPLITTABLE DETECTION			            */
/****************************************************************************/

safe_splitting(ID, Unsplittable) :-
findall(edge(ID, S, R, Expr), edge(ID, S, R, Expr), Edges),
safe_split(Edges, [], Unsplittable), 
write('\nUnsplittable list\n'),
print_list(Unsplittable).

safe_split([], Unsplittable, Unsplittable).

safe_split([edge(_ID, _S, _R, Expr)|Tail], Unsplit, Unsplittable) :-
   not(minimum_prefix_before_intersection(Expr, _MinExpr)),
   safe_split(Tail, Unsplit, Unsplittable).

safe_split([edge(_ID, S, R, Expr)|Tail], Unsplit, Unsplittable) :-
   minimum_prefix_before_intersection(Expr, MinExpr),
   member((MinExpr, UnsplitAgents), Unsplit),
   delete(Unsplit, (MinExpr, UnsplitAgents), Rem),
   setof(X, member(X, [S, R|UnsplitAgents]), NewUnsplit),
   safe_split(Tail, [(MinExpr, NewUnsplit)|Rem], Unsplittable).


safe_split([edge(_ID, S, R, Expr)|Tail], Unsplit, Unsplittable) :-
   minimum_prefix_before_intersection(Expr, MinExpr),
   not(member((MinExpr, _UnsplitAgents), Unsplit)),
   safe_split(Tail, [(MinExpr, [S, R])|Unsplit], Unsplittable).



minimum_prefix_before_intersection([((/\), Num)|_T], [((/\), Num)]) :- !.

minimum_prefix_before_intersection([H|T], [H|Min]) :-
   minimum_prefix_before_intersection(T, Min).

 

/****************************************************************************/
/* 	     	NODE AND EDGE COLLAPSING	                            */
/****************************************************************************/
  

graph_collapsing(ID, Unsplittable) :-
   node_collapsing(ID, Unsplittable, [], NodesToCollapse),
   edge_collapsing(ID, Unsplittable),
   edge_singleton(ID, NodesToCollapse).   

node_collapsing(ID, [(_Expr, NodesToCollapse)|Tail], CurrentListOfNodesOnly, FinalList) :-
length(NodesToCollapse, L),
assert(pnode(ID, NodesToCollapse, L)),
append(CurrentListOfNodesOnly, NodesToCollapse, NewListOfNodesOnly),
node_collapsing(ID, Tail, NewListOfNodesOnly, FinalList).

node_collapsing(ID, [], ListOfNodesOnly, ListOfNodesOnly) :-
findall(pnode(ID, [Ag], 1), (node(ID, Ag), not(member(Ag, ListOfNodesOnly))), SingletonNodesList), 
assert_list(SingletonNodesList).

edge_collapsing(_ID, []).

edge_collapsing(ID, [(_Expr, NodesToCollapse)|Tail]) :-
findall(pedge(ID, NodesToCollapse, [R]), (edge(ID, S, R, _), member(S, NodesToCollapse), not(member(R, NodesToCollapse))), EdgeListRec),
findall(pedge(ID, [S], NodesToCollapse), (edge(ID, S, R, _), member(R, NodesToCollapse), not(member(S, NodesToCollapse))), EdgeListSend),
append(EdgeListRec, EdgeListSend, EdgeList),
assert_pedge_list(EdgeList), 
edge_collapsing(ID, Tail).

edge_singleton(ID, NodesToCollapse) :-
   findall(pedge(ID, [S], [R]), (edge(ID, S, R, _), not(member(S, NodesToCollapse)), not(member(R, NodesToCollapse))), EdgeList),
   assert_pedge_list(EdgeList).

assert_pedge_list([]).

assert_pedge_list([pedge(ID, S, R)|T]) :-
not(pedge(ID, S, R)), 
not(pedge(ID, R, S)), 
!, 
assert(pedge(ID, S, R)), 
assert_pedge_list(T).

assert_pedge_list([pedge(ID, S, R)|T]) :-
(pedge(ID, R, S);pedge(ID, S, R)), !, 
assert_pedge_list(T).

/****************************************************************************/
/* 	     		COLLAPSED GRAPH GENERATION                           */
/****************************************************************************/

collapsed_graph_generation(ID) :-
findall((X, E1), retract(node(ID, X, E1)), _), 
findall((Y, Z, E2), retract(edge(ID, Y, Z, E2)), _),
findall((PX, PW), retract(pnode(ID, PX, PW)), _), 
findall((PY, PZ), retract(pedge(ID, PY, PZ)), _),
adv_graph_extraction(ID),
safe_splitting(ID, Unsplittable),
graph_collapsing(ID, Unsplittable).


/****************************************************************************/
/* 	     			METIS ENCODING                             */
/****************************************************************************/


metis_encode(ID, MetisFileName) :-
collapsed_graph_generation(ID),
findall(metis_node(ID, N, W), pnode(ID, N, W), NodeList),
add_numbers_to_nodes(NodeList, NumberedNodeList, 1),
assert_list(NumberedNodeList),
length(NumberedNodeList, NodeNum),
findall(metis_edge(ID, S, R), pedge(ID, S, R), EdgeList),
length(EdgeList, EdgeNum),
open(MetisFileName, write, Str),
write(Str, '% Metis file enconding protocol '),
write(Str, ID),
write(Str, ' %'),
write(Str, '\n% Nodes: '), 
write(Str, NumberedNodeList), 
write(Str, '\n% Edges: '), 
write(Str, EdgeList),
write(Str,'\n'), 
write(Str, NodeNum),
write(Str, ' '),
write(Str, EdgeNum),
write(Str, ' 010'), 
scan_node_list(Str, NumberedNodeList),
close(Str).


add_numbers_to_nodes([], [], _Num).

add_numbers_to_nodes([metis_node(ID, N, W)|T], [metis_node(ID, Num, N, W)|NT], Num) :-
NewNum is Num+1, 
add_numbers_to_nodes(T, NT, NewNum).

scan_node_list(_, []).

scan_node_list(Str, [metis_node(ID, _Num, N, W)|T]) :-
write(Str, '\n'),
write(Str, W), write(Str, ' '),
findall((N, R, RNum), (pedge(ID, N, R), metis_node(ID, RNum, R, _WR), write(Str, RNum), write(Str, ' ')), _),
findall((N, S, SNum), (pedge(ID, S, N), metis_node(ID, SNum, S, _WS), write(Str, SNum), write(Str, ' ')), _),
scan_node_list(Str, T).


/****************************************************************************/
/* 	     			METIS DECODING                             */
/****************************************************************************/


metis_decode(ID, OutputMetisFileName, Partitions) :-
open(OutputMetisFileName, read, Str),
read_line_by_line(ID, Str, 1, [], Partitions).

read_line_by_line(ID, Str, NodeNum, ComputedPartitions, Partitions) :-
get(Str, PartitionIdCode),  PartitionIdCode \= -1, !, char_code(PartitionId, PartitionIdCode),
metis_node(ID, NodeNum, NodeID, _WR),
(member((PartitionId, List), ComputedPartitions) ->
      (NewNum is NodeNum + 1, 
      delete(ComputedPartitions, (PartitionId, List), PartitionsRest),      
      read_line_by_line(ID, Str, NewNum, [(PartitionId, [NodeID | List])|PartitionsRest], Partitions));
      (NewNum is NodeNum + 1,    
      read_line_by_line(ID, Str, NewNum, [(PartitionId, [NodeID])|ComputedPartitions], Partitions))
).

read_line_by_line(_ID, _Str, _NodeNum, Partitions, Partitions).


/****************************************************************************/
/* 	     		PROTOCOL PARTITIONING                               */
/****************************************************************************/


partition(ID, NumPart) :-  
   partition(ID, NumPart, './defaultOutput.txt'). 

partition(ID, NumPart, OutFileName) :-
  tell(OutFileName),
  metis_encode(ID, ID),
  atom_codes('gpmetis', GPCODE),
  atom_codes(ID, FILENAMECODE),
  atom_codes(NumPart, NUMPARTCODE),
  atom_codes(' ', SPACECODE),
  atom_codes('.part.', PARTSCODE),
  append(GPCODE, SPACECODE, L1), 
  append(L1, FILENAMECODE, L2),
  append(L2, SPACECODE, L3), 
  append(L3, NUMPARTCODE, COMMANDCODE),
  atom_codes(CommandLine, COMMANDCODE),
  (shell(CommandLine) ->
     (append(FILENAMECODE, PARTSCODE, L4),
      append(L4, NUMPARTCODE, METISCODE),
      atom_codes(METISOutFileName, METISCODE),
      metis_decode(ID, METISOutFileName, Partitions),
      print_partitions(ID, Partitions));
      write('\nPartition failed\n')),
  findall(node(ID, NODEX), retract(node(ID, NODEX)), NODES), 
  findall(pnode(ID, PX, PW), retract(pnode(ID, PX, PW)), PNODES), 
  findall(pedge(ID, PY, PZ), retract(pedge(ID, PY, PZ)), PEDGES),
  findall((XRNum, XR, XWR), retract(metis_node(ID, XRNum, XR, XWR)), _),
  findall(node(ID, XX, XE1), retract(node(ID, XX, XE1)), _), 
  findall(edge(ID, YY, ZZ, YE2), retract(edge(ID, YY, ZZ, YE2)), EDGES),
  write('\nNodes\n'), print_list(NODES),
  write('\nExtended edges\n'), print_list(EDGES),
  write('\nCollapsed nodes\n'), print_list(PNODES),
  write('\nCollapsed edges\n'), print_list(PEDGES),
  told.

print_partitions(ID, Partitions) :-
   type(ID, Type),
   write('\nThe trace expressions\n', Type, '\ncan be partitioned into\n'),
   print_partitions(Partitions), write('\n\n').

print_partitions([]).

print_partitions([(_PID, Elems)|T]) :-
write('\n{\n'),
print_list(Elems), 
write('}\n\n'),
print_partitions(T).



/****************************************************************************/
/* 	  INVOLVES PREDICATE: can be redefined to consider agent roles      */
/****************************************************************************/

involves(IntType, List) :-  write('\n\nINVOLVES PREDICATE ', IntType, ' ',  List),
has_type(msg(Sender, Receiver, _, _), IntType),
write('\n\nHAS TYPE: '), write(has_type(msg(Sender, Receiver, _, _), IntType)),
(member(Sender, List);
member(Receiver, List)).


/****************************************************************************/
/* 				UTILITIES				    */
/****************************************************************************/


write(A, B, C) :- write(A), write(B), write(C).
write(A, B, C, D) :- write(A), write(B), write(C), write(D).
write(A, B, C, D, E) :- write(A), write(B), write(C), write(D), write(E).
write(A, B, C, D, E, F) :- write(A), write(B), write(C), write(D), write(E), write(F).

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,[(R,X)|L]) :- 
print_list(S,X),write(S,R),write(S,'\n\n'), print_list_of_lists(S,L).

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



/****************************************************************************/
/* 	          The protocol-dependent part starts here                   */
/****************************************************************************/


/****************************************************************************/
/* 					AnBn				    */
/****************************************************************************/

type(anbn, Forever) :- 
/* The type is not contractive, cannot be projected!!! */
Forever = (AB * Forever), 
AB = a:((AB*(b:lambda))\/(b:lambda)).

has_type(msg(alice, bob, tell, a), a).
has_type(msg(bob, alice, tell, b), b).


/****************************************************************************/
/* 				SOCKS PROTOCOL				    */
/****************************************************************************/

type(socks, SOCKS) :-
RIGHT = (put_right_sock:put_right_shoe:ok_right:lambda) \/ (put_right_shoe:oblige_remove_right_shoe:removed_right_shoe:RIGHT),
LEFT = (put_left_sock:put_left_shoe:ok_left:lambda) \/ (put_left_shoe:oblige_remove_left_shoe:removed_left_shoe:LEFT),
SOCKS = (RIGHT | LEFT).

event(msg(right_robot, right_node_monitor, tell, put_sock)).
event(msg(right_robot, right_node_monitor, tell, put_shoe)).
event(msg(right_robot, right_node_monitor, tell, removed_shoe)).
event(msg(right_node_monitor, right_robot, tell, oblige_remove_shoe)).
event(msg(right_node_monitor, plan_monitor, tell, ok)).
event(msg(left_robot, left_node_monitor, tell, put_sock)).
event(msg(left_robot, left_node_monitor, tell, put_shoe)).
event(msg(left_robot, left_node_monitor, tell, removed_shoe)).
event(msg(left_node_monitor, left_robot, tell, oblige_remove_shoe)).
event(msg(left_node_monitor, plan_monitor, tell, ok)).

has_type(
msg(right_robot, right_node_monitor, tell, put_sock),
put_right_sock
).

has_type(
msg(right_robot, right_node_monitor, tell, put_shoe),
put_right_shoe
).

has_type(
msg(right_robot, right_node_monitor, tell, removed_shoe),
removed_right_shoe
).

has_type(
msg(right_node_monitor, right_robot, tell, oblige_remove_shoe),
oblige_remove_right_shoe
).

has_type(
msg(right_node_monitor, plan_monitor, tell, ok),
ok_right
).

has_type(
msg(left_robot, left_node_monitor, tell, put_sock),
put_left_sock
).

has_type(
msg(left_robot, left_node_monitor, tell, put_shoe),
put_left_shoe
).

has_type(
msg(left_robot, left_node_monitor, tell, removed_shoe),
removed_left_shoe
).

has_type(
msg(left_node_monitor, left_robot, tell, oblige_remove_shoe),
oblige_remove_left_shoe
).

has_type(
msg(left_node_monitor, plan_monitor, tell, ok),
ok_left
).


/****************************************************************************/
/* 					ABP				    */
/****************************************************************************/

event(msg(bob, alice, tell, m1)).
event(msg(alice, bob, tell, a1)).
event(msg(bob, carol, tell, m2)).
event(msg(carol, bob, tell, a2)).
event(msg(bob, dave, tell, m3)).
event(msg(dave, bob, tell, a3)).

event(msg(sbob, salice, tell, mm1)).
event(msg(salice, sbob, tell, aa1)).
event(msg(sbob, scarol, tell, mm2)).
event(msg(scarol, sbob, tell, aa2)).
event(msg(sbob, sdave, tell, mm3)).
event(msg(sdave, sbob, tell, aa3)).

event(msg(blob, allice, tell, mmm1)).
event(msg(allice, blob, tell, aaa1)).
event(msg(blob, carlol, tell, mmm2)).
event(msg(carlol, blob, tell, aaa2)).
event(msg(blob, dlave, tell, mmm3)).
event(msg(dlave, blob, tell, aaa3)).

event(msg(bob, boss, tell, start_abp)).
event(msg(boss, bob, tell, ok_start_abp_bob)).
event(msg(boss, bob, tell, no_start_abp_bob)).

event(msg(sbob, boss, tell, start_abp)).
event(msg(boss, sbob, tell, ok_start_abp_sbob)).
event(msg(boss, sbob, tell, no_start_abp_sbob)).

event(msg(blob, boss, tell, start_abp)).
event(msg(boss, blob, tell, ok_start_abp_blob)).
event(msg(boss, blob, tell, no_start_abp_blob)).

event(msg(boss, megaboss, tell, ciaociao)).

event(msg(megaboss, gigaboss, tell, ciaociaociao)).

has_type(
msg(bob, alice, tell, m1),
m1
).

has_type(
msg(alice, bob, tell, a1),
a1
).

has_type(
msg(bob, carol, tell, m2),
m2
).

has_type(
msg(carol, bob, tell, a2),
a2
).

has_type(
msg(bob, dave, tell, m3),
m3
).

has_type(
msg(dave, bob, tell, a3),
a3
). 

has_type(
msg(bob, boss, tell, start_abp_bob),
bobasks
). 

has_type(
msg(boss, bob, tell, ok_start_abp_bob),
okbob
).

has_type(
msg(boss, bob, tell, no_start_abp_bob),
nobob
).

has_type(
msg(sbob, salice, tell, mm1),
mm1
).

has_type(
msg(salice, sbob, tell, aa1),
aa1
).

has_type(
msg(sbob, scarol, tell, mm2),
mm2
).

has_type(
msg(scarol, sbob, tell, aa2),
aa2
).

has_type(
msg(sbob, sdave, tell, mm3),
mm3
).

has_type(
msg(sdave, sbob, tell, aa3),
aa3
). 

has_type(
msg(sbob, boss, tell, start_abp),
sbobasks
).

has_type(
msg(boss, sbob, tell, ok_start_abp_sbob),
oksbob
).

has_type(
msg(boss, sbob, tell, no_start_abp_sbob),
nosbob
). 


has_type(
msg(blob, allice, tell, mmm1),
mmm1
).

has_type(
msg(allice, blob, tell, aaa1),
aaa1
).

has_type(
msg(blob, carlol, tell, mmm2),
mmm2
).

has_type(
msg(carlol, blob, tell, aaa2),
aaa2
).

has_type(
msg(blob, dlave, tell, mmm3),
mmm3
).

has_type(
msg(dlave, blob, tell, aaa3),
aaa3
). 

has_type(
msg(blob, boss, tell, start_abp),
blobasks
).

has_type(
msg(boss, blob, tell, ok_start_abp_blob),
okblob
).

has_type(
msg(boss, blob, tell, no_start_abp_blob),
noblob
). 


has_type(
msg(boss, megaboss, tell, ciaociao),
ciaociao
). 

has_type(
msg(megaboss, gigaboss, tell, ciaociaociao),
ciaociaociao
).

has_type(E,msg_ack(1)) :- E=msg(bob, alice, tell, m1);E=msg(alice, bob, tell, a1).
has_type(E,msg_ack(2)) :- E=msg(bob, carol, tell, m2);E=msg(carol, bob, tell, a2).
has_type(E,msg_ack(3)) :- E=msg(bob, dave, tell, m3);E=msg(dave, bob, tell, a3).
has_type(E,msg) :- E=msg(bob, alice, tell, m1);E=msg(bob, carol, tell, m2).
has_type(E,not_msg) :- E=msg(alice, bob, tell, a1);E=msg(carol, bob, tell, a2).
has_type(E,msg3) :- E=msg(bob, alice, tell, m1);E=msg(bob, carol, tell, m2);E=msg(bob, dave, tell, m3).

has_type(E,mmsg_ack(1)) :- E=msg(sbob, salice, tell, mm1);E=msg(salice, sbob, tell, aa1).
has_type(E,mmsg_ack(2)) :- E=msg(sbob, scarol, tell, mm2);E=msg(scarol, sbob, tell, aa2).
has_type(E,mmsg_ack(3)) :- E=msg(sbob, sdave, tell, mm3);E=msg(sdave, sbob, tell, aa3).
has_type(E,mmsg) :- E=msg(sbob, salice, tell, mm1);E=msg(sbob, scarol, tell, mm2).
has_type(E,mmsg3) :- E=msg(sbob, salice, tell, mm1);E=msg(sbob, scarol, tell, mm2);E=msg(sbob, sdave, tell, mm3).

has_type(E,mmmsg_ack(1)) :- E=msg(blob, allice, tell, mmm1);E=msg(allice, blob, tell, aaa1).
has_type(E,mmmsg_ack(2)) :- E=msg(blob, carlol, tell, mmm2);E=msg(carlol, blob, tell, aaa2).
has_type(E,mmmsg_ack(3)) :- E=msg(blob, dlave, tell, mmm3);E=msg(dlave, blob, tell, aaa3).
has_type(E,mmmsg) :- E=msg(blob, allice, tell, mmm1);E=msg(blob, carlol, tell, mmm2).
has_type(E,mmmsg3) :- E=msg(blob, allice, tell, mmm1);E=msg(blob, carlol, tell, mmm2);E=msg(blob, dlave, tell, mmm3).



/* alt bit protocol with two kinds of messages */

type(abp2, T) :- M1M2=m1:m2:M1M2,M1A1=m1:a1:M1A1,M2A2=m2:a2:M2A2,T=(msg>>M1M2)/\(msg_ack(1)>>M1A1)/\(msg_ack(2)>>M2A2).


/* alt bit protocol with three kinds of messages */

type(abp3, T) :- M1M2M3=m1:m2:m3:M1M2M3,M1A1=m1:a1:M1A1,M2A2=m2:a2:M2A2,M3A3=m3:a3:M3A3,T=(msg3>>M1M2M3)/\(msg_ack(1)>>M1A1)/\(msg_ack(2)>>M2A2)/\(msg_ack(3)>>M3A3).


/* double alt bit protocol with three kinds of messages */

type(double_abp3, DABP) :- 

M1M2M3=m1:m2:m3:M1M2M3,M1A1=m1:a1:M1A1,M2A2=m2:a2:M2A2,M3A3=m3:a3:M3A3,T1=(msg3>>M1M2M3)/\(msg_ack(1)>>M1A1)/\(msg_ack(2)>>M2A2)/\(msg_ack(3)>>M3A3),

MM1M2M3=mm1:mm2:mm3:MM1M2M3,MM1A1=mm1:aa1:MM1A1,MM2A2=mm2:aa2:MM2A2,MM3A3=mm3:aa3:MM3A3,T2=(mmsg3>>MM1M2M3)/\(mmsg_ack(1)>>MM1A1)/\(mmsg_ack(2)>>MM2A2)/\(mmsg_ack(3)>>MM3A3),

DABP = (((bobasks:lambda)|(sbobasks:lambda))*((okbob:nosbob:T1)\/(oksbob:nobob:T2))).


/* triple alt bit protocol with three kinds of messages and other messages before */

type(triple_abp3, TABP) :- 

M1M2M3=m1:m2:m3:M1M2M3,M1A1=m1:a1:M1A1,M2A2=m2:a2:M2A2,M3A3=m3:a3:M3A3,T1=(msg3>>M1M2M3)/\(msg_ack(1)>>M1A1)/\(msg_ack(2)>>M2A2)/\(msg_ack(3)>>M3A3),

MM1M2M3=mm1:mm2:mm3:MM1M2M3,MM1A1=mm1:aa1:MM1A1,MM2A2=mm2:aa2:MM2A2,MM3A3=mm3:aa3:MM3A3,T2=(mmsg3>>MM1M2M3)/\(mmsg_ack(1)>>MM1A1)/\(mmsg_ack(2)>>MM2A2)/\(mmsg_ack(3)>>MM3A3),

MMM1M2M3=mmm1:mmm2:mmm3:MMM1M2M3,MMM1A1=mmm1:aaa1:MMM1A1,MMM2A2=mmm2:aaa2:MMM2A2,MMM3A3=mmm3:aaa3:MMM3A3,T3=(mmmsg3>>MMM1M2M3)/\(mmmsg_ack(1)>>MMM1A1)/\(mmmsg_ack(2)>>MMM2A2)/\(mmmsg_ack(3)>>MMM3A3),

TABP = (((bobasks:lambda)|(sbobasks:lambda)|(blobasks:lambda))*((okbob:nosbob:ciaociao:ciaociaociao:T1)\/(oksbob:nobob:ciaociao:ciaociaociao:T2)\/(okblob:noblob:ciaociao:ciaociaociao:T3))).
