pev_abstraction.cpp
Go to the documentation of this file.
1 /** @file pev_abstraction.cpp Conflict preserving abstractions */
2 
3 
4 /* FAU Discrete Event Systems Library (libfaudes)
5 
6  Copyright (C) 2023 Yiheng Tang
7  Copyright (C) 2025 Thomas Moor
8  Exclusive copyright is granted to Klaus Schmidt
9 
10  This library is free software; you can redistribute it and/or
11  modify it under the terms of the GNU Lesser General Public
12  License as published by the Free Software Foundation; either
13  version 2.1 of the License, or (at your option) any later version.
14 
15  This library is distributed in the hope that it will be useful,
16  but WITHOUT ANY WARRANTY; without even the implied warranty of
17  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
18  Lesser General Public License for more details.
19 
20  You should have received a copy of the GNU Lesser General Public
21  License along with this library; if not, write to the Free Software
22  Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA */
23 
24 
25 #include "corefaudes.h"
26 #include "pev_pgenerator.h"
27 #include "pev_sparallel.h"
28 #include "pev_abstraction.h"
29 
30 // local debug
31 #undef FD_DF
32 #define FD_DF(a) FD_WARN(a)
33 
34 namespace faudes {
35 
36 /*
37 ************************************
38 Implementation of class Candidate
39 ************************************
40 */
41 
42 // Merge equivalent classes, i.e. perform quotient abstraction
43 // (this implementation works fine with a small amount of small equiv classes)
45  Generator& rGen,
46  TransSetX2EvX1& rRevTrans,
47  const std::list< StateSet >& rClasses,
48  const EventSet& silent
49  )
50 {
51  // iterators
52  StateSet::Iterator sit;
53  StateSet::Iterator sit_end;
57  TransSet::Iterator tit_end;
58  std::map<Idx,Idx> result;
59  // record for delayed delete
60  StateSet delstates;
61  // iterate classes
62  std::list< StateSet >::const_iterator qit=rClasses.begin();
63  for(;qit!=rClasses.end();++qit) {
64  sit=qit->Begin();
65  sit_end=qit->End();
66  Idx q1=*(sit++); // this than denotes the name of quotient
67  result.insert({q1,q1});
68  for(;sit!=sit_end;++sit){
69  Idx q2=*sit;
70  result.insert({q2,q1});
71  // merge outgoing transitions form q2 to q1
72  tit = rGen.TransRelBegin(q2);
73  tit_end = rGen.TransRelEnd(q2);
74  for(;tit!=tit_end;++tit) {
75  // // if X2 of this transition is still in this class with a silent ev, skip -- we shall do selfloop removal extern
76  // if (silent.Exists(tit->Ev) && (*qit).Exists(tit->X2)) continue;
77  rGen.SetTransition(q1,tit->Ev,tit->X2);
78  rRevTrans.Insert(q1,tit->Ev,tit->X2);
79  }
80  // merge incomming transitions form q2 to q1
81  rit = rRevTrans.BeginByX2(q2);
82  rit_end = rRevTrans.EndByX2(q2);
83  for(;rit!=rit_end;++rit) {
84  // // if X1 of this transition is still in this class with a silent ev, skip -- we shall do selfloop removal extern
85  // if (silent.Exists(rit->Ev) && (*qit).Exists(rit->X1)) continue;
86  rGen.SetTransition(rit->X1,rit->Ev,q1);
87  rRevTrans.Insert(rit->X1,rit->Ev,q1);
88  }
89  // fix marking: if q2 was not marked, need to un-mark q1 (original by Michael Meyer)
90  // if(!(rGen.ExistsMarkedState(q2)))
91  // rGen.ClrMarkedState(q1);
92  // fix marking: if q2 was marked, so becomes q1 (quotient by the books)
93  if(rGen.ExistsMarkedState(q2))
94  rGen.InsMarkedState(q1);
95  // fix initial states: if q2 was initial, so becomes q1
96  if((rGen.ExistsInitState(q2)))
97  rGen.InsInitState(q1);
98  // log for delete
99  delstates.Insert(q2);
100  }
101  }
102  // do delete
103  rGen.DelStates(delstates);
104 
105  // update mergemap (only used for counter example)
106  std::map<Idx,Idx>::iterator mit = mMergeMap.begin();
107  for(;mit!=mMergeMap.end();mit++){
108  std::list< StateSet >::const_iterator classit = rClasses.begin();
109  for (;classit!=rClasses.end();classit++){
110  if ((*classit).Exists(mit->second)){
111  // this shall be consistent with codes above, in that the Idx of quotient class
112  // is always the FIRST member of the class. Here is something to notice: StateSet
113  // is based on TBaseSet, whose core is the std::set which is automatically sorted.
114  // This means, as long as the eqclass is not inserted with new elements (note the
115  // input rClasses is const), the first element of the class will not change, i.e.
116  // always the "smallest" element.
117  mit->second = *(*classit).Begin();
118  break;
119  }
120  }
121  }
122 }
123 
124  // Compute extended transition relation '=>', i.e. relate each two states that
125 // can be reached by one non-slilent event and an arbitrary amount of silent
126 // events befor/after the non-silent event
127 //
128 // Note: currently all silent events are treated equivalent, as if they
129 // had been substituted by a single silent event "tau"; we should perform
130 // this substitution beforehand.
131 // YT: the original implementation is replaced by the following new iteration
132 // where for each iteration we only consider those new augmented transitions.
133 
134 // but it seem that the codes is not obviously getting faster.
135 
136 void Candidate::ExtendedTransRel(const Generator& rGen, const EventSet& rSilentAlphabet, TransSet& rXTrans) {
137 
138  // HELPERS:
139  TransSet::Iterator tit1;
140  TransSet::Iterator tit1_end;
141  TransSet::Iterator tit2;
142  TransSet::Iterator tit2_end;
143  TransSet newtrans;
144 
145  // initialize result with original transitionrelation
146  rXTrans=rGen.TransRel();
147  newtrans = rGen.TransRel(); // initialize iteration
148  // loop for fixpoint
149  while(!newtrans.Empty()) {
150  // store new transitions for next iteration
151  TransSet nextnewtrans;
152  // loop over all transitions in newtrans
153  tit1=newtrans.Begin();
154  tit1_end=newtrans.End();
155  for(;tit1!=tit1_end; ++tit1) {
156  // if it is silent add transition to non silent successor directly
157  if(rSilentAlphabet.Exists(tit1->Ev)) {
158  tit2=rXTrans.Begin(tit1->X2);
159  tit2_end=rXTrans.End(tit1->X2);
160  for(;tit2!=tit2_end; ++tit2) {
161  // if(!rSilentAlphabet.Exists(tit2->Ev)) // tmoor 18-09-2019
162  if (!rXTrans.Exists(tit1->X1,tit2->Ev,tit2->X2))
163  nextnewtrans.Insert(tit1->X1,tit2->Ev,tit2->X2);
164  }
165  }
166  // if it is not silent add transition to silent successor directly
167  else {
168  tit2=rXTrans.Begin(tit1->X2);
169  tit2_end=rXTrans.End(tit1->X2);
170  for(;tit2!=tit2_end; ++tit2) {
171  if(rSilentAlphabet.Exists(tit2->Ev)){
172  if (!rXTrans.Exists(tit1->X1,tit1->Ev,tit2->X2))
173  nextnewtrans.Insert(tit1->X1,tit1->Ev,tit2->X2);
174  }
175  }
176  }
177  }
178  // insert new transitions
179  rXTrans.InsertSet(nextnewtrans);
180  // update trans for next iteration.
181  newtrans = nextnewtrans;
182  }
183 }
184 
186  FD_DF("ObservationEquivalentQuotient(): prepare for t#"<<g.TransRelSize());
187 
188  // have extendend/reverse-ordered transition relations
189  TransSetX2EvX1 rtrans;
190  g.TransRel().ReSort(rtrans);
191 
192  Generator xg(g); // a copy of input g, which will be augmented with some fancy transitions
193  TransSet xtrans;
194  ExtendedTransRel(xg,silent,xtrans);
195  FD_DF("ObservationEquivalentQuotient(): ext. trans t#"<<xtrans.Size());
196 
197  // figure observation equivalent states
198  std::list< StateSet > eqclasses;
199  xg.InjectTransRel(xtrans);
200  // install silent selfloops
201  if (!silent.Empty()){
202  StateSet::Iterator sit = xg.StatesBegin();
203  for(;sit!=xg.StatesEnd();sit++){
204  EventSet::Iterator eit = silent.Begin();
205  xg.SetTransition(*sit,*eit,*sit);
206  }
207  }
208  ComputeBisimulationCTA(xg,eqclasses);
209 
210 
211  // merge classes
212  FD_DF("ObservationEquivalentQuotient(): merging classes #"<< eqclasses.size());
213  MergeEquivalenceClasses(g,rtrans,eqclasses,silent);
214 
215  FD_DF("ObservationEquivalentQuotient(): done with t#"<<g.TransRelSize());
216 }
217 
218 // perform quotient construction for reverse obsevation equivalence with active tau,
219 // see C. Pilbrow and R. Malik 2015. Current algorithm is perhaps suboptimal as it
220 // install a total new generator copy with all transitions reversed. Then the normal
221 // bisim-algorithm is performed, where eqclasses are refined to such that all states
222 // in a class has active tau event.
224  Generator rev_g; // have a copy to reverse all trans
225  rev_g.InsEvents(g.Alphabet());
226  rev_g.InsStates(g.States());
227 
228  // install reversed transition
230  TransSet::Iterator tit_end = g.TransRelEnd();
231  for(;tit!=tit_end;tit++){
232  rev_g.SetTransition(tit->X2,tit->Ev,tit->X1);
233  }
234 
235  // implement explicit "reverse_omega" for original initial states
236  Idx rev_omega = rev_g.InsEvent("_REV_OMEGA_");
237  Idx rev_dummy_omega = rev_g.InsEvent("_REV_DUMMY_OMEGA_");
238  Idx rev_terminal = rev_g.InsState("_REV_TERMINAL_");
239  rev_g.SetTransition(rev_terminal,rev_dummy_omega,rev_terminal);
240  StateSet::Iterator sit = g.InitStatesBegin();
241  StateSet::Iterator sit_end = g.InitStatesEnd();
242  for(;sit!=sit_end;sit++){
243  rev_g.SetTransition(*sit,rev_omega,rev_terminal);
244  }
245 
246  // figure out eqclasses, see e.g. ObservationEquivalentQuotient
247  TransSet xtrans;
248  ExtendedTransRel(rev_g,silent,xtrans);
249  rev_g.InjectTransRel(xtrans);
250  if (!silent.Empty()){
251  StateSet::Iterator sit2 = rev_g.StatesBegin();
252  StateSet::Iterator sit2_end = rev_g.StatesEnd();
253  for(;sit2!=sit2_end;sit2++){
254  rev_g.SetTransition(*sit2,*silent.Begin(),*sit2);
255  }
256  }
257  std::list<StateSet> eqclasses;
258  ComputeBisimulationCTA(rev_g,eqclasses);
259 
260  // refine eqclasses in that all states in a class has outgoing tau
261  std::list<StateSet> eqclasses_fine; // store result in new list, as some classes may be directly abandoned
262  std::list<StateSet>::iterator classit = eqclasses.begin();
263  std::list<StateSet>::iterator classit_end = eqclasses.end();
264  for (;classit!=classit_end;classit++){
265  StateSet newclass; // record refined class
266  StateSet::Iterator sit2 = classit->Begin();
267  StateSet::Iterator sit2_end = classit->End();
268  for(;sit2!=sit2_end;sit2++){
269  if (!(g.ActiveEventSet(*sit2) * silent).Empty()) newclass.Insert(*sit2);
270  }
271  if (newclass.Size()>=2) eqclasses_fine.push_back(newclass); // only store non-trivial classes
272  }
273 
274 
275  // merge refined eqclasses
276  TransSetX2EvX1 rtrans;
277  g.TransRel().ReSort(rtrans);
278  MergeEquivalenceClasses(g,rtrans,eqclasses_fine,silent);
279 
280 }
281 
282 // Performs weak observation equivalent abstraction;
283 // This is a re-imp of ObservationEquivalentQuotient in that we delete silent transitions
284 // after transition augmentation. FURHTERMORE, WE SHALL NOTICE that the resulting quotient
285 // is not built on input generator, but on the saturated generator with all tau deleted.
287  FD_DF("ObservationEquivalentQuotient(): prepare for t#"<<g.TransRelSize());
288 
289  // have extendend/reverse-ordered transition relations
290 
291  TransSet xtrans;
292  ExtendedTransRel(g,silent,xtrans);
293  FD_DF("ObservationEquivalentQuotient(): ext. trans t#"<<xtrans.Size());
294 
295  // remove silent events from extended transition relation
296  // yt: in weak observation equivalence, see e.g. Rong Su et al. (2010),
297  // only non-empty transitions are relevant
298  xtrans.RestrictEvents(g.Alphabet()-silent);
299 
300  // figure observation equivalent states
301  std::list< StateSet > eqclasses;
302  g.InjectTransRel(xtrans);
303  ComputeBisimulationCTA(g,eqclasses);
304  // merge classes
305  TransSetX2EvX1 rtrans;
306  g.TransRel().ReSort(rtrans);
307  FD_DF("ObservationEquivalentQuotient(): merging classes #"<< eqclasses.size());
308  MergeEquivalenceClasses(g,rtrans,eqclasses,silent); // here silent as input is dummy
309 
310  FD_DF("ObservationEquivalentQuotient(): done with t#"<<g.TransRelSize());
311 }
312 
313 // compute the incoming trans set of a state in a saturated
314 // and tau-removed generator. Instead of directly return a
315 // set of TransSet, a set of pair <Idx (source state), Idx (ev)>
316 // is returned for a better performance, hopefully. Moreover,
317 // for the sake of reachability from some intial state, a special pair
318 // <0,0> indicates that this state can be silently reached from some
319 // initial state.
321  const Generator& rGen,
322  const EventSet& silent,
323  const Idx& state,
324  std::set<std::pair<Idx, Idx>>& result){
325  result.clear(); // initialize result
326  TransSetX2EvX1 rtrans;
327  rGen.TransRel().ReSort(rtrans);
328  std::stack<Idx> todo; // states to process
329  std::set<Idx> visited; // states processed
330  todo.push(state);
331  visited.insert(state);
332 
333  while (!todo.empty()){
334  Idx cstate = todo.top();
335  todo.pop();
336 
337  // a "flag" indicating that this state can be silently reached by
338  // some initial state, see remark at the beginning
339  if (rGen.InitStates().Exists(cstate))
340  result.insert({0,0});
341  TransSetX2EvX1::Iterator rtit = rtrans.BeginByX2(cstate);
342  TransSetX2EvX1::Iterator rtit_end = rtrans.EndByX2(cstate);
343  for(;rtit!=rtit_end;rtit++){
344  if (!silent.Exists(rtit->Ev))
345  result.insert({rtit->X1,rtit->Ev});
346  else{
347  if (visited.find(rtit->X1) == visited.end()){
348  todo.push(rtit->X1);
349  visited.insert(rtit->X1);
350  }
351  }
352  }
353  }
354 }
355 
356 // compute the non-silent active events of a given generator.
357 // this algo is similar to IncomingTransSet, but we shall notice
358 // that IncomingTransSet record the source state as well but here not.
360  const Generator &rGen,
361  const EventSet &silent,
362  const Idx &state,
363  EventSet &result){
364  result.Clear(); // initialize result
365  std::stack<Idx> todo; // states to process
366  std::set<Idx> visited; // states processed (stack shall also work)
367  todo.push(state);
368  visited.insert(state);
369 
370  while (!todo.empty()){
371  Idx cstate = todo.top();
372  todo.pop();
373 
374  TransSet::Iterator rtit = rGen.TransRelBegin(cstate);
375  TransSet::Iterator rtit_end = rGen.TransRelEnd(cstate);
376  for(;rtit!=rtit_end;rtit++){
377  if (!silent.Exists(rtit->Ev))
378  result.Insert(rtit->Ev);
379  else{
380  if (visited.find(cstate) == visited.end()){
381  todo.push(rtit->X2);
382  visited.insert(rtit->X2);
383  }
384  }
385  }
386  }
387 }
388 
389 // Active events rule; see cited literature 3.2.1
390 // Note: this is a re-write of Michael Meyer's implementation to refer to the
391 // ext. transistion relation, as indicated by the literature.
392 // YT: Now it also partly supports Enabled Continuation Rule, see C. Pilbrow and R. Malik 2015
394  Generator& g,
395  const EventSet& silent){
396  // convenient typedef for incoming trans. This is for the incoming eq partition and,
397  // instead of directly set up std::set<TransSet>, we hope the set of pairs<Idx(source state), Idx(ev)>
398  // will perform better.
399  typedef std::set<std::pair<Idx,Idx>> TransSetX1Ev;
400 
401  // start the incoming equivalence partition
402  StateSet::Iterator sit = g.StatesBegin();
403  StateSet::Iterator sit_end = g.StatesEnd();
404 
405  // set up a map <incoming transset->class> to fast access incoming transset
406  // of existing classes. This map is only meant to check incoming equivalence.
407  std::map<TransSetX1Ev,StateSet> incomingeqclasses;
408  std::map<TransSetX1Ev,StateSet>::iterator mit;
409  for(;sit!=sit_end;sit++){
410  TransSetX1Ev rec_income;
411  IncomingTransSet(g,silent,*sit,rec_income);
412  mit = incomingeqclasses.find(rec_income);
413  if (mit != incomingeqclasses.end()){ // existing class found
414  mit->second.Insert(*sit);
415  }
416  else { // no class for this state found
417  StateSet newclass;
418  newclass.Insert(*sit);
419  incomingeqclasses.insert({rec_income,newclass});
420  }
421  }
422 
423  // Following the explanation in Chapter 4.2 of C. Pilbrow and R. Malik 2015,
424  // we first merge states via ActiveEventsRule. Then the incoming eq classes
425  // will be updated, then merge states via EnabledContinuationRule.
426  // And we avoid the the second time of ActiveEventsRule, which is acturally
427  // suggested in the aforementioned paper
428 
429  std::list<StateSet> eqclasses; // store result
430  TransSetX2EvX1 rtrans; // convenient declaration for MergeEqClasses
431 
432  // 1 - ActiveEventsRule
433  mit = incomingeqclasses.begin();
434  for (;mit!=incomingeqclasses.end();mit++){
435  StateSet fineclass; // refined class
436  StateSet::Iterator sit = mit->second.Begin();
437  fineclass.Insert(*sit);
438  EventSet activeevs;
439  ActiveNonTauEvs(g,silent,*sit,activeevs); // xg: exclude tau
440  StateSet::Iterator sit_compare = sit;
441  sit_compare++;
442  while(sit_compare!=mit->second.End()){
443  EventSet activeevs_compare;
444  ActiveNonTauEvs(g,silent,*sit,activeevs_compare);
445  if (activeevs_compare==activeevs){
446  fineclass.Insert(*sit_compare);
447  StateSet::Iterator todelete = sit_compare;
448  sit_compare++;
449  mit->second.Erase(todelete);
450  }
451  else sit_compare++;
452  }
453  if (fineclass.Size()>1) eqclasses.push_back(fineclass);
454  }
455  g.TransRel().ReSort(rtrans);
456  MergeEquivalenceClasses(g,rtrans,eqclasses,silent);
457 
458  // 2 - EnabledContinuationRule
459  eqclasses.clear();
460  rtrans.Clear();
461  mit = incomingeqclasses.begin();
462  for (;mit!=incomingeqclasses.end();mit++){
463  StateSet fineclass; // refined class
464  StateSet::Iterator sit = mit->second.Begin();
465  while(sit!=mit->second.End()){
466  if (!(g.ActiveEventSet(*sit) * silent).Empty()){ // g: has outgoing tau
467  fineclass.Insert(*sit);
468  // (this #if is actually unnecessary if we dont apply ActiveEventsRule again)
469  if (fineclass.Size()>1){ // fineclass is untrivial
470  StateSet::Iterator todelete = sit;
471  sit++;
472  mit->second.Erase(todelete);
473  }
474  else sit++;
475  }
476  else sit++;
477  }
478  if (fineclass.Size()>1) eqclasses.push_back(fineclass);
479  }
480  g.TransRel().ReSort(rtrans);
481  MergeEquivalenceClasses(g,rtrans,eqclasses,silent);
482 }
483 
484 
485 
486 // simple function removing tau self loops
489  TransSet::Iterator tit_end = g.TransRelEnd();
490  while(tit!=tit_end){
491  if (tit->X1 == tit->X2 && silent.Exists(tit->Ev)) g.ClrTransition(tit++);
492  else tit++;
493  }
494 }
495 
496 // as a special case of observation equivalence, states on a tau-loop are all equivalent
497 // and can be merged to a single state. This step is preferred to be done before
498 // (weak) observation equivalence, as they require transition saturation which is quite
499 // expensive.
501 
502  TransSetX2EvX1 rtrans;
503  g.TransRel().ReSort(rtrans);
504 
505  // have a generator copy where only silent transitions are preserved
506  Generator copyg(g);
507  TransSet::Iterator tit = copyg.TransRel().Begin();
508  while (tit!=copyg.TransRelEnd()){
509  if (!silent.Exists(tit->Ev)) // if not a silent trans, delete
510  copyg.ClrTransition(tit++);
511  else tit++;
512  }
513 
514  // compute eqclass and merge on original generator
515  std::list<StateSet> eqclasses;
516  StateSet dummy;
517  ComputeScc(copyg,eqclasses,dummy);
518 
519  // delete trivial eqclasses (yt: I dont want to hack into the computescc function)
520  std::list<StateSet>::iterator sccit = eqclasses.begin();
521  while (sccit!=eqclasses.end()){
522  if ((*sccit).Size()==1) eqclasses.erase(sccit++);
523  else sccit++;
524  }
525 
526  MergeEquivalenceClasses(g,rtrans,eqclasses,silent);
527 }
528 
529 // Certain conflicts. see cited literature 3.2.3
530 // -- remove outgoing transitions from not coaccessible states
532  StateSet notcoaccSet=g.States()-g.CoaccessibleSet();
533  StateSet::Iterator sit=notcoaccSet.Begin();
534  StateSet::Iterator sit_end=notcoaccSet.End();
535  for(;sit!=sit_end;++sit){
537  TransSetX1EvX2::Iterator tit_end=g.TransRelEnd(*sit);
538  for(;tit!=tit_end;) g.ClrTransition(tit++);
539  //FD_DF("RemoveCertainConflictA: remove outgoing from state "<<*sit);
540  }
541 }
542 
543 // Certain conflicts. see cited literature 3.2.3
544 // -- remove outgoing transitions from states that block by a silent event
546  FD_DF("BlockingSilentEvent(): prepare for t#"<<g.TransRelSize());
547  StateSet coacc=g.CoaccessibleSet();
548  StateSet sblock;
549  TransSet::Iterator tit;
550  TransSet::Iterator tit_end;
551  StateSet::Iterator sit;
552  StateSet::Iterator sit_end;
553  // loop all transitions to figure certain blocking states
554  tit=g.TransRelBegin();
555  tit_end=g.TransRelEnd();
556  for(;tit!=tit_end;++tit) {
557  if(silent.Exists(tit->Ev))
558  if(!coacc.Exists(tit->X2))
559  sblock.Insert(tit->X1);
560  }
561  // unmark blocking states and eliminate possible future
562  sit=sblock.Begin();
563  sit_end=sblock.End();
564  for(;sit!=sit_end;++sit) {
565  g.ClrMarkedState(*sit);
566  tit=g.TransRelBegin(*sit);
567  tit_end=g.TransRelEnd(*sit);
568  for(;tit!=tit_end;)
569  g.ClrTransition(tit++);
570  }
571  FD_DF("BlockingSilentEvent(): done with t#"<<g.TransRelSize());
572 }
573 
574 // Certain conflicts. see cited literature 3.2.3
575 // -- merge all states that block to one representative
577  StateSet notcoacc=g.States()-g.CoaccessibleSet();
578  // bail out on trovial case
579  if(notcoacc.Size()<2) return;
580  // have a new state
581  Idx qnc=g.InsState();
582  // fix init status
583  if((notcoacc * g.InitStates()).Size()>0)
584  g.SetInitState(qnc);
585  // fix transitions
587  TransSet::Iterator tit_end=g.TransRelEnd();
588  for(;tit!=tit_end;++tit){
589  if(notcoacc.Exists(tit->X2))
590  g.SetTransition(tit->X1,tit->Ev,qnc);
591  }
592  // delete original not coacc
593  g.DelStates(notcoacc);
594 }
595 
596 // Certain conflicts. see cited literature 3.2.3
597 // -- if a transition blocks, remove all transitions from the same state with the same label
599  FD_DF("BlockingEvent(): prepare for t#"<<g.TransRelSize());
600  StateSet coacc=g.CoaccessibleSet();
601  TransSet::Iterator tit;
602  TransSet::Iterator tit_end;
603  TransSet::Iterator dit;
604  TransSet::Iterator dit_end;
605  TransSet deltrans;
606  // loop all transitions to figure transitions to blocking states
607  tit=g.TransRelBegin();
608  tit_end=g.TransRelEnd();
609  for(;tit!=tit_end;++tit) {
610  // silent events are treated by a separat rule;
611  if(silent.Exists(tit->Ev)) continue;
612  // look for transitions that block
613  if(coacc.Exists(tit->X1)) continue;
614  if(coacc.Exists(tit->X2)) continue;
615  // consider all transitions with the same event to block
616  dit=g.TransRelBegin(tit->X1,tit->Ev);
617  dit_end=g.TransRelEnd(tit->X1,tit->Ev);
618  for(;dit!=dit_end;++dit) {
619  // keep selfloops (Michael Meyer)
620  if(dit->X1==dit->X2) continue;
621  // rcord to delete later
622  deltrans.Insert(*dit);
623  }
624  }
625  // delete transitions
626  dit=deltrans.Begin();
627  dit_end=deltrans.End();
628  for(;dit!=dit_end;++dit)
629  g.ClrTransition(*dit);
630  FD_DF("BlockingEvent(): done with t#"<<g.TransRelSize());
631 }
632 
633 // Only silent incomming rule; see cited literature 3.2.4
634 // Note: input generator must be silent-SCC-free
635 // Note: this is a complete re-re-write and needs testing for more than one candidates
637 
638  // figure states with only silent incomming transitions
639  // note: Michael Meyer proposed to only consider states with at least two incomming
640  // events -- this was dropped in the re-write
641  StateSet cand=g.States()-g.InitStates(); // note the initial state set is preserved
643  TransSet::Iterator tit_end = g.TransRelEnd();
644  for(;tit!=tit_end;++tit)
645  if(!silent.Exists(tit->Ev)) cand.Erase(tit->X2);
646 
647  // bail out on trivial
648  if(cand.Size()==0) {
649  return;
650  }
651 
652  StateSet::Iterator sit = cand.Begin();
653  StateSet::Iterator sit_end = cand.End();
654  while (sit!=sit_end){
655  TransSet::Iterator tit2 = g.TransRelBegin(*sit);
656  TransSet::Iterator tit2_end = g.TransRelEnd(*sit);
657  for (;tit2!=tit2_end;tit2++){
658  if (silent.Exists(tit2->Ev)){
659  break;
660  }
661  }
662 
663  if (tit2!=tit_end) { // there is at least one tau outgoing
664  // redirect transitions
665  TransSetX2EvX1 rtrans;
666  g.TransRel().ReSort(rtrans);
667  TransSetX2EvX1::Iterator rtit = rtrans.BeginByX2(*sit);
668  TransSetX2EvX1::Iterator rtit_end = rtrans.EndByX2(*sit);
669  for(;rtit!=rtit_end;rtit++){
670  TransSet::Iterator tit3 = g.TransRelBegin(*sit);
671  TransSet::Iterator tit3_end = g.TransRelEnd(*sit);
672  for (;tit3!=tit3_end;tit3++){
673  g.SetTransition(rtit->X1,tit3->Ev,tit3->X2);
674  }
675  }
676  StateSet::Iterator todelete = sit;
677  sit++;
678  g.DelState(*todelete);
679  }
680  else sit++;
681  }
682 
683  // yt: interestingly, according to the discussion with R. Malik,
684  // we do not need to assign the merge map information in this step -- this is counter-intuitive
685  // meaning that the deleted state has its merge map unchanged, but it will never be used because
686  // this state is "skipped" and thus can never be the final state of a counter example. Thus, it
687  // will not be utilized by line 12 of Algo 1, R. Malik and S. Ware 2018. Note we need the merge map
688  // only when executing line 12 of Algo 1.
689 
690 }
691 
692 
693 // Only silent outgoing rule; see cited literature 3.2.5
694 // Note: input generator must be silent-SCC-free
696  StateSet::Iterator sit = g.StatesBegin();
697  StateSet::Iterator sit_end = g.StatesEnd();
698  while(sit!=sit_end){
699  // figure out whether this state is only silent outgoing
700  if (g.MarkedStates().Exists(*sit)) {sit++;continue;}
701  TransSet::Iterator tit2 = g.TransRelBegin(*sit);
702  TransSet::Iterator tit2_end = g.TransRelEnd(*sit);
703  if (tit2==tit2_end) {sit++;continue;} // sit points to a deadend state (nonmarked state without outgoing trans)
704  for (;tit2!=tit2_end;tit2++){
705  if (!silent.Exists(tit2->Ev)) break;
706  }
707  if (tit2 != tit2_end) {sit++;continue;} // sit has non-silent outgoing trans
708 
709  // sit has passed the test. relink outgoing transitions of predecessor
710  TransSetX2EvX1 rtrans;
711  g.TransRel().ReSort(rtrans);
712  // (repair intial state quicker by first iterate outgoing trans)
713  tit2 = g.TransRelBegin(*sit);
714  tit2_end = g.TransRelEnd(*sit);
715  for (;tit2!=tit2_end;tit2++){
716  TransSetX2EvX1::Iterator rtit = rtrans.BeginByX2(*sit); // incoming trans to *sit
717  TransSetX2EvX1::Iterator rtit_end = rtrans.EndByX2(*sit);
718  for (;rtit!=rtit_end;rtit++){
719  g.SetTransition(rtit->X1,rtit->Ev,tit2->X2);
720  }
721  if (g.ExistsInitState(*sit))
722  g.SetInitState(tit2->X2);
723  }
724  StateSet::Iterator todelete = sit;
725  sit++;
726  g.DelState(*todelete);
727  }
728 }
729 
732  EventSet msilentevs=mGenRaw.Alphabet()*silent;
733  if(msilentevs.Empty()){
735  return;
736  }
737  Idx tau=*(msilentevs.Begin());
738  SetTau(tau);
739  SetSilentevs(msilentevs);
740  msilentevs.Erase(tau); // from now on, msilentevs exclude tau
741  silent.EraseSet(msilentevs);
742  if (msilentevs.Empty()){// in this case, only one 1 silent event is set to tau and no need to hide
744  return;
745  }
748  for(;tit!=tit_end;) {
749  if(!msilentevs.Exists(tit->Ev)) {++tit; continue;}
750  Transition t(tit->X1,tau,tit->X2);
751  mGenHidden.ClrTransition(tit++);
754  }
757 }
758 
760  // hide must be performed beforehand.
761  // we use tau itself as silent event set to
762  // access abstraction algorithms
763  HidePrivateEvs(silent);
764  EventSet tau;
765  if (mtau!=0)
766  tau.Insert(mtau);
767 
768  // current codes does not support counterexample computation for certain conflicts.
769  // Anyway, in R. Malik and S. Ware 2018, it shows no definitely postive result
770  // when considering certain conf in counter example computation due to the fact
771  // that we need to compute paralle product at each step of iteration. Furthermore,
772  // we would like to have counter example which goes into the blocking zone as
773  // far as possible, namely ends up at either a deadlocking state or a state in a livelock
774  // -- this also contradicts with certain conflicts conceptionally.
775 
776  // ***************** abstraction rules *******************
779  // OnlySilentIncoming(mGenMerged,tau);
780  // OnlySilentOutgoing(mGenMerged,tau);
783  // ReverseObservationEquivalentQuotient(mGenMerged,tau);
784 }
785 
786 
787 /*
788 ************************************
789 END: Candidate
790 ************************************
791 */
792 
793 
794 
795 
796 
797 void PrintEventTable(const pGenerator& rPGen){
798  EventSet::Iterator eit = rPGen.AlphabetBegin();
799  for(;eit!=rPGen.AlphabetEnd();eit++)
800  std::cout<<"EvName: "<<rPGen.EventName(*eit)<<"\t\t"<<"Index:"<<ToStringInteger(*eit)
801  <<"\t\t"<<"Priority: "<<ToStringInteger(rPGen.EventAttribute(*eit).Priority())<<std::endl;
802 }
803 
804 void PrintEqclasses(const std::list<StateSet>& rEqclasses){
805  std::list<StateSet>::const_iterator eqit = rEqclasses.begin();
806  for(;eqit!=rEqclasses.end();eqit++){
807  StateSet::Iterator sit = eqit->Begin();
808  std::cout<<"[";
809  for(;sit!=eqit->End();sit++){
810  std::cout<<ToStringInteger(*sit)+"\t";
811  }
812  std::cout<<"]"<<std::endl;
813  }
814 
815 }
816 
818  Idx omega = rPGen.InsEvent("_OMEGA_");
819  Idx omega_terminal = rPGen.InsEvent("_OMEGA_TERMINAL_");
820 
821  // Handle event prioriy
822  const Idx lowest = rPGen.LowestPriority() + 1; // YT-2025-04
823  rPGen.EventAttributep(omega)->Priority(lowest);
824  rPGen.EventAttributep(omega_terminal)->Priority(lowest);
825  rPrios.InsPriority("_OMEGA_",lowest);
826  rPrios.InsPriority("_OMEGA_TERMINAL_",lowest);
827  Idx terminal = rPGen.InsState("_TERMINAL_");
828  rPGen.SetTransition(terminal,omega_terminal,terminal);
829  StateSet::Iterator sit = rPGen.MarkedStatesBegin();
830  for(;sit!=rPGen.MarkedStatesEnd();sit++){
831  rPGen.SetTransition(*sit,omega,terminal);
832  }
833  rPGen.SetMarkedState(terminal); // cosmetic
834 
835  // handle fairness constraints
836  EventSet fairc;
837  fairc.Insert(omega);
838  fairc.Insert(omega_terminal);
839  FairnessConstraints fair;
840  fair.Append(fairc);
841  rPGen.GlobalAttributep()->Fairness(fair);
842 }
843 
844 
845 // convenient wrapper to show priority of each event
846 void WritePrio (const pGenerator& rPGen){
847  EventSet::Iterator eit = rPGen.AlphabetBegin();
848  for(;eit!=rPGen.AlphabetEnd();eit++){
849  std::cout<< rPGen.EventName(*eit) << "\t\t";
850  std::cout<<ToStringInteger(rPGen.EventAttribute(*eit).Priority())<<std::endl;
851  }
852 }
853 
854 // shaping priosities for specified preempting events (retains unreachable states)
855 void ShapeUpsilon(vGenerator& rGen, const EventPriorities& rPrios, const EventSet& rUpsilon){
856  Idx lowest = rPrios.LowestPriority();
857  StateSet::Iterator sit = rGen.StatesBegin();
858  for(;sit!=rGen.StatesEnd();sit++){
859  // figure gighest enabled priority
860  Idx highest = lowest;
861  TransSet::Iterator tit = rGen.TransRelBegin(*sit);
862  TransSet::Iterator tit_end = rGen.TransRelEnd(*sit);
863  for(;tit!=tit_end; ++tit){
864  Idx prio=rPrios.Priority(tit->Ev);
865  if(prio > highest)
866  if(rUpsilon.Exists(tit->Ev))
867  highest = prio;
868  }
869  // bail out if all enabled events are of lowest priority
870  if(highest == lowest) continue;
871  // remove preempted transitions
872  tit = rGen.TransRelBegin(*sit);
873  tit_end = rGen.TransRelEnd(*sit);
874  while(tit!=tit_end) {
875  if(rPrios.Priority(tit->Ev)<highest){
876  if(rPrios.SymbolicName(tit->Ev)=="_OMEGA_")
877  rGen.ClrMarkedState(tit->X1); // unmark if remove omega transition, cosmetic
878  rGen.ClrTransition(tit++);
879  } else {
880  ++tit;
881  }
882  }
883  }
884 }
885 
886 // API using pGenerator
887 void ShapeUpsilon(pGenerator& rPGen, const EventSet& rUpsilon){
888  const EventPriorities prios=rPGen.Priorities();
889  ShapeUpsilon(rPGen,prios,rUpsilon);
890 }
891 
892 // API ordinary shaping by priority, incl. removal of unreachable states
893 void ShapePriorities(vGenerator& rGen, const EventPriorities& rPrios){
894  ShapeUpsilon(rGen,rPrios,rGen.Alphabet());
895  rGen.Accessible();
896 }
897 
898 // API ordinary shaping by priority, incl. removal of unreachable states
900  const EventPriorities prios=rPGen.Priorities();
901  ShapeUpsilon(rPGen,prios,rPGen.Alphabet());
902  rPGen.Accessible();
903 }
904 
905 
906 
907 
908 // shape by set of preempting events only (TM2025: need this old version to compile/link example)
909 void ShapePreemption(Generator& rGen, const EventSet &pevs){
910  StateSet::Iterator sit = rGen.StatesBegin();
911  StateSet::Iterator sit_end = rGen.StatesEnd();
912  for(;sit!=sit_end; sit++){
913  if ((rGen.ActiveEventSet(*sit) * pevs).Empty()) continue; // not a preemptive state
914  TransSet::Iterator tit = rGen.TransRelBegin(*sit);
915  TransSet::Iterator tit_end = rGen.TransRelEnd(*sit);
916 
917  while(tit!=tit_end){
918  if (pevs.Exists(tit->Ev)) tit++;
919  else rGen.ClrTransition(tit++);
920  }
921  }
922  rGen.Accessible();
923  rGen.Name("S(" + rGen.Name() + ")");
924 }
925 
926 
927 // require WF!
928 void RemoveRedSilentSelfloops (pGenerator& rPGen, const EventSet& rSilent){
929  TransSet::Iterator tit=rPGen.TransRelBegin();
930  while(tit!=rPGen.TransRelEnd()){
931  if (tit->X1!=tit->X2) {tit++; continue;}
932  if (!rSilent.Exists(tit->Ev)) {tit++; continue;}
933  TransSet::Iterator tit2 = rPGen.TransRelBegin(tit->X1);
934  for(;tit2!=rPGen.TransRelEnd(tit->X1);tit2++){
935  if (rSilent.Exists(tit2->Ev) && tit2->X2 != tit->X1)
936  break;
937  }
938  if (tit2!=rPGen.TransRelEnd(tit->X1)){
939  rPGen.ClrTransition(tit++);
940  }
941  else tit++;
942  }
943 }
944 
945 // OLD NOTE: EXCLUDE unprioritised events, since this function evaluates the potential
946 // of a transition being preempted by NonsilHigherThen events.
948  const EventSet& rSilent,
949  const Idx& rState,
950  const Idx& rK){
951  EventSet result;
952  if(rK==rPGen.HighestPriority()) return result;
953  result = rPGen.ActiveEventSet(rState);
954  EventSet::Iterator eit = result.Begin();
955  while(eit!=result.End()){
956  if(!rSilent.Exists(*eit))
957  if(rPGen.Priority(*eit) > rK) {
958  eit++;
959  continue;
960  }
961  result.Erase(eit++);
962  }
963  return result;
964 }
965 
966 // find the silent event at given priority.
967 Idx SilentEvAtPrio(const pGenerator& rPGen, const EventSet& rSilent, const Idx& rK){
968  EventSet::Iterator eit = rPGen.AlphabetBegin();
969  for(;eit!=rPGen.AlphabetEnd();eit++){
970  if (!rSilent.Exists(*eit)) continue;
971  if (rPGen.Priority(*eit)==rK) return *eit;
972  }
973  throw Exception("SilentEvAtPrio()", "no such event found", 599);
974  return 0;
975 }
976 
978  pGenerator& rPGen,
979  const EventSet& rSilent,
980  const std::map< StateSet, Idx >& rLivelocks,
981  const std::list< StateSet >& rClasses)
982 {
983  FD_DF("MergeEquivalenceClasses()");
984  TransSetX2EvX1 rtrans;
985  rPGen.TransRel().ReSort(rtrans);
986  // iterators
987  StateSet::Iterator sit;
988  StateSet::Iterator sit_end;
990  TransSetX2EvX1::Iterator rtit_end;
991  TransSet::Iterator tit;
992  TransSet::Iterator tit_end;
993  // record for delayed delete
994  StateSet delstates;
995  // iterate classes
996  std::list< StateSet >::const_iterator qit=rClasses.begin();
997  for(;qit!=rClasses.end();++qit) {
998  sit=qit->Begin();
999  sit_end=qit->End();
1000  Idx q1=*(sit++); // this than denotes the name of quotient, i.e.[q1]
1001  for(;sit!=sit_end;++sit){
1002  Idx q2=*sit;
1003  // merge outgoing transitions form q2 to q1
1004  tit = rPGen.TransRelBegin(q2);
1005  tit_end = rPGen.TransRelEnd(q2);
1006  for(;tit!=tit_end;++tit) {
1007  // skip silent self-loop (handled later)
1008  if (qit->Exists(tit->X2)&&rSilent.Exists(tit->Ev))
1009  continue;
1010  rPGen.SetTransition(q1,tit->Ev,tit->X2);
1011  rtrans.Insert(q1,tit->Ev,tit->X2);
1012  }
1013  // merge incomming transitions form q2 to q1
1014  rtit = rtrans.BeginByX2(q2);
1015  rtit_end = rtrans.EndByX2(q2);
1016  for(;rtit!=rtit_end;++rtit) {
1017  // skip silent self-loop (handled later)
1018  if (qit->Exists(rtit->X1)&&rSilent.Exists(rtit->Ev))
1019  continue;
1020  rPGen.SetTransition(rtit->X1,rtit->Ev,q1);
1021  rtrans.Insert(rtit->X1,rtit->Ev,q1);
1022  }
1023  if(rPGen.ExistsMarkedState(q2))
1024  rPGen.InsMarkedState(q1);
1025  if((rPGen.ExistsInitState(q2)))
1026  rPGen.InsInitState(q1);
1027  delstates.Insert(q2);
1028  }
1029  // handle livelock selfloop
1030  std::map<StateSet,Idx>::const_iterator livelockit = rLivelocks.find(*qit);
1031  if(livelockit!=rLivelocks.end()){
1032  rPGen.SetTransition(*(qit->Begin()),livelockit->second,*(qit->Begin()));
1033  }
1034  }
1035  // do delete
1036  rPGen.DelStates(delstates);
1037 }
1038 
1039 
1040 // return a generator with silent transitions only (non silent are REMOVED, not hidden)
1041 // p -i-> q (i for prio) implies that there is a transition p => q on which the lowest priorit
1042 // (maximal value) is i.
1043 // NOTE: generates tau_0 self-loops.
1044 void SaturateLowestPrio(const pGenerator& rPGen, const EventSet& rSilent, pGenerator& rResult){
1045  FD_DF("SaturateLowestPrio()");
1046  rResult=rPGen;
1047  // only preserve silent transitions
1048  TransSet::Iterator tit = rResult.TransRelBegin();
1049  while (tit!=rResult.TransRelEnd()){
1050  if (!rSilent.Exists(tit->Ev)) // if not a silent trans, delete
1051  rResult.ClrTransition(tit++);
1052  else tit++;
1053  }
1054 
1055  if (rSilent.Empty()) return;
1056  // HELPERS:
1057  TransSet::Iterator tit1;
1058  TransSet::Iterator tit1_end;
1059  TransSet::Iterator tit2;
1060  TransSet::Iterator tit2_end;
1061 
1062  // initialize result with original transitionrelation
1063  TransSet xTrans=rResult.TransRel();
1064  TransSet newtrans = xTrans; // initialize iteration
1065  // loop for fixpoint
1066  while(!newtrans.Empty()) {
1067  // store new transitions for next iteration
1068  TransSet nextnewtrans;
1069  // loop over all transitions in newtrans
1070  tit1=newtrans.Begin();
1071  tit1_end=newtrans.End();
1072  for(;tit1!=tit1_end; ++tit1) {
1073  tit2=xTrans.Begin(tit1->X2);
1074  tit2_end=xTrans.End(tit1->X2);
1075  for(;tit2!=tit2_end; ++tit2) {
1076  // saturate the lower priority silent transition
1077  // copy first tit1's event
1078  if (rResult.Priority(tit1->Ev)<rResult.Priority(tit2->Ev)){
1079  if (!xTrans.Exists(tit1->X1,tit1->Ev,tit2->X2))
1080  nextnewtrans.Insert(tit1->X1,tit1->Ev,tit2->X2);
1081  }
1082  else{
1083  if (!xTrans.Exists(tit1->X1,tit2->Ev,tit2->X2))
1084  nextnewtrans.Insert(tit1->X1,tit2->Ev,tit2->X2);
1085  }
1086  }
1087  }
1088  // insert new transitions
1089  xTrans.InsertSet(nextnewtrans);
1090  // update trans for next iteration.
1091  newtrans = nextnewtrans;
1092  }
1093  rResult.InjectTransRel(xTrans);
1094 
1095  // install self loops of tau_inf on all states
1096  StateSet::Iterator sit = rPGen.StatesBegin();
1097  StateSet::Iterator sit_end = rPGen.StatesEnd();
1098  for(;sit!=sit_end;sit++){
1099  rResult.SetTransition(*sit,SilentEvAtPrio(rPGen,rSilent,rPGen.HighestPriority()),*sit);
1100  }
1101 }
1102 
1103 // saturate the transition (x)=epsilon=>->_Sig:k where
1104 // Sig is the set of active events of x if mode == 0, or
1105 // also include the successive =epsilon=>_0 part if mode==1
1106 void SaturatePDelayed(const pGenerator& rPGen,
1107  const EventSet& rSilent,
1108  const bool& _mode,
1109  pGenerator& rResult){
1110  rResult=rPGen;
1111 
1112  if (rSilent.Empty()) return;
1113  FD_DF("SaturatePDelayed()");
1114  // HELPERS:
1115  TransSet::Iterator tit1;
1116  TransSet::Iterator tit1_end;
1117  TransSet::Iterator tit2;
1118  TransSet::Iterator tit2_end;
1119 
1120  // initialize result with all self loops
1121  TransSet xTrans;
1122  StateSet::Iterator sit = rPGen.StatesBegin();
1123  Int kmin = rPGen.LowestPriority();
1124  Int kmax = rPGen.HighestPriority();
1125  for(;sit!=rPGen.StatesEnd();sit++){
1126  Int k;
1127  for(k=kmin;k<=kmax;k++){
1128  xTrans.Insert(*sit,SilentEvAtPrio(rPGen,rSilent,k),*sit);
1129  }
1130  }
1131  TransSet newtrans = xTrans; // initialize iteration
1132  // loop for fixpoint
1133  while(!newtrans.Empty()) {
1134  // store new transitions for next iteration
1135  TransSet nextnewtrans;
1136  // loop over all transitions in newtrans
1137  tit1=newtrans.Begin();
1138  tit1_end=newtrans.End();
1139  for(;tit1!=tit1_end; ++tit1) {
1140  if (_mode==0 && !rSilent.Exists(tit1->Ev)) continue; // in mode 0, do not saturate non-sil trans
1141  tit2=rPGen.TransRelBegin(tit1->X2);
1142  tit2_end=rPGen.TransRelEnd(tit1->X2);
1143  Idx tit1EvPrio = rPGen.Priority(tit1->Ev);
1144  for(;tit2!=tit2_end; ++tit2) {
1145  Idx tit2EvPrio = rPGen.Priority(tit2->Ev);
1146  // saturate the lower priority silent transition
1147  // copy first tit1's event
1148  if (rSilent.Exists(tit2->Ev)){ // if the next trans is silent
1149  if (rSilent.Exists(tit1->Ev)){ // both tit1's ev and tit2's are silent
1150  // to saturate, if must be at priority not lower than tit1's ev, and the
1151  // active ev inclusion must hold
1152  if (tit2EvPrio >= tit1EvPrio
1153  && NonsilHigherThen(rPGen,rSilent,tit2->X1,tit1EvPrio)<=NonsilHigherThen(rPGen,rSilent,tit1->X1,tit1EvPrio)){
1154  if (!xTrans.Exists(tit1->X1,tit1->Ev,tit2->X2))
1155  nextnewtrans.Insert(tit1->X1,tit1->Ev,tit2->X2);
1156  }
1157  }
1158  else if (_mode==1){ // tit1 not silent, then only saturate in mode1
1159  if (tit2EvPrio == 0){
1160  if (!xTrans.Exists(tit1->X1,tit1->Ev,tit2->X2))
1161  nextnewtrans.Insert(tit1->X1,tit1->Ev,tit2->X2);
1162  }
1163  }
1164  }
1165  else{ // the next transition is not silent
1166  // we also need to check that tit1 is silent
1167  if (rSilent.Exists(tit1->Ev)
1168  && tit2EvPrio <= tit1EvPrio
1169  && NonsilHigherThen(rPGen,rSilent,tit2->X1,tit1EvPrio)<=NonsilHigherThen(rPGen,rSilent,tit1->X1,tit1EvPrio)){
1170  if (!xTrans.Exists(tit1->X1,tit2->Ev,tit2->X2)){
1171  if (_mode==0)
1172  xTrans.Insert(tit1->X1,tit2->Ev,tit2->X2); // no need to iterate again in mode 0
1173  else
1174  nextnewtrans.Insert(tit1->X1,tit2->Ev,tit2->X2);
1175  }
1176  }
1177  }
1178  }
1179  }
1180  // insert new transitions
1181  xTrans.InsertSet(nextnewtrans);
1182  // update trans for next iteration (saturation front)
1183  newtrans = nextnewtrans;
1184  }
1185  rResult.InjectTransRel(xTrans);
1186 }
1187 
1188 
1189 // detect livelocks and store in rResult. rResult is a map of livelock->the SILENT EV whose priority describes the livelo
1190 // NOTE: WELL-FORMEDNESS REQUIRED!
1191 void DetectLiveLocks(const pGenerator &rPGen, const EventSet &rSilent, std::map<StateSet, Idx>& rResult){
1192  FD_DF("DetectLiveLocks()");
1193  rResult.clear();
1194 
1195  // have a generator copy where only silent transitions are preserved
1196  pGenerator copyg(rPGen);
1197  TransSet::Iterator tit = copyg.TransRel().Begin();
1198  while (tit!=copyg.TransRelEnd()){
1199  if (!rSilent.Exists(tit->Ev)) // if not a silent trans, delete
1200  copyg.ClrTransition(tit++);
1201  else tit++;
1202  }
1203 
1204  // compute eqclass and merge on original generator
1205  std::list<StateSet> eqclasses;
1206  StateSet dummy;
1207  ComputeScc(copyg,eqclasses,dummy);
1208 
1209  // delete spurious SCCs which are: trivial but non-selflooping, loop but with silent exit
1210  // note: well-formedness required
1211  std::list<StateSet>::const_iterator sccit = eqclasses.begin();
1212  for (;sccit!=eqclasses.end();sccit++){
1213  if ((*sccit).Size()==1){
1214  EventSet activesil = rPGen.ActiveEventSet(*sccit->Begin()) * rSilent;
1215  if (!activesil.Empty()) {
1216  TransSet::Iterator tit = rPGen.TransRelBegin(*sccit->Begin(),*activesil.Begin());
1217  for (;tit!=rPGen.TransRelEnd(*sccit->Begin(),*activesil.Begin());tit++){
1218  if (tit->X2!=tit->X1){ // there is a silent exit (regardless the existence of a sil selfloop)
1219  break;
1220  }
1221  }
1222  if (tit==rPGen.TransRelEnd(*sccit->Begin(),*activesil.Begin())){ // break was not executed
1223  rResult[*sccit] = *activesil.Begin();
1224  }
1225  }
1226  }
1227  else{ // a SCC with at least two states
1228  StateSet::Iterator sit = sccit->Begin();
1229  Idx livelockprio = rPGen.HighestPriority(); // initialise livelock lowest priority
1230  bool skip = false; // set to true if *sccit is not a livelock
1231  for(;sit!=sccit->End();sit++){
1232  EventSet activesil = rPGen.ActiveEventSet(*sit) * rSilent;
1233  if (!activesil.Empty()) {
1234  TransSet::Iterator tit = rPGen.TransRelBegin(*sit,*activesil.Begin());
1235  for (;tit!=rPGen.TransRelEnd(*sit,*activesil.Begin());tit++){
1236  if (!(*sccit).Exists(tit->X2)){ // there is a silent exit
1237  skip = true;
1238  break;
1239  }
1240  }
1241  if (skip) break;
1242  Idx newprio = rPGen.Priority(*activesil.Begin());
1243  if (newprio<livelockprio) livelockprio = newprio;
1244  }
1245  }
1246  if (!skip){
1247  rResult[*sccit] = SilentEvAtPrio(rPGen,rSilent,livelockprio);
1248  }
1249  }
1250  }
1251 }
1252 
1253 
1254 // typedef of incoming transitions. The 3 elements in the tuple are referred to as:
1255 // 0: from which state (=0 as "any initial state")
1256 // 1: via which (non-silent) event (=0 as "silently from any initial state")
1257 // 2: all silent prio events, each of which is denotes a hookarrow transition
1258 typedef std::map<std::pair<Idx, Idx>, EventSet> IncTransSet;
1259 
1260 // compute the incoming non-tau trans set of a state in a saturated
1261 // and tau-removed generator. Instead of directly return a
1262 // set of TransSet, a set of pair <Idx (source state), Idx (ev)>
1263 // is returned for a better performance, hopefully. Moreover,
1264 // for the sake of reachability from some intial state, a special pair
1265 // <0,0> indicates that this state can be silently reached from some
1266 // initial state.
1267 // ******input arguments:
1268 // rClosureFull: a result from SaturatePDelay with mode = 0, i.e. closure of =>->_Sig:k
1269 // rClosureLowest: a restricted result of SaturateLowestPrio
1270 // ******return bool: false if some silent pred has higher prio non-sil ev
1272  const pGenerator& rPGen,
1273  const pGenerator& rClosureFull,
1274  const pGenerator& rClosureLowest,
1275  const TransSetX2EvX1& rtrans_full,
1276  const TransSetX2EvX1& rtrans_lowest,
1277  const EventSet& rSilent,
1278  const Idx& rState,
1279  IncTransSet& rResult){
1280  FD_DF("IncommingTransSet()");
1281  TransSetX2EvX1 trans_lowest = rtrans_lowest;
1282  rResult.clear();
1283  // 1. test if there are silent pred with higher prio non-sil ev
1284  // if a silent pred can execute tau, then (due to wf) this tau must reach
1285  // rState.
1286  TransSetX2EvX1::Iterator rtit = rtrans_full.BeginByX2(rState);
1287  for(;rtit!=rtrans_full.EndByX2(rState);rtit++){
1288  if (!rSilent.Exists(rtit->Ev)) continue;
1289  EventSet activesil = rPGen.ActiveEventSet(rtit->X1) * rSilent;
1290  if (activesil.Empty()) continue;
1291  Idx k = rPGen.Priority(*activesil.Begin());
1292  if (!NonsilHigherThen(rPGen,rSilent,rtit->X1,k).Empty()) return false; // abort if test fails
1293  }
1294  // 2. test passed. compute incoming transset
1295  TransSetX2EvX1::Iterator rtit_lowest = trans_lowest.BeginByX2(rState);
1296  for (;rtit_lowest!=trans_lowest.EndByX2(rState);rtit_lowest++){
1297  EventSet ks;
1298  ks.Insert(rtit_lowest->Ev);
1299  // collect all possible hookarrows to rtit->X2
1300  TransSet::Iterator tit = rClosureLowest.TransRelBegin(rtit_lowest->X1);
1301  for(;tit!=rClosureLowest.TransRelEnd(rtit_lowest->X1);tit++){
1302  if (tit->X2 != rtit_lowest->X2
1303  || tit->Ev == rtit_lowest->Ev) continue; // skip self or wrong successor
1304  ks.Insert(tit->Ev);
1305  trans_lowest.Erase(*tit); // this cannot be the same as rtit, so OK
1306  }
1307  // find all non-sil predeccessors (or check if is initial state)
1308  if (rClosureFull.InitStates().Exists(rtit_lowest->X1)){
1309  std::pair<Idx,Idx> cstate = std::make_pair(0,0);
1310  IncTransSet::iterator visited = rResult.find(cstate);
1311  if(visited == rResult.end()){
1312  rResult[cstate] = ks;
1313  }
1314  else{
1315  rResult[cstate].InsertSet(ks);
1316  }
1317  }
1318  TransSetX2EvX1::Iterator rtit_original = rtrans_full.BeginByX2(rtit_lowest->X1);
1319  for(;rtit_original != rtrans_full.EndByX2(rtit_lowest->X1);rtit_original++){
1320  if (rSilent.Exists(rtit_original->Ev)) continue; // skip silent event
1321  std::pair<Idx,Idx> cstate = std::make_pair(rtit_original->X1,rtit_original->Ev);
1322  IncTransSet::iterator visited = rResult.find(cstate);
1323  if(visited == rResult.end()){
1324  rResult[cstate] = ks;
1325  }
1326  else{
1327  rResult[cstate].InsertSet(ks);
1328  }
1329  }
1330  }
1331  return true; // TM2025
1332 }
1333 
1334 // return eq classes of =_inc. Instead of returning list of state sets,
1335 // this function retunrs a map where the keys are the (source state, (non-tau)event) - pairs
1336 // and the value of each key is the corresponding eq class. Effectively, the keys are just
1337 // for efficient internal search of existing classes and will not be utilised in any other
1338 // functions which requies incoming eq (they will only need the values)
1339 void IncomingEquivalentClasses(const pGenerator& rPGen, const EventSet& rSilent, std::list<StateSet>& rResult){
1340  FD_DF("IncommingEquivalent()");
1341  // Preparation: saturate closureFull and closureLowest (necessary for incomingtransset)
1342  pGenerator closurefull;
1343  SaturatePDelayed(rPGen,rSilent,0,closurefull); // do not saturate the successive 0 part
1344  pGenerator closurelowest;
1345  // since hookarrow does not want the silent transitions to have active higher priority events
1346  pGenerator rPGen_shaped(rPGen);
1347  ShapePriorities(rPGen_shaped);
1348  SaturateLowestPrio(rPGen_shaped,rSilent,closurelowest);
1349 
1350  TransSetX2EvX1 trans_lowest; // buffer the rev trans of closurelowest
1351  closurelowest.TransRel().ReSort(trans_lowest);
1352  TransSetX2EvX1 trans_full; // buffer the rev trans of original gen
1353  closurefull.TransRel().ReSort(trans_full);
1354 
1355  // start the incoming equivalence partition
1356  StateSet::Iterator sit = rPGen.StatesBegin();
1357  StateSet::Iterator sit_end = rPGen.StatesEnd();
1358  // set up a map <incoming transset->class> to fast access incoming transset
1359  // of existing classes. This map is only meant to check incoming equivalence.
1360  std::map<IncTransSet,StateSet> incomingeqclasses;
1361  std::map<IncTransSet,StateSet>::iterator mit;
1362  for(;sit!=sit_end;sit++){
1363  IncTransSet rec_income;
1364  bool ok = IncomingTransSet(rPGen,closurefull,closurelowest,trans_full,trans_lowest,rSilent,*sit,rec_income);
1365  if (!ok) continue;
1366  if (rec_income.empty()) continue; // this should be redundant, as covered by "ok" above
1367  mit = incomingeqclasses.find(rec_income);
1368  if (mit != incomingeqclasses.end()){ // existing class found
1369  mit->second.Insert(*sit);
1370  }
1371  else { // no class for this state found
1372  StateSet newclass;
1373  newclass.Insert(*sit);
1374  incomingeqclasses[rec_income] = newclass;
1375  }
1376  }
1377 
1378  // return non-trivial classes
1379  rResult.clear();
1380  mit = incomingeqclasses.begin();
1381  for(;mit!=incomingeqclasses.end();mit++){
1382  if (mit->second.Size()>1) rResult.push_back(mit->second);
1383  }
1384 }
1385 
1386 // partition according to active events rule (AE) or silent continuation rule (SC)
1387 void AESCClasses(const pGenerator& rPGen, const EventSet& rSilent, std::list<StateSet>& rResult){
1388  FD_DF("AESCClasses()");
1389  rResult.clear();
1390  std::map<StateSet, Idx> livelocks; // only need keys, values are livelock prios which are irrelevant
1391  DetectLiveLocks(rPGen,rSilent,livelocks);
1392  //
1393  std::list<StateSet> inceq;
1394  IncomingEquivalentClasses(rPGen,rSilent,inceq); //prepartition inceq into result. then refine
1395  std::list<StateSet>::const_iterator inceqit = inceq.begin();
1396  // refine each inceq class
1397  for(;inceqit!=inceq.end();inceqit++){
1398  // never equalise states in livelocks
1399  std::map<StateSet,Idx>::const_iterator livelocksit = livelocks.begin();
1400  for(;livelocksit!=livelocks.end();livelocksit++){
1401  if (!(livelocksit->first * (*inceqit)).Empty())
1402  break;
1403  }
1404  if (livelocksit!=livelocks.end())
1405  continue;
1406  StateSet todo = *inceqit;
1407  // refine this eq class
1408  while (!todo.Empty()){
1409  Idx cstate = *todo.Begin();
1410  todo.Erase(todo.Begin());
1411  StateSet newclass;
1412  newclass.Insert(cstate);
1413  EventSet activesil = rPGen.ActiveEventSet(cstate)*rSilent;
1414  if (activesil.Empty()){ // no active silent evs. try AE
1415  StateSet::Iterator sit = todo.Begin();
1416  while(sit!=todo.End()){
1417  if (rPGen.ActiveEventSet(*sit) == rPGen.ActiveEventSet(cstate)){
1418  newclass.Insert(*sit);
1419  todo.Erase(sit++);
1420  }
1421  else
1422  sit++;
1423  }
1424  }
1425  else{ // then try SC
1426  StateSet::Iterator sit = todo.Begin();
1427  while(sit!=todo.End()){
1428  Idx tauprio = rPGen.Priority(*activesil.Begin());
1429  if ((rPGen.ActiveEventSet(*sit)*rSilent) == activesil // same active silent event
1430  &&
1431  NonsilHigherThen(rPGen,rSilent,*sit,tauprio).Size()+ NonsilHigherThen(rPGen,rSilent,cstate,tauprio).Size()==0){
1432  newclass.Insert(*sit);
1433  todo.Erase(sit++);
1434  }
1435  else
1436  sit++;
1437  }
1438  }
1439  if (newclass.Size()>1) rResult.push_back(newclass);
1440  }
1441  }
1442 }
1443 
1444 void MergeAESC(pGenerator& rPGen, const EventSet& rSilent){
1445  std::map<StateSet, Idx> livelocks;
1446  DetectLiveLocks(rPGen,rSilent,livelocks);
1447  std::list<StateSet> eqclasses;
1448  AESCClasses(rPGen, rSilent, eqclasses);
1449  MergeEquivalenceClasses(rPGen,rSilent,livelocks,eqclasses);
1450 }
1451 
1452 // saturate pwb by connecting =>_<k (with target state not having tau<k) and =>_Sig:k closure
1453 void SaturatePWB(const pGenerator& rPGen,
1454  const EventSet& rSilent,
1455  pGenerator& rResult){
1456  FD_DF("SaturatePWB()");
1457  rResult = rPGen;
1458  pGenerator closurelowest;
1459  SaturateLowestPrio(rPGen,rSilent,closurelowest);
1460  pGenerator closurefull;
1461  SaturatePDelayed(rPGen,rSilent, 1,closurefull);
1462  // figure out the highest possible k for =>_<k (with target not tau<k) transitions for each two states
1463  TransSet resulttrans; // put saturated trans here. Inject to rResult eventually
1464  StateSet::Iterator sit = closurelowest.StatesBegin();
1465  for(;sit!=closurelowest.StatesEnd();sit++){
1466  StateSet visitedtarget; // buffer a set of visited target states of transitions from sit
1467  TransSet::Iterator tit_lowest = closurelowest.TransRelBegin(*sit);
1468  for(;tit_lowest!=closurelowest.TransRelEnd(*sit);tit_lowest++){
1469  if (visitedtarget.Exists(tit_lowest->X2))
1470  continue;
1471  visitedtarget.Insert(tit_lowest->X2);
1472  // find the highest lowest priority to tit->X2 (X2 not >k not treated yet)
1473  Idx highest = rPGen.Priority(tit_lowest->Ev);
1474  if(highest<rPGen.HighestPriority()){
1475  TransSet::Iterator tit2_lowest = closurelowest.TransRelBegin(*sit);
1476  for(;tit2_lowest!=closurelowest.TransRelEnd(*sit);tit2_lowest++){
1477  if (tit2_lowest->X2 != tit_lowest->X2) continue;
1478  Idx newprio = rPGen.Priority(tit2_lowest->Ev);
1479  if (newprio > highest) highest = newprio;
1480  if (highest==rPGen.HighestPriority()) break;
1481  }
1482  }
1483  // now check if X2 cannot >k, if k<maxprio
1484  // in the following, highest's meaning is changed to "the highest k tit allows for successive transitions"
1485  bool ismax = (highest==rPGen.HighestPriority()); // highest = max is a special case
1486  // (does not need ++ to allow successive maxprio trans)
1487  highest--; // for highest \neq maxprio, the highest allowed prioity is actually highest--
1488  Idx lowest = rPGen.LowestPriority(); // allowed lowest priority, changed if some tau is active on X2
1489  EventSet activesil = rPGen.ActiveEventSet(tit_lowest->X2) * rSilent;
1490  if (!activesil.Empty()){
1491  Idx k_activesil = rPGen.Priority(*activesil.Begin());
1492  lowest = k_activesil;
1493  // bail out when transition extension is already impossible
1494  if (!ismax && lowest > highest) continue;
1495  }
1496  // now we have the lowest k allowed. Check for possible trans extension from closurefull
1497  TransSet::Iterator tit_full = closurefull.TransRelBegin(tit_lowest->X2); // sit is tit->X1
1498  for(;tit_full!=closurefull.TransRelEnd(tit_lowest->X2);++tit_full){
1499  Idx k_succ = rPGen.Priority(tit_full->Ev);
1500  if ((k_succ >= lowest && k_succ <= highest)
1501  || (ismax && k_succ==rPGen.HighestPriority())){ // its OK!
1502  resulttrans.Insert(*sit,tit_full->Ev,tit_full->X2);
1503  }
1504  }
1505  }
1506  }
1507  rResult.InjectTransRel(resulttrans);
1508 }
1509 
1510 void MergePWB(pGenerator& rPGen, const EventSet& rSilent){
1511  std::map<StateSet, Idx> livelocks;
1512  DetectLiveLocks(rPGen,rSilent,livelocks);
1513  pGenerator pwbclosure;
1514  SaturatePWB(rPGen,rSilent,pwbclosure);
1515  std::list<StateSet> eqclasses;
1516  ComputeBisimulation(pwbclosure,eqclasses);
1517  MergeEquivalenceClasses(rPGen,rSilent,livelocks,eqclasses);
1518 }
1519 
1520 
1521 void RedundantSilentStep(pGenerator& rPGen, const EventSet& rSilent){
1522  FD_DF("RedundantSilentStep()");
1523  TransSetX2EvX1 rtrans;
1524  rPGen.TransRel().ReSort(rtrans);
1525  StateSet::Iterator sit = rPGen.StatesBegin();
1526  while(sit!=rPGen.StatesEnd()){
1527  if ((rPGen.InitStates() + rPGen.MarkedStates()).Exists(*sit)) {sit++;continue;}
1528  TransSet::Iterator tit = rPGen.TransRelBegin(*sit);
1529  Idx count = 0;
1530  for(;tit!=rPGen.TransRelEnd(*sit);tit++){
1531  count++;
1532  }
1533  if (count!=1) {sit++;continue;} // only have one outgoing trans
1534  tit = rPGen.TransRelBegin(*sit);
1535  if (!rSilent.Exists(tit->Ev)) {sit++;continue;} // and this trans must be silent
1536  // are all incoming trans silent with no higher priority?
1537  Idx k = rPGen.Priority(tit->Ev);
1538  TransSetX2EvX1::Iterator rtit = rtrans.BeginByX2(*sit);
1539  for(;rtit!=rtrans.EndByX2(*sit);rtit++){
1540  if (!rSilent.Exists(rtit->Ev)) break;
1541  if (rPGen.Priority(rtit->Ev)>=k) break;
1542  }
1543  if (rtit!=rtrans.EndByX2(*sit)) {sit++;continue;}
1544  // sit qualified. Remove and redirect transition
1545  rtit=rtrans.BeginByX2(*sit);
1546  for(;rtit!=rtrans.EndByX2(*sit);rtit++){
1547  rPGen.SetTransition(rtit->X1,rtit->Ev,tit->X2);
1548  }
1549  StateSet::Iterator todelete = sit++;
1550  rPGen.DelState(*todelete);
1551  // update rtrans
1552  rtrans.Clear();
1553  rPGen.TransRel().ReSort(rtrans);
1554  }
1555 }
1556 
1557 // input automaton should be redundant silent loop free
1558 void OnlySilentIncoming(pGenerator& rPGen, const EventSet& rSilent, const StateSet& rLivelocks){
1559  FD_DF("OnlySilentIncomming()");
1560  // figure states with only silent incomming transitions
1561  TransSetX2EvX1 rtrans;
1562  rPGen.TransRel().ReSort(rtrans);
1563  // pre-filter uncapable states
1564  StateSet cand=rPGen.States()-rPGen.InitStates()-rLivelocks; // lasily exclude initial states
1565  TransSet::Iterator tit = rPGen.TransRelBegin();
1566  TransSet::Iterator tit_end = rPGen.TransRelEnd();
1567  for(;tit!=tit_end;++tit){
1568  if(!rSilent.Exists(tit->Ev)
1569  || rPGen.Priority(tit->Ev)!=rPGen.HighestPriority()) cand.Erase(tit->X2);
1570  }
1571  // bail out on trivial
1572  if(cand.Size()==0) return;
1573 
1574  StateSet::Iterator sit = cand.Begin();
1575  StateSet::Iterator sit_end = cand.End();
1576  while (sit!=sit_end){
1577  TransSet::Iterator tit2 = rPGen.TransRelBegin(*sit);
1578  TransSet::Iterator tit2_end = rPGen.TransRelEnd(*sit);
1579  for (;tit2!=tit2_end;tit2++){
1580  if (rSilent.Exists(tit2->Ev)&&rPGen.Priority(tit2->Ev)==rPGen.HighestPriority()){
1581  break;
1582  }
1583  }
1584  if (tit2!=tit2_end) { // there is at least one tau_max outgoing
1585  // redirect transitions
1586  TransSetX2EvX1::Iterator rtit = rtrans.BeginByX2(*sit);
1587  TransSetX2EvX1::Iterator rtit_end = rtrans.EndByX2(*sit);
1588  for(;rtit!=rtit_end;rtit++){
1589  TransSet::Iterator tit3 = rPGen.TransRelBegin(*sit);
1590  TransSet::Iterator tit3_end = rPGen.TransRelEnd(*sit);
1591  for (;tit3!=tit3_end;tit3++){
1592  if (rtit->X1 == tit3->X2 && rSilent.Exists(tit3->Ev)) continue; // avoid generating silent self loop
1593  rPGen.SetTransition(rtit->X1,tit3->Ev,tit3->X2);
1594  }
1595  // if the state to delete is marked, then pred-state should be marked as well
1596  if (rPGen.ExistsMarkedState(*sit))
1597  rPGen.SetMarkedState(rtit->X1);
1598  }
1599  StateSet::Iterator todelete = sit++;
1600  rPGen.DelState(*todelete);
1601  }
1602  else sit++;
1603 
1604  // update rtrans
1605  rtrans.Clear();
1606  rPGen.TransRel().ReSort(rtrans);
1607  }
1608 }
1609 
1610 void OnlySilentOutgoing(pGenerator& rPGen, const EventSet& rSilent, const StateSet& rLivelocks){
1611  FD_DF("OnlySilentOutgoing()");
1612  TransSetX2EvX1 rtrans;
1613  rPGen.TransRel().ReSort(rtrans);
1614  StateSet::Iterator sit = rPGen.StatesBegin();
1615  StateSet::Iterator sit_end = rPGen.StatesEnd();
1616  while(sit!=sit_end){
1617  // figure out whether this state is only silent outgoing
1618  if ((rPGen.MarkedStates()+rLivelocks).Exists(*sit)) {sit++;continue;}
1619  TransSet::Iterator tit2 = rPGen.TransRelBegin(*sit);
1620  TransSet::Iterator tit2_end = rPGen.TransRelEnd(*sit);
1621  if (tit2==tit2_end) {sit++;continue;} // sit points to a deadend state (nonmarked state without outgoing trans)
1622  for (;tit2!=tit2_end;tit2++){
1623  if (!rSilent.Exists(tit2->Ev)) break;// sit has non-silent outgoing trans
1624  if (rPGen.Priority(tit2->Ev)!=rPGen.HighestPriority()) break; // must be with prio = max
1625  }
1626  if (tit2 != tit2_end) {sit++;continue;}
1627 
1628  // sit has passed the test. relink outgoing transitions of predecessor
1629  // (repair initial state quicker by first iterate outgoing trans)
1630  tit2 = rPGen.TransRelBegin(*sit);
1631  tit2_end = rPGen.TransRelEnd(*sit);
1632  for (;tit2!=tit2_end;tit2++){
1633  TransSetX2EvX1::Iterator rtit = rtrans.BeginByX2(*sit); // incoming trans to *sit
1634  TransSetX2EvX1::Iterator rtit_end = rtrans.EndByX2(*sit);
1635  for (;rtit!=rtit_end;rtit++){
1636  if (rtit->X1 == tit2->X2 && rSilent.Exists( rtit->Ev)) continue; // avoid generating silent self loop
1637  rPGen.SetTransition(rtit->X1,rtit->Ev,tit2->X2);
1638  }
1639  if (rPGen.ExistsInitState(*sit))
1640  rPGen.SetInitState(tit2->X2);
1641  }
1642  StateSet::Iterator todelete = sit++;
1643  rPGen.DelState(*todelete);
1644 
1645  // update rtrans
1646  rtrans.Clear();
1647  rPGen.TransRel().ReSort(rtrans);
1648  }
1649 }
1650 
1651 // return the set of set of strongly coacc states depending on
1652 // the fairness constraints.
1653 // NOTE: this shall be considered as a member function of pGenerator,
1654 // to reimplement
1656  FD_DF("StronglyCoaccessibleSet()");
1657  Generator copy = rPGen;
1658  copy.Accessible();
1659  StateSet result = copy.States();
1661  for(;fpos<rPGen.GlobalAttribute().Fairness().Size();++fpos) {
1662  const EventSet& fair = rPGen.GlobalAttribute().Fairness().At(fpos);
1663  copy.ClearMarkedStates();
1664  StateSet::Iterator sit = copy.StatesBegin();
1665  for(;sit!=copy.StatesEnd();sit++){
1666  // if a state can execute a fair event, it's "marked" for this fairness constraint
1667  if(!(copy.ActiveEventSet(*sit) * fair).Empty()){
1668  copy.SetMarkedState(*sit);
1669  }
1670  }
1671  result = result * copy.CoaccessibleSet(); //this is the ordinary function for marked states
1672  }
1673  return result;
1674 }
1675 
1676 // Certain conflicts. see cited literature 3.2.3
1677 // -- remove outgoing transitions from not coaccessible states
1679  FD_DF("RemoveNonCoaccessible()");
1680  StateSet notcoacc=rPGen.States()-StronglyCoaccessibleSet(rPGen);
1681  StateSet::Iterator sit=notcoacc.Begin();
1682  StateSet::Iterator sit_end=notcoacc.End();
1683  for(;sit!=sit_end;++sit){
1684  TransSet::Iterator tit=rPGen.TransRelBegin(*sit);
1685  TransSet::Iterator tit_end=rPGen.TransRelEnd(*sit);
1686  while(tit!=tit_end)
1687  rPGen.ClrTransition(tit++);
1688  }
1689  rPGen.Accessible();
1690 }
1691 
1692 // Certain conflicts. see cited literature 3.2.3
1693 // -- remove outgoing transitions from states that block by a silent event
1694 void BlockingSilentEvent(pGenerator& rPGen,const EventSet& rSilent){
1695  FD_DF("BlockingSilentEvent(): prepare for t#"<<rPGen.TransRelSize());
1696  StateSet coacc=StronglyCoaccessibleSet(rPGen);
1697  StateSet sblock; // states with outgoing silent event with highest active priority and leads to block
1698  TransSet::Iterator tit;
1699  TransSet::Iterator tit_end;
1700  StateSet::Iterator sit;
1701  StateSet::Iterator sit_end;
1702  // loop all transitions to figure certain blocking states
1703  tit=rPGen.TransRelBegin();
1704  tit_end=rPGen.TransRelEnd();
1705  for(;tit!=tit_end;++tit) {
1706  if(rSilent.Exists(tit->Ev))
1707  if(!coacc.Exists(tit->X2)){
1708  // is this silent event with the highest priority at this state?
1709  EventSet active = rPGen.ActiveEventSet(tit->X1);
1710  EventSet::Iterator eit = active.Begin();
1711  Idx highest = rPGen.LowestPriority();
1712  for(;eit!=active.End();eit++){
1713  if (rPGen.Priority(*eit)>highest)
1714  highest = rPGen.Priority(*eit);
1715  }
1716  if(rPGen.Priority(tit->Ev)==highest)
1717  sblock.Insert(tit->X1);
1718  }
1719  }
1720  // unmark blocking states and eliminate possible future
1721  sit=sblock.Begin();
1722  sit_end=sblock.End();
1723  for(;sit!=sit_end;++sit) {
1724  rPGen.ClrMarkedState(*sit);
1725  tit=rPGen.TransRelBegin(*sit);
1726  tit_end=rPGen.TransRelEnd(*sit);
1727  while(tit!=tit_end)
1728  rPGen.ClrTransition(tit++);
1729  }
1730  rPGen.Accessible();
1731  FD_DF("BlockingSilentEvent(): done with t#"<<rPGen.TransRelSize());
1732 }
1733 
1734 // -- merge all states that block to one representative
1736  FD_DF("MergeNonCoaccessible()");
1737  StateSet notcoacc=rPGen.States()-StronglyCoaccessibleSet(rPGen);
1738  // bail out on trivial case
1739  if(notcoacc.Size()<2) return;
1740  // bail out with blocking init state
1741  if((notcoacc * rPGen.InitStates()).Size()>0){
1742  rPGen.DelStates(rPGen.States());
1743  Idx qnc = rPGen.InsState();
1744  rPGen.SetInitState(qnc);
1745  return;
1746  }
1747  // have a new state
1748  Idx qnc=rPGen.InsState();
1749  // fix transitions by iterating over predecessors of notcoacc
1750  TransSetX2EvX1 rtrans;
1751  rPGen.TransRel().ReSort(rtrans);
1752  StateSet::Iterator sit = notcoacc.Begin();
1753  for(;sit!=notcoacc.End();sit++){
1754  TransSetX2EvX1::Iterator rtit = rtrans.BeginByX2(*sit);
1755  for(;rtit!=rtrans.EndByX2(*sit);rtit++){
1756  rPGen.SetTransition(rtit->X1,rtit->Ev,qnc);
1757  }
1758  }
1759  // delete original not coacc
1760  rPGen.DelStates(notcoacc);
1761 }
1762 
1763 
1764 // -- if a transition blocks, remove all transitions from the same state with the same label
1765 void BlockingEvent(pGenerator& rPGen,const EventSet& rSilent){
1766  FD_DF("BlockingEvent(): prepare for t#"<<rPGen.TransRelSize());
1767  StateSet coacc=StronglyCoaccessibleSet(rPGen);
1768  StateSet notcoacc = rPGen.States()-coacc;
1769  TransSetX2EvX1 rtrans;
1770  rPGen.TransRel().ReSort(rtrans);
1771  TransSet::Iterator tit;
1772  TransSet::Iterator tit_end;
1773  StateSet::Iterator sit;
1774  StateSet::Iterator sit_end;
1776  TransSetX2EvX1::Iterator rtit_end;
1777  TransSet deltrans;
1778  // loop over notcoacc (normally smaller than coacc) and find coacc pred
1779  sit = notcoacc.Begin();
1780  sit_end = notcoacc.End();
1781  for(;sit!=sit_end;sit++){
1782  rtit = rtrans.BeginByX2(*sit);
1783  rtit_end = rtrans.EndByX2(*sit);
1784  for(;rtit!=rtit_end;rtit++){
1785  if (rSilent.Exists(rtit->Ev)) continue; // silent blocking evs are handled elsewhere
1786  if (!coacc.Exists(rtit->X1)) continue; // incoming trans from coacc
1787  // current rtit is such that X1 is coacc but X2 is not, Ev is nonsilent
1788  // record transitions from the X1 with the same event BUT not rtit
1789  tit = rPGen.TransRelBegin(rtit->X1);
1790  tit_end = rPGen.TransRelEnd(rtit->X1);
1791  for(;tit!=tit_end;tit++){
1792  if(tit->X2 == rtit->X2) continue; // skip for tit==rtit
1793  if(tit->Ev == rtit->Ev)
1794  deltrans.Insert(*tit);
1795  }
1796  }
1797  }
1798  // delete transitions
1799  tit=deltrans.Begin();
1800  tit_end=deltrans.End();
1801  for(;tit!=tit_end;++tit)
1802  rPGen.ClrTransition(*tit);
1803  FD_DF("BlockingEvent(): done with t#"<<rPGen.TransRelSize());
1804 }
1805 
1807  pGenerator& rPGen,
1808  const EventSet& rSilent){
1809  if (rSilent.Empty()) return;
1810  FD_DF("PConflictPreservingAbstraction()");
1811  // preparation: augment fictive silent events if not existing in rPGen's alphabet
1812  EventSet augsilent = rSilent;
1813  // record silent ev priorities
1814  std::set<Idx> existingsil_k;
1815  EventSet::Iterator eit = rSilent.Begin(); // NOTE: rSilent should be a subset of rPGen.Alphabet
1816  for(;eit!=rSilent.End();eit++)
1817  existingsil_k.insert(rPGen.Priority(*eit));
1818  // loop over all silentevent priorities
1819  std::set<Idx>::iterator kit=existingsil_k.begin();
1820  for(;kit!=existingsil_k.end();++kit) {
1821  Idx k=*kit;
1822  FD_DF("PConflictPreservingAbstraction(): prio "<<k);
1823  std::string silevname = ":::" + ToStringInteger(k);
1824  if(rPGen.Alphabet().Exists(silevname)){
1825  std::stringstream errstr;
1826  errstr << "Alphabet of '" << rPGen.Name() << "' inculdes reserved symbolic name " << silevname;
1827  throw Exception("PConflictPreservingAbstraction", errstr.str(), 599);
1828  }
1829  Idx silev = rPGen.InsEvent(silevname);
1830  rPGen.Priority(silev,k);
1831  augsilent.Insert(silev);
1832  }
1833  ShapeUpsilon(rPGen,augsilent); // enforce well-formedness
1834  rPGen.Accessible();
1835  FD_DF("PConflictPreservingAbstraction(): loop A done");
1836 
1837 
1838  // certain conflicts
1839  // ******************NOTE: empty fairness constraints = trivial Nonblocking!
1840  if (rPGen.GlobalAttribute().Fairness().Size()>0){ // cosmetically skip
1841  BlockingEvent(rPGen,augsilent);
1842  BlockingSilentEvent(rPGen,augsilent);
1843  RemoveNonCoaccessibleOut(rPGen);
1844  MergeNonCoaccessible(rPGen);
1845  }
1846  // redundant silent step rule
1847  RedundantSilentStep(rPGen,augsilent); // quick, may produce silent selfloop, guarantee well-formedness
1848  // only silent in/out rules
1849  RemoveRedSilentSelfloops(rPGen,augsilent); // no redundant silent loops any more
1850  std::map<StateSet,Idx> livelocks;
1851  DetectLiveLocks(rPGen,augsilent,livelocks);
1852  StateSet skipstates;
1853  std::map<StateSet,Idx>::const_iterator livelockit = livelocks.begin();
1854  for(;livelockit!=livelocks.end();++livelockit){
1855  skipstates.InsertSet(livelockit->first);
1856  }
1857  OnlySilentIncoming(rPGen,augsilent,skipstates);
1858  OnlySilentOutgoing(rPGen,augsilent,skipstates);
1859  // AESC and PWB
1860  MergePWB(rPGen,augsilent);
1861  MergeAESC(rPGen,augsilent);
1862 
1863  // cosmetically set clean state names
1864  rPGen.SetDefaultStateNames();
1865 
1866  // OPTIONAL: remove augmented silent events
1867  EventSet remove = augsilent - rSilent;
1868  if (!remove.Empty())
1869  rPGen.DelEvents(remove);
1870  FD_DF("PConflictPreservingAbstraction(): done");
1871 }
1872 
1873 bool IsHideable(const pGenerator& rPGen,
1874  const EventSet& rSilent,
1875  const Transition& rTrans){
1876  FD_DF("IsHidable()");
1877  if (!rSilent.Exists(rTrans.Ev)) return false; // this is not a silent event at all (e.g. _OMEGA_)
1878  FairnessConstraints relevant; // collect all fairness constraints containing rTrans->Ev
1880  for(;fpos<rPGen.GlobalAttribute().Fairness().Size();++fpos){
1881  const EventSet& fair = rPGen.GlobalAttribute().Fairness().At(fpos);
1882  if(fair.Exists(rTrans.Ev))
1883  relevant.Append(fair);
1884  }
1885  if (relevant.Empty()) return true; // this event is not in any fairness constraint
1886  // get the =>_Sig:k closure from rTrans->X2
1887  StateSet todo;
1888  StateSet visited;
1889  const Idx k = rPGen.Priority(rTrans.Ev);
1890  const EventSet x1active = NonsilHigherThen(rPGen,rSilent,rTrans.X1,k);
1891  if (NonsilHigherThen(rPGen,rSilent,rTrans.X2,k)<=x1active){
1892  todo.Insert(rTrans.X2);
1893  }
1894  while (!todo.Empty()){
1895  Idx cstate = *todo.Begin();
1896  todo.Erase(todo.Begin());
1897  visited.Insert(cstate);
1898  FairnessConstraints relevant_copy = relevant; // buffer a copy of relevant fairness constraints
1899  StateSet todo_new; // buffer a state set for qualified silent successors
1900  TransSet::Iterator tit = rPGen.TransRelBegin(cstate);
1901  for(;tit!=rPGen.TransRelEnd(cstate);tit++){
1902  if (!rSilent.Exists(tit->Ev)) continue;
1903  if (rPGen.Priority(tit->Ev) <k) continue; // required both for colouring or silent successor
1904  if (*tit == rTrans) continue;
1905  // how many relevant fairness constraints are satisfied?
1907  for(;fpos<relevant_copy.Size();++fpos){
1908  const EventSet& fair = relevant_copy.At(fpos);
1909  if (fair.Exists(tit->Ev)){
1910  relevant_copy.Erase(fpos); // remove when this fairness cons is satisfied
1911  continue;
1912  }
1913  fpos++;
1914  }
1915  if (relevant_copy.Empty()) return true;
1916  // is tit->X2 a suitable silent successor?
1917  if (NonsilHigherThen(rPGen,rSilent,tit->X2,k)<=x1active){
1918  todo_new.Insert(tit->X2);
1919  }
1920  }
1921  todo.InsertSet(todo_new - visited);
1922  }
1923  return false;
1924 }
1925 
1926 // substitute all private events with a new event with the same priority
1927 // while also fix the private event set rPrivate
1928 // THE fairness version
1929 // pUnhideable: a set of always unhideable events
1931  EventSet& rPrivate,
1932  EventPriorities& rPrios,
1933  Idx& rTau,
1934  const EventSet* pUnHideable = nullptr){
1935  EventSet result;
1936  EventSet msilentevs=rPGen.Alphabet() * rPrivate;
1937  if(msilentevs.Empty()){
1938  return result;
1939  }
1940  FD_DF("HidePrivateEvs(): HP " << rPGen.HighestPriority() << " LP " << rPGen.LowestPriority());
1941  // install tau events to alphabet
1942  std::vector<Idx> tauevs; // buffer a vector for fast search. Position index = priority
1943  tauevs.reserve(rPGen.HighestPriority()+1);
1944  Idx k = rPGen.LowestPriority();
1945  for(;k<=rPGen.HighestPriority();++k){
1946  FD_DF("HidePrivateEvs(): prio " << k);
1947  std::string tauevname = "__TAU"+ToStringInteger(rTau)+":"+ToStringInteger(k);
1948  if (rPGen.Alphabet().Exists(tauevname)){
1949  std::stringstream errstr;
1950  errstr << "Alphabet of '" << rPGen.Name() << "' inculdes reserved symbolic name "<< tauevname;
1951  throw Exception("HidePrivateEvs", errstr.str(), 599);
1952  }
1953  Idx tauev = rPGen.InsEvent(tauevname);
1954  tauevs.push_back(tauev); // the index coincides the k mius offset value
1955  result.Insert(tauev);
1956  rPGen.Priority(tauev,k);
1957  rPrios.InsPriority(tauev,k);
1958  }
1959  rTau++; // updates tau index
1960  TransSet::Iterator tit = rPGen.TransRelBegin();
1961  EventSet unhideable;
1962  if (pUnHideable != nullptr) unhideable = *pUnHideable;
1963  while(tit!=rPGen.TransRelEnd()){
1964  if (!IsHideable(rPGen,msilentevs+result,*tit)||result.Exists(tit->Ev)||unhideable.Exists(tit->Ev)){
1965  tit++;
1966  continue;
1967  }
1968  Transition trans(tit->X1,tauevs.at(rPGen.LowestPriority()+rPGen.Priority(tit->Ev)),tit->X2);
1969  rPGen.SetTransition(trans);
1970  rPGen.ClrTransition(tit++);
1971  }
1972  rPrivate.EraseSet(msilentevs); // benefits other automata
1973  FD_DF("HidePrivateEvs(): done");
1974  return result;
1975 }
1976 
1977 // monolithic fairness check
1978 // NOTE: Does not shape. For prioritised automaton consider Shape first.
1980  FD_DF("IsStronglyNonblocking()");
1981  Generator copy = rPGen;
1982  copy.Accessible();
1984  for(;fpos<rPGen.GlobalAttribute().Fairness().Size();++fpos){
1985  const EventSet& fair = rPGen.GlobalAttribute().Fairness().At(fpos);
1986  copy.ClearMarkedStates();
1987  StateSet::Iterator sit = copy.StatesBegin();
1988  for(;sit!=copy.StatesEnd();sit++){
1989  // if a state can execute a fair event, it's "marked" for this fairness constraint
1990  if(!(copy.ActiveEventSet(*sit) * fair).Empty()){
1991  copy.SetMarkedState(*sit);
1992  }
1993  }
1994  if (!faudes::IsNonblocking(copy)){
1995  StateSet blocking = copy.BlockingStates();
1996  std::cout<<"****** THE BLOCKING: "+ToStringInteger(*blocking.Begin())<<std::endl;
1997  return false; // fails at this fairness constraint
1998  }
1999  }
2000  return true;
2001 }
2002 
2003 
2004 // merge the fairness constraint of two pGenerators
2005 void MergeFairness(const pGenerator& rPGen1, const pGenerator& rPGen2, FairnessConstraints& rFairRes){
2006  rFairRes = rPGen1.GlobalAttribute().Fairness();
2008  for(;fpos<rPGen2.GlobalAttribute().Fairness().Size();++fpos){
2009  const EventSet& fair = rPGen2.GlobalAttribute().Fairness().At(fpos);
2010  rFairRes.Append(fair);
2011  }
2012 }
2013 
2014 
2015 // The main function for non-conflict check.
2016 // a) if rFairVec is non-empty, fairness constraints are considered
2017 // b) if rFairVec is empty we treat omega-termination as the acceptance condition (see below wraper)
2019  const EventPriorities& rPrios,
2020  const std::vector<FairnessConstraints>& rFairVec) {
2021 
2022  FD_DF("IsPFNonblocking()");
2023  // have a writable copy
2024  EventPriorities prios=rPrios;
2025 
2026  // consistency check for coloured marking
2027  if(rFairVec.size()>0){
2028  if (rGvec.Size()!=rFairVec.size()){
2029  std::stringstream errstr;
2030  errstr << "consistency check fails (vector length mismatch)";
2031  throw Exception("IsPFNonconflicting", errstr.str(), 599);
2032  }
2033  Idx git = 0;
2034  for(;git!=rGvec.Size();git++){
2036  for(;fpos<rFairVec.at(git).Size();++fpos){
2037  const EventSet& fair = rFairVec.at(git).At(fpos);
2038  if (!(fair<=rGvec.At(git).Alphabet())){
2039  std::stringstream errstr;
2040  errstr << "Consistency check fails";
2041  errstr << "Generator '"<<rGvec.At(git).Name() <<"' contains fairness event not in its alphabet";
2042  throw Exception("IsPFNonconflicting", errstr.str(), 599);
2043  }
2044  }
2045  }
2046  }
2047  Idx tau = 0; // index for "full hiding"
2048 
2049  EventSet merging;
2050  std::map<std::string,Idx>::const_iterator mit;
2051  // if isSFC==1, set up merging events. Also check priority (disjunct is checked by SFC_Parallel)
2052 
2053 
2054  PCOMPVER_VERB1("IsPFNonconflicting:: Installing priority and appending omega termination")
2055  // rearrange for consecutive priorities starting at 1 // TM2025/04
2056  //prios.NormalisePriorities();
2057  // get lowest/highest priority (PWB requires on extra prioity below internally) TMPRIO
2058  Idx lowest = prios.LowestPriority();
2059  Idx highest = prios.HighestPriority();
2060  if(lowest==0){
2061  throw Exception("IsPFNonconflicting()", "priority 0 reserved for internal use", 599);
2062  }
2063  lowest--;
2064  // encode priority and fairness information into pgen
2065  std::vector<pGenerator> pgenvec;
2066  pgenvec.reserve(rGvec.Size());
2067  Idx git = 0;
2068  for(;git!=rGvec.Size();git++){
2069  pGenerator pgen=rGvec.At(git);
2070  pgen.Priorities(prios);
2071  pgen.LowestPriority(lowest);
2072  pgen.HighestPriority(highest);
2073  if (rFairVec.size()==0){ // go for omega termination
2074  AppendOmegaTermination(pgen,prios);
2075  }
2076  else{ // install predefined fairness
2077  pgen.Fairness(rFairVec.at(git));
2078  }
2079  pgenvec.push_back(pgen);
2080  }
2081  bool firstCycle = true;
2082  while (true){
2083  PCOMPVER_VERB1("========================================")
2084  PCOMPVER_VERB1("Remaining automata: "<<pgenvec.size())
2085 
2086  // trivial cases
2087  if(pgenvec.size()==0) return true;
2088  if(pgenvec.size()==1) break;
2089 
2090  // figure silent events
2091  EventSet silent, all, shared;
2092  Idx git = 0;
2093  while(true){
2094  all = all+pgenvec.at(git).Alphabet();
2095  Idx git_next = git+1;
2096  if (git_next == pgenvec.size()) break;
2097  for(;git_next!=pgenvec.size();git_next++){
2098  shared = shared
2099  + (pgenvec.at(git).Alphabet())
2100  * (pgenvec.at(git_next).Alphabet());
2101  }
2102  git++;
2103  }
2104  silent=all-shared; // all silent events in all current candidates
2105  // normalize for one silent event at each priority level per generator, and then abstract.
2106  // note from the second iteration, this is only necessary for the
2107  // automaton composed from former candidates. This is realized by
2108  // the break at the end
2109  git = 0;
2110  for(;git!=pgenvec.size();git++){
2111  //abstraction
2112  pGenerator& g = pgenvec.at(git);
2113  PCOMPVER_VERB1("Abstracting Automaton "<< g.Name()<<", with state count: "<<g.Size())
2114  ShapeUpsilon(g,silent); // enforce well-formedness
2115  g.Accessible();
2116  EventSet upsilon = HidePrivateEvs(g,silent,prios,tau,&merging);
2117  PConflictPreservingAbstraction(g, upsilon);
2118  PCOMPVER_VERB1("State count after abstraction: "<<g.Size())
2119  if (!firstCycle) break;
2120  }
2121  firstCycle = false;
2122 
2123  // candidate choice heuritics. Branch by different tasks
2124  Idx imin = 0;
2125  Idx jmin = 0;
2126 
2127  // // candidat pairs with fewest transitions 'minT'
2128  // git = 1;
2129  // for(;git!=pgenvec.size();git++){
2130  // if(pgenvec.at(git).TransRelSize()<pgenvec.at(imin).TransRelSize());
2131  // imin = git;
2132  // }
2133  // // candidat pairs with most common events 'maxC'
2134  // git = jmin;
2135  // Int score=-1;
2136  // for(; git!=pgenvec.size(); git++){
2137  // if(git==imin) continue;
2138  // Int sharedsize = (pgenvec.at(git).Alphabet() * pgenvec.at(imin).Alphabet()).Size();
2139  // if ( sharedsize > score){
2140  // jmin = git;
2141  // score = sharedsize;
2142  // }
2143  // }
2144  // compose candidate pair
2145  imin = 0;
2146  jmin = 1;
2147 
2148  // get new private event for SParallel
2149  EventSet myevs;
2150  EventSet otherevs;
2151  git = 0;
2152  for(;git!=pgenvec.size();git++){
2153  if (git==imin || git==jmin)
2154  myevs = myevs + pgenvec.at(git).Alphabet();
2155  else
2156  otherevs = otherevs + pgenvec.at(git).Alphabet();
2157  }
2158  EventSet privateevs = myevs-otherevs;
2159 
2160  // *************** compose Gi and Gj and reinstall attributes to gij
2161  std::vector<pGenerator> newpgenvec;
2162  pGenerator gij;
2163  FairnessConstraints newfairness;
2164  PCOMPVER_VERB1("Composing automata "<<pgenvec.at(imin).Name()<<" and "<<pgenvec.at(jmin).Name());
2165  SUParallel(pgenvec.at(imin),pgenvec.at(jmin),merging,privateevs,prios,gij);
2166  pGenerator pgij = gij;
2167  pgij.Priorities(prios);
2168  newpgenvec.push_back(pgij); // the composed generator is always the first element
2169  UParallel_MergeFairness(pgenvec.at(imin), pgenvec.at(jmin),gij, merging, newfairness);
2170 
2171  newpgenvec[0].Fairness(newfairness);
2172  newpgenvec[0].LowestPriority(lowest);
2173  newpgenvec[0].HighestPriority(highest);
2174  // and retain other uncomposed automata
2175  git = 0;
2176  for(;git!=pgenvec.size();git++){
2177  if (git == imin || git == jmin) continue;
2178  newpgenvec.push_back(pgenvec.at(git)); // all other candidates are just copied to the next iteraion
2179  }
2180  pgenvec = newpgenvec;
2181  }
2182  ShapePriorities(pgenvec.at(0));
2183  pgenvec.at(0).Accessible();
2184  std::cout<<"Final state count: "<<ToStringInteger(pgenvec.at(0).Size())<<std::endl;
2185  return IsStronglyNonblocking(pgenvec.at(0));
2186 }
2187 
2188 // wrapper for no fairness constraints
2189 bool IsPNonblocking(const GeneratorVector& rGvec, const EventPriorities& rPrios) {
2190  std::vector<FairnessConstraints> dummy;
2191  return IsPFNonblocking(rGvec,rPrios,dummy);
2192 }
2193 
2194 
2195 
2196 /*
2197 ***********
2198 NEED OLD (?) VERSION DUMMIES TO COMPILE (TM 2025)
2199 ******
2200 */
2201 
2203  FD_ERR("MergeSilentLoops(): revise pev-abstraction.cpp??");
2204 }
2205 
2207  mGenHidden = mGenRaw;
2208  mGenHidden.Name(mGenRaw.Name() + "_H");
2209  EventSet msilentevs = (mGenRaw.Alphabet()*silent) - mPevs;
2210  EventSet mpsilentevs = (mGenRaw.Alphabet()*silent) * mPevs;
2211  if(msilentevs.Empty() && mpsilentevs.Empty()){
2213  mGenMerged.Name(mGenRaw.Name()+"_M");
2214  return;
2215  }
2216  Idx tau;
2217  Idx ptau;
2218  if (!msilentevs.Empty()){
2219  tau=*(msilentevs.Begin());
2220  SetTau(tau);
2221  SetSilentevs(msilentevs);
2222  msilentevs.Erase(tau); // from now on, msilentevs exclude tau
2223  }
2224  if (!mpsilentevs.Empty()){
2225  ptau = *(mpsilentevs.Begin());
2226  SetPtau(ptau);
2227  SetPSilentevs(mpsilentevs);
2228  mpsilentevs.Erase(ptau);
2229  }
2230 
2231  silent.EraseSet(msilentevs);
2232  silent.EraseSet(mpsilentevs);
2233 
2234  if (msilentevs.Empty() && mpsilentevs.Empty()){// in this case, only one 1 silent event is set to tau and no need to hide
2236  mGenMerged.Name(mGenRaw.Name()+"_M");
2237  return;
2238  }
2241  for(;tit!=tit_end;) {
2242  if(!(msilentevs+mpsilentevs).Exists(tit->Ev)) {++tit; continue;}
2243  Transition t;
2244  if (msilentevs.Exists(tit->Ev))
2245  t = Transition(tit->X1,tau,tit->X2);
2246  else
2247  t = Transition(tit->X1,ptau,tit->X2);
2248  mGenHidden.ClrTransition(tit++);
2249  if (!mGenHidden.ExistsTransition(t))
2251  }
2252  mGenHidden.InjectAlphabet(mGenHidden.Alphabet()-msilentevs-mpsilentevs);
2254  mGenMerged.Name(mGenRaw.Name()+"_M");
2255 }
2256 
2258  const EventSet &silent){
2259  FD_ERR("ObservationEquivalenceQuotient_NonPreemptive(): revise pev_abstraction.cpp??");
2260 }
2261 
2262 
2264  FD_ERR("ObservationEquivalenceQuotient_Preemptive(): revise pev_abstraction.cpp??");
2265 }
2266 
2268  FD_ERR("ConflictEquivalentAbstraction(): revise pev_abstraction.cpp??");
2269 }
2270 
2271 
2272 
2273 } // namespace faudes
#define FD_ERR(message)
void OnlySilentIncoming(Generator &g, const EventSet &silent)
void BlockingSilentEvent(Generator &g, const EventSet &silent)
virtual void HidePrivateEvs(EventSet &silent)
void RemoveTauSelfloops(Generator &g, const EventSet &silent)
void SetTau(Idx tau)
void RemoveNonCoaccessibleOut(Generator &g)
void ActiveNonTauEvs(const Generator &rGen, const EventSet &silent, const Idx &state, EventSet &result)
void SetSilentevs(EventSet silentevs)
std::map< Idx, Idx > mMergeMap
void ActiveEventsANDEnabledContinuationRule(Generator &g, const EventSet &silent)
void MergeEquivalenceClasses(Generator &rGen, TransSetX2EvX1 &rRevTrans, const std::list< StateSet > &rClasses, const EventSet &silent)
virtual void MergeSilentLoops(Generator &g, const EventSet &silent)
void OnlySilentOutgoing(Generator &g, const EventSet &silent)
virtual void ConflictEquivalentAbstraction(EventSet &silent)
void BlockingEvent(Generator &g, const EventSet &silent)
void WeakObservationEquivalentQuotient(Generator &g, const EventSet &silent)
void IncomingTransSet(const Generator &rGen, const EventSet &silent, const Idx &state, std::set< std::pair< Idx, Idx >> &result)
void ReverseObservationEquivalentQuotient(Generator &g, const EventSet &silent)
void ObservationEquivalentQuotient(Generator &g, const EventSet &silent)
void ExtendedTransRel(const Generator &rGen, const EventSet &rSilentAlphabet, TransSet &rXTrans)
void MergeNonCoaccessible(Generator &g)
const std::string & Name(void) const
Definition: cfl_types.cpp:422
bool Exists(const Idx &rIndex) const
virtual void InsertSet(const NameSet &rOtherSet)
bool Insert(const Idx &rIndex)
void EraseSet(const NameSet &rOtherSet)
virtual bool Erase(const Idx &rIndex)
virtual void HidePrivateEvs(EventSet &silent)
HidePrivateEvs replace all private events.
void SetPSilentevs(EventSet psilentevs)
void SetPtau(Idx ptau)
virtual void MergeSilentLoops(Generator &g, const EventSet &silent)
virtual void ConflictEquivalentAbstraction(EventSet &silent)
void ObservationEquivalenceQuotient_NonPreemptive(Generator &g, const EventSet &silent)
void ObservationEquivalenceQuotient_Preemptive(Generator &g, const EventSet &silent, const bool &flag)
std::vector< int >::size_type Position
virtual Iterator Erase(const Iterator &vit)
virtual const T & At(const Position &pos) const
Iterator Begin(void) const
Iterator End(void) const
bool Exists(const Transition &t) const
Iterator BeginByX2(Idx x2) const
bool Insert(const Transition &rTransition)
Iterator EndByX2(Idx x2) const
bool Erase(const Transition &t)
void RestrictEvents(const EventSet &rEventSet)
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
void ReSort(TTransSet< OtherCmp > &res) const
GlobalAttr * GlobalAttributep(void)
void EventAttribute(Idx index, const EventAttr &rAttr)
EventAttr * EventAttributep(Idx index)
bool InsEvent(Idx index)
const TaStateSet< StateAttr > & States(void) const
const TaEventSet< EventAttr > & Alphabet(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
void InjectTransRel(const TransSet &rNewtransrel)
const ATransSet & TransRel(void) const
void GlobalAttribute(const GlobalAttr &rAttr)
Idx Priority(const std::string &rName) const
Idx LowestPriority(void) const
Idx HighestPriority(void) const
void InsPriority(const Idx idx, const Idx prio)
Idx Priority(const Idx index) const
FairnessConstraints Fairness(void) const
void HighestPriority(const Idx rPriority)
void Priorities(const TpEventSet< EventAttr > &rOtherSet)
Idx LowestPriority(void) const
bool Empty(void) const
virtual void Append(const Type &rElem)
Idx Size(void) const
StateSet::Iterator StatesBegin(void) const
StateSet::Iterator InitStatesBegin(void) const
const TransSet & TransRel(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
const StateSet & MarkedStates(void) const
const EventSet & Alphabet(void) const
EventSet ActiveEventSet(Idx x1) const
void DelEvents(const EventSet &rEvents)
const StateSet & InitStates(void) const
TransSet::Iterator TransRelBegin(void) const
void ClrTransition(Idx x1, Idx ev, Idx x2)
void InsEvents(const EventSet &events)
void ClrMarkedState(Idx index)
EventSet::Iterator AlphabetBegin(void) const
StateSet BlockingStates(void) const
void ClearMarkedStates(void)
bool ExistsTransition(const std::string &rX1, const std::string &rEv, const std::string &rX2) const
void SetInitState(Idx index)
void InsStates(const StateSet &rStates)
StateSet::Iterator MarkedStatesBegin(void) const
bool DelState(Idx index)
StateSet::Iterator StatesEnd(void) const
void DelStates(const StateSet &rDelStates)
TransSet::Iterator TransRelEnd(void) const
StateSet::Iterator MarkedStatesEnd(void) const
void InjectTransRel(const TransSet &rNewtransrel)
void SetMarkedState(Idx index)
bool InsEvent(Idx index)
StateSet::Iterator InitStatesEnd(void) const
void SetDefaultStateNames(void)
Idx TransRelSize(void) const
std::string EventName(Idx index) const
EventSet::Iterator AlphabetEnd(void) const
StateSet CoaccessibleSet(void) const
Idx Size(void) const
bool ExistsInitState(Idx index) const
bool ExistsMarkedState(Idx index) const
const StateSet & States(void) 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
virtual void Clear(void)
Definition: cfl_baseset.h:1962
Iterator End(void) const
Definition: cfl_baseset.h:1956
virtual void InsertSet(const TBaseSet &rOtherSet)
Definition: cfl_baseset.h:2052
Iterator Begin(void) const
Definition: cfl_baseset.h:1951
virtual bool Erase(const T &rElem)
Definition: cfl_baseset.h:2084
Idx Size(void) const
Definition: cfl_baseset.h:1782
void ComputeBisimulation(const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition)
bool ComputeScc(const Generator &rGen, const SccFilter &rFilter, std::list< StateSet > &rSccList, StateSet &rRoots)
void ShapePriorities(vGenerator &rGen, const EventPriorities &rPrios)
void ShapePreemption(Generator &rGen, const EventSet &pevs)
bool IsPFNonblocking(const GeneratorVector &rGvec, const EventPriorities &rPrios, const std::vector< FairnessConstraints > &rFairVec)
bool IsPNonblocking(const GeneratorVector &rGvec, const EventPriorities &rPrios)
uint32_t Idx
void BlockingSilentEvent(Generator &g, const EventSet &silent)
std::map< std::pair< Idx, Idx >, EventSet > IncTransSet
void IncomingTransSet(const Generator &rGen, const TransSetX2EvX1 &rRTrans, const EventSet &silent, const Idx &state, SetX1Ev &result)
EventSet NonsilHigherThen(const pGenerator &rPGen, const EventSet &rSilent, const Idx &rState, const Idx &rK)
void UParallel_MergeFairness(const pGenerator &rPGen1, const pGenerator &rPGen2, const Generator &rGen12, const EventSet &rMerge, FairnessConstraints &rFairRes)
void AppendOmegaTermination(Generator &rGen)
void OnlySilentIncoming(Generator &g, const EventSet &silent)
StateSet StronglyCoaccessibleSet(const pGenerator &rPGen)
void RemoveNonCoaccessibleOut(Generator &g)
void WritePrio(const pGenerator &rPGen)
bool IsHideable(const pGenerator &rPGen, const EventSet &rSilent, const Transition &rTrans)
void MergeEquivalenceClasses(Generator &rGen, TransSetX2EvX1 &rRevTrans, const std::list< StateSet > &rClasses)
void OnlySilentOutgoing(Generator &g, const EventSet &silent)
Idx SilentEvAtPrio(const pGenerator &rPGen, const EventSet &rSilent, const Idx &rK)
bool IsNonblocking(const GeneratorVector &rGvec)
std::map< SetX1Ev, StateSet > IncomingEquivalentClasses(const Generator &rGen, const EventSet &silent)
void SaturatePWB(const pGenerator &rPGen, const EventSet &rSilent, pGenerator &rResult)
void PrintEqclasses(const std::list< StateSet > &rEqclasses)
void ShapeUpsilon(vGenerator &rGen, const EventPriorities &rPrios, const EventSet &rUpsilon)
void PrintEventTable(const pGenerator &rPGen)
EventSet HidePrivateEvs(pGenerator &rPGen, EventSet &rPrivate, EventPriorities &rPrios, Idx &rTau, const EventSet *pUnHideable=nullptr)
void MergeAESC(pGenerator &rPGen, const EventSet &rSilent)
void SUParallel(const pGenerator &rPGen1, const pGenerator &rPGen2, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, EventSet &rMerge, const EventSet &rPrivate, EventPriorities &rPrios, pGenerator &rPRes)
void PConflictPreservingAbstraction(pGenerator &rPGen, const EventSet &rSilent)
void RemoveRedSilentSelfloops(pGenerator &rPGen, const EventSet &rSilent)
void ComputeBisimulationCTA(const Generator &rGen, std::list< StateSet > &rResult)
ComputeBisimulationCTA basic bisimulation partition algorithm based on change-tracking algorithm.
std::string ToStringInteger(Int number)
Definition: cfl_utils.cpp:43
void MergePWB(pGenerator &rPGen, const EventSet &rSilent)
void AESCClasses(const pGenerator &rPGen, const EventSet &rSilent, std::list< StateSet > &rResult)
bool IsStronglyNonblocking(const pGenerator &rPGen)
void BlockingEvent(pGenerator &rPGen, const EventSet &rSilent)
void RedundantSilentStep(pGenerator &rPGen, const EventSet &rSilent)
void DetectLiveLocks(const pGenerator &rPGen, const EventSet &rSilent, std::map< StateSet, Idx > &rResult)
void SaturateLowestPrio(const pGenerator &rPGen, const EventSet &rSilent, pGenerator &rResult)
void MergeFairness(const pGenerator &rPGen1, const pGenerator &rPGen2, FairnessConstraints &rFairRes)
long int Int
void MergeNonCoaccessible(Generator &g)
void SaturatePDelayed(const pGenerator &rPGen, const EventSet &rSilent, const bool &_mode, pGenerator &rResult)
#define FD_DF(a)
#define PCOMPVER_VERB1(msg)

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