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
53
54
55
56
57
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
86
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
134
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
|
// Visualization interface to Graphviz dotty(1) -*- c++ -*-
#ifndef DOTTY_H_
# define DOTTY_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include "typedefs.h"
/** @file Dotty.h
* Visualization interface to Graphviz dotty(1)
*/
/* Copyright 2001-2003 Marko Mkel (msmakela@tcs.hut.fi).
This file is part of MARIA, a reachability analyzer and model checker
for high-level Petri nets.
MARIA 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, or (at your option)
any later version.
MARIA 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.
The GNU General Public License is often shipped with GNU software, and
is generally kept in a file called COPYING or LICENSE. If you do not
have a copy of the license, write to the Free Software Foundation,
59 Temple Place, Suite 330, Boston, MA 02111 USA. */
/** Graphviz dotty(1) interface */
class Dotty
{
protected:
/** Constructor */
Dotty ();
private:
/** Copy constructor */
Dotty (const class Dotty& old);
/** Assignment operator */
class Dotty& operator= (const class Dotty& old);
public:
/** Destructor */
~Dotty ();
/** Set the name of the visualization program */
static void useVisual (const char* name);
/** Start the visualization process
* @return pointer to the visualization object; NULL on failure
*/
static class Dotty* startVisual ();
/** Stop the visualization process */
static void stopVisual ();
private:
/** Clear the visualization variables */
void clearVisual ();
public:
/** Dump the syntax tree of the model
* @param net the model being dumped
* @param adding flag: add to existing graph
*/
void dump (const class Net& net,
bool adding) const;
/** Display a state
* @param reporter the reachability graph interface
* @param state number of the state to be displayed
* @param adding flag: add to existing graph
*/
void show (const class GraphReporter& reporter,
card_t state, bool adding) const;
/** Display successor arcs
* @param reporter the reachability graph interface
* @param state number of the originating state
* @param seq flag: fully expand deterministic sequences
* @param adding flag: add to existing graph
*/
void succ (class GraphReporter& reporter,
card_t state, bool seq, bool adding) const;
/** Display predecessor arcs
* @param reporter the reachability graph interface
* @param state number of the target state
* @param seq flag: fully expand deterministic sequences
* @param adding flag: add to existing graph
*/
void pred (const class GraphReporter& reporter,
card_t state, bool seq, bool adding) const;
/** Display a graph of strongly connected components
* @param cgraph the graph of strongly connected components
* @param adding flag: add to existing graph
*/
void components (const class ComponentGraph& cgraph,
bool adding) const;
/** Display a strongly connected component
* @param reporter the reachability graph interface
* @param comp number of the component
* @param cond condition for picking the states in the component
* @param adding flag: add to existing graph
*/
void component (const class GraphReporter& reporter,
card_t comp,
const class Expression* cond,
bool adding) const;
/** Dump the reachability graph of the model
* @param reporter the reachability graph interface
* @param adding flag: add to existing graph
*/
void dumpgraph (const class GraphReporter& reporter,
bool adding) const;
/** Display the succeeding components of a strongly connected component
* @param cgraph the graph of strongly connected components
* @param comp number of the component
* @param adding flag: add to existing graph
*/
void comp_succ (const class ComponentGraph& cgraph,
card_t comp, bool adding) const;
/** Display the preceding components of a strongly connected component
* @param cgraph the graph of strongly connected components
* @param comp number of the component
* @param adding flag: add to existing graph
*/
void comp_pred (const class ComponentGraph& cgraph,
card_t comp, bool adding) const;
/** Display a path in a reachability graph
* @param reporter the reachability graph interface
* @param path state numbers on the path
* @param adding flag: add to existing graph
* @param reverse flag: reverse the arcs
*/
void show (const class GraphReporter& reporter,
const card_t* path,
bool adding,
bool reverse) const;
/** @name The lower-level interface for displaying counterexample paths */
/*@{*/
/** Display the graph prologue
* @param adding flag: add to existing graph
*/
void displayPrologue (bool adding) const;
/** Display the graph epilogue */
void displayEpilogue () const;
/** Display a node in a counterexample path
* @param m the marking to be displayed
*/
void displayMarking (const class GlobalMarking& m) const;
/** Display an edge in a counterexample path
* @param transition the transition
* @param valuation the valuation
* @param m the destination node
*/
void displayEdge (const class Transition& transition,
const class Valuation& valuation,
const class GlobalMarking& m) const;
/*@}*/
private:
/** The singleton object */
static class Dotty theDotty;
/** The output stream */
class Printer* myOut;
};
#endif // DOTTY_H_
|
