con_cctrim.cpp
Go to the documentation of this file.
1 /** @file con_cctrim.cpp more efficient Trim() operation */
2 
3 /*
4  *
5  * Copyright (C) 2011 Tomas Masopust
6  *
7  * Implementation of a bit more efficient Trim() function
8  * based on graph algorithms
9  *
10  */
11 
12 #include "con_cctrim.h"
13 #include <vector>
14 #include <string>
15 #include <queue>
16 
17 using namespace std;
18 
19 namespace faudes {
20 
21 // The graph adjecency list representation
22 class adjlist {
23  private:
24  unsigned int root;
26  unsigned int numberOfNodes;
27  struct node {
28  unsigned int state;
31  };
32  vector<node*> nodeArray;
33  vector<bool> examined;
34  public:
35  adjlist(const Generator& gen);
36  unsigned int getRoot();
37  unsigned int getNumberOfNodes();
38  void Display();
39  void SetExamined(bool b);
41  StateSet CoAccessible();
42  void ReverseAndRoot();
43  bool IsAccessible();
44  ~adjlist();
45 };
46 
47 // Constructor
48 adjlist::adjlist(const Generator& gen) :
49  root(gen.InitState()),
50  finalStates(gen.MarkedStates()),
51  numberOfNodes(gen.States().MaxIndex()),
52  nodeArray(gen.States().MaxIndex()),
53  examined(gen.States().MaxIndex()) {
54  // Better to use gen.Size() instead of gen.States().MaxIndex(), but there is a problem with numbered states!
55  // Or add some additional table with refering my indexes to the original indexes
56  // The array of nodes and examine flags
57  for (unsigned int i=0; i < numberOfNodes; i++) {
58  nodeArray[i] = NULL;
59  examined[i] = false;
60  }
61  // List of adjecent nodes to each node
63  for (eit = gen.TransRelBegin(); eit != gen.TransRelEnd(); ++eit) {
64  if (eit->X1 != eit->X2) { // we can ignore loops
65  node* n = new node;
66  n->state = eit->X2;
67  n->link = nodeArray[eit->X1-1];
68  n->blink = NULL;
69  if (nodeArray[eit->X1-1] == NULL) {
70  nodeArray[eit->X1-1] = n;
71  } else {
72  nodeArray[eit->X1-1]->blink = n;
73  nodeArray[eit->X1-1] = n;
74  }
75  }
76  }
77  // remove multiedges
78  vector<unsigned int> mult (numberOfNodes);
79  for (unsigned int i=0; i < numberOfNodes; i++) {
80  mult[i] = 0;
81  }
82  for (unsigned int i=0; i < nodeArray.size(); i++) {
83  node* q=nodeArray[i];
84  while (q != NULL) {
85  if (mult[q->state-1] != i+1) {
86  mult[q->state-1] = i+1;
87  q=q->link;
88  } else {
89  if (q->blink != NULL) {
90  node* p = q->blink;
91  p->link = q->link;
92  if (p->link != NULL) {
93  p->link->blink = p;
94  }
95  delete q;
96  q = p->link;
97  } else {
98  nodeArray[i] = q->link;
99  node* p = q;
100  delete p;
101  if (nodeArray[i] != NULL) {
102  nodeArray[i]->blink = NULL;
103  }
104  q = nodeArray[i];
105  }
106  }
107  }
108  }
109 }
110 
111 unsigned int adjlist::getRoot() {
112  return root;
113 }
114 
116  return numberOfNodes;
117 }
118 
120  cout << " ===== Displaying the graph ===== " << endl;
121  for (unsigned int i=0; i < nodeArray.size(); i++) {
122  node *q;
123  cout << "Neighbours of " << i+1 << ": ";
124  for(q=nodeArray[i]; q != NULL; q=q->link) {
125  cout << q->state << ", ";
126  }
127  cout << endl;
128  }
129 }
130 
131 // Sets all examined flags of nodes to a value b
132 void adjlist::SetExamined(bool b) {
133  for (unsigned int i=0; i < nodeArray.size(); i++) {
134  examined[i] = false;
135  }
136 }
137 
138 // Returns the set of accessible states
140  this->SetExamined(false);
141  StateSet AccessibleSet;
142  queue<Idx> que;
143  que.push(root);
144  examined[root-1]=true;
145  Idx index;
146  while (!que.empty()) {
147  index = que.front();
148  que.pop();
149  AccessibleSet.Insert(index);
150  node* q=nodeArray[index-1];
151  while (q != NULL) {
152  if (!examined[q->state-1]) {
153  que.push(q->state);
154  examined[q->state-1] = true;
155  }
156  q=q->link;
157  }
158  }
159  return AccessibleSet;
160 }
161 
162 // Returns the set of coaccessible states
164  // Reverse the graph -- adds new root node
165  this->ReverseAndRoot();
166  // Check if the reversed rooted graph is accessible
167  return this->Accessible();
168 }
169 
170 // Reverses the graph and creates a new unique root
172  vector<node*> v(numberOfNodes+1);
173  for (unsigned int i=0; i < v.size(); i++) {
174  v[i] = NULL;
175  }
176  for (unsigned int i=0; i < nodeArray.size(); i++) {
177  for(node* q=nodeArray[i]; q != NULL; q=q->link) {
178  node* sNode = new node;
179  sNode->state = i+1;
180  sNode->link = v[q->state-1];
181  v[q->state-1] = sNode;
182  }
183  }
184  nodeArray.resize(numberOfNodes+1);
185  nodeArray = v;
186  // new root node linked with all original final states
187  StateSet::Iterator sit;
188  for (sit = finalStates.Begin(); sit != finalStates.End(); ++sit) {
189  node* n = new node;
190  n->state = *sit;
193  }
194  root = numberOfNodes+1;
195 }
196 
198  StateSet acc = this->Accessible();
199  if (this->getNumberOfNodes() == acc.Size()) {
200  return true;
201  }
202  return false;
203 }
204 
205 // Destructor
207  for (unsigned int i=0; i < nodeArray.size(); i++) {
208  node* p = nodeArray[i];
209  node* q;
210  while (p != NULL) {
211  q = p->link;
212  delete p;
213  p = q;
214  }
215  }
216 }
217 // end of the adjacency list
218 
219 
220 // ccTrim() function
221 bool ccTrim(const Generator& gen, Generator& trimGen) {
222  // This means that states are number
223  if (gen.Size() != gen.States().MaxIndex()) {
224  cerr << "=============================================================================\n"
225  << "You probably use numbers for state names, and some state-numbers are missing.\n"
226  << "Rename states for the algorithm to work more efficiently.\n"
227  << "=============================================================================" << endl;
228  }
229 
230  if (!IsDeterministic(gen)) {
231  cerr << "The generator is not deterministic." << endl;
232  return false;
233  }
234 
235  if (gen.InitStatesSize() != 1) {
236  cerr << "The generator does not have only one initial state." << endl;
237  return false;
238  }
239 
240  trimGen = gen;
241  // Create the graph representation of the generator gen
242  adjlist graph (trimGen);
243  // Set of accessible states
244  StateSet acc = graph.Accessible();
245  // Set of unaccessible states
246  StateSet unacc = trimGen.States() - acc;
247  // Set of coaccessible states
248  StateSet coacc = graph.CoAccessible();
249  // Set of uncoaccessible states
250  StateSet uncoacc = trimGen.States() - coacc;
251  // Set of states that are not accessible or coaccessible
252  StateSet un = unacc + uncoacc;
253  trimGen.DelStates(un);
254  return un.Size()==0;
255 }
256 
257 } //end namespace
Set of indices.
Definition: cfl_indexset.h:78
Idx Insert(void)
Insert new index to set.
Idx MaxIndex(void) const
Get maximum index used in this set (0 for emptyset)
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Iterator on transition.
Definition: cfl_transset.h:269
StateSet CoAccessible()
Definition: con_cctrim.cpp:163
unsigned int numberOfNodes
Definition: con_cctrim.cpp:26
StateSet Accessible()
Definition: con_cctrim.cpp:139
StateSet finalStates
Definition: con_cctrim.cpp:25
vector< bool > examined
Definition: con_cctrim.cpp:33
void SetExamined(bool b)
Definition: con_cctrim.cpp:132
unsigned int getNumberOfNodes()
Definition: con_cctrim.cpp:115
unsigned int root
Definition: con_cctrim.cpp:24
vector< node * > nodeArray
Definition: con_cctrim.cpp:32
unsigned int getRoot()
Definition: con_cctrim.cpp:111
void ReverseAndRoot()
Definition: con_cctrim.cpp:171
Base class of all FAUDES generators.
TransSet::Iterator TransRelBegin(void) const
Iterator to Begin() of transition relation.
Idx InitStatesSize(void) const
Get number of initial states.
void DelStates(const StateSet &rDelStates)
Delete a set of states Cleans mpStates, mInitStates, mMarkedStates, mpTransrel, and mpStateSymboltabl...
TransSet::Iterator TransRelEnd(void) const
Iterator to End() of transition relation.
Idx Size(void) const
Get generator size (number of states)
const StateSet & States(void) const
Return reference to state set.
more efficient Trim() operation
Iterator End(void) const
Iterator to the end of set.
Definition: cfl_baseset.h:1896
Iterator Begin(void) const
Iterator to the begin of set.
Definition: cfl_baseset.h:1891
Idx Size(void) const
Get Size of TBaseSet.
Definition: cfl_baseset.h:1819
bool ccTrim(const Generator &gen, Generator &trimGen)
A more efficient Trim() operation.
Definition: con_cctrim.cpp:221
bool IsAccessible(const vGenerator &rGen)
RTI wrapper function.
void Accessible(vGenerator &rGen)
RTI wrapper function.
bool IsDeterministic(const vGenerator &rGen)
RTI wrapper function.
libFAUDES resides within the namespace faudes.
uint32_t Idx
Type definition for index type (allways 32bit)
unsigned int state
Definition: con_cctrim.cpp:28

libFAUDES 2.32b --- 2024.03.01 --- c++ api documentaion by doxygen