KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > Crossing


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // directory tree for the complete NOSA document.
10 //
11 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18 //
19
20 /**
21  * This is the famous Bridge-crossing puzzle. The aim is to see what the minimum
22  * amount of time is for 4 people to cross with flash-light (torch): 10.5.2.1.
23  * The answer is 17 for the given configuration.
24  *
25  * One can find this solution with JPF in BFS search mode - DFS will not
26  * work since this is an infinite-state program (time keeps increasing).
27  *
28  * If one uses the ignoreIf(cond) call the branches that will lead to
29  * solutions worst than the current will be cut-off and this will allow
30  * DFS also to complete - and BFS to terminate faster.
31  *
32  * When setting the native flag in main one can also save information
33  * from one run to the next using JPF's native peer methods -
34  * see JPF_Crossing.java for the code of getTotal() and setTotal(int).
35  */
36 import gov.nasa.jpf.jvm.Verify;
37
38
39 /**
40  * DOCUMENT ME!
41  */
42 class Constants {
43   public static final boolean east = true;
44   public static final boolean west = false;
45 }
46
47 /**
48  * DOCUMENT ME!
49  */
50 class Torch {
51   public static boolean side = Constants.east;
52
53   public String JavaDoc toString () {
54     if (side == Constants.east) {
55       return "east";
56     } else {
57       return "west";
58     }
59   }
60 }
61
62 /**
63  * DOCUMENT ME!
64  */
65 class Bridge {
66   static Person[] onBridge = new Person[2];
67   static int numOnBridge = 0;
68
69   public static boolean isFull () {
70     return numOnBridge != 0;
71   }
72
73   public static int Cross () {
74     int time = 0;
75     Torch.side = !Torch.side;
76
77     if (numOnBridge == 1) {
78       onBridge[0].side = Torch.side;
79       time = onBridge[0].time;
80       /*
81       System.out.println("Person " + onBridge[0] +
82                          " moved to " + (Torch.side ? "east" : "west") +
83                          " in time " + time);
84        */
85     } else {
86       onBridge[0].side = Torch.side;
87       onBridge[1].side = Torch.side;
88
89       if (onBridge[0].time > onBridge[1].time) {
90         time = onBridge[0].time;
91       } else {
92         time = onBridge[1].time;
93       }
94       /*
95       System.out.println("Person " + onBridge[0] +
96                          " and Person " + onBridge[1] +
97                          " moved to " + (Torch.side ? "east" : "west") +
98                          " in time " + time);
99        */
100     }
101
102     return time;
103   }
104
105   public static void clearBridge () {
106     if (numOnBridge == 0) {
107       return;
108     } else if (numOnBridge == 1) {
109       onBridge[0] = null;
110       numOnBridge = 0;
111     } else {
112       onBridge[0] = null;
113       onBridge[1] = null;
114       numOnBridge = 0;
115     }
116   }
117
118   public static void initBridge () {
119     onBridge[0] = null;
120     onBridge[1] = null;
121     numOnBridge = 0;
122   }
123
124   public static boolean tryToCross (Person th) {
125     if ((numOnBridge < 2) && (onBridge[0] != th) && (onBridge[1] != th)) {
126       onBridge[numOnBridge++] = th;
127
128       return true;
129     } else {
130       return false;
131     }
132   }
133 }
134
135 /**
136  * DOCUMENT ME!
137  */
138 class Person {
139   // person to cross the bridge
140 int id;
141   public int time;
142   public boolean side;
143
144   public Person (int i, int t) {
145     time = t;
146     side = Constants.east;
147     id = i;
148   }
149
150   public void move () {
151     if (side == Torch.side) {
152       if (!Verify.randomBool()) {
153         Bridge.tryToCross(this);
154       }
155     }
156   }
157
158   public String JavaDoc toString () {
159     return Integer.toString(id);
160   }
161 }
162
163 /**
164  * DOCUMENT ME!
165  */
166 public class Crossing {
167   public static native void setTotal (int time);
168
169   // due to these natives the code only runs in JPF
170 public static native int getTotal ();
171
172   public static void main (String JavaDoc[] args) {
173     Verify.beginAtomic();
174
175     // when natives are used one can record the minimal value found so
176 // far to get a better one on the next execution - this
177 // requires the -mulitple-errors option and then the last error
178 // found must be replayed
179 boolean isNative = false;
180
181     if (isNative) {
182       setTotal(30); // set to value larger than solution (17)
183 }
184
185     int total = 0;
186     boolean finished = false;
187     Bridge.initBridge();
188
189     Person p1 = new Person(1, 1);
190     Person p2 = new Person(2, 2);
191     Person p3 = new Person(3, 5);
192     Person p4 = new Person(4, 10);
193     Verify.endAtomic();
194
195     while (!finished) {
196       Verify.beginAtomic();
197       p1.move();
198       p2.move();
199       p3.move();
200       p4.move();
201
202       if (Bridge.isFull()) {
203         total += Bridge.Cross();
204
205         if (isNative) {
206           Verify.ignoreIf(total > getTotal());
207         } else {
208           Verify.ignoreIf(total > 17); //with this DFS will also find error
209 }
210
211         Bridge.clearBridge();
212
213
214         //printConfig(p1,p2,p3,p4,total);
215 finished = !(p1.side || p2.side || p3.side || p4.side);
216       }
217
218       Verify.endAtomic();
219     }
220
221     Verify.beginAtomic();
222
223     if (isNative) {
224       if (total < getTotal()) {
225         System.out.println("new total " + total);
226         setTotal(total);
227         assert (total > getTotal());
228       }
229     } else {
230       System.out.println("total time = " + total);
231       assert (total > 17);
232     }
233
234     Verify.endAtomic();
235   }
236
237   static void printConfig (Person p1, Person p2, Person p3, Person p4,
238                            int total) {
239     System.out.print( Integer.toString(total));
240     System.out.print(" : ");
241     
242     if (p1.side == Constants.east) {
243       System.out.print(" p1(" + p1.time + ")");
244     }
245
246     if (p2.side == Constants.east) {
247       System.out.print(" p2(" + p2.time + ")");
248     }
249
250     if (p3.side == Constants.east) {
251       System.out.print(" p3(" + p3.time + ")");
252     }
253
254     if (p4.side == Constants.east) {
255       System.out.print(" p4(" + p4.time + ")");
256     }
257
258     System.out.print(" -> ");
259
260     if (p1.side == Constants.west) {
261       System.out.print(" p1(" + p1.time + ")");
262     }
263
264     if (p2.side == Constants.west) {
265       System.out.print(" p2(" + p2.time + ")");
266     }
267
268     if (p3.side == Constants.west) {
269       System.out.print(" p3(" + p3.time + ")");
270     }
271
272     if (p4.side == Constants.west) {
273       System.out.print(" p4(" + p4.time + ")");
274     }
275
276     System.out.println();
277   }
278 }
279
Free Books   Free Magazines  
Popular Tags