Java > Open Source Codes > SOFA > SOFAnode > Util > machineImpl


1 /* $Id: machineImpl.java,v 1.2 2004/05/20 14:23:53 bures Exp $ */
2
3 package SOFA.SOFAnode.Util;
4
5 import java.util.Collection ;
6 import java.util.Comparator ;
7 import java.util.Hashtable ;
8 import java.util.Iterator ;
9 import java.util.LinkedList ;
10 import java.util.List ;
11 import java.util.TreeMap ;
12 import java.util.Vector ;
13
14
15 /**
16  * The implementation class for automata.
17  *
18  * @author Stanislav Visnovsky
19  * @version 1.0.0
20 */
21 public class machineImpl implements Machine, Printer {
22
23 /**
24  * list of states
25 */
26     public IntVector states[][];
27     public boolean marked[];
28
29     private int allocated;
30
31 /**
32  * reference to the starting state
33 */
34     private int start;
35
36 /**
37  * the list of accepting states
38 */
39     private Hashtable stop;
40
41 /**
42  * the list of update states
43 */
44     private Hashtable update;
45
46 /**
47  * ID counter for new states
48 */
49     public int nextID;
50
51 /**
52  * Constructor for an automaton. It just sets defaults, i.e., no states at all.
53  *
54  * @author Stanislav Visnovsky
55  * @version 1.0.0
56 */
57     public machineImpl() {
58         int i,j;
59
60     states = new IntVector[10][EdgeFactory.getActionTokensNum()];
61     nextID = 0;
62     allocated = 10;
63         stop = new Hashtable ();
64     update = new Hashtable ();
65         start = 0;
66     marked = new boolean[allocated];
67     }
68
69     public machineImpl(int size) {
70         int i,j;
71
72     Debug.println(2, "Initial size "+size+" states (no resize)");
73     states = new IntVector[size][EdgeFactory.getActionTokensNum()];
74     nextID = 0;
75     allocated = size;
76         stop = new Hashtable ();
77     update = new Hashtable ();
78         start = 0;
79     marked = new boolean[allocated];
80     if( maxstates < allocated ) maxstates = allocated;
81     }
82 /**
83  * Adds a new state to the automaton.
84  *
85  * @author Stanislav Visnovsky
86  * @version 1.0.0
87  * @param n the new state to be added
88 */
89     public void AddState( IntVector n[] ){
90     if( nextID == allocated ) Resize( allocated+5 );
91         states[ nextID ] = n;
92         nextID++;
93     }
94
95
96 /**
97  * Eliminates all unreachable states. It marks all reachable states by BFS algorithm and
98  * then eliminates all unmarked states.
99  *
100  * @author Stanislav Visnovsky
101  * @version 1.0.0
102  * @see State#Mark
103 */
104     public void Reachable() {
105
106     int a,t,tgt,st;
107
108     TidyUp();
109
110     Debug.println(3, "Cleaned");
111
112     LinkedList buffer = new LinkedList ();
113     buffer.add( new Integer (start) );
114     while( !buffer.isEmpty() ) {
115         a = ((Integer )buffer.removeFirst()).intValue();
116         if( !marked[a] ) {
117         marked[a] = true;
118         for( t = 0; t< EdgeFactory.getActionTokensNum(); t++) {
119             IntVector edges = states[a][t];
120             if( edges != null )
121                 for( tgt = 0 ; tgt < edges.used ; tgt++ )
122                     if( !marked[ edges.data[tgt] ] ) buffer.add( new Integer ( edges.data[tgt] ) );
123         }
124         }
125     }
126
127     Debug.println(3, "Reachable found, creating mapping");
128
129     int map[] = new int[ nextID ];
130     IntVector[][] newstates = new IntVector[ nextID ][ EdgeFactory.getActionTokensNum()];
131     
132     int mapnext = 0;
133
134     for( a = 0 ; a < nextID ; a++ )
135         if( marked[a] ) map[a] = mapnext++;
136
137     Debug.println(3, "Reachable mapping found");
138
139     for( a = 0 ; a < nextID ; a++ )
140         if( marked[a] ) {
141         for( t = 0; t < EdgeFactory.getActionTokensNum(); t++ )
142         if( states[a][t] != null ) {
143             if( newstates[map[a]][t] == null ) newstates[map[a]][t] = new IntVector();
144             for( tgt = 0; tgt < states[a][t].used; tgt++ )
145             newstates[map[a]][t].sortedAddIntIfNExists( map[ states[a][t].data[tgt] ] );
146         }
147         } else Debug.println(2,"Reachable deletes "+a);
148
149     Hashtable newstop = new Hashtable ();
150     for( Iterator i = stop.values().iterator(); i.hasNext(); ) {
151         st = ((Integer )i.next()).intValue();
152         if( marked[ st ] ) {
153         Integer newst = new Integer ( map[st] );
154         newstop.put( newst, newst );
155         }
156         }
157
158     Hashtable newupdate = new Hashtable ();
159     for( Iterator i = update.values().iterator(); i.hasNext(); ) {
160         st = ((Integer )i.next()).intValue();
161         if( marked[ st ] ) {
162         Integer newst = new Integer ( map[st] );
163         newupdate.put( newst, newst );
164         }
165         }
166
167     states = newstates;
168     stop = newstop;
169     update = newupdate;
170     start = map[start];
171
172     allocated = nextID;
173     
174     marked = new boolean[allocated];
175     
176     nextID = mapnext;
177
178     if( maxstates < allocated ) maxstates = allocated;
179
180     Print(2);
181     }
182
183 /**
184  * Adds new states to the automaton. It also must set IDs. However, edges are not added
185  *
186  * @author Stanislav Visnovsky
187  * @version 1.0.0
188  * @param n a list of new states to be added
189 */
190     public int[] AddStates( IntVector n[][], int size ){
191
192     int a,t,tgt;
193
194     int map[] = new int[ size ];
195
196     if( allocated <= size+nextID ) Resize( size+nextID );
197
198     int mapnext = nextID;
199
200     for( a = 0 ; a < size ; a++ )
201         map[a] = nextID++;
202
203     for( a = 0 ; a < size ; a++ ) {
204         for( t = 0; t < EdgeFactory.getActionTokensNum(); t++ )
205         if( n[a][t] != null ) {
206             if( states[map[a]][t] == null ) states[map[a]][t] = new IntVector();
207             for( tgt = 0; tgt < n[a][t].used; tgt++ )
208             states[map[a]][t].sortedAddIntIfNExists( map[ n[a][t].data[tgt] ] );
209         }
210         }
211     return map;
212     }
213
214 /**
215  * Adds a new accepting state of the automaton.
216  *
217  * @author Stanislav Visnovsky
218  * @version 1.0.0
219  * @param n the new accepting state
220 */
221     public void AddStop( int n ){
222         Integer nn = new Integer (n);
223     stop.put( nn, nn );
224     }
225
226     public int addState() {
227     if( nextID == allocated ) Resize( allocated+5 );
228         return nextID++;
229     }
230
231 /**
232  * Adds a list of new accepting states of the automaton.
233  *
234  * @author Stanislav Visnovsky
235  * @version 1.0.0
236  * @param n a list of new accepting states
237 */
238     public void AddStops( Collection n ){
239     Integer a;
240         Iterator i = n.iterator();
241     while( i.hasNext() ) {
242         a = (Integer )i.next();
243         stop.put( a, a );
244     }
245     }
246
247 /**
248  * Sets a new starting state of the automaton.
249  *
250  * @author Stanislav Visnovsky
251  * @version 1.0.0
252  * @param n the new starting state
253 */
254     public void SetStart( int n ){
255         start = n;
256     }
257
258 /**
259  * Print the debugging info through Debug class.
260  *
261  * @author Stanislav Visnovsky
262  * @version 2.0.0
263  *
264  * @see Debug
265 */
266     public void Print(int level) {
267     if( level > Debug.debug ) return;
268         Debug.println(level,"Machine:");
269         Debug.print(level,"Start:");
270         Debug.println(level, start );
271         Debug.print(level,"Stop:");
272         Iterator i = stop.values().iterator();
273         while( i.hasNext() ) {
274             Debug.print(level, ((Integer ) i.next()).intValue());
275             Debug.print(level," , ");
276         }
277         Debug.print(level,"Update:");
278         i = update.values().iterator();
279         while( i.hasNext() ) {
280             Debug.print(level, ((Integer ) i.next()).intValue());
281             Debug.print(level," , ");
282         }
283         Debug.println(level);
284         Debug.println(level,"States:");
285     for ( int j = 0 ; j < nextID ; j++ ) {
286         Debug.println( level, j );
287         for( int k = 0; k < EdgeFactory.getActionTokensNum(); k++ )
288         if( states[j][k] != null && states[j][k].used > 0 )
289         Debug.println( "--" + EdgeFactory.ActionTokens[k].name+"-->" + states[j][k].dump() );
290     }
291     }
292   
293     public void Print() {
294     this.Print(1);
295     }
296
297 /**
298  * Returns the starting state of the automaton.
299  *
300  * @author Stanislav Visnovsky
301  * @version 1.0.0
302  * @return the starting state
303 */
304     public int Start() { return start; }
305
306 /**
307  * Returns the list of accepting states of automaton.
308  *
309  * @author Stanislav Visnovsky
310  * @version 1.0.0
311  * @return the list of states
312 */
313     public Hashtable Stop() { return stop; }
314
315 /**
316  * Returns the list of update states of automaton.
317  *
318  * @author Stanislav Visnovsky
319  * @version 1.0.0
320  * @return the list of states
321 */
322     public Hashtable Update() { return update; }
323
324 /**
325  * Reduces the automaton, that all equivalent states are represented as only one state.
326  *
327  * @author Stanislav Visnovsky
328  * @version 2.0.0
329 */
330     public void Reduce() {
331
332         List Sets = new LinkedList ();
333
334     IntVector setof[] = new IntVector[ nextID ]; // references for the set of equivalent states
335
336     IntVector s1 = new IntVector();
337     IntVector s2 = new IntVector();
338
339     for( int n = 0; n < nextID; n++ ) {
340             if( stop.containsKey( new Integer (n) ) ) {
341             s1.addInt(n);
342             setof[n] = s1;
343         } else {
344                 s2.addInt(n);
345             setof[n] = s2;
346         }
347         }
348
349         Debug.println(1,"Reduce: Starting equivalence done");
350         if( s1.used > 0 ) Sets.add(s1);
351         if( s2.used > 0 ) Sets.add(s2);
352
353     TidyUp();
354
355     boolean in_n, in_n1, OKstate = true;
356     int e,n,n1,nstate,n1state;
357     Iterator i;
358     List Sets2;
359     IntVector s;
360     
361         boolean changed;
362         do {
363             changed = false;
364
365             Sets2 = new LinkedList ();
366             i = Sets.iterator();
367             while( i.hasNext() ) { // for all sets
368 s = (IntVector) i.next();
369         for( n = 0; n < s.used; n++ ) {
370             nstate = s.data[n];
371                     if( !marked[ nstate ] ) { // not done yet
372 s1 = new IntVector(); // it's own set
373 Sets2.add( s1 );
374                         s1.addInt( nstate );
375             setof[ nstate ] = s1;
376                         marked[ nstate ]=true;
377                         for( n1 = n+1; n1<s.used; n1++ ) {
378                 n1state = s.data[n1];
379                             if( !marked[ n1state ] ) {
380                 // first test, whether they are both in update
381 if( update.containsKey( new Integer (nstate) ) !=
382                     update.containsKey( new Integer (n1state) ) ) OKstate = false;
383                 else
384                                 for( e = 0 ; e < EdgeFactory.getActionTokensNum(); e++ ) {
385                         // let us require deterministic automaton :-)
386 in_n = states[nstate][e] != null ;
387                     in_n1 = states[n1state][e] != null ;
388                     if( in_n && in_n1 ) {
389                     OKstate =
390                        setof[ states[n1state][e].data[0]] == setof[ states[nstate][e].data[0] ];
391                     } else OKstate = ( !in_n && !in_n1 );
392                     if( !OKstate ) break;
393                                 }
394
395                         if( OKstate ) {
396                                     s1.addInt( n1state ); // add to n's set
397 setof[n1state]=s1;
398                                     marked[n1state] = true;
399                                 } else changed = true;
400                             }
401                         }
402                     }
403                 }
404             }
405             Sets = Sets2; // changed, use new sets
406 TidyUp();
407         } while( changed );
408
409         Debug.println(1,"Reduce: Equivalence found");
410
411             if( Debug.debug >2 ) {
412                 i = Sets.iterator();
413                 while( i.hasNext() ) {
414                     IntVector j = ((IntVector)i.next());
415                     Debug.print(2, "{ " );
416                     for( n = 0; n< j.used; n++ ) {
417                     Debug.print(2, j.data[n] );
418                     if( n < j.used-1 ) Debug.print( 2,", " );
419                     }
420                     Debug.println(2,"}");
421                 }
422                 Debug.println(2,"---------------------------");
423             }
424
425     // create reduced machine based on Sets
426
427         IntVector oldstates[][] = states;
428         Hashtable oldstop = stop;
429     Hashtable oldupdate = update;
430     int oldstart = start;
431         stop = new Hashtable ();
432     update = new Hashtable ();
433     
434         states = new IntVector[Sets.size()][EdgeFactory.getActionTokensNum()];
435     allocated = Sets.size();
436     marked = new boolean[ allocated ];
437     nextID = 0;
438     if( maxstates < allocated ) maxstates = allocated;
439
440         Hashtable map = new Hashtable ();
441
442         for( Iterator index = Sets.iterator() ; index.hasNext(); ) {
443         s = (IntVector) index.next() ;
444             map.put( s, new Integer ( nextID++ ) );
445         Debug.println(3, "Map: "+s+" -> "+(nextID-1) );
446         }
447
448         Debug.println(1,"New states created");
449
450     int j,j1;
451     int nextindex = 0;
452         for( Iterator index = Sets.iterator() ; index.hasNext(); ) {
453         s = (IntVector) index.next();
454         int state = s.data[0];
455         Debug.println( 3, "As a example for "+nextindex+" taken "+state );
456         for( j1 = 0 ; j1 < EdgeFactory.getActionTokensNum() ; j1++ ) {
457         if( oldstates[state][j1] != null && oldstates[state][j1].used>0 )
458         {
459             if( states[nextindex][j1] == null ) states[nextindex][j1] = new IntVector();
460             for( j = 0; j < oldstates[state][j1].used; j++ ) {
461             Debug.println( 3, "-- "+EdgeFactory.ActionTokens[j1].name+" --> "+setof[oldstates[state][j1].data[j]] );
462             Integer a = (Integer ) map.get( setof[oldstates[state][j1].data[j]] );
463             if( a == null ) Debug.println( 3, "Null !!!");
464             states[nextindex][j1].sortedAddIntIfNExists( a.intValue() );
465             }
466             }
467         }
468         if( oldstop.containsKey( new Integer ( state ) ) ) stop.put( new Integer ( nextindex ), new Integer (nextindex) );
469         if( oldupdate.containsKey( new Integer ( state ) ) ) update.put( new Integer ( nextindex ), new Integer (nextindex) );
470         nextindex++;
471         }
472
473     Debug.println(3, "Now setting new start state to "+setof[ oldstart ]);
474     start = ((Integer ) map.get( setof[ oldstart ] )).intValue();
475
476     Print(2);
477     }
478
479 /**
480  * A Vector-like class for handling arrays of primitive types (int)
481  *
482  * @author Vladimir Mencl
483  * @version 1.0.0
484  */
485
486     public static class IntVectorComparator implements Comparator {
487       public int compare(Object o1, Object o2) {
488     IntVector v1,v2;
489
490     v1=(IntVector)o1;
491     v2=(IntVector)o2;
492
493     if (v1.used<v2.used) return -1;
494     else if (v1.used>v2.used) return 1;
495     else {
496       for (int i=0;i<v1.used;i++) {
497         if (v1.data[i]<v2.data[i]) return -1;
498         else if (v1.data[i]>v2.data[i]) return 1;
499       };
500       return 0;
501     }
502       }
503     };
504
505 /**
506  * Transforms the automaton to a deterministic one.
507  *
508  * Optimized by Vladimir Mencl
509  *
510  * @author Vladimir Mencl
511  * @version 2.0.0
512  */
513     public void Determinize() {
514
515       Debug.println(1,"Starting new determinize");
516       this.Print(2);
517
518       Vector represents, newedges, newtokens;
519       IntVector newstop;
520       IntVector newupdate;
521       int newNstates;
522
523       /* variables representing the new deterministic machine *
524        * Vector of int[] represents;
525        * * Idxs of original states represented by state Idx
526        *
527        * Vector of IntVector newedges;
528        * * for each new state, Idxes of edge targets
529        *
530        * Vector of IntVector newtokens;
531        * * for newedges (above), IDs of tokens
532        */
533       
534       Vector origedges, origtokens;
535       IntVector origstops;
536       IntVector origupdate;
537       int origNstates, origstart;
538
539
540       /* variables representing the original non-deterministic machine *
541        *
542        * Vector of IntVector edges;
543        * * for each new state, Idxes of edge targets
544        *
545        * Vector of IntVector tokens;
546        * * for edges (above), IDs of tokens
547        *
548        * idx2states and state2idx map idxs and original states the same way
549        * as tokenname maps (below)
550        */
551
552
553       /* for mapping the concept of ActionToken objects to int[]
554        * tokennames is indexed by tokenID and contains the ActionToken object
555        * tokenIDs is indexed by token names (getHashCode())
556        * and contains Integer(tokenIdx)
557        */
558
559       /* Phase 1: represent original graph in new structures */
560
561       
562       origedges = new Vector (nextID);
563       origtokens = new Vector (nextID);
564       origstops = new IntVector();
565       origupdate = new IntVector();
566
567
568       {
569     for (int tstate=0;tstate<nextID;tstate++) {
570       origedges.add(new IntVector());
571       origtokens.add(new IntVector());
572       if (stop.containsKey( new Integer (tstate))) {
573         origstops.addInt(tstate);
574         Debug.println(3, "Adding original stop "+tstate);
575       }
576       if (update.containsKey( new Integer (tstate))) {
577         origupdate.addInt(tstate);
578         Debug.println(3, "Adding original update "+tstate);
579       }
580     };
581       };
582
583       Debug.println(2, "Original stops: "+origstops.used );
584       Debug.println(2, "Original update: "+origupdate.used );
585
586       origNstates = nextID;
587       origstart = start;
588
589       Debug.println(2, "New determinize: states created, now edges");
590
591       /* token translations - only create vectors, data will be entered
592        * on-the-fly */
593
594       {
595     int si,t;
596     int tedge;
597
598     for (si=0; si<origNstates; si++) {
599       for( t = 0 ; t < EdgeFactory.getActionTokensNum(); t ++ )
600          if( states[si][t] != null )
601         for( tedge = 0 ; tedge < states[si][t].used; tedge ++ ) {
602
603             ((IntVector)origedges.elementAt(si)).addInt( states[si][t].data[tedge]);
604             ((IntVector)origtokens.elementAt(si)).addInt(t);
605       };
606     };
607       }; /* scope block */
608       Debug.println(1,"Phase 1: "+nextID+" states");
609
610       if( Debug.debug >1 ) {
611       Debug.println( 2, "Machine representation:");
612       for( int si = 0; si < origNstates; si ++ )
613       for( int t = 0 ; t < EdgeFactory.getActionTokensNum(); t ++ )
614          if( states[si][t] != null )
615         Debug.println( 2, "State "+si+": states "+ ((IntVector)origedges.elementAt(si)).dump()+" -> tokens "+((IntVector)origtokens.elementAt(si)).dump() );
616       }
617
618       /* Phase 2: determinize the machine - create new machine in new* */
619
620        /* Note: after creating a state (the "represents" element),
621         * the array of state ids has to be sorted to allow for fast
622         * _n_-time comparision
623         */
624       /* create an empty state as the initial state of the new machine,
625        * put this state into the buffer */
626
627
628       { LinkedList buffer = new LinkedList ();
629     IntVector cedges, ctokens; /* current - being created */
630     IntVector oedges, otokens; /* old - edges and corresponding tokens
631                     * of an original state */
632
633     TreeMap altrep;
634
635     int ostates [];
636
637     newNstates = 0;
638     int npasses = 0;
639     int debugDeterminize = Integer.parseInt(System.getProperty(
640         "debugDeterminize","0"));
641     newedges = new Vector ();
642     newtokens = new Vector ();
643     represents = new Vector ();
644     altrep = new TreeMap (new IntVectorComparator());
645
646     { int a[];
647       Integer b;
648       IntVector iv;
649
650       newedges.add(new IntVector());
651       newtokens.add(new IntVector());
652       represents.add(a=new int [] { origstart } );
653       altrep.put( iv=new IntVector(a,false),b=new Integer (0));
654       if (debugDeterminize>=2) Debug.println(1,"Adding state "+iv.dump());
655       buffer.add( b );
656     };
657
658     Debug.println(1,"#tokens="+EdgeFactory.getActionTokensNum()+", origNstates="+
659         origNstates+", sizeof matrix="+EdgeFactory.getActionTokensNum()*origNstates);
660
661     int sidx1,osidx,ti;
662
663     while (! buffer.isEmpty()) {
664
665       sidx1 = ((Integer )buffer.getFirst()).intValue();
666       buffer.removeFirst();
667           if (npasses % 100 == 0)
668              Debug.println(1,"Already created "+represents.size()+" new states, [buffer]="+buffer.size());
669       npasses++;
670
671       cedges = (IntVector)newedges.elementAt(sidx1);
672       ctokens = (IntVector)newtokens.elementAt(sidx1);
673       ostates = (int [])represents.elementAt(sidx1);
674       if (debugDeterminize>=2) Debug.println(1,"Processing state "+new IntVector(ostates,false).dump());
675
676       /* [tokens] sorted { vectorids }
677         Vector [tokenId] of int[] - sized by origNstates
678
679         alternative represents:
680           sorted { sorted vectorids }
681           */
682
683       IntVector statematrix[] = new IntVector[ EdgeFactory.getActionTokensNum()];
684       for (int i=0; i<EdgeFactory.getActionTokensNum(); i++)
685         statematrix[i]=new IntVector();
686
687       /* iterate over states in represents and outgoing edges */
688       /* create Vector [tokenIDs] of IntVector [stateIDs]
689        */
690       for (int i=0; i<ostates.length; i++) {
691         osidx=ostates[i];
692         oedges = (IntVector)origedges.elementAt(osidx);
693         otokens = (IntVector)origtokens.elementAt(osidx);
694         for (int j=0; j<oedges.used; j++) {
695           ti=otokens.data[j];
696           statematrix[ti].sortedAddIntIfNExists(oedges.data[j]);
697         };
698       };
699
700       /* now, statematrix has for each tokens and new state
701        * the count of transitions to that state
702        */
703
704       /* iterate over transitions, for each check, whether a target
705        * state already exists in the new state set, create it if not
706        */
707       for (int i=0; i<EdgeFactory.getActionTokensNum(); i++) if (statematrix[i].used>0) {
708         IntVector trep = new IntVector(statematrix[i]);
709                    /* target represents */
710         int tri; /* Targer Represents Id */
711         Integer trio;
712
713         if ((trio=(Integer )altrep.get(trep))!=null) {
714           tri=trio.intValue();
715         } else {
716           /* add state */
717           tri=represents.size(); trio=new Integer (tri);
718           if (debugDeterminize>=2) Debug.println(1,"Adding state "+trep.dump());
719           altrep.put(trep,trio);
720           represents.add(trep.data);
721           newedges.add(new IntVector());
722           newtokens.add(new IntVector());
723           buffer.add(trio);
724         };
725         cedges.addInt(tri);
726         ctokens.addInt(i);
727       };
728
729     };
730       };
731       Debug.println(1,"Done phase 2: "+represents.size()+" states");
732
733       /* Phase 2s: create newstop data */
734
735       {
736     int oldstopmatrix[] = new int[origNstates];
737     int r[];
738     int i,j;
739
740
741     /* create an "hash-array" - indexed by statenumber, >0 when state is a stop-state */
742     for ( i=0;i<origstops.used;i++) oldstopmatrix[origstops.data[i]]++;
743
744     newstop=new IntVector();
745     for ( i=0;i<represents.size();i++) {
746       r=(int[])represents.elementAt(i);
747       for ( j=0;j<r.length;j++)
748         if (oldstopmatrix[r[j]]>0) {
749                   Debug.println(3, "Added new stop "+i);
750                   newstop.addInt(i); break;
751             };
752     };
753       };
754       Debug.println(1,"Done phase 2s!");
755
756       /* Phase 2u: create newupdate data */
757
758       {
759     int oldupdatematrix[] = new int[origNstates];
760     int r[];
761     int i,j;
762
763
764     /* create an "hash-array" - indexed by statenumber, >0 when state is a update-state */
765     for ( i=0;i<origupdate.used;i++) oldupdatematrix[origupdate.data[i]]++;
766
767     newupdate=new IntVector();
768     for ( i=0;i<represents.size();i++) {
769       r=(int[])represents.elementAt(i);
770       for ( j=0;j<r.length;j++)
771         if (oldupdatematrix[r[j]]>0) {
772                   Debug.println(3, "Added new update "+i);
773                   newupdate.addInt(i); break;
774             };
775     };
776       };
777       Debug.println(1,"Done phase 2u!");
778
779       /* Phase 3: create a traditional representation of new data */
780
781       {
782     states = new IntVector[represents.size()][ EdgeFactory.getActionTokensNum()];
783     allocated = nextID = represents.size();
784     marked = new boolean[allocated];
785     if( maxstates < allocated ) maxstates = allocated;
786
787     IntVector cedges,ctokens,v;
788     int i,j;
789
790     for (i=0;i < nextID ;i++) {
791       cedges = (IntVector)newedges.elementAt(i);
792       ctokens = (IntVector)newtokens.elementAt(i);
793       for (j=0;j<cedges.used;j++) {
794           v = states[i][ctokens.data[j]];
795           if( v == null ) v = states[i][ctokens.data[j]] = new IntVector();
796         Debug.println(3, "Adding edge "+i+" --"+ctokens.data[j]+"-->"+cedges.data[j]);
797           v.sortedAddIntIfNExists(cedges.data[j]);
798       }
799     };
800
801     start = 0;
802     stop = new Hashtable ();
803     update = new
804 Hashtable ();
805
806     for (i=0;i<newstop.used;i++) {
807       Integer num = new Integer ( newstop.data[i] );
808       stop.put(num, num);
809     };
810
811     for (i=0;i<newupdate.used;i++) {
812       Integer num = new Integer ( newupdate.data[i] );
813       update.put(num, num);
814     };
815
816     Print(3);
817       };
818     };
819
820
821 /**
822  * Find trace from starting state to the given state. Used for counterexample lookup.
823  * Expects that endState is reachable.
824  *
825  * @author Stanislav Visnovsky
826  * @version 2.0.0
827  * @param endState end state of the trace
828  * @return trace found
829 */
830     private String findTraceTo( int fromState, int edgetransition, int edgetarget ) {
831
832     Iterator j;
833
834     Debug.println(2, "Trying to find a trace to state "+fromState );
835
836     // cleanup
837 TidyUp();
838
839     // using BSF algorithm with recording shortest path by edges to use
840 LinkedList paths = new LinkedList ();
841     LinkedList buffer = new LinkedList ();
842     buffer.addLast( new Integer (start) );
843     paths.addLast( new LinkedList () ); // to start state is no path
844 marked[start] = true;
845     while( buffer.size() > 0 ) {
846         int current = ((Integer )buffer.removeFirst()).intValue();
847         LinkedList pathToCurrent = (LinkedList )paths.removeFirst();
848
849         Debug.println(3, "FindTrace: at state:"+current );
850         if( current == fromState ) {
851         Debug.println( 3, "Current ("+current+") is endstate");
852         
853         String trace = "";
854         
855         while( !pathToCurrent.isEmpty() ) {
856             int t = ((Integer )pathToCurrent.removeFirst()).intValue();
857             trace = trace + EdgeFactory.ActionTokens[ t ].name + ",";
858             Debug.println( 3, trace );
859         }
860         
861         trace = trace + EdgeFactory.ActionTokens[edgetransition].name;
862
863         // cleanup
864 TidyUp();
865
866         return "<"+trace+">";
867         } else {
868         Debug.println(3, "Filling buffer");
869         for( int t = 0; t < EdgeFactory.getActionTokensNum(); t++ )
870         if( states[current][t] != null ) {
871         for( int f = 0; f < states[current][t].used ; f++ )
872             if( ! marked[ states[current][t].data[f] ] ) {
873                 Debug.println(3, "Adding state "+states[current][t].data[f]+" to buffer");
874                 buffer.addLast( new Integer ( states[current][t].data[f] ) );
875                 LinkedList newpath = (LinkedList )pathToCurrent.clone();
876                 newpath.addLast( new Integer ( t ) );
877                 paths.addLast( newpath );
878                 marked[ states[current][t].data[f] ] = true;
879             }
880         }}
881     }
882
883     // cleanup
884 TidyUp();
885
886     return "Unable to find a counterexample";
887     }
888
889 /**
890  * Query the automaton, whether its language is included in other automaton
891  * given as the argument.
892  *
893  * @author Stanislav Visnovsky
894  * @version 1.0.0
895  * @param m the automaton to be compared
896  * @return null, if is included, counterexample otherwise
897 */
898     public String isIncludedIn( Machine m1 ) {
899
900     machineImpl m = (machineImpl) m1;
901
902     Debug.println( 1, "This is inclusion lookup for these automata");
903     if( Debug.debug >1 ) {
904         ((Printer)m).Print(2);
905         Debug.println(2, "and");
906         Print(2);
907     }
908
909     int max = m.nextID > nextID ? m.nextID : nextID;
910     int iso[][] = new int[ max ] [2];
911
912     Debug.println(2, "Maximal number of states: "+max );
913
914     // if this.start is stop and other start is not, wrong
915 if( (stop.containsKey( new Integer (start) ) && !m.Stop().containsKey( new Integer (m.Start() ) ) ) )
916     {
917              Debug.println( 1, "Not both of start states are/are not stop states, not included" );
918              return "NULL";
919     }
920     
921     if( (update.containsKey( new Integer (start) ) && !m.Update().containsKey( new Integer (m.Start() ) ) ) )
922     {
923              Debug.println( 1, "Not both of start states are/are not update states, not included" );
924              return "NULL";
925     }
926     
927     iso[0][0] = start;
928     iso[0][1] = m.Start();
929         Debug.print( 2, "Associating state ");
930     Debug.print( 2, start );
931     Debug.print( 2, " of machine 1 and state ");
932     Debug.print( 2, m.Start() );
933     Debug.println( 2, " of machine 2 at index 0");
934
935     int index,index2,i,nextindex = 1;
936
937     List buffer = new LinkedList ();
938     buffer.add( new Integer (0) );
939     IntVector v;
940
941     while( ! buffer.isEmpty() ) {
942         index = ((Integer )buffer.get(0)).intValue();
943         buffer.remove(0);
944         Debug.println(2,"Started new round with index "+index);
945         Debug.println(2,"Starting edge walk");
946         for( i = 0 ; i < EdgeFactory.getActionTokensNum(); i++ )
947         if( states[iso[index][0]][i] != null ) { // is there an edge for this transition from state index?
948 v = m.states[iso[index][1]][i];
949         if( v == null ) {
950            Debug.println(2,"corresponding edge not found");
951            Debug.println( 1, "edges are not equivalent, not included");
952            return findTraceTo( iso[index][0], i, states[iso[index][0]][i].data[0] );
953         }
954         // now we need determinism, i.e., in v should be only one item
955 for( index2 = 0; (index2 < nextindex ) && (iso[index2][1]!=v.data[0] ) ; index2++ );
956         Debug.println( 2, "State lookup finished at:"+index2 );
957
958                 if( (stop.containsKey(new Integer ( states[iso[index][0]][i].data[0] ) )
959           && !m.Stop().containsKey( new Integer ( v.data[0] ) ) ) )
960             {
961                     Debug.println(1, "Not both of states "+states[iso[index][0]][i].data[0]+" and " +v.data[0]+ " are/are not stop states, not included" );
962             return findTraceTo( iso[index][0], i, states[iso[index][0]][i].data[0] );
963                 }
964                 if( (update.containsKey(new Integer ( states[iso[index][0]][i].data[0] ) )
965           && !m.Update().containsKey( new Integer ( v.data[0] ) ) ) )
966             {
967                     Debug.println(1, "Not both of states "+states[iso[index][0]][i].data[0]+" and " +v.data[0]+ " are/are not update states, not included" );
968             return findTraceTo( iso[index][0], i, states[iso[index][0]][i].data[0] );
969                 }
970         if( index2 == nextindex ) {
971             iso[ nextindex ][0] = states[iso[index][0]][i].data[0];
972             iso[ nextindex ][1] = m.states[ iso[index][1]][i].data[0];
973             Debug.print( 2,"Associating state ");
974             Debug.print( 2, states[iso[index][0]][i].data[0] );
975             Debug.print( 2," of machine 1 and state ");
976             Debug.print( 2,m.states[ iso[index][1]][i].data[0]);
977             Debug.println( 2," of machine 2 at index "+nextindex);
978             buffer.add( new Integer (nextindex++) );
979         }
980          }
981     }
982     Debug.println(1,"Included");
983     return null;
984     }
985
986
987
988 /**
989  * Restrict the automaton by the set passed as the argument.
990  *
991  * @author Stanislav Visnovsky
992  * @version 2.0.0
993  * @param restrict the set of action tokens to be eliminated
994 */
995     public void Restrict( ActionTokenArray restrict ) {
996
997     int ed[];
998
999     Debug.println(1,"Starting event restriction");
1000    Print(2);
1001    Debug.println( 2,restrict.toString() );
1002
1003    // tidy up
1004 TidyUp();
1005
1006    IntVector newstates[][] = new IntVector[ allocated ][EdgeFactory.getActionTokensNum()]; // table for new states
1007
1008    // find all edges to be eliminated
1009
1010    int actual,e,target;
1011
1012    Debug.println(2,"Edges to be eliminated:");
1013    Hashtable edgesToBeEliminated = new Hashtable ();
1014    for( actual = 0; actual < nextID; actual ++ ) {
1015        Debug.println(2,"State: "+actual );
1016
1017        // identify the edges to be eliminated
1018 for( e = 0; e < EdgeFactory.getActionTokensNum(); e++ )
1019    if( states[actual][e] != null ) {
1020            if( !restrict.tokens[e] )
1021        for( target = 0; target < states[actual][e].used ; target++) {
1022            ed = new int[3];
1023            ed[0] = actual;
1024            ed[1] = e;
1025            ed[2] = states[actual][e].data[target];
1026                    edgesToBeEliminated.put(ed,ed);
1027                    Debug.print(2,"Added to be eliminated: ");
1028            Debug.print(2, actual+"--"+EdgeFactory.ActionTokens[e].name+"--> "+states[actual][e].data[target]);
1029                }
1030    }
1031    }
1032
1033    Debug.println(1,"List is completed");
1034
1035    if( Debug.debug >1 ) {
1036        Iterator edgs = edgesToBeEliminated.values().iterator();
1037        while( edgs.hasNext() ) {
1038      ed = (int[])edgs.next();
1039      Debug.println(2, ed[0]+"--"+EdgeFactory.ActionTokens[ed[1]].name+"--> "+ed[2]); }
1040        Debug.println(2,"That's all");
1041    }
1042
1043    // propagate stop states
1044
1045    Hashtable stops = new Hashtable ();
1046    Iterator nowstops = stop.values().iterator();
1047    while( nowstops.hasNext() ) {
1048    Integer s = (Integer )nowstops.next();
1049    stops.put( s, s);
1050    }
1051    
1052    int oldsize = -1;
1053    while( oldsize != stops.size() ) {
1054        
1055    Debug.println( 2,"Stop state propagation cycle" );
1056        oldsize = stops.size();
1057    
1058        Iterator ie = edgesToBeEliminated.values().iterator();
1059        while( ie.hasNext() ) {
1060
1061        ed = (int [])ie.next();
1062
1063        if( stops.containsKey( new Integer ( ed[2] ) ) ) {
1064        Integer n = new Integer ( ed[0] );
1065            Debug.print(2,"Adding stop state:"+ed[0]+" due " );
1066        Debug.println(2, ed[0]+"--"+EdgeFactory.ActionTokens[ed[1]].name+"--> "+ed[2]);
1067        stops.put( n, n );
1068        } Debug.println( 3,"State "+ed[2]+" is not stop" );
1069
1070    }
1071    }
1072
1073    Debug.println(1,"Stop state propagation done");
1074
1075    stop = stops; // use new stop states
1076
1077    // find new sets of edges
1078
1079    for( actual = 0 ; actual<nextID ; actual++ ) {
1080    Debug.println(2, "Lookup edges to be added to "+actual );
1081    eliminationClosure( actual, actual, restrict, newstates );
1082    TidyUp();
1083    }
1084
1085    states = newstates;
1086    
1087    // eliminate updates if necessary
1088 if( !restrict.tokens[1] ) update = new Hashtable ();
1089
1090    // tidy up
1091 TidyUp();
1092
1093        Reachable();
1094
1095    Debug.println(1,"Finishing event restriction");
1096    Print(2);
1097    }
1098
1099    private void eliminationClosure( int s, int addToState, ActionTokenArray edgesToSurvive, IntVector newstates[][] ) {
1100    int t,j;
1101
1102        marked[s] = true;
1103    for( t = 0; t < EdgeFactory.getActionTokensNum(); t++ )
1104    if( states[s][t] != null )
1105        for( j = 0; j < states[s][t].used; j++ ) {
1106            if( !edgesToSurvive.tokens[t] && !marked[ states[s][t].data[j] ] )
1107                eliminationClosure( states[s][t].data[j], addToState, edgesToSurvive, newstates );
1108            else
1109        if( edgesToSurvive.tokens[t] ) {
1110            Debug.print(2, "To state "+addToState+" will be added edge ");
1111            Debug.print(2, "--"+EdgeFactory.ActionTokens[t].name+"--> "+states[s][t].data[j]);
1112            if( newstates[addToState][t] == null ) newstates[addToState][t] = new IntVector();
1113            newstates[addToState][t].sortedAddIntIfNExists( states[s][t].data[j] );
1114        }
1115
1116        }
1117    }
1118
1119    public void ClearStops() {
1120    stop.clear();
1121    }
1122
1123    public void addEdge( int from, int transition, int to ) {
1124    if( states[from][transition] == null ) states[from][transition] = new IntVector();
1125    states[from][transition].sortedAddIntIfNExists( to );
1126    }
1127
1128    public void addUpdateEdge( int from ) {
1129        Integer nn = new Integer (from);
1130    update.put( nn, nn );
1131    }
1132
1133    public void TidyUp() {
1134        for( int tidy = 0; tidy < nextID; tidy++ )
1135        marked[tidy] = false;
1136
1137    }
1138
1139    private void Resize( int newsize ) {
1140    int i,j;
1141    Debug.println(2, "Trying resize to "+newsize+" states");
1142    IntVector a[][] = new IntVector[ newsize ][ EdgeFactory.getActionTokensNum() ];
1143    boolean newmarked[] = new boolean[ newsize ];
1144    for( i=0; i<allocated; i++ )
1145        for( j = 0; j < EdgeFactory.getActionTokensNum(); j++ ) {
1146        a[i][j] = states[i][j];
1147        newmarked[i] = marked[i];
1148        }
1149    states = a;
1150    marked = newmarked;
1151    allocated = newsize;
1152    if( maxstates < allocated ) maxstates = allocated;
1153    }
1154
1155    public void checkSpace( int required ) {
1156    if( required > allocated ) Resize( required );
1157    }
1158
1159    public void Merge( int to, int from ) {
1160    int j,k;
1161    for( j = 0; j< EdgeFactory.getActionTokensNum(); j++)
1162    if( states[from][j] != null ) {
1163        if( states[to][j] == null ) states[to][j] = new IntVector();
1164        for( k = 0; k < states[from][j].used; k++ )
1165        states[to][j].sortedAddIntIfNExists( states[from][j].data[k] );
1166    }
1167    }
1168
1169    public static int maxstates = 0;
1170
1171    public void Minimize() {
1172    Determinize();
1173    Reduce();
1174    }
1175    
1176    public void NonUpdateOnly() {
1177    // simply clear the list of states, from which the update event exists
1178 update = new Hashtable ();
1179    }
1180    
1181    public void UpdateOnly() {
1182    // simply clear the list of stop states. Since update states are stop states.
1183 stop = new Hashtable ();
1184    }
1185    
1186    public void StrippedUpdateOnly() {
1187    // update list becomes stop list and update list is cleared (stripping [UPDATE])
1188 stop = update;
1189    update = new Hashtable ();
1190    }
1191}
1192

A to Z: JavaDoc & Examples

---

Daily Java News & Articles

---

Open Source Projects

---

Open Source Codes

---

Free Computer Books

---

Remove Frame

---

Popular Tags