KickJava   Java API By Example, From Geeks To Geeks.

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


1 /*
2  * $Id: RestrictionNode.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.Stack JavaDoc;
22 import java.util.ArrayList JavaDoc;
23 import java.util.Iterator JavaDoc;
24
25 import SOFA.SOFAnode.Util.DFSRChecker.DFSR.CheckingException;
26 import SOFA.SOFAnode.Util.DFSRChecker.state.State;
27 import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPair;
28 import SOFA.SOFAnode.Util.DFSRChecker.state.TransitionPairs;
29 import SOFA.SOFAnode.Util.DFSRChecker.utils.AnotatedProtocol;
30
31 /**
32  * This class represents the Restriction operator
33  */

34 public class RestrictionNode extends TreeNode {
35
36     /** Creates a new instance of RestrictionNode */
37     public RestrictionNode(TreeNode node, TreeSet JavaDoc restriction,
38             ActionRepository repository) {
39         super("(" + node.protocol + ")\\\\{" + getRestr(restriction, repository) + "}");
40         this.restriction = restriction;
41
42         this.nodes = new TreeNode[1];
43         this.nodes[0] = node;
44
45     }
46
47     /**
48      *
49      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getInitial()
50      */

51     public SOFA.SOFAnode.Util.DFSRChecker.state.State getInitial() {
52         return nodes[0].getInitial();
53     }
54
55     /**
56      *
57      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#isAccepting(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
58      */

59     public boolean isAccepting(
60             SOFA.SOFAnode.Util.DFSRChecker.state.State state) {
61         if (nodes[0].isAccepting(state))
62             return true;
63         else {
64             try {
65                 return getAccepting(state);
66             } catch (InvalidParameterException e) {
67                 System.out.println("!!!! Exception while processing RestrictionNode::getAccepting() !!!!\n");
68                 System.exit(1);
69                 return false;
70             }
71         }
72     }
73
74     /**
75      *
76      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getTransitions(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
77      */

78     public TransitionPairs getTransitions(State state)
79             throws InvalidParameterException, CheckingException {
80
81         Stack JavaDoc stack = new Stack JavaDoc();
82         TreeSet JavaDoc processed = new TreeSet JavaDoc();
83         ArrayList JavaDoc result = new ArrayList JavaDoc();
84
85         stack.push(state);
86
87         while (stack.size() > 0) {
88             State actual = (State) stack.pop();
89
90             if (!processed.contains(actual)) {
91                 TransitionPair[] trans = nodes[0].getTransitions(actual).transitions;
92
93                 for (int i = 0; i < trans.length; ++i) {
94                     Integer JavaDoc evindex = new Integer JavaDoc(trans[i].eventIndex);
95                     boolean restricted = restriction.contains(new Integer JavaDoc(ActionRepository.getPure(evindex.intValue())));
96
97                     if (restricted)
98                         result.add(trans[i]);
99                     else
100                         stack.push(trans[i].state);
101                 }
102
103                 processed.add(actual);
104             }
105         }
106
107         TransitionPair[] result1 = new TransitionPair[result.size()];
108         Iterator JavaDoc it = result.iterator();
109         int i = 0;
110         while (it.hasNext())
111             result1[i++] = (TransitionPair) it.next();
112
113         return new TransitionPairs(result1);
114
115     }
116
117     /**
118      * Finds an accepting state among the states to be collapsed.
119      *
120      * @return true if there is an accepting state amon the collapsed states,
121      * false otherwise
122      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#isAccepting(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
123      */

124     private boolean getAccepting(State state) throws InvalidParameterException {
125
126         Stack JavaDoc stack = new Stack JavaDoc();
127         TreeSet JavaDoc processed = new TreeSet JavaDoc();
128
129         stack.push(state);
130
131         while (stack.size() > 0) {
132             State actual = (State) stack.pop();
133             TransitionPair[] trans = null;
134             try {
135                 trans = nodes[0].getTransitions(actual).transitions;
136             }
137             // only consent can throw this exception
138
catch (CheckingException e) {
139                 throw new RuntimeException JavaDoc("Internal error error");
140             }
141
142             for (int i = 0; i < trans.length; ++i) {
143                 if (!restriction.contains(new Integer JavaDoc(ActionRepository.getPure(trans[i].eventIndex)))) {
144                     if (nodes[0].isAccepting(trans[i].state))
145                         return true;
146                     else if (!processed.contains(trans[i].state))
147                         stack.push(trans[i].state);
148                 }
149             }
150             processed.add(actual);
151         }
152
153         return false;
154     }
155
156     /**
157      *
158      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getWeight()
159      */

160     public long getWeight() {
161         if (weight != -1)
162             return weight;
163         else {
164             return weight = nodes[0].getWeight();
165         }
166     }
167
168     /**
169      *
170      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#forwardCut(java.util.TreeSet)
171      */

172     public TreeNode forwardCut(TreeSet JavaDoc livingevents) {
173         TreeSet JavaDoc exlivev = new TreeSet JavaDoc();
174
175         Iterator JavaDoc it = livingevents.iterator();
176
177         while (it.hasNext()) {
178             Integer JavaDoc event = (Integer JavaDoc) it.next();
179             if (restriction.contains(new Integer JavaDoc(ActionRepository.getPure(event.intValue()))))
180                 exlivev.add(event);
181         }
182
183         nodes[0] = nodes[0].forwardCut(exlivev);
184
185         if (nodes[0] == null)
186             return null;
187
188         else
189             return this;
190     }
191
192     /**
193      * @return the symbolic name of the treenode denoting its type
194      */

195     public String JavaDoc[] getTypeName() {
196         String JavaDoc[] result = { "Restriction", "\\\\" };
197         return result;
198     }
199
200     /**
201      * @see SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.node.TreeNode#getAnotatedProtocol(SOFA.SOFAnode.Util.objectweb.fractal.behprotocols.checker.state.State)
202      */

203     public AnotatedProtocol getAnotatedProtocol(State state) {
204         return nodes[0].getAnotatedProtocol(state);
205     }
206
207     /**
208      * Creates the human-readable list of operations
209      *
210      * @param restriction
211      * the set of events indices
212      * @param repository
213      * Action repository to obtain the events labels
214      * @return the list of operation NOT to be restricted
215      */

216     private static String JavaDoc getRestr(TreeSet JavaDoc restriction,
217             ActionRepository repository) {
218         String JavaDoc result = new String JavaDoc();
219         Iterator JavaDoc it = restriction.iterator();
220
221         result = repository.getItemString(((Integer JavaDoc) it.next()).intValue());
222
223         while (it.hasNext())
224             result += ", " + repository.getItemString(((Integer JavaDoc) it.next()).intValue());
225
226         return result;
227     }
228
229     //--------------------------------------------------------------------------
230

231     /**
232      * The set of transitions (eventIndices) that should be omitted from the
233      * transition graph
234      */

235     final private TreeSet JavaDoc restriction;
236
237 }
Popular Tags