1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(avl_ugraphs,[avl_set_to_ugraph/2,
6		ugraph_to_avl_set/2,
7		avl_transitive_closure/2,
8		avl_scc_sets/2]).
9
10		% a module to interface ProB's avl_set relations with the SICStus ugraph library (unweighted graphs)
11
12		:- use_module(library(avl)).
13		:- use_module(library(lists)).
14		:- use_module(library(ugraphs),[vertices_edges_to_ugraph/3,
15		transitive_closure/2, edges/2,
16		reduce/2, vertices/2]).
17
18		pair_to_minus((A,B),A-B).
19		%pair_to_minus((A,B),CA-CB) :- convert_val(A,CA), convert_val(B,CB).
20		minus_to_pair(A-B,(A,B)-true).
21		%minus_to_pair(A-B,(CA,CB)-true) :- reconvert_val(A,CA), reconvert_val(B,CB).
22
23		%convert_val(int(X),R) :- !, R=X.
24		%convert_val(R,R).
25		%reconvert_val(X,R) :- number(X),!, R=int(X).
26		%reconvert_val(R,R).
27
28		% closure1(%x.(x:1..2000|x*x)) is much slower with this than with the version in custom-explicit sets (1 secs vs 10ms)
29		% closure1(%x.(x:1..1000|x*x) \/ %x.(x:1..2000|x+x) \/ %x.(x:1..1000|x/2)): 9.3 seconds vs 2 seconds
30		% others like closure1(nxt \/ nxt~) for TrackUp.mch are faster (110ms vs 380ms)
31
32		avl_set_to_ugraph(A,UGraph) :-
33		avl_domain(A,AList),
34		maplist(pair_to_minus,AList,InEdges),
35		vertices_edges_to_ugraph([],InEdges,UGraph).
36
37		ugraph_to_avl_set(UGraph,Res) :-
38		edges(UGraph,Edges),
39		maplist(minus_to_pair,Edges,Res).
40
41
42		avl_transitive_closure(A,Res) :- % print(start1),debug:nl_time,
43		avl_set_to_ugraph(A,UGraph), %print(ug(UGraph)),nl,
44		transitive_closure(UGraph,TUG), %print(tc(TUG)),debug:nl_time,
45		edges(TUG,Edges), %print(edg(Edges)),debug:nl_time,
46		maplist(minus_to_pair,Edges,ListRes),
47		sort(ListRes,SListRes), %print(sl(SListRes)),debug:nl_time,
48		ord_list_to_avl(SListRes,Res). % could be empty
49		%print(stop1),debug:nl_time,fail.
50
51		%Note: result could be empty, use: construct_avl_set on Res
52
53		:- use_module(custom_explicit_sets,[convert_to_avl/2]).
54
55		% compute strongly connected components, returning a set of sets of vertices
56		avl_scc_sets(A,Res) :- %print(start_scc),debug:nl_time,
57		avl_set_to_ugraph(A,UGraph), %print(ug(UGraph)),nl,
58		reduce(UGraph,SCCGraph),
59		vertices(SCCGraph,VList), %print(vl(VList)),nl,
60		%print(stop_scc),debug:nl_time,
61		%maplist(convert_to_avl,V,SCCList),
62		convert_to_avl(VList,avl_set(Res)). % could be empty
63
64		/* TO DO:
65
66		reduce(+Graph, -Reduced)
67		is true if Reduced is the reduced graph for Graph. The vertices of the reduced
68		graph are the strongly connected components of Graph. There is an edge in
69		Reduced from u to v iff there is an edge in Graph from one of the vertices in u
70		to one of the vertices in v. A strongly connected component is a maximal set
71		of vertices where each vertex has a path to every other vertex. Algorithm from
72		"Algorithms" by Sedgewick, page 482, Tarjan’s algorithm.
73
74		| ?- vertices_edges_to_ugraph([a,b,c],[a-b,b-c,c-b,b-d],G), reduce(G,G2), edges(G2,Edges).
75		G = [a-[b],b-[c,d],c-[b],d-[]],
76		G2 = [[a]-[[b,c]],[b,c]-[[d]],[d]-[]],
77		Edges = [[a]-[b,c],[b,c]-[d]] ?
78
79		reachable(+Vertex, +Graph, -Reachable)
80		is given a Graph and a Vertex of that Graph, and returns the set of vertices
81		that are Reachable from that Vertex. Takes O(N^2) time.
82
83		random_ugraph(+P, +N, -Graph)
84		where P is a probability, unifies Graph with a random graph of N vertices where
85		each possible edge is included with probability P.
86
87		*/