DFSRTraverser


1   /*
2    * $Id: DFSRTraverser.java,v 1.4 2005/07/08 12:04:11 kofron Exp $
3    * 
4    * Copyright 2004
5    *    Distributed Systems Research Group
6    *    Department of Software Engineering
7    *    Faculty of Mathematics and Physics
8    *    Charles University, Prague
9    *
10   * Copyright 2005
11   *    Formal Methods In Software Engineering Group
12   *    Institute of Computer Science
13   *    Academy of Sciences of the Czech Republic
14   * 
15   * This code was developed by Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
16   */
17  
18  package SOFA.SOFAnode.Util.DFSRChecker.DFSR;
19  
20  import java.util.Stack  ;
21  import java.util.Iterator  ;
22  
23  import SOFA.SOFAnode.Util.DFSRChecker.node.ActionRepository;
24  import SOFA.SOFAnode.Util.DFSRChecker.node.InvalidParameterException;
25  import SOFA.SOFAnode.Util.DFSRChecker.node.TreeNode;
26  import SOFA.SOFAnode.Util.DFSRChecker.parser.Debug;
27  import SOFA.SOFAnode.Util.DFSRChecker.state.Signature;
28  import SOFA.SOFAnode.Util.DFSRChecker.state.State;
29  import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPair;
30  
31  
32  /**
33   * DFSR traverser performs the traversing of the graph generated by the given parse tree. 
34   * It uses the DFS with Replacement algorithm.
35   */
36  public class DFSRTraverser {
37  
38      /**
39       * Creates a new instance of DFSRTraverser.
40       * 
41       * @param node the root of the parse tree
42       * @param repository the action repository for printing the action names.
43       */
44      public DFSRTraverser(TreeNode node, ActionRepository repository) {
45          this.node = node;
46  
47          if ((Options.action == Options.ACTIONTESTCOMPLIANCE) || (Options.action == Options.ACTIONTESTCONSENT)) { 
48              //heuristics - a signature takes approximatelly 100B of memory
49                  this.globalCache = new StateCache(Options.statememory * (100000 / Signature.getSize()));
50          } else
51              this.globalCache = new StateCache(0);
52  
53          this.pathCache = new StateCache(0);
54          this.pathStack = new Stack  ();
55          this.repository = repository;
56          this.secondStage = false;
57      }
58  
59      /**
60       * Performs the traversing through the graph and calling the appropriate methods of the given backend.
61       * 
62       * @param implementation the backend (either consent or visualization.
63       * 
64       * @throws CheckingException in the case a composition error is found
65       */
66      public void run(IDFSRExtension implementation) throws InvalidParameterException, ItemAlreadyPresentException, ItemNotPresentException, CheckingException {
67          Stack   poppedstack = new Stack  ();
68          long statecnt = 1;
69          State newstate;
70          // initialization of the traversing
71          newstate = node.getInitial();
72          TransitionPair[] inittrans = null;
73          boolean popflag = false;
74          /*
75          try {
76              inittrans = node.getTransitions(initstate);
77          } catch (CheckingException e) { // an accepting state found while
78                                          // checking compliance
79              throw e.addMessage("<initial state>");
80          }
81          */
82  
83          pathStack.push(new DFSRPathItem(-1, inittrans, newstate));
84          pathCache.insert(newstate.getSignature());
85          globalCache.insert(newstate.getSignature());
86          //Debug.println(2, "state signature: " + initstate.getSignature());
87  
88          // action for the first state
89          implementation.action(newstate);
90  
91          try {
92              implementation.actionNew(newstate);
93          } catch (AcceptingStateException e) {
94              throw new AcceptingStateException("<initial state>");
95          }
96          
97          Debug.print(3, "(S0) ");
98  
99          // main cycle of the traversing
100         try {
101 
102             while (pathStack.size() > 0) {
103                 DFSRPathItem currentstatetuple = (DFSRPathItem) pathStack.peek();
104                 //Debug.println("state: " + statecnt++);
105                 
106                 TransitionPair[] transitions = node.getTransitions(currentstatetuple.state).transitions;
107     
108                 // initialize the count of possible transitions
109                 if (currentstatetuple.stateIndex == -1) 
110                     currentstatetuple.stateIndex = transitions.length;
111                     
112                 if (popflag && (currentstatetuple.stateIndex < transitions.length)) {
113                     Debug.println(3, repository.getItemString(transitions[currentstatetuple.stateIndex].eventIndex) + " ");
114                     popflag = false;
115                 }
116     
117                 // we decrease the index of active transition
118                 if (currentstatetuple.stateIndex > 0) {
119                     currentstatetuple.stateIndex--;
120     
121                     newstate = transitions[currentstatetuple.stateIndex].state;
122                     
123                     Debug.print(3, repository.getItemString(transitions[currentstatetuple.stateIndex].eventIndex) + " ");
124                     Debug.print(3, "\n(S" + statecnt + ") ");
125                     if ((statecnt & 1023) == 0) {
126                         Debug.println(2, Long.toString(statecnt));
127                         Debug.println(2, "Stack size:" + pathStack.size());
128                     }
129     
130                     // we've found a cycle
131                     if (pathCache.isPresent(newstate.getSignature())) {
132                         Debug.print(3, "cycle - staying current - ");
133                         implementation.action(newstate);
134                         if (Options.infiniteactivity != Options.IANO) {
135                             
136                             Iterator   it = pathStack.iterator();
137                             Signature sig = newstate.getSignature();
138                             State stackstate = null;
139                             int stateindex = 0;
140                             while (it.hasNext()) {
141                                 stackstate = ((DFSRPathItem) it.next()).state;
142                                 if (sig.equals(stackstate.getSignature()))
143                                     break;
144                                 ++stateindex;
145                             }
146                             
147                             Debug.println(3, stackstate.label);
148                             
149                             if ((Options.infiniteactivity == Options.IAYES) && secondStage) {
150                                 completeStack(pathStack,stateindex);
151                                 ((DFSRPathItem)pathStack.peek()).transitions = node.getTransitions(((DFSRPathItem)pathStack.peek()).state).transitions;
152             
153                                 stackstate.cycleTrace = getStack(pathStack, stateindex) + "(" + stackstate.label + ")";
154                             }
155                             
156                             implementation.actionCycle(stackstate);
157                             
158                             long oldid = currentstatetuple.state.getSignature().getCycleId();
159                             long newid = stackstate.getSignature().getCycleId();
160                             
161                             if ((oldid == Long.MAX_VALUE) || (oldid > newid)) {
162                                 currentstatetuple.state.getSignature().setCycleId(newid);
163                                 currentstatetuple.state.cycleStart = false;
164                                 globalCache.updateItem(currentstatetuple.state.getSignature());
165                             }
166                             
167                             if (stateindex == pathStack.size())
168                                 stackstate.cycleStart = false;
169                             
170                             if (!currentstatetuple.state.isAcceptingReachable() && (Options.infiniteactivity != Options.IANO)) {
171                                 if (globalCache.acceptingReach(newstate.getSignature())) {
172                                     currentstatetuple.state.getSignature().setAcceptingReachable(true);
173                                     globalCache.setAcceptingReach(currentstatetuple.state.getSignature());
174                                 }
175                             }
176                             
177                                 
178                         }
179     
180                     }
181     
182                     // an already visited node is visiting again
183                     else if (globalCache.isPresent(newstate.getSignature())) {
184                         Debug.print(3, "back - ");
185                         Debug.print(3, newstate.getSignature().toString());
186                         implementation.action(newstate);
187                         implementation.actionVisited(newstate);
188                         if (Options.infiniteactivity != Options.IANO) {
189                             if (!currentstatetuple.state.isAcceptingReachable() && (Options.infiniteactivity != Options.IANO)) {
190                                 if (globalCache.acceptingReach(newstate.getSignature())) {
191                                     currentstatetuple.state.getSignature().setAcceptingReachable(true);
192                                     globalCache.setAcceptingReach(currentstatetuple.state.getSignature());
193                                     Debug.print(3, " accepting - ");
194                                 }
195                             }
196                             
197                             long oldid = currentstatetuple.state.getSignature().getCycleId();
198                             long newid = globalCache.getCycleId(newstate.getSignature());
199                             
200                             if ((oldid == Long.MAX_VALUE) || (oldid > newid)) {
201                                 currentstatetuple.state.getSignature().setCycleId(newid);
202                                 currentstatetuple.state.cycleStart = false;
203                                 globalCache.updateItem(currentstatetuple.state.getSignature());
204                             }
205                         }
206                         Debug.println(3);
207                     }
208     
209                     // a new node found (or a node removed from the global cache
210                     // because of the memory amount used)
211                     else {
212                         statecnt++;
213                         Debug.print(3, newstate.getSignature().toString());
214                         implementation.action(newstate);
215     
216                             boolean isAccepting = false;
217                             if (implementation.actionNew(newstate)) {
218                                 newstate.getSignature().setAcceptingReachable(true);
219                                 isAccepting = true;
220                                 Debug.print(3, "accepting - ");
221                             }
222     
223     
224                             // creating the new stackitem
225                             //TransitionPair[] newtrans = node.getTransitions(newstate);
226     
227                             DFSRPathItem newitem = new DFSRPathItem(-1, null, newstate);
228                             pathStack.push(newitem);
229                             //newstate.createSignature();
230                             pathCache.insert(newstate.getSignature());
231                             globalCache.insert(newstate.getSignature());
232                             if ((Options.infiniteactivity != Options.IANO) && isAccepting)
233                                 globalCache.updateItem(newstate.getSignature());
234     
235                     }
236                 }
237     
238                 // all path from current node were explored
239                 else {
240                     popflag = true;
241                     State current = currentstatetuple.state;
242                     implementation.actionBack(current);
243     
244                     pathStack.pop();
245     
246                     if (pathStack.size() > 0) {
247                         
248                         if (Options.infiniteactivity != Options.IANO) {
249                             State above = ((DFSRPathItem) pathStack.peek()).state;
250                             
251                             Debug.print(3, current.isAcceptingReachable() ? "pop: accepting - " : "pop:not accepting - ");
252                             Debug.print(3, current.label + " " + current.getSignature().toString() + " - ");
253                             /*
254                             if (transitions.length > 0)
255                                 Debug.println(3, repository.getItemString(transitions[0].eventIndex));
256                             */
257         
258                             if (current.cycleStart && Options.action != Options.ACTIONVISUALIZE) {
259                                 if (!current.isAcceptingReachable()) {
260                                      if (!secondStage && Options.infiniteactivity == Options.IAYES) {
261                                         popflag = false;
262                                         Debug.println(2, "Infinite activity detected, reconstructing cycle trace");
263                                         Debug.println(3, "Stack size: " + pathStack.size());
264                                         Stack   tmp = (Stack  )pathStack.clone();
265                                         completeStack(tmp, 0);
266                                         ((DFSRPathItem)tmp.peek()).transitions = node.getTransitions(((DFSRPathItem)tmp.peek()).state).transitions;
267                                         
268                                         System.out.print("Prefix: " + getStack(shortenStack(tmp), 0));
269                                         
270                                         secondStage = true;
271                                         currentstatetuple.stateIndex = -1;
272                                         pathStack.push(currentstatetuple);
273                                         globalCache.clear();
274                                         pathCache.clear();
275                                         implementation.reset();
276                                         
277                                         for (int i = 0; i < pathStack.size(); ++i) {
278                                             Signature sig = ((DFSRPathItem)pathStack.get(i)).state.getSignature();
279                                             globalCache.insert(sig);
280                                             pathCache.insert(sig);
281                                             implementation.actionNew(((DFSRPathItem)pathStack.get(i)).state);
282                                         }
283                                         
284                                     }
285                                     else 
286                                     {
287                                         node.getAnotatedProtocol(current).prettyPrint(true);
288                                         completeStack(pathStack, 0);
289                                         
290                                         ((DFSRPathItem)pathStack.peek()).transitions = node.getTransitions(((DFSRPathItem)pathStack.peek()).state).transitions;
291                                         
292                                         System.out.println('(' + current.label + ')' + "\nCycle: " + (Options.infiniteactivity == Options.IAYES ? current.cycleTrace : "cycle trace no available, run with --infiniteactivity=yes"));
293                                         throw new InfiniteActivityException("divergence.");
294                                     }
295                                 }
296                             } else {
297                                 long aboveid = above.getSignature().getCycleId();
298                                 long currentid = current.getSignature().getCycleId();
299                                 if (((aboveid == Long.MAX_VALUE) || (aboveid > currentid)) && (currentid != Long.MAX_VALUE)) {
300                                     above.getSignature().setCycleId(currentid);
301                                     above.cycleStart = false;
302                                     poppedstack.push(currentstatetuple);
303                                 }
304                             }
305                             
306                             if (!above.isAcceptingReachable() && current.isAcceptingReachable()) {
307                                     above.getSignature().setAcceptingReachable(true);
308                                     globalCache.updateItem(above.getSignature());
309                             }
310                         }
311                     }
312     
313                     if (popflag)
314                         pathCache.remove(currentstatetuple.state.getSignature());
315                     // the node should stay in the global cache for now
316                     
317                     popflag = true;
318                 }
319                 
320     
321             }
322             Debug.println(statecnt + " states visited.");
323 
324         }
325         catch (InfiniteActivityException e) {
326             Debug.println(statecnt + " states visited (some of them are counted more than once).");
327             node.getAnotatedProtocol(newstate).prettyPrint(true);
328             throw e;
329         } 
330         catch (CheckingException e) { // an accepting state found while checking compliance
331             //pathStack.push(new DFSRPathItem(0, new TransitionPair[0], newstate));
332             Debug.println(statecnt + " states visited.");
333             node.getAnotatedProtocol(newstate).prettyPrint(true);
334             
335             completeStack(pathStack, 0);
336             
337             throw e.addMessage(getStack(shortenStack(pathStack), 0));
338         }
339 
340     }
341 
342     /**
343      * @return the action sequence stored at the stack
344      */
345     private String   getStack(Stack   stack, int from) {
346         String   result = new String  ("\n");
347         
348         if (stack.size() == 1)
349             return ("<initial state>");
350         else {
351 
352             for (int i = from; i < stack.size(); ++i) {
353                 DFSRPathItem item = (DFSRPathItem) stack.get(i);
354                 result += "(" + item.state.label + ")";
355                 if ((item.stateIndex >= 0) && (item.transitions.length > 0) && (item.stateIndex < item.transitions.length))
356                     result += " " + repository.getItemString(item.transitions[item.stateIndex].eventIndex) + " \n";
357                 
358             }
359     
360             return result;
361         }
362     }
363 
364     /**
365      * Optimizes the stack listing by omitting those transitions that are not
366      * necessary (omitting "cycles")
367      * 
368      * @return eventually shortened trace
369      */
370     private Stack   shortenStack(Stack   stack) {
371         // the main cycle from the stack top to the bottom
372         int i = stack.size() - 1;
373         while (i > 0) {
374             State higherstate = ((DFSRPathItem) stack.get(i)).state;
375             int j = 0;
376             while (j < i - 1) {
377                 DFSRPathItem lower = (DFSRPathItem) stack.get(j);
378                 int transcnt = lower.transitions.length;
379                 for (int k = 0; k < transcnt; ++k) {
380                     if (lower.transitions[k].state.equals(higherstate)) { // we
381                                                                           // found
382                                                                           // a
383                                                                           // "cycle"
384                         for (int l = i - 1; l > j; --l) {
385                             stack.removeElementAt(l);
386                         }
387 
388                         lower.stateIndex = k;
389                         i = j;
390                         j = -1;
391                         break;
392                     }
393                 }
394                 ++j;
395             }
396             --i;
397         }
398 
399         return stack;
400     }
401     
402     /**
403      * Regenerates all transitions for state at stack.
404      * @param stack the stack
405      */
406     private void completeStack(Stack   stack, int stateindex) {
407         for (int i = stateindex; i < stack.size() - 1; ++i) {
408             DFSRPathItem item = (DFSRPathItem)stack.get(i);
409             try {
410                 item.transitions = node.getTransitions(item.state).transitions;
411             }
412             catch (CheckingException e) {
413                 System.out.println("Internal checker error");
414             }
415             catch (InvalidParameterException e) {
416                 System.out.println("Internal checker error");
417             }
418         }
419     }
420 
421     /**
422      * Initial node of the traversing
423      */
424     private TreeNode node;
425 
426     /**
427      * The cache for storing already globally visited states.
428      */
429     private StateCache globalCache;
430 
431     /**
432      * The cache for the stack of actual traversal path for fast lookup.
433      */
434     private StateCache pathCache;
435 
436     /**
437      * The stack for storing the actual path.
438      */
439     private Stack   pathStack;
440 
441     /**
442      * Action repository
443      */
444     private ActionRepository repository;
445     
446     /**
447      * Flag for denoting the stage phase when reporting the infinite activity
448      */
449     private boolean secondStage;
450 
451 }
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags