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
|
// Graph of strongly connected components -*- c++ -*-
#ifndef COMPONENTGRAPH_H_
# define COMPONENTGRAPH_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include "typedefs.h"
# include "file.h"
/** @file ComponentGraph.h
* Graph of strongly connected components
*/
/* Copyright 2000-2001 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. */
/** Graph of strongly connected components */
class ComponentGraph
{
public:
/** Constructor
* @param graph the underlying graph
*/
explicit ComponentGraph (const class Graph& graph);
private:
/** Copy constructor */
ComponentGraph (const class ComponentGraph& old);
/** Assignment operator */
class ComponentGraph& operator= (const class ComponentGraph& old);
public:
/** Destructor */
~ComponentGraph ();
private:
/** Open the component graph files with temporary names
* @return true if everything succeeded
*/
inline bool openFiles ();
/** Set the component number of a state
* @param state the state
* @param comp the component
*/
inline void setComponent (card_t state, card_t comp);
/** Compute the arcs of the component graph */
inline void computeArcs ();
public:
/** Compute the strongly connected components
* @param state start state of the search
* @param cond condition for exploring states (NULL=true)
* @return number of strongly connected components (0=fail)
*/
unsigned compute (card_t state,
const class Expression* cond);
/** Determine the number of strongly connected components in the graph */
unsigned size () const { return myNumComponents; }
/** Determine the number of terminal components in the component graph */
unsigned getNumTerminals () const { return myNumTerminals; }
/** Determine the component a state belongs to
* @param state the state number
* @return the corresponding component, or CARD_T_MAX if none
*/
card_t getComponent (card_t state) const;
/** Determine the states a component consists of
* @param comp the component number
* @return the amount and numbers of the contained states
*/
card_t* getStates (card_t comp) const;
/** Determine the number of successors of a component
* @param comp the component number
* @return the number of successors
*/
card_t getNumSucc (card_t comp) const;
/** Determine the number of predecessors of a component
* @param comp the component number
* @return the number of predecessors
*/
card_t getNumPred (card_t comp) const;
/** Determine the successors of a component
* @param comp the component number
* @return the amount and numbers of the successor components
*/
card_t* getSucc (card_t comp) const;
/** Determine the predecessors of a component
* @param comp the component number
* @return the amount and numbers of the predecessor components
*/
card_t* getPred (card_t comp) const;
/** Determine the shortest path from a state to a component
* @param state the state number
* @param comp the component number
* @param pathc condition that must hold in every state on the path
* @return the amount and numbers of the states on the path
*/
card_t* path (card_t state, card_t comp,
const class Expression* pathc) const;
/** Determine the shortest path to a state from a component
* @param state the state number
* @param comp the component number
* @param pathc condition that must hold in every state on the path
* @return the amount and numbers of the states on the path
*/
card_t* rpath (card_t state, card_t comp,
const class Expression* pathc) const;
private:
/** The underlying graph */
const class Graph& myGraph;
/** Number of components in the graph (0=not computed) */
card_t myNumComponents;
/** Number of terminal components in the graph (0=not computed) */
card_t myNumTerminals;
/** Mapping from state numbers to component numbers */
file_t myStateComponents;
/** Component directory */
file_t myComponentDirectory;
/** Mapping from component numbers to state numbers */
FILE* myComponentStates;
/** Successor components of a component (forward arcs) */
FILE* mySuccComponents;
/** Predecessor components of a component (backward arcs) */
FILE* myPredComponents;
};
#endif // COMPONENTGRAPH_H_
|
