View Javadoc

1   package net.kwfgrid.gworkflowdl.analysis;
2   
3   import java.util.ArrayList;
4   import java.util.HashSet;
5   import java.util.Iterator;
6   
7   /***
8    * Created by IntelliJ IDEA.
9    * User: hans
10   * Date: 28.10.2005
11   * Time: 13:59:48
12   * To change this template use File | Settings | File Templates.
13   */
14  public class KarpMillerTree extends Net {
15      public static  int MAX_COMPLEXITY = 200000;
16      // int complexity = 0;
17  
18      private HashSet unprocessed = new HashSet();
19      Node root;
20      public boolean[] unboundedPlace;
21  
22      /*
23      public KarpMillerTree(Workflow workflow) {
24          super(workflow);
25          type = Net.KARP_MILLER_TREE;
26          build();
27      }
28      */
29  
30  
31      public static class Node {
32          public Marking marking;
33          public Node parent;
34          public ArrayList childs;
35          public String type = "";
36          public int transitionIndex = -1;
37  
38          public Node() {
39              parent = null;
40              childs = new ArrayList();
41          }
42      }
43  
44      public void build() {
45          type = Net.KARP_MILLER_TREE;
46          unboundedPlace = new boolean[N];
47          for (int i = 0; i < N; i++) {
48              unboundedPlace[i] = false;
49          }
50          root = new KarpMillerTree.Node();
51          root.marking = initial;
52          unprocessed.add(root);
53          if (capacities == null) {
54              capacities = new Marking(N, KarpMillerTree.INFINITY);
55          }
56          int nodeCount = 1;
57  
58          while (!unprocessed.isEmpty()) {
59              if (complexity > MAX_COMPLEXITY) {
60                  complete = false;
61                  break;
62              }
63              //System.out.println("size "  + unprocessed.size());
64              //final Node actNode = (Node) unprocessed.remove(0);
65              Iterator it = unprocessed.iterator();
66              final Node actNode = (Node) it.next();
67              unprocessed.remove(actNode);
68              //System.out.println(actNode.marking.toString());
69  
70              // look if there is an ancestor with the same marking
71              Node node = actNode;
72              boolean flag = false;
73              while (true) {
74                  node = node.parent;
75                  if (node == null) {
76                      break;
77                  }
78                  if (Marking.equals(actNode.marking, node.marking)) {
79                      flag = true;
80                      break;
81                  }
82  
83              }
84              if (flag) {
85                  // ancestor with same marking
86                  actNode.type = "=";
87                  infiniteRun = true;
88                  continue;
89              } else {
90                  final Marking tmp = (Marking) actNode.marking.clone();
91                  node = actNode;
92                  while (true) {
93                      node = node.parent;
94                      if (node == null) {
95                          break;
96                      }
97                      if (Marking.lessOrEqual(node.marking, actNode.marking)) {
98                          for (int i = 0; i < N; i++) {
99                              if (node.marking.get(i) < actNode.marking.get(i) &&
100                                     capacities.get(i) == KarpMillerTree.INFINITY) {
101                                 infiniteRun = true;
102                                 unbounded = true;
103                                 unboundedPlace[i] = true;
104                                 tmp.set(i, KarpMillerTree.INFINITY);
105                             }
106                         }
107 
108                     }
109                 }
110                 actNode.marking = tmp;
111                 int count = 0;
112                 for (int i = 0; i < transitions.length; i++) {
113                     final Marking newMarking = transitions[i].fire(actNode.marking, capacities);
114                     if (newMarking != null) {
115                         count++;
116                         final Node newNode = new Node();
117                         newNode.parent = actNode;
118                         newNode.marking = newMarking;
119                         newNode.transitionIndex = i;
120                         actNode.childs.add(newNode);
121                         unprocessed.add(newNode);
122                         complexity += N;
123                         nodeCount++;
124                         /*
125                         if (nodeCount % 500 == 0) {
126                             System.out.println(nodeCount);
127                         }
128                         */
129                     }
130                 }
131                 if (count == 0) {
132                     actNode.type = "+";
133                 }
134             }
135         }
136         //System.out.println("nodeCount = " + nodeCount);
137     }
138 
139     public boolean isQuasiLive(int p) {
140         Marking m = new Marking(N);
141         m.set(p, 1);
142         return traverseCoverable(root, m);
143     }
144 
145     public boolean isUnbounded(int p) {
146         return unboundedPlace[p];
147     }
148 
149     public boolean traverseCoverable(Node node, Marking m) {
150         if (Marking.lessOrEqual(m, node.marking)) {
151             return true;
152         }
153         for (int i = 0; i < node.childs.size(); i++) {
154             if (traverseCoverable((Node) node.childs.get(i), m)) {
155                 return true;
156             }
157         }
158         return false;
159     }
160 
161     public boolean isFireable(int transitionIndex) {
162         return traverseFireable(root, transitionIndex);
163     }
164 
165     public boolean traverseFireable(Node node, int transitionIndex) {
166         if (node.transitionIndex == transitionIndex) {
167             return true;
168         }
169         for (int i = 0; i < node.childs.size(); i++) {
170             if (traverseFireable((Node) node.childs.get(i), transitionIndex)) {
171                 return true;
172             }
173         }
174         return false;
175     }
176 
177     public boolean mustFire(int transitionIndex) {
178         if (infiniteRun) {
179             return false;
180         }
181         return traverseMustFire(root, transitionIndex);
182 
183     }
184 
185     private boolean traverseMustFire(Node node, int transitionIndex) {
186         if (node.transitionIndex == transitionIndex) {
187             //System.out.println("mode.ti " + node.transitionIndex);
188             return true;
189         }
190         if (node.childs.size() == 0) {
191             return false;
192         }
193         for (int i = 0; i < node.childs.size(); i++) {
194             if (!traverseMustFire((Node) node.childs.get(i), transitionIndex)) {
195                 return false;
196             }
197         }
198         return true;
199     }
200 
201     public boolean isFinallyMarked(int p) {
202         if (infiniteRun) {
203             return false;
204         }
205         Marking m = new Marking(N);
206         m.set(p, 1);
207         return traverseFinallyMarked(root, m);
208     }
209 
210     private boolean traverseFinallyMarked(Node node, Marking m) {
211         if (node.type.equals("+")) {
212             return Marking.lessOrEqual(m, node.marking);
213         } else {
214             boolean ret = true;
215             for (int i = 0; i < node.childs.size(); i++) {
216                 Node child = (Node) node.childs.get(i);
217                 ret = ret && traverseFinallyMarked(child, m);
218             }
219             return ret;
220         }
221     }
222 
223     public boolean oneOfIsFinallyMarked(int[] is) {
224         return traverseOneOfIsFinallyMarked(root, is);
225     }
226 
227     public boolean traverseOneOfIsFinallyMarked(Node node, int[] is) {
228         if (node.type.equals("+")) {
229             for (int i = 0; i < is.length; i++) {
230                 if (node.marking.get(is[i]) > 0) {
231                     return true;
232                 }
233             }
234             return false;
235             //return Marking.lessOrEqual(in, node.marking);
236         } else {
237             boolean ret = true;
238             for (int i = 0; i < node.childs.size(); i++) {
239                 Node child = (Node) node.childs.get(i);
240                 ret = ret && traverseOneOfIsFinallyMarked(child, is);
241             }
242             return ret;
243         }
244     }
245 
246     public void traverseConflictPairs(Node node, ArrayList cp) {
247         AnalysisTransition[] ts = transitions;
248         for (int i = 1; i < node.childs.size(); i++) {
249             KarpMillerTree.Node ni = (KarpMillerTree.Node) node.childs.get(i);
250             Marking mi = ni.marking;
251             int ti = ni.transitionIndex;
252             for (int j = 0; j < i; j++) {
253                 KarpMillerTree.Node nj = (KarpMillerTree.Node) node.childs.get(j);
254                 Marking mj = nj.marking;
255                 int tj = nj.transitionIndex;
256                 if (!ts[ti].isEnabled(mj, capacities) || !ts[tj].isEnabled(mi, capacities)) {
257                     boolean isIn = false;
258                     IntPair ip = new IntPair(ti, tj);
259                     for (int l = 0; l < cp.size(); l++) {
260                         if (ip.equals((IntPair) cp.get(l))) {
261                             isIn = true;
262                             break;
263                         }
264                     }
265                     if (!isIn) {
266                         cp.add(ip);
267                     }
268                 }
269             }
270         }
271 
272         for (int i = 0; i < node.childs.size(); i++) {
273             Node child = (Node) node.childs.get(i);
274             traverseConflictPairs(child, cp);
275         }
276     }
277 
278 
279     public HashSet gatherDecisions() {
280         HashSet gather = new HashSet();
281         traverseGetDecisions(root, gather);
282         return gather;
283     }
284 
285     public void traverseGetDecisions(Node node, HashSet gather) {
286         Marking m = node.marking;
287 
288         // take
289         for (int i = 0; i < N; i++) {
290 
291             //ArrayList list = new ArrayList();
292             int type = -1;
293             if (m.get(i) == 1) {
294                 //list.add(new Integer(Decision.TAKE_CONFLICT));
295                 type = Decision.TAKE_CONFLICT;
296             } else {
297                 //list.add(new Integer(Decision.TAKE_CHOICE));
298                 type = Decision.TAKE_CHOICE;
299             }
300 
301             //list.add(new Integer(i));
302             int placeIndex = i;
303 
304             ArrayList list = new ArrayList();
305             for (int j = 0; j < node.childs.size(); j++) {
306                 Node child = (Node) node.childs.get(j);
307                 int t = child.transitionIndex;
308                 Marking in = transitions[t].in;
309                 if (in.get(i) > 0) {
310                     list.add(new Integer(t));
311                 }
312             }
313             /*
314             if (list.size() > 3 && !isIn(list, gather)) {
315                 gather.add(list);
316             }
317             */
318             if (list.size() > 1) {
319                 IndexDecision id = new IndexDecision();
320                 id.type = type;
321                 id.placeIndex = placeIndex;
322                 id.transitionIndices = list;
323                 gather.add(id);
324             }
325         }
326 
327         // put
328         for (int i = 0; i < N; i++) {
329             /*
330             if (capacities.get(i) == KarpMillerTree1.INFINITY) {
331                 continue;
332             }
333             */
334             ArrayList list = new ArrayList();
335             int type = -1;
336             if (m.get(i) == capacities.get(i) - 1) {
337                 //list.add(new Integer(Decision.PUT_CONFLICT));
338                 type = Decision.PUT_CONFLICT;
339             } else {
340                 //list.add(new Integer(Decision.PUT_CHOICE));
341                 type = Decision.PUT_CHOICE;
342 
343             }
344             //list.add(new Integer(i));
345             int placeIndex = i;
346 
347             for (int j = 0; j < node.childs.size(); j++) {
348                 Node child = (Node) node.childs.get(j);
349                 int t = child.transitionIndex;
350                 Marking in = transitions[t].in;
351                 Marking out = transitions[t].out;
352                 //if (out.get(i) - in.get(i) > 0) {
353                 if (out.get(i) > 0) {
354                     list.add(new Integer(t));
355                 }
356             }
357 
358             /*
359             if (list.size() > 3 && !isIn(list, gather)) {
360                 gather.add(list);
361             }
362             */
363             if (list.size() > 1) {
364                 IndexDecision id = new IndexDecision();
365                 id.type = type;
366                 id.placeIndex = placeIndex;
367                 id.transitionIndices = list;
368                 gather.add(id);
369             }
370 
371         }
372 
373         for (int i = 0; i < node.childs.size(); i++) {
374             Node child = (Node) node.childs.get(i);
375             traverseGetDecisions(child, gather);
376         }
377 
378     }
379 
380 
381 
382     // debug tools
383 
384     public void show() {
385         show("", root);
386     }
387 
388     public void show(String indent, Node node) {
389         System.out.print(toString(indent, node));
390     }
391 
392     public String toString(String indent, Node node) {
393         StringBuffer buffer = new StringBuffer();
394         buffer.append(indent).append(node.marking.toString()).append(node.type);
395         for (int i = 0; i < node.childs.size(); i++) {
396             buffer.append("\n").append(toString(indent + "  ", (Node) node.childs.get(i)));
397         }
398         return buffer.toString();
399     }
400 
401     public String toString() {
402         return toString("", root) + "\n";
403     }
404 }