Node


1   
2   //
3   // Copyright (C) 2005 United States Government as represented by the
4   // Administrator of the National Aeronautics and Space Administration
5   // (NASA).  All Rights Reserved.
6   // 
7   // This software is distributed under the NASA Open Source Agreement
8   // (NOSA), version 1.3.  The NOSA has been approved by the Open Source
9   // Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
10  // directory tree for the complete NOSA document.
11  // 
12  // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
13  // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
14  // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
15  // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
16  // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
17  // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
18  // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
19  //
20  
21  // Written by Dimitra Giannakopoulou, 19 Jan 2001
22  package gov.nasa.ltl.trans;
23  
24  import java.util.*;
25  
26  
27  /**
28   * DOCUMENT ME!
29   */
30  class Node implements Comparable   {
31    public static int      accepting_conds = 0;
32    private static boolean init_collapsed = false;
33    private int            nodeId;
34    private TreeSet        incoming;
35    private TreeSet        toBeDone;
36    private TreeSet        old;
37    private TreeSet        next;
38    private BitSet         accepting;
39    private BitSet         right_of_untils;
40    private Node           OtherTransitionSource;
41    private int equivalenceId;
42  
43    public Node () {
44      nodeId = Pool.assign();
45      incoming = new TreeSet();
46      toBeDone = new TreeSet();
47      old = new TreeSet();
48      next = new TreeSet();
49      OtherTransitionSource = null;
50      accepting = new BitSet(accepting_conds);
51      right_of_untils = new BitSet(accepting_conds);
52    }
53  
54    public Node (TreeSet in, TreeSet newForm, TreeSet done, TreeSet nx, 
55                 BitSet acc, BitSet rous) {
56      nodeId = Pool.assign();
57      incoming = new TreeSet(in);
58      toBeDone = new TreeSet(newForm);
59      old = new TreeSet(done);
60      next = new TreeSet(nx);
61      OtherTransitionSource = null;
62      accepting = new BitSet(accepting_conds);
63      accepting.or(acc);
64      right_of_untils = new BitSet(accepting_conds);
65      right_of_untils.or(rous);
66    }
67  
68    public static int getAcceptingConds () {
69      return accepting_conds;
70    }
71  
72    public static Node createInitial (Formula form) {
73      accepting_conds = form.initialize(); // first mark right forms of untils;
74  
75      //    System.out.println("Accepting conditions: " + accepting_conds);
76      Node init = new Node();
77      init.nodeId = 0;
78  
79      if (form.getContent() != 't') {
80        init.decompose_ands_for_next(form);
81      }
82  
83      return init;
84    }
85  
86    public static void reset_static () {
87      accepting_conds = 0;
88      init_collapsed = false;
89    }
90  
91    public TreeSet getField_next () {
92      return next;
93    }
94  
95    public TreeSet getField_old () {
96      return old;
97    }
98  
99    public int getId () {
100     return nodeId;
101   }
102 
103   public boolean isInitial () {
104     return nodeId == 0;
105   }
106 
107   public int getNodeId () {
108     return nodeId;
109   }
110 
111   public void RTstructure (State[] RTautomaton) {
112     boolean safety = false;
113 
114     if (RTautomaton[nodeId] == null) {
115       RTautomaton[nodeId] = new State(accepting, equivalenceId);
116     } else {
117       RTautomaton[nodeId].update_acc(accepting, equivalenceId);
118     }
119 
120     if (is_safety_acc_node()) {
121       RTautomaton[nodeId].update_safety_acc(true);
122       safety = true;
123     }
124 
125     Node Alternative = this;
126 
127     while (Alternative != null) {
128       Iterator iterIncom = Alternative.incoming.iterator();
129       Node     nextNode;
130 
131       while (iterIncom.hasNext()) {
132         nextNode = (Node) iterIncom.next();
133 
134         int stateId = nextNode.getId();
135 
136         if (RTautomaton[stateId] == null) {
137           RTautomaton[stateId] = new State();
138         }
139 
140         RTautomaton[stateId].add(
141               new Transition(Alternative.old, equivalenceId, accepting, safety));
142       }
143 
144       Alternative = Alternative.OtherTransitionSource;
145     }
146   }
147 
148   public int compareTo (Object   f) {
149     if (this == f) {
150       return 0;
151     } else {
152       return 1;
153     }
154   }
155 
156   public boolean compare_accepting (Node nd) {
157     //if (nodeId == 0) 
158     //  System.out.println("Has it been collapsed yet? : " + init_collapsed);
159     if ((nodeId == 0) && !init_collapsed) {
160       // System.out.println("Potentially collapse " + nodeId + " with " + nd.nodeId);
161       return true;
162     }
163 
164     return (accepting.equals(nd.accepting)); // compare their BitSets
165   }
166 
167   /*
168      public void print() 
169      {
170        System.out.println("\n\nPrinting node " + nodeId);
171        Iterator iterNext = next.iterator();
172        Formula nextForm = null;
173      
174          // all formulas present must be of type V or W, otherwise false
175          while (iterNext.hasNext()) 
176          {
177            nextForm = (Formula) iterNext.next();
178            System.out.println("Formula: " + nextForm.toString());
179          }
180        }
181    */
182   public void debug () {
183     Iterator iterOld = old.iterator();
184     Formula  nextForm = null;
185 
186     //      System.out.println("debugging now");
187     while (iterOld.hasNext()) {
188       nextForm = (Formula) iterOld.next();
189 
190       //            System.out.println("Content is " + nextForm.getContent());
191     }
192   }
193 
194   public void decompose_ands_for_next (Formula form) {
195     if (form.getContent() == 'A') {
196       decompose_ands_for_next(form.getSub1());
197       decompose_ands_for_next(form.getSub2());
198     } else if (is_redundant(next, null, form) == false) {
199       next.add(form);
200     }
201   }
202 
203   public Automaton expand (Automaton states) {
204     //      System.out.println("expand entered"); // debugging
205     Node tempNode;
206 
207     if (toBeDone.isEmpty()) {
208       if (nodeId != 0) {
209         update_accepting();
210       }
211 
212 
213       // System.out.println("New is empty!");
214       tempNode = states.alreadyThere(this);
215 
216       if (tempNode != null) {
217         // System.out.println("Node " + nodeId + " collapsed with " + tempNode.nodeId);
218         tempNode.modify(this);
219 
220         return states;
221       } else {
222         Node NewN = new Node();
223         NewN.incoming.add(this);
224         NewN.toBeDone.addAll(next);
225 
226         states.add(this);
227 
228         return (NewN.expand(states));
229       }
230     } else // toBeDone is not empty
231     {
232       Formula temp_form;
233       Formula ita = (Formula) toBeDone.first();
234       toBeDone.remove(ita);
235 
236       //System.out.println("\n\nExpanding " + ita + " for node " + nodeId);
237       if (testForContradictions(ita)) {
238         //System.out.println("Finished expand - contradiction");
239         return states;
240       }
241 
242       // no contradiction
243       // look in tech report why we do this even when ita is redundant
244       if (ita.is_right_of_until(accepting_conds)) {
245         right_of_untils.or(ita.get_rightOfWhichUntils());
246       }
247 
248       TreeSet set_checked_against = new TreeSet();
249       set_checked_against.addAll(old);
250       set_checked_against.addAll(toBeDone);
251 
252       if (is_redundant(set_checked_against, next, ita)) {
253         return expand(states);
254       }
255 
256       // not redundant either
257       // look in tech report why this only when not redundant
258       if (ita.getContent() == 'U') { // this is an until formula 
259         accepting.set(ita.get_untils_index());
260 
261         //          System.out.println("Just set an eventuality requirement");
262       }
263 
264       if (!ita.is_literal()) {
265         switch (ita.getContent()) {
266         case 'U':
267         case 'W':
268         case 'V':
269         case 'O':
270 
271           Node node2 = split(ita);
272 
273           return node2.expand(this.expand(states));
274 
275         case 'X':
276           decompose_ands_for_next(ita.getSub1());
277 
278           return expand(states);
279 
280         case 'A':
281           temp_form = ita.getSub1();
282 
283           if (!old.contains(temp_form)) {
284             toBeDone.add(temp_form);
285           }
286 
287           temp_form = ita.getSub2();
288 
289           if (!old.contains(temp_form)) {
290             toBeDone.add(temp_form);
291           }
292 
293           return expand(states);
294 
295         default:
296           System.out.println("default case of switch entered");
297 
298           return null;
299         }
300       } else // ita represents a literal
301       {
302         //  System.out.println("Now working on literal " + ita.getContent());
303         // must do a test for contradictions first
304         if (ita.getContent() != 't') {
305           old.add(ita);
306         }
307 
308         //  System.out.println("added to " + nodeId + " formula " + ita);
309         return (expand(states));
310       }
311     }
312   }
313 
314   public int get_equivalenceId () {
315     return equivalenceId;
316   }
317 
318   public void set_equivalenceId (int value) {
319     equivalenceId = value;
320   }
321 
322   public void update_accepting () {
323     accepting.andNot(right_of_untils);
324 
325     // just do now the bitwise or so that accepting gets updated
326   }
327 
328   private static boolean is_redundant (TreeSet main_set, TreeSet next_set, 
329                                        Formula ita) {
330     if ((ita.is_special_case_of_V(main_set)) || // my addition - correct??? 
331         ((ita.is_synt_implied(main_set, next_set)) && 
332               (!(ita.getContent() == 'U') || 
333                 (ita.getSub2().is_synt_implied(main_set, next_set))))) {
334       //System.out.println("Looks like formula was redundant");
335       return true;
336     } else {
337       return false;
338     }
339   }
340 
341   private boolean is_safety_acc_node () {
342     if (next.isEmpty()) {
343       return true;
344     }
345 
346     Iterator iterNext = next.iterator();
347     Formula  nextForm = null;
348 
349     // all formulas present must be of type V or W, otherwise false
350     while (iterNext.hasNext()) {
351       nextForm = (Formula) iterNext.next();
352 
353       if ((nextForm.getContent() != 'V') && (nextForm.getContent() != 'W')) {
354         return false;
355       }
356     }
357 
358     return true;
359   }
360 
361   private void modify (Node current) {
362     boolean match = false;
363     Node    Tail = this;
364     Node    Alternative = this;
365 
366     if ((this.nodeId == 0) && !init_collapsed) {
367       accepting = current.accepting;
368       init_collapsed = true;
369     }
370 
371     while (Alternative != null) {
372       if (Alternative.old.equals(current.old)) {
373         Alternative.incoming.addAll(current.incoming);
374         match = true;
375       }
376 
377       Tail = Alternative;
378       Alternative = Alternative.OtherTransitionSource;
379     }
380 
381     if (!match) {
382       Tail.OtherTransitionSource = current;
383     }
384   }
385 
386   private Node split (Formula form) {
387     //System.out.println("Split is entered");
388     Formula temp_form;
389 
390     // first create Node 2
391     Node Node2 = new Node(this.incoming, this.toBeDone, this.old, this.next, 
392                           this.accepting, this.right_of_untils);
393 
394     temp_form = form.getSub2();
395 
396     if (!old.contains(temp_form)) //New2(n) not in old
397 
398     {
399       Node2.toBeDone.add(temp_form);
400     }
401 
402     if (form.getContent() == 'V') // both subformulas are added to New2
403     {
404       temp_form = form.getSub1();
405 
406       if (!old.contains(temp_form)) // subformula not in old
407 
408       {
409         Node2.toBeDone.add(temp_form);
410       }
411     }
412 
413 
414     // then substitute current Node with Node 1
415     temp_form = form.getSub1();
416 
417     if (!old.contains(temp_form)) //New1(n) not in old
418 
419     {
420       toBeDone.add(temp_form);
421     }
422 
423     temp_form = form.getNext();
424 
425     if (temp_form != null) {
426       decompose_ands_for_next(temp_form);
427     }
428 
429     /* following lines are probably unecessary because we never split literals!*/
430     if (form.is_literal())/* because we only store literals... */
431     {
432       old.add(form);
433       System.out.println("added " + form); // never supposed to see that
434       Node2.old.add(form);
435     }
436 
437     //System.out.println("Node split into itself and node : " + Node2.nodeId);
438     //print();
439     //Node2.print();
440     return Node2;
441   }
442 
443   private boolean testForContradictions (Formula ita) {
444     Formula Not_ita = ita.negate();
445 
446     if (Not_ita.is_synt_implied(old, next)) {
447       return true;
448     } else {
449       return false;
450     }
451   }
452 }
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags