syn_functions.cpp
Go to the documentation of this file.
1 /** @file syn_functions.cpp Misc functions related to synthesis */
2 
3 /* FAU Discrete Event Systems Library (libfaudes)
4 
5  Copyright (C) 2010 Thomas Moor
6 
7  This library is free software; you can redistribute it and/or
8  modify it under the terms of the GNU Lesser General Public
9  License as published by the Free Software Foundation; either
10  version 2.1 of the License, or (at your option) any later version.
11 
12  This library is distributed in the hope that it will be useful,
13  but WITHOUT ANY WARRANTY; without even the implied warranty of
14  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15  Lesser General Public License for more details.
16 
17  You should have received a copy of the GNU Lesser General Public
18  License along with this library; if not, write to the Free Software
19  Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA */
20 
21 
22 //#define FAUDES_DEBUG_FUNCTION
23 
24 #include "syn_functions.h"
25 #include "omg_buechifnct.h"
26 
27 
28 namespace faudes {
29 
30 
31 
32 
33 /*
34 ***************************************************************************************
35 ***************************************************************************************
36  Implementation
37 ***************************************************************************************
38 ***************************************************************************************
39 */
40 
41 
42 
43 //IsRelativelyMarked(rGenPlant,rGenCand)
44 bool IsRelativelyMarked(const Generator& rGenPlant, const Generator& rGenCand) {
45 
46  // alphabets must match
47  if ( rGenPlant.Alphabet() != rGenCand.Alphabet()) {
48  std::stringstream errstr;
49  errstr << "Alphabets of generators do not match.";
50  throw Exception("IsRelativelyMarked", errstr.str(), 100);
51  }
52 
53 #ifdef FAUDES_CHECKED
54  // generators are meant to be nonblocking
55  if ( !IsNonblocking(rGenCand) || !IsNonblocking(rGenPlant)) {
56  std::stringstream errstr;
57  errstr << "Arguments are expected to be nonblocking.";
58  throw Exception("IsRelativelyMarked", errstr.str(), 201);
59  }
60 #endif
61 
62 #ifdef FAUDES_CHECKED
63  // generators are meant to be deterministic
64  if ( !IsDeterministic(rGenCand) || !IsDeterministic(rGenPlant)) {
65  std::stringstream errstr;
66  errstr << "Arguments are expected to be deterministic.";
67  throw Exception("IsRelativelyMarked", errstr.str(), 202);
68  }
69 #endif
70 
71  // perform composition
72  std::map< std::pair<Idx,Idx> , Idx> revmap;
73  Generator product;
74  product.StateNamesEnabled(false);
75  Product(rGenPlant,rGenCand,revmap,product);
76 
77  // test all reachable states
78  std::map< std::pair<Idx,Idx> , Idx>::iterator rit;
79  for(rit=revmap.begin(); rit!=revmap.end(); ++rit) {
80  // ok: not GPlant-marked state is not considered
81  if(!rGenPlant.ExistsMarkedState(rit->first.first))
82  continue;
83  // ok: GPlant-marked state also has GCand-mark
84  if(rGenCand.ExistsMarkedState(rit->first.second))
85  continue;
86  // failure: GPlant-marked state has no GCand-mark
87  break;
88  }
89 
90  // ok if loop passed
91  return rit==revmap.end();
92 
93 }
94 
95 
96 
97 //IsRelativelyClosed(rGenPlant,rGenCand)
98 bool IsRelativelyClosed(const Generator& rGenPlant, const Generator& rGenCand) {
99 
100  FD_DF("IsRelativelyClosed(\"" << rGenPlant.Name() << "\", \"" << rGenCand.Name() << "\")");
101 
102  // alphabets must match
103  if ( rGenPlant.Alphabet() != rGenCand.Alphabet()) {
104  std::stringstream errstr;
105  errstr << "Alphabets of generators do not match.";
106  throw Exception("IsRelativelyClosed", errstr.str(), 100);
107  }
108 
109 #ifdef FAUDES_CHECKED
110  // generators are meant to be nonblocking
111  if ( !IsNonblocking(rGenCand) || !IsNonblocking(rGenPlant)) {
112  std::stringstream errstr;
113  errstr << "Arguments are expected to be nonblocking.";
114  throw Exception("IsRelativelyClosed", errstr.str(), 201);
115  }
116 #endif
117 
118 #ifdef FAUDES_CHECKED
119  // generators are meant to be deterministic
120  if ( !IsDeterministic(rGenCand) || !IsDeterministic(rGenPlant)) {
121  std::stringstream errstr;
122  errstr << "Arguments are expected to be deterministic.";
123  throw Exception("IsRelativelyClosed", errstr.str(), 202);
124  }
125 #endif
126 
127  // perform composition (variation from cfl_parallel.cpp)
128  FD_DF("IsRelativelyClosed(..): perform product");
129 
130  // todo stack
131  std::stack< std::pair<Idx,Idx> > todo;
132  // current pair, new pair
133  std::pair<Idx,Idx> currentstates, newstates;
134  // accessible states
135  std::set< std::pair<Idx,Idx> > productstates;
136  // iterators
137  StateSet::Iterator lit1, lit2;
138  TransSet::Iterator tit1, tit1_end, tit2, tit2_end;
139  std::set< std::pair<Idx,Idx> >::iterator rcit;
140  // sense violation of L(GCand) <= L(GPlant)
141  bool inclusion12=true;
142 
143  // push all combinations of initial states on todo stack
144  FD_DF("IsRelativelyClosed(..): perform product: adding all combinations of initial states to todo");
145  for (lit1 = rGenCand.InitStatesBegin();
146  lit1 != rGenCand.InitStatesEnd(); ++lit1) {
147  for (lit2 = rGenPlant.InitStatesBegin();
148  lit2 != rGenPlant.InitStatesEnd(); ++lit2) {
149  currentstates = std::make_pair(*lit1, *lit2);
150  todo.push(currentstates);
151  productstates.insert(currentstates);
152  FD_DF("IsRelativelyClosed(..): perform product: (" <<
153  *lit1 << "|" << *lit2 << ")");
154  }
155  }
156 
157  // start algorithm
158  FD_DF("IsRelativelyClosed(..): perform product: Product: processing reachable states:");
159  while (! todo.empty() && inclusion12) {
160  // allow for user interrupt
161  LoopCallback();
162  // get next reachable state from todo stack
163  currentstates = todo.top();
164  todo.pop();
165  FD_DF("Processing (" << currentstates.first << "|"
166  << currentstates.second << ")");
167  // iterate over all rGenCand transitions
168  tit1 = rGenCand.TransRelBegin(currentstates.first);
169  tit1_end = rGenCand.TransRelEnd(currentstates.first);
170  tit2 = rGenPlant.TransRelBegin(currentstates.second);
171  tit2_end = rGenPlant.TransRelEnd(currentstates.second);
172  Idx curev1=0;
173  bool resolved12=true;
174  while((tit1 != tit1_end) && (tit2 != tit2_end)) {
175  // sense new event
176  if(tit1->Ev != curev1) {
177  if(!resolved12) inclusion12=false;
178  curev1=tit1->Ev;
179  resolved12=false;
180  }
181  // shared event
182  if(tit1->Ev == tit2->Ev) {
183  resolved12=true;
184  newstates = std::make_pair(tit1->X2, tit2->X2);
185  // add to todo list if composition state is new
186  rcit = productstates.find(newstates);
187  if(rcit == productstates.end()) {
188  todo.push(newstates);
189  productstates.insert(newstates);
190  FD_DF("Product: todo push: (" << newstates.first << "|"
191  << newstates.second << ")");
192  }
193  ++tit1;
194  ++tit2;
195  }
196  // try resync tit1
197  else if (tit1->Ev < tit2->Ev) {
198  ++tit1;
199  }
200  // try resync tit2
201  else if (tit1->Ev > tit2->Ev) {
202  ++tit2;
203  }
204  }
205  // last event was not resolved in the product
206  if(!resolved12) inclusion12=false;
207  }
208  // report
209 #ifdef FAUDES_DEBUG_FUNCTION
210  FD_DF("IsRelativelyClosed(): Product: done");
211  if(!inclusion12) {
212  FD_DF("IsRelativelyClosed(): Product: inclusion L(G1) <= L(G2) not satisfied");
213  }
214 #endif
215 
216  // bail out when inclusion condition is violated
217  if(!inclusion12) return false;
218 
219  // test all reachable states
220  std::set< std::pair<Idx,Idx> >::iterator rit;
221  for(rit=productstates.begin(); rit!=productstates.end(); ++rit) {
222  // ok: state is GPlant-marked and GCand-marked
223  if(rGenPlant.ExistsMarkedState(rit->second))
224  if(rGenCand.ExistsMarkedState(rit->first))
225  continue;
226  // ok: state is neither GPlant-marked nor GCand-marked
227  if(!rGenPlant.ExistsMarkedState(rit->second))
228  if(!rGenCand.ExistsMarkedState(rit->first))
229  continue;
230  // failure: markin mismatch
231  break;
232  }
233 
234  // ok if loop passed
235  return rit==productstates.end();
236 
237 }
238 
239 
240 // SupRelativelyClosed(rPlantGen, rCAlph, rSpecGen, rResGen)
242  const Generator& rPlantGen,
243  const Generator& rSpecGen,
244  Generator& rResGen)
245 {
246 
247  // CONSISTENCY CHECK: alphabets must match
248  if ( rPlantGen.Alphabet() != rSpecGen.Alphabet()) {
249  EventSet only_in_plant = rPlantGen.Alphabet() - rSpecGen.Alphabet();
250  EventSet only_in_spec = rSpecGen.Alphabet() - rPlantGen.Alphabet();
251  only_in_plant.Name("Only_In_Plant");
252  only_in_spec.Name("Only_In_Specification");
253  std::stringstream errstr;
254  errstr << "Alphabets of generators do not match.";
255  if(!only_in_plant.Empty())
256  errstr << " " << only_in_plant.ToString() << ".";
257  if(!only_in_spec.Empty())
258  errstr << " " << only_in_spec.ToString() << ".";
259  throw Exception("SupCon/SupCon", errstr.str(), 100);
260  }
261 
262  // CONSISTENCY CHECK: plant and spec must be deterministic
263  bool plant_det = rPlantGen.IsDeterministic();
264  bool spec_det = rSpecGen.IsDeterministic();
265  if ((plant_det == false) && (spec_det == true)) {
266  std::stringstream errstr;
267  errstr << "Plant generator must be deterministic, "
268  << "but is nondeterministic";
269  throw Exception("ControllableConsistencyCheck", errstr.str(), 201);
270  }
271  else if ((plant_det == true) && (spec_det == false)) {
272  std::stringstream errstr;
273  errstr << "Spec generator must be deterministic, "
274  << "but is nondeterministic";
275  throw Exception("ControllableConsistencyCheck", errstr.str(), 203);
276  }
277  else if ((plant_det == false) && (spec_det == false)) {
278  std::stringstream errstr;
279  errstr << "Plant and spec generator must be deterministic, "
280  << "but both are nondeterministic";
281  throw Exception("ControllableConsistencyCheck", errstr.str(), 204);
282  }
283 
284  // HELPERS:
285  std::map< std::pair<Idx,Idx>, Idx> rcmap;
286 
287  // ALGORITHM:
288  SupRelativelyClosedUnchecked(rPlantGen, rSpecGen, rcmap, rResGen);
289 }
290 
291 
292 // SupRelativelyClosedUnchecked(rPlantGen, rSpecGen, rCompositionMap, rResGen)
294  const Generator& rPlantGen,
295  const Generator& rSpecGen,
296  std::map< std::pair<Idx,Idx>, Idx>& rCompositionMap,
297  Generator& rResGen)
298 {
299  FD_DF("SupRelativelyClosed(" << &rPlantGen << "," << &rSpecGen << ")");
300 
301  // PREPARE RESULT:
302  Generator* pResGen = &rResGen;
303  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
304  pResGen= rResGen.New();
305  }
306  pResGen->Clear();
307  pResGen->Name(CollapsString("SupRpc(("+rPlantGen.Name()+"),("+rSpecGen.Name()+"))"));
308  pResGen->InjectAlphabet(rPlantGen.Alphabet());
309 
310  // ALGORITHM:
311  StateSet pmarked;
312  StateSet smarked;
313  Product(rPlantGen, rSpecGen, rCompositionMap, pmarked, smarked, *pResGen);
314 
315  // make resulting generator relatively prefix closed
316  StateSet::Iterator six=pResGen->StatesBegin();
317  while(six!= pResGen->StatesEnd()) {
318  Idx s=*(six++);
319  if(!pmarked.Exists(s)) continue;
320  if(smarked.Exists(s)) continue;
321  pResGen->DelState(s);
322  }
323  pResGen->Trim();
324 
325  // copy result
326  if(pResGen != &rResGen) {
327  pResGen->Move(rResGen);
328  delete pResGen;
329  }
330 
331 }
332 
333 
334 // lagcy wrappers
335 bool IsRelativelyPrefixClosed(const Generator& rGenPlant, const Generator& rGenCand){
336  FD_WARN("SupRelativelyPrefixClosed(): API depreciated; use SupRelativelyClosed()");
337  return IsRelativelyClosed(rGenPlant,rGenCand);
338 }
339 void SupRelativelyPrefixClosed(const Generator& rPlantGen, const Generator& rSpecGen,
340  Generator& rResGen) {
341  FD_WARN("SupRelativelyPrefixClosed(): API depreciated; use SupRelativelyClosed()");
342  SupRelativelyClosed(rPlantGen,rSpecGen,rResGen);
343 }
344 
345 
346 
347 } // name space
#define FD_WARN(message)
#define FD_DF(message)
const std::string & Name(void) const
Definition: cfl_types.cpp:422
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Definition: cfl_types.cpp:175
StateSet::Iterator StatesBegin(void) const
StateSet::Iterator InitStatesBegin(void) const
const EventSet & Alphabet(void) const
virtual void Move(vGenerator &rGen)
TransSet::Iterator TransRelBegin(void) const
virtual vGenerator * New(void) const
bool DelState(Idx index)
StateSet::Iterator StatesEnd(void) const
TransSet::Iterator TransRelEnd(void) const
bool IsDeterministic(void) const
bool StateNamesEnabled(void) const
StateSet::Iterator InitStatesEnd(void) const
virtual void Clear(void)
bool ExistsMarkedState(Idx index) const
void InjectAlphabet(const EventSet &rNewalphabet)
bool Empty(void) const
Definition: cfl_baseset.h:1787
bool Exists(const T &rElem) const
Definition: cfl_baseset.h:2180
void Product(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
bool IsDeterministic(const vGenerator &rGen)
bool IsRelativelyMarked(const Generator &rGenPlant, const Generator &rGenCand)
void SupRelativelyClosed(const Generator &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
bool IsRelativelyClosed(const Generator &rGenPlant, const Generator &rGenCand)
uint32_t Idx
void LoopCallback(bool pBreak(void))
Definition: cfl_utils.cpp:679
void SupRelativelyClosedUnchecked(const Generator &rPlantGen, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
bool IsNonblocking(const GeneratorVector &rGvec)
bool IsRelativelyPrefixClosed(const Generator &rGenPlant, const Generator &rGenCand)
void SupRelativelyPrefixClosed(const Generator &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
std::string CollapsString(const std::string &rString, unsigned int len)
Definition: cfl_utils.cpp:91

libFAUDES 2.33h --- 2025.06.18 --- c++ api documentaion by doxygen