OGtoGraphviz.sml 8.42 KB
Newer Older
Michael Westergaard's avatar
Import  
Michael Westergaard committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
(************************************************************************)
(* CPN Tools                                                            *)
(* Copyright 2010-2011 AIS Group, Eindhoven University of Technology    *)
(*                                                                      *)
(* CPN Tools is originally developed by the CPN Group at Aarhus         *)
(* University from 2000 to 2010. The main architects behind the tool    *)
(* are Kurt Jensen, Soren Christensen, Lars M. Kristensen, and Michael  *)
(* Westergaard.  From the autumn of 2010, CPN Tools is transferred to   *)
(* the AIS group, Eindhoven University of Technology, The Netherlands.  *)
(*                                                                      *)
(* This file is part of CPN Tools.                                      *)
(*                                                                      *)
(* CPN Tools is free software: you can redistribute it and/or modify    *)
(* it under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or    *)
(* (at your option) any later version.                                  *)
(*                                                                      *)
(* CPN Tools is distributed in the hope that it will be useful,         *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
(* GNU General Public License for more details.                         *)
(*                                                                      *)
(* You should have received a copy of the GNU General Public License    *)
(* along with CPN Tools.  If not, see <http://www.gnu.org/licenses/>.   *)
(************************************************************************)
(* 
 * Module:      OGtoGraphviz
 * 
 * Description:  Export graph structure of state spaces and 
 *               SCC graphs to Graphviz
 *
 * Graphviz must be downloaded and installed from
 *     http://www.research.att.com/sw/tools/graphviz/
 *
 *)


structure OGtoGraphviz = struct

(* Given a node from either a state space or a SCC graph, 
 * generate a node id in the DOT language for Graphviz
 *)
fun nodeToNodeID (CPN'node : Node) = 
    if CPN'node > 0 
    then "N"^mkst_Node(CPN'node)(* a state space node *)
    else "SCC"^mkst_Node(abs CPN'node) (* a scc node *)


(* Given a node from either a state space or a SCC graph, 
 * generate a node statement in the DOT language for Graphviz
 *)
fun genNodeStmt CPN'node = 
53
    "  "^nodeToNodeID(CPN'node)^" [label=\""^(NodeDescriptor(CPN'node))^"\"];\n" 
Michael Westergaard's avatar
Import  
Michael Westergaard committed
54
55
56


fun arcToEdgeLabel (CPN'arc: Arc) =
57
    "A"^st_Arc(CPN'arc)^":"^st_BE(ArcToBE(CPN'arc))
Michael Westergaard's avatar
Import  
Michael Westergaard committed
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85

(* Given a (sourceNode,arc,destNode) tuple from the state space, 
 * generate an edge statement in the DOT language for Graphviz 
 * for the arc from the sourceNode to the destNode
 *)
fun genEdgeStmt (CPN'sourceNode,CPN'arc,CPN'destNode) = 
    "  "^nodeToNodeID(CPN'sourceNode)^" -> "^
    nodeToNodeID(CPN'destNode)^ 
    " [ label=\""^arcToEdgeLabel(CPN'arc)^"\" ];\n"


(* Check that all specified nodes exist in state space *)
fun checkNodes (CPN'nodes : Node list) = 
    if CPN'nodes = EntireGraph
    then ()
    else case List.find (not o CPN'OGUtils.NodeExists) CPN'nodes of
	     NONE => ()
	   | SOME CPN'node => 
	     raise CPN'Error ("Node "^mkst_Node(CPN'node)^
			      " does not exist in the state space")
		   
(* Check that all specified arcs exist in state space *)
fun checkArcs (CPN'arcs : Arc list) = 
    if CPN'arcs = EntireGraph
    then ()
    else case List.find (not o CPN'OGUtils.ArcExists) CPN'arcs of
	     NONE => ()
	   | SOME CPN'arc => 
86
	     raise CPN'Error ("Arc "^st_Arc(CPN'arc)^
Michael Westergaard's avatar
Import  
Michael Westergaard committed
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
			      " does not exist in the state space")
(* 
 * function createGraphvizFile
 *
 * Exports the state space graph structure of the nodes determined
 * by stateSpaceArea to the file filename *)
fun createGraphvizFile (CPN'filename: string, 
			CPN'nodes: Node list,
			CPN'edges: (Node * Arc * Node) list) = 
    let
	val fid = TextIO.openOut CPN'filename
	
	(* The beginning of the Graphviz file *)
	val _ = TextIO.output(fid, "digraph cpn_tools_graph {\n")

	fun outputStmt stmt = TextIO.output(fid,stmt)

	val _ =  EvalNodes (CPN'nodes, outputStmt o genNodeStmt)

	val edgeStmts = map genEdgeStmt CPN'edges
	val _ = map outputStmt edgeStmts

	(* Add the final information to the Graphviz file *)
	val _ = TextIO.output(fid,"}")
    in
	TextIO.closeOut(fid)
    end

fun CPN'nodePathToEdges [] = [] (* should not happen *)
  | CPN'nodePathToEdges [CPN'node] = []
  | CPN'nodePathToEdges (CPN'node1::(CPN'node2::CPN'nodes)) = 
    case Arcs(CPN'node1,CPN'node2) of 
	[] => raise CPN'Error ("No arc between nodes "^
			      mkst_Node(CPN'node1)^" and "^
			      mkst_Node(CPN'node2)^" in CPN'nodesToEdge")
      | CPN'arcs => (map (fn CPN'arc => (CPN'node1,CPN'arc,CPN'node2)) CPN'arcs)^^(CPN'nodePathToEdges(CPN'node2::CPN'nodes))
	    
fun CPN'arcToEdge CPN'arc = 
    (SourceNode(CPN'arc),CPN'arc,DestNode(CPN'arc))

fun CPN'arcPathToEdges [] = [] (* should not happen *)
  | CPN'arcPathToEdges [CPN'arc] = [CPN'arcToEdge CPN'arc]
  | CPN'arcPathToEdges (CPN'arc1::(CPN'arc2::CPN'rest)) = 
    if DestNode(CPN'arc1)=SourceNode(CPN'arc2)
	then (CPN'arcToEdge CPN'arc1)::(CPN'arcPathToEdges (CPN'arc2::CPN'rest))
    else raise CPN'Error ("No node between arcs "^
			  mkst_Node(CPN'arc1)^" and "^
134
			 mkst_Node(CPN'arc2)^" in CPN'arcPathToEdges")
Michael Westergaard's avatar
Import  
Michael Westergaard committed
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
	
(* Duplicates not removed *)
fun ExportNodes (CPN'filename: string, []) = 
    raise CPN'Error "No nodes to export in ExportNodes" 
  | ExportNodes (CPN'filename: string, CPN'nodes: Node list) =
	(checkNodes(CPN'nodes);
	 createGraphvizFile (CPN'filename, CPN'nodes, []));

	    
fun ExportNodePath(CPN'filename: string, []) = 
    raise CPN'Error "No path to export in ExportNodePath" 
  | ExportNodePath(CPN'filename: string, CPN'nodes: Node list) = 
    	(checkNodes(CPN'nodes);
	 createGraphvizFile (CPN'filename, 
			     case CPN'nodes of
				 [CPN'node] => [CPN'node]
			       | _ => [], 
			     CPN'nodePathToEdges CPN'nodes))

(* Duplicates not removed *)
fun ExportArcs (CPN'filename: string, []) = 
    raise CPN'Error "No arcs to export in ExportArcs" 
  | ExportArcs(CPN'filename: string, CPN'arcs: Arc list) = 
	(checkArcs(CPN'arcs);
	 createGraphvizFile(CPN'filename, [],
			    rev(EvalArcs(CPN'arcs,CPN'arcToEdge))))

fun ExportArcPath(CPN'filename: string, []) = 
    raise CPN'Error "No path to export in ExportArcPath" 
  | ExportArcPath(CPN'filename: string, CPN'arcs: Arc list) = 
	(checkArcs(CPN'arcs);
	createGraphvizFile(CPN'filename, [],
			   CPN'arcPathToEdges CPN'arcs))
		    

(* Duplicates not removed *)
fun ExportSuccessors (CPN'filename: string, []) = 
    raise CPN'Error "No nodes in ExportSuccessors"
  | ExportSuccessors (CPN'filename: string, CPN'nodes: Node list) = 
	let
	    val _ = checkNodes CPN'nodes
	    fun nodeToSuccessorEdges CPN'node = 
		map (fn arc => (CPN'node,arc,DestNode(arc))) 
		(OutArcs(CPN'node))
	    val nodesWithoutSuccessors = 
		rev(PredNodes (CPN'nodes, (fn CPN'node => OutArcs(CPN'node)=[]),NoLimit))
	    val allSuccessorEdges = 
		flatten (rev(EvalNodes(CPN'nodes, nodeToSuccessorEdges)))
	in
	    createGraphvizFile(CPN'filename, nodesWithoutSuccessors, allSuccessorEdges)
	end	


(* Duplicates not removed *)
fun ExportPredecessors (CPN'filename: string, []) = 
    raise CPN'Error "No nodes in ExportPredecessors"
  | ExportPredecessors (CPN'filename: string, CPN'nodes: Node list) = 
	let
	    val _ = checkNodes CPN'nodes
	    fun nodeToPredecessorEdges CPN'node = 
		map (fn arc => (SourceNode(arc),arc,CPN'node)) 
		(InArcs(CPN'node))
	    val nodesWithoutPredecessors = 
		rev(PredNodes(CPN'nodes,(fn CPN'node => InArcs(CPN'node)=[]), NoLimit))
	    val allPredecessorEdges = 
		flatten(rev(EvalNodes (CPN'nodes, nodeToPredecessorEdges)))
	in
	    createGraphvizFile(CPN'filename, nodesWithoutPredecessors,allPredecessorEdges)
	end	


fun ExportStateSpace (CPN'filename: string) = 
    ExportSuccessors(CPN'filename, EntireGraph);

fun ExportSccGraph (CPN'filename: string) = 
    let
	fun sccToSuccessorEdges (CPN'scc: Scc) = 
	    map (fn CPN'arc => (CPN'scc,CPN'arc,SccDestNode(CPN'arc))) 
		(SccOutArcs(CPN'scc))
	val sccsWithoutSuccessors = 
	    rev(PredAllSccs (fn CPN'scc => SccOutArcs(CPN'scc)=[]))
	val allSuccessorEdges = 
	    flatten (rev(EvalAllSccs(sccToSuccessorEdges)))
    in
	createGraphvizFile(CPN'filename, sccsWithoutSuccessors, allSuccessorEdges)
    end	
	
end;