Java > Open Source Codes > SOFA > SOFAnode > Util > DFSRChecker > node > ConsentNode


1 /*
2  * $Id: ConsentNode.java,v 1.2 2005/07/08 12:04:12 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.node;
19
20 import java.util.HashMap ;
21 import java.util.LinkedList ;
22 import java.util.TreeSet ;
23 import java.util.ArrayList ;
24 import java.util.TreeMap ;
25 import java.util.Iterator ;
26
27
28 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.BadActivityException;
29 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.CheckingException;
30 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.NoActivityException;
31 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.Options;
32 import SOFA.SOFAnode.Util.DFSRChecker.state.CompositeState;
33 import SOFA.SOFAnode.Util.DFSRChecker.state.State;
34 import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPair;
35 import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPairs;
36 import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPairs.IntPair;
37 import SOFA.SOFAnode.Util.DFSRChecker.utils.AnotatedProtocol;
38
39 /**
40  * Represents the consent operator.
41  */
42 public class ConsentNode extends TreeNode {
43
44     /**
45      * ctor.
46      *
47      * @param node1
48      * node representing the first protocol to be combined via
49      * consent operator
50      * @param node2
51      * node representing the second protocol to be combined via
52      * consent operator
53      * @param events
54      * set of events on which to synchronize
55      * @param unboundEvents
56      * set of events on which to synchronize
57      * @param repository
58      * reference to action repository
59      * @param test
60      * true if testing composition errors, false when visualizing
61      */
62     public ConsentNode(TreeNode node1, TreeNode node2, TreeSet events,
63             TreeSet unboundEvents, ActionRepository repository, boolean test) {
64         super("(" + node1.protocol + ")%(" + node2.protocol + ")");
65
66         this.events = events;
67         this.unboundEvents = unboundEvents;
68         this.repository = repository;
69         this.topmost = true;
70         this.test = test;
71
72         this.nodes = new TreeNode[2];
73         this.nodes[0] = node1;
74         this.nodes[1] = node2;
75
76         // setup the topmost atribute for the children
77 if (node1 instanceof ConsentNode)
78             ((ConsentNode) node1).topmost = false;
79
80         if (node2 instanceof ConsentNode)
81             ((ConsentNode) node2).topmost = false;
82
83         this.boundEvents = new TreeSet ();
84         this.boundAtomicActions = new boolean[2][];
85         this.dependecies = new LinkedList [2];
86         this.delayed = new HashMap ();
87     }
88
89     /**
90      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getWeight()
91      */
92     public long getWeight() {
93         if (weight != -1)
94             return weight;
95         else {
96             // this is heuristic - potentially it can be a product of subtrees!
97 long w1 = nodes[0].getWeight(), w2 = nodes[1].getWeight();
98             return weight = (long) (0.5f * w1 * w2 + 0.25f * ((w1 + w2) / 2));
99         }
100     }
101
102     /**
103      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getInitial()
104      */
105     public State getInitial() {
106         State[] states = new State[2];
107         states[0] = nodes[0].getInitial();
108         states[1] = nodes[1].getInitial();
109
110         return new CompositeState(states);
111     }
112
113     /**
114      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#isAccepting(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
115      */
116     public boolean isAccepting(State state) {
117         CompositeState cstate = (CompositeState) state;
118
119         return (nodes[0].isAccepting(cstate.states[0])) && (nodes[1].isAccepting(cstate.states[1]));
120     }
121
122     /**
123      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getTransitions(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
124      */
125     public TransitionPairs getTransitions(State state) throws InvalidParameterException, CheckingException {
126         CompositeState cstate = (CompositeState) state;
127         delayed.clear();
128
129         TransitionPairs transp1 = nodes[0].getTransitions(cstate.states[0]);
130         TransitionPairs transp2 = nodes[1].getTransitions(cstate.states[1]);
131
132         TransitionPair[] trans1 = transp1.transitions;
133         TransitionPair[] trans2 = transp2.transitions;
134
135         currentdeps = new LinkedList ();
136         dependecies[0] = transp1.deps;
137         dependecies[1] = transp2.deps;
138
139         ArrayList result = new ArrayList ();
140         TreeMap sync = new TreeMap ();
141         this.boundAtomicActions[0] = new boolean[trans1.length];
142         this.boundAtomicActions[1] = new boolean[trans2.length];
143
144         //we divide the transitions of node1 (states[0]) into two groups
145 // - that of not present within the synchro events set and the others
146 for (int i = 0; i < trans1.length; ++i) {
147             Integer key = new Integer (trans1[i].eventIndex);
148
149             if (key.intValue() < 0) {
150                 //atomic event
151 if (makeAtomicTransition(i, trans1, trans2, cstate, result, 0))
152                     boundAtomicActions[0][i] = true;
153             }
154
155             else if (events.contains(new Integer (ActionRepository.getPure(trans1[i].eventIndex)))) {
156                 // the following is not necessary since we have to have the
157 // deterministic nodes below this node
158 /*
159                  * if (sync.containsKey(key))
160                  * ((ArrayList)sync.get(key)).add(trans1[i]); else { ArrayList
161                  * value = new ArrayList(); value.add(trans1[i]); sync.put(new
162                  * Integer(trans1[i].eventIndex), value); }
163                  */
164
165                 sync.put(new Integer (trans1[i].eventIndex), trans1[i]);
166                 
167                 
168                 for (Iterator it = currentdeps.iterator(); it.hasNext(); ) {
169                     IntPair item = (IntPair)it.next();
170                     
171                     if (item.second == trans1[i].eventIndex)
172                         it.remove();
173                 }
174                 
175                 delayed.put(key, null);
176             }
177
178             // check for missing binding
179 else if (topmost && unboundEvents.contains(new Integer (ActionRepository.getPure(trans1[i].eventIndex)))) {
180                 boolean isResponse = repository.isResponse(trans1[i].eventIndex);
181                 if ((Options.badactivity) && (test) && (!isResponse))
182                     throw new BadActivityException("missing binding for request '" + repository.getItemString(trans2[i].eventIndex) + "':");
183             }
184
185             // else just don't synchronize
186 else {
187                 State[] states = new State[2];
188                 states[0] = trans1[i].state;
189                 states[1] = cstate.states[1];
190
191                 result.add(new TransitionPair(trans1[i].eventIndex, new CompositeState(states)));
192             }
193         }
194
195         boundEvents.clear();
196         boundEvents.addAll(sync.keySet());
197
198         // now complete the result array
199 for (int i = 0; i < trans2.length; ++i) {
200             Integer key = new Integer (trans2[i].eventIndex);
201             if (key.intValue() < 0) {
202                 //atomic event
203 if (!boundAtomicActions[1][i])
204                     makeAtomicTransition(i, trans2, trans1, cstate, result, 1);
205             }
206
207             else if (events.contains(new Integer (ActionRepository.getPure(trans2[i].eventIndex)))) {
208                 Integer invkey = new Integer (repository.getInverseAction(trans2[i].eventIndex));
209                 if (sync.containsKey(invkey)) {
210                     /*
211                      * Iterator it = ((ArrayList)sync.get(invkey)).iterator();
212                      *
213                      * while(it.hasNext()) { State[] states = new State[2];
214                      * states[0] = ((TransitionPair)it.next()).state; states[1] =
215                      * trans2[i].state;
216                      *
217                      * result.add(new
218                      * TransitionPair(repository.getTauAction(trans2[i].eventIndex),
219                      * new CompositeState(states))); }
220                      *
221                      * boundEvents.remove(invkey);
222                      */
223
224                     State[] states = new State[2];
225                     states[0] = ((TransitionPair) sync.get(invkey)).state;
226                     states[1] = trans2[i].state;
227
228                     result.add(new TransitionPair(repository.getTauAction(trans2[i].eventIndex), new CompositeState(states)));
229                     
230                     
231                     for (Iterator it = currentdeps.iterator(); it.hasNext(); ) {
232                         IntPair item = (IntPair)it.next();
233                         
234                         if (item.second == trans2[i].eventIndex)
235                             it.remove();
236                     }
237                     
238
239                     boundEvents.remove(invkey);
240                     delayed.put(key, null);
241                 }
242
243                 else { // Bad activity detected
244 boolean isResponse = repository.isResponse(trans2[i].eventIndex);
245                     if ((Options.badactivity) && (test) && (!isResponse) && !boundAtomicActions[1][i] && (!unboundEvents.contains(new Integer (ActionRepository.getPure(trans2[i].eventIndex)))))
246                         throw new BadActivityException("bad activity(" + repository.getItemString(trans2[i].eventIndex) + "):");
247                     else {
248
249                     }
250                 }
251                 
252                 //tady
253 if (topmost && test && unboundEvents.contains(new Integer (ActionRepository.getPure(trans2[i].eventIndex))) && (!repository.isResponse(trans2[i].eventIndex))) {
254                     throw new BadActivityException("missing binding for request '" + repository.getItemString(trans2[i].eventIndex) + "':");
255                 }
256                 //tady
257 }
258             // test the missing binding
259 else if (topmost && unboundEvents.contains(new Integer (ActionRepository.getPure(trans2[i].eventIndex)))) {
260                 boolean isResponse = repository.isResponse(trans2[i].eventIndex);
261                 if ((Options.badactivity) && (test) && (!isResponse))
262                     throw new BadActivityException("missing binding for request '" + repository.getItemString(trans2[i].eventIndex) + "':");
263             }
264
265             // else just don't synchronize
266 else {
267                 State[] states = new State[2];
268                 states[0] = cstate.states[0];
269                 states[1] = trans2[i].state;
270
271                 result.add(new TransitionPair(trans2[i].eventIndex, new CompositeState(states)));
272             }
273         }
274
275         Iterator it = boundEvents.iterator();
276
277         while (it.hasNext()) {
278             int action = ((Integer ) it.next()).intValue();
279             if ((Options.badactivity) && (test) && (!repository.isResponse(action)))
280                 throw new BadActivityException("bad activity (" + repository.getItemString(action) + "):");
281         }
282         
283         // check for possible bad activities (delayed ba)
284 for (Iterator it2 = delayed.keySet().iterator(); it2.hasNext() ;) {
285             IntPair data = (IntPair)delayed.get(it2.next());
286             if (data != null)
287                 throw new BadActivityException("Bad activity (atomic action " + repository.getItemString(data.first) + " cannot accept " + repository.getItemString(repository.getInverseAction(data.second)) + "). Trace: ");
288         }
289         
290         // eliminating unbound provided operations
291 if (topmost) {
292             for (Iterator it3 = result.iterator(); it3.hasNext(); ) {
293                 if (unboundEvents.contains(new Integer (ActionRepository.getPure(((TransitionPair)it3.next()).eventIndex))))
294                     it3.remove();
295             }
296         }
297
298         TransitionPair[] result1 = new TransitionPair[result.size()];
299         Iterator it2 = result.iterator();
300         int i = 0;
301
302         while (it2.hasNext())
303             result1[i++] = (TransitionPair) it2.next();
304
305         // no activity error (=deadlock) detection
306 if (result1.length == 0) {
307             if ((Options.noactivity) && (test) && (!this.isAccepting(state))) {
308                 throw new NoActivityException("no activity:");
309             }
310         }
311         
312         if (topmost) {
313             for (int j = 0; j < result1.length; ++j) {
314                 if (result1[j].eventIndex < 0) { //atomic action
315 for (Iterator itt = currentdeps.iterator(); itt.hasNext(); ) {
316                         TransitionPairs.IntPair item = (IntPair) itt.next();
317                         if (item.first == result1[j].eventIndex) // error
318 throw new BadActivityException("Atomic action " + repository.getItemString(item.first) + " raised a bad activity exception. Trace:");
319                     }
320                     
321                 }
322                 
323             }
324         }
325
326         return new TransitionPairs(result1, currentdeps);
327     }
328
329     /**
330      * Try to make a transition over an atomic action
331      *
332      * @param index
333      * index of the action within the first atomic set
334      * @param first
335      * set of transitions of the first component
336      * @param second
337      * the set of the transitions of the other component
338      * @param result
339      * the list for addding the possible transitions
340      * @return true if first[index] can be bound to one or more inverse atomic
341      * actions
342      */
343     private boolean makeAtomicTransition(int index, TransitionPair[] first,
344             TransitionPair[] second, CompositeState starting, ArrayList result,
345             int tooglebit) throws BadActivityException {
346
347         LinkedList trans = makeTransition(index, first, second, starting, tooglebit);
348
349         if (trans.size() > 0) {
350             result.addAll(trans);
351             return true;
352         } else
353             return false;
354     }
355
356     /**
357      * Try to make a transitive closure of atomic action to satisfy its
358      * requirement
359      *
360      * @param index
361      * index of the atomic action within the first set to be
362      * performed
363      * @param first
364      * the set of possible transitions of the first component
365      * @param second
366      * the set of possible transitions of the second component
367      * @return list of possible transitions over this atomic action
368      */
369     private LinkedList makeTransition(int index, final TransitionPair[] first, final TransitionPair[] second, CompositeState starting, int tooglebit) throws BadActivityException {
370         int atomicactionindex = first[index].eventIndex;
371         final AtomicAction aaction = repository.getAtomicEvents(atomicactionindex);
372         AtomicAction synchroaction = new AtomicAction();
373         LinkedList result = new LinkedList ();
374         LinkedList nosynchro = new LinkedList ();
375         boolean bound = false;
376         boolean boundsimple = false;
377         AtomicAction newaa = null;
378
379         Iterator it = aaction.iterator();
380
381         while (it.hasNext()) {
382             Integer event = (Integer ) it.next();
383
384             if (events.contains(new Integer (ActionRepository.getPure(event.intValue()))))
385                 synchroaction.add(event);
386             else
387                 nosynchro.add(event);
388         }
389
390         //check if the atomic action is well formed - i.e. contains only one
391 // simple action for this binding
392 if (synchroaction.size() > 1)
393             //not well formed!
394 throw new BadActivityException("Atomic action not well-formed (" + repository.getItemString(first[index].eventIndex) + ") - contains more than 1 simple action on a binding. Trace: ");
395
396         // no synchro on this binding
397 if (synchroaction.size() == 0) {
398             State[] states = new State[2];
399             states[tooglebit] = first[index].state;
400             states[1 - tooglebit] = starting.states[1 - tooglebit];
401             result.add(new TransitionPair(first[index].eventIndex, new CompositeState(states)));
402             
403             // keep all items with transition within the dependency list
404 for (Iterator it2 = dependecies[tooglebit].iterator(); it2.hasNext(); ) {
405                 TransitionPairs.IntPair item = (TransitionPairs.IntPair)it2.next();
406                 if (item.first == first[index].eventIndex)
407                     currentdeps.add(item);
408             }
409             return result;
410         }
411
412         else {
413
414             int synchroactionidx = ((Integer ) synchroaction.first()).intValue();
415     
416             for (int i = 0; i < second.length; ++i) {
417                 if ((tooglebit == 1) && boundAtomicActions[0][i])
418                     continue;
419     
420                 if (second[i].eventIndex >= 0) { //single action - no atomic
421 // action
422 if (synchroactionidx == repository.getInverseAction(second[i].eventIndex)) {
423                         //bound
424 newaa = new AtomicAction(aaction);
425                         newaa.remove(new Integer (synchroactionidx));
426                         newaa.add(new Integer (repository.getTauAction(synchroactionidx)));
427                         State[] states = new State[2];
428                         states[tooglebit] = first[index].state;
429                         states[1 - tooglebit] = second[i].state;
430                         result.add(new TransitionPair(repository.getItemIndex(newaa), new CompositeState(states)));
431                         
432                         /*
433                         for (Iterator it2 = dependecies[tooglebit].iterator(); it2.hasNext(); ) {
434                             TransitionPairs.IntPair item = (TransitionPairs.IntPair)it2.next();
435                             if (item.first == first[index].eventIndex) {
436                                 item.first = repository.getItemIndex(newaa);
437                                 currentdeps.add(item);
438                             }
439                         }
440
441                         if (repository.isResponse(synchroactionidx))
442                             currentdeps.add(new TransitionPairs.IntPair(first[index].eventIndex, synchroactionidx));
443                          */
444                         
445                         boundAtomicActions[1 - tooglebit][i] = true;
446                         bound = true;
447                         boundsimple = true;
448                     }
449     
450                     else if (repository.isResponse(synchroactionidx)) {
451                         //bad activity may occur here, but cannot find out now,
452 // cache the information
453 currentdeps.add(new TransitionPairs.IntPair(first[index].eventIndex, second[i].eventIndex));
454                     }
455     
456                 } else { // atomic action
457 newaa = new AtomicAction(repository.getAtomicEvents(second[i].eventIndex));
458     
459                     Iterator it2 = repository.getAtomicEvents(second[i].eventIndex).iterator();
460     
461                     while (it2.hasNext()) {
462                         Integer event = (Integer ) it2.next();
463                         AtomicAction bounding = new AtomicAction(repository.getAtomicEvents(event.intValue()));
464                         boolean was = bounding.remove(new Integer (repository.getInverseAction(synchroactionidx)));
465     
466                         if (was) {
467                             newaa.remove(new Integer (synchroactionidx));
468                             newaa.add(new Integer (repository.getTauAction(synchroactionidx)));
469                             newaa.addAll(bounding);
470                             State[] states = new State[2];
471                             states[tooglebit] = first[index].state;
472                             states[1 - tooglebit] = second[i].state;
473                             result.add(new TransitionPair(repository.getItemIndex(newaa), new CompositeState(states)));
474                             bound = true;
475                             boundAtomicActions[1 - tooglebit][i] = true;
476
477                             /*
478                             for (Iterator it3 = dependecies[tooglebit].iterator(); it3.hasNext(); ) {
479                                 TransitionPairs.IntPair item = (TransitionPairs.IntPair)it3.next();
480                                 if (item.first == first[index].eventIndex) {
481                                     item.first = repository.getItemIndex(newaa);
482                                     currentdeps.add(item);
483                                 }
484                             }
485
486                             for (Iterator it3 = dependecies[1-tooglebit].iterator(); it3.hasNext(); ) {
487                                 TransitionPairs.IntPair item = (TransitionPairs.IntPair)it3.next();
488                                 if (item.first == event.intValue()) {
489                                     item.first = repository.getItemIndex(newaa);
490                                     currentdeps.add(item);
491                                 }
492                             }
493                             */
494
495                             break; // only one simple action can be bound at this binding
496 }
497                     }
498                 }
499             }
500             
501             if (!bound) {
502                 if (repository.isResponse(synchroactionidx)) {
503                     for (Iterator iterator = currentdeps.iterator(); iterator.hasNext() ;) {
504                         TransitionPairs.IntPair item = (TransitionPairs.IntPair)iterator.next();
505                         
506                         if (item.first == first[index].eventIndex) {
507                             if (repository.isResponse(item.second)) {
508                                 if (!delayed.containsKey(new Integer (item.second)))
509                                     delayed.put(new Integer (item.second), item);
510                                         
511                                 //throw new BadActivityException("Bad activity (atomic action " + repository.getItemString(first[index].eventIndex) + " cannot accept " + repository.getItemString(repository.getInverseAction(item.second)) + "). Trace: ");
512 } else {
513                                 iterator.remove();
514                                 delayed.put(new Integer (item.second), null);
515                             }
516                         }
517                     }
518
519                     return result;
520                 }
521                 else { // unbound request!
522
523                     for (Iterator it2 = dependecies[tooglebit].iterator(); it2.hasNext(); ) {
524                         TransitionPairs.IntPair item = (TransitionPairs.IntPair)it2.next();
525                         if (item.first == first[index].eventIndex) {
526                             item.first = repository.getItemIndex(newaa); // that should work
527 currentdeps.add(item);
528                         }
529                     }
530
531                     result.add(new TransitionPair(first[index].eventIndex, null));
532                     currentdeps.add(new TransitionPairs.IntPair(first[index].eventIndex, synchroactionidx));
533                     return result;
534                 }
535             }
536             else
537                 return result;
538         }
539     }
540
541     /**
542      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getTypeName()
543      */
544     public String [] getTypeName() {
545         String [] result = { "Consent", "%" };
546         return result;
547     }
548
549     /**
550      *
551      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#forwardCut(java.util.TreeSet)
552      */
553     public TreeNode forwardCut(TreeSet livingevents) {
554         TreeSet exlivev = new TreeSet (livingevents);
555
556         exlivev.addAll(events);
557         TreeSet exlivev2 = new TreeSet (exlivev);
558
559         nodes[0] = nodes[0].forwardCut(exlivev);
560         nodes[1] = nodes[1].forwardCut(exlivev2);
561
562         if (nodes[0] == null)
563             nodes[0] = new NullNode();
564
565         if (nodes[1] == null)
566             nodes[1] = new NullNode();
567
568         return this;
569     }
570
571     /**
572      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getAnotatedProtocol(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
573      */
574     public AnotatedProtocol getAnotatedProtocol(State state) {
575         CompositeState cstate = (CompositeState) state;
576         int nodecnt = nodes.length;
577         String result = new String ();
578         ArrayList indicesresult = new ArrayList ();
579
580         for (int i = 0; i < nodecnt; ++i) {
581             AnotatedProtocol subresult = nodes[i].getAnotatedProtocol((cstate != null) ? cstate.states[i] : null);
582
583             for (int j = 0; j < subresult.indices.size(); ++j)
584                 indicesresult.add(new Integer (((Integer ) subresult.indices.get(j)).intValue() + result.length()));
585
586             result += subresult.protocol;
587
588             if (i < nodecnt - 1)
589                 result += " % ";
590         }
591
592         return new AnotatedProtocol(result, indicesresult);
593     }
594
595     //--------------------------------------------------------------------------
596
597     /**
598      * The set of synchronizing events for the consent operator
599      */
600     final private TreeSet events;
601
602     /**
603      * The set of events on unbound interfaces
604      */
605     final private TreeSet unboundEvents;
606
607     /**
608      * Action repository for seeking the tau and other event indices
609      */
610     private ActionRepository repository;
611
612     /**
613      * Flag for the topmost consent operator. This is necessary for bad activity
614      * detection
615      */
616     private boolean topmost;
617
618     /**
619      * Determines whether the tree is intended for testing or visualization
620      */
621     private boolean test;
622
623     /**
624      * Set of already bound events
625      */
626     private TreeSet boundEvents;
627
628     /**
629      * Indices of bound atomic actions within the first sequence
630      */
631     private boolean[][] boundAtomicActions;
632     
633     /**
634      * Dependencies for atomic actions from subtrees
635      */
636     private LinkedList [] dependecies;
637
638     /**
639      * atomic action dependecies
640      */
641     private LinkedList currentdeps;
642     
643     /**
644      * Delayed bad ectivity exceptions
645      */
646     private HashMap delayed;
647 }

A to Z: JavaDoc & Examples

---

Daily Java News & Articles

---

Open Source Projects

---

Open Source Codes

---

Free Computer Books

---

Remove Frame

---

Popular Tags