KickJava   Java API By Example, From Geeks To Geeks.

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


1 /*
2  * $Id: CompositionNode.java,v 1.4 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.TreeSet JavaDoc;
21 import java.util.ArrayList JavaDoc;
22 import java.util.Iterator JavaDoc;
23 import java.util.TreeMap JavaDoc;
24
25 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.CheckingException;
26 import SOFA.SOFAnode.Util.DFSRChecker.state.CompositeState;
27 import SOFA.SOFAnode.Util.DFSRChecker.state.State;
28 import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPair;
29 import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPairs;
30 import SOFA.SOFAnode.Util.DFSRChecker.utils.AnotatedProtocol;
31
32
33 /**
34  * Represents the old composition operator.
35  */
36 public class CompositionNode extends TreeNode {
37
38     /** Creates a new instance of CompositionNode */
39     public CompositionNode(TreeNode node1, TreeNode node2, TreeSet JavaDoc events, ActionRepository repository) {
40         //super(getUnion(node1, node2));
41 super("(" + node1.protocol + ")&(" + node2.protocol + ")");
42         this.events = events;
43         this.repository = repository;
44
45         this.nodes = new TreeNode[2];
46         this.nodes[0] = node1;
47         this.nodes[1] = node2;
48     }
49
50     /**
51      *
52      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getInitial()
53      */
54     public State getInitial() {
55         State[] states = new State[2];
56         states[0] = nodes[0].getInitial();
57         states[1] = nodes[1].getInitial();
58
59         return new CompositeState(states);
60     }
61
62     /**
63      *
64      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#isAccepting(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
65      */
66     public boolean isAccepting(State state) {
67         CompositeState cstate = (CompositeState) state;
68
69         return (nodes[0].isAccepting(cstate.states[0])) && (nodes[1].isAccepting(cstate.states[1]));
70     }
71
72     /**
73      *
74      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getTransitions(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
75      */
76     public TransitionPairs getTransitions(State state) throws InvalidParameterException, CheckingException {
77         CompositeState cstate = (CompositeState) state;
78
79         TransitionPair[] trans1 = nodes[0].getTransitions(cstate.states[0]).transitions;
80         TransitionPair[] trans2 = nodes[1].getTransitions(cstate.states[1]).transitions;
81
82         ArrayList JavaDoc result = new ArrayList JavaDoc();
83         TreeMap JavaDoc sync = new TreeMap JavaDoc();
84
85         //we divide the transitions of node1 (states[0]) into two groups
86 // - that of not present within the events set and the others
87 for (int i = 0; i < trans1.length; ++i) {
88             Integer JavaDoc key = new Integer JavaDoc(trans1[i].eventIndex);
89
90             if (events.contains(new Integer JavaDoc(ActionRepository.getPure(trans1[i].eventIndex))))
91                 if (sync.containsKey(key))
92                     ((ArrayList JavaDoc) sync.get(key)).add(trans1[i]);
93                 else {
94                     ArrayList JavaDoc value = new ArrayList JavaDoc();
95                     value.add(trans1[i]);
96                     sync.put(new Integer JavaDoc(trans1[i].eventIndex), value);
97                 }
98             else {
99                 State[] states = new State[2];
100                 states[0] = trans1[i].state;
101                 states[1] = cstate.states[1];
102
103                 result.add(new TransitionPair(trans1[i].eventIndex, new CompositeState(states)));
104             }
105         }
106
107         // now complete the result array
108 for (int i = 0; i < trans2.length; ++i) {
109             Integer JavaDoc key = new Integer JavaDoc(trans2[i].eventIndex);
110             if (events.contains(new Integer JavaDoc(ActionRepository.getPure(trans2[i].eventIndex)))) {
111                 Integer JavaDoc invkey = new Integer JavaDoc(repository.getInverseAction(trans2[i].eventIndex));
112                 if (sync.containsKey(invkey)) {
113                     Iterator JavaDoc it = ((ArrayList JavaDoc) sync.get(invkey)).iterator();
114
115                     while (it.hasNext()) {
116                         State[] states = new State[2];
117                         states[0] = (State) it.next();
118                         states[1] = trans2[i].state;
119
120                         result.add(new TransitionPair(repository.getTauAction(trans2[i].eventIndex), new CompositeState(states)));
121                     }
122                 }
123             } else {
124                 State[] states = new State[2];
125                 states[0] = cstate.states[0];
126                 states[1] = trans2[i].state;
127
128                 result.add(new TransitionPair(trans2[i].eventIndex, new CompositeState(states)));
129             }
130
131         }
132
133         TransitionPair[] result1 = new TransitionPair[result.size()];
134         Iterator JavaDoc it = result.iterator();
135         int i = 0;
136
137         while (it.hasNext())
138             result1[i++] = (TransitionPair) it.next();
139
140         return new TransitionPairs(result1);
141
142     }
143
144     /**
145      *
146      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getWeight()
147      */
148     public long getWeight() {
149         if (weight != -1)
150             return weight;
151         else {
152             return weight = nodes[0].getWeight() * nodes[1].getWeight();
153         }
154     }
155
156     /**
157      *
158      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#forwardCut(java.util.TreeSet)
159      */
160     public TreeNode forwardCut(TreeSet JavaDoc livingevents) {
161         TreeSet JavaDoc exlivev = new TreeSet JavaDoc(livingevents);
162
163         exlivev.addAll(events);
164         TreeSet JavaDoc exlivev2 = new TreeSet JavaDoc(exlivev);
165
166         nodes[0] = nodes[0].forwardCut(exlivev);
167         nodes[1] = nodes[1].forwardCut(exlivev2);
168
169         if ((nodes[0] == null) || (nodes[1] == null))
170             return null;
171
172         else
173             return this;
174     }
175
176     /**
177      * @return the symbolic name of the treenode denoting its type
178      */
179     public String JavaDoc[] getTypeName() {
180         String JavaDoc[] result = { "Composition", "&" };
181         return result;
182     }
183
184
185     /**
186      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getAnotatedProtocol(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
187      */
188     public AnotatedProtocol getAnotatedProtocol(State state) {
189         throw new RuntimeException JavaDoc(this.getClass().getName() + ".getAnotatedProtocol is not implemented");
190     }
191
192
193     
194     //--------------------------------------------------------------------------
195
196     /**
197      * The set of event for composition operator
198      */
199     final private TreeSet JavaDoc events;
200
201     /**
202      * Action repository for seeking the tau and other event indices
203      */
204     private ActionRepository repository;
205
206 }
Popular Tags