1 17 18 package SOFA.SOFAnode.Util.DFSRChecker.node; 19 20 import java.util.TreeSet ; 21 import java.util.Stack ; 22 import java.util.ArrayList ; 23 import java.util.Iterator ; 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 34 public class RestrictionNode extends TreeNode { 35 36 37 public RestrictionNode(TreeNode node, TreeSet 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 51 public SOFA.SOFAnode.Util.DFSRChecker.state.State getInitial() { 52 return nodes[0].getInitial(); 53 } 54 55 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 78 public TransitionPairs getTransitions(State state) 79 throws InvalidParameterException, CheckingException { 80 81 Stack stack = new Stack (); 82 TreeSet processed = new TreeSet (); 83 ArrayList result = new ArrayList (); 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 evindex = new Integer (trans[i].eventIndex); 95 boolean restricted = restriction.contains(new Integer (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 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 124 private boolean getAccepting(State state) throws InvalidParameterException { 125 126 Stack stack = new Stack (); 127 TreeSet processed = new TreeSet (); 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 catch (CheckingException e) { 139 throw new RuntimeException ("Internal error error"); 140 } 141 142 for (int i = 0; i < trans.length; ++i) { 143 if (!restriction.contains(new Integer (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 160 public long getWeight() { 161 if (weight != -1) 162 return weight; 163 else { 164 return weight = nodes[0].getWeight(); 165 } 166 } 167 168 172 public TreeNode forwardCut(TreeSet livingevents) { 173 TreeSet exlivev = new TreeSet (); 174 175 Iterator it = livingevents.iterator(); 176 177 while (it.hasNext()) { 178 Integer event = (Integer ) it.next(); 179 if (restriction.contains(new Integer (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 195 public String [] getTypeName() { 196 String [] result = { "Restriction", "\\\\" }; 197 return result; 198 } 199 200 203 public AnotatedProtocol getAnotatedProtocol(State state) { 204 return nodes[0].getAnotatedProtocol(state); 205 } 206 207 216 private static String getRestr(TreeSet restriction, 217 ActionRepository repository) { 218 String result = new String (); 219 Iterator it = restriction.iterator(); 220 221 result = repository.getItemString(((Integer ) it.next()).intValue()); 222 223 while (it.hasNext()) 224 result += ", " + repository.getItemString(((Integer ) it.next()).intValue()); 225 226 return result; 227 } 228 229 231 235 final private TreeSet restriction; 236 237 } | Popular Tags |