KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > ltl > trans > Transition


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 package gov.nasa.ltl.trans;
21
22 import gov.nasa.ltl.graph.*;
23
24 import java.util.*;
25
26
27 /**
28  * DOCUMENT ME!
29  */
30 class Transition {
31   private TreeSet propositions;
32   private int pointsTo;
33   private BitSet accepting;
34   private boolean safe_accepting;
35
36   public Transition (TreeSet prop, int nd_id, BitSet acc, boolean safety) {
37     propositions = prop;
38     pointsTo = nd_id;
39     accepting = new BitSet(Node.getAcceptingConds());
40     accepting.or(acc);
41     safe_accepting = safety;
42   }
43
44   public void FSPoutput () {
45     if (propositions.isEmpty()) {
46       System.out.print("TRUE{");
47     } else {
48       // first print the propositions involved
49 Iterator it = propositions.iterator();
50       Formula nextForm = null;
51       StringBuffer JavaDoc act = new StringBuffer JavaDoc();
52       char cont; // stores content of formula
53 boolean need_AND = false; // connect with AND multiple propositions
54
55       while (it.hasNext()) {
56         nextForm = (Formula) it.next();
57         cont = nextForm.getContent();
58
59         if (need_AND) {
60           act.append("_AND_");
61         }
62
63         need_AND = true;
64
65         switch (cont) {
66         case 'N':
67           act.append('N');
68           act.append(nextForm.getSub1().getName());
69
70           break;
71
72         case 't':
73           act.append("TRUE");
74
75           break;
76
77         default:
78           act.append(nextForm.getName());
79
80           break;
81         }
82       }
83
84       System.out.print(act + "{");
85     }
86
87     if (Node.accepting_conds == 0) {
88       if (safe_accepting == true) {
89         System.out.print("0");
90       }
91     } else {
92       for (int i = 0; i < Node.accepting_conds; i++) {
93         if (!accepting.get(i)) {
94           System.out.print(i);
95         }
96       }
97     }
98
99
100     // and then the rest - easy
101 System.out.print("} -> S" + pointsTo + " ");
102   }
103
104   public void SMoutput (gov.nasa.ltl.graph.Node[] nodes,
105                         gov.nasa.ltl.graph.Node node) {
106     String JavaDoc guard = "-";
107     String JavaDoc action = "-";
108
109     if (!propositions.isEmpty()) {
110       Iterator it = propositions.iterator();
111       Formula nextForm = null;
112       StringBuffer JavaDoc sb = new StringBuffer JavaDoc();
113       char cont; // stores content of formula
114 boolean need_AND = false; // connect with AND multiple propositions
115
116       while (it.hasNext()) {
117         nextForm = (Formula) it.next();
118         cont = nextForm.getContent();
119
120         if (need_AND) {
121           sb.append("&");
122         }
123
124         need_AND = true;
125
126         switch (cont) {
127         case 'N':
128           sb.append('!');
129           sb.append(nextForm.getSub1().getName());
130
131           break;
132
133         case 't':
134           sb.append("true");
135
136           break;
137
138         default:
139           sb.append(nextForm.getName());
140
141           break;
142         }
143       }
144
145       guard = sb.toString();
146     }
147
148     Edge e = new Edge(node, nodes[pointsTo], guard, action);
149
150     if (Node.accepting_conds == 0) {
151       // Dimitra - Jan 10 2003
152 // Believe there is a bug with the way we decided whether node was safety accepting
153 // with example !<>(Xa \/ <>c)
154 // System.out.println("Entered the safety part of accepting conditions");
155 // if (safe_accepting == true) {
156 // System.out.println("But did I actually set it correctly?");
157 e.setBooleanAttribute("acc0", true);
158
159       // }
160 } else {
161       for (int i = 0; i < Node.accepting_conds; i++) {
162         if (!accepting.get(i)) {
163           e.setBooleanAttribute("acc" + i, true);
164
165           // System.out.println("Transition belongs to set " + i);
166 }
167       }
168     }
169   }
170
171   public boolean enabled (Hashtable ProgramState) {
172     Iterator mustHold = propositions.iterator();
173     Formula form = null;
174     char c;
175     Boolean JavaDoc value;
176
177     while (mustHold.hasNext()) {
178       form = (Formula) mustHold.next();
179
180       switch (c = form.getContent()) {
181       case 'N':
182         value = (Boolean JavaDoc) ProgramState.get(form.getSub1().getName());
183
184         if (value == null) {
185           // System.out.println("Proposition not defined in program state");
186 return false;
187         } else if (value.booleanValue()) {
188           return false;
189         }
190
191         break;
192
193       case 't':
194         break;
195
196       case 'p':
197         value = (Boolean JavaDoc) ProgramState.get(form.getName());
198
199         if (value == null) {
200           // System.out.println("Proposition not defined in program state");
201 return false;
202         } else if (!value.booleanValue()) {
203           return false;
204         }
205
206         break;
207       }
208     }
209
210     return true;
211   }
212
213   public int goesTo () {
214     return pointsTo;
215   }
216 }
Popular Tags