KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > mc > 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 package gov.nasa.jpf.mc;
37
38 import gov.nasa.jpf.jvm.Verify;
39
40
41 class Constants {
42   public static final boolean east = true;
43   public static final boolean west = false;
44 }
45
46 class Torch {
47   public static boolean side = Constants.east;
48
49   public String JavaDoc toString () {
50     if (side == Constants.east) {
51       return "east";
52     } else {
53       return "west";
54     }
55   }
56 }
57
58 class Bridge {
59   static Person[] onBridge = new Person[2];
60   static int numOnBridge = 0;
61
62   public static boolean isFull () {
63     return numOnBridge != 0;
64   }
65
66   public static int Cross () {
67     int time = 0;
68     Torch.side = !Torch.side;
69
70     if (numOnBridge == 1) {
71       onBridge[0].side = Torch.side;
72       time = onBridge[0].time;
73
74       //System.out.println("Person " + onBridge[0] +
75 // " moved to " + Torch.side +
76 // " in time " + time);
77 } else {
78       onBridge[0].side = Torch.side;
79       onBridge[1].side = Torch.side;
80
81       if (onBridge[0].time > onBridge[1].time) {
82         time = onBridge[0].time;
83       } else {
84         time = onBridge[1].time;
85       }
86
87       //System.out.println("Person " + onBridge[0] +
88 // " and Person " + onBridge[1] +
89 // " moved to " + Torch.side +
90 // " in time " + time);
91 }
92
93     return time;
94   }
95
96   public static void clearBridge () {
97     if (numOnBridge == 0) {
98       return;
99     } else if (numOnBridge == 1) {
100       onBridge[0] = null;
101       numOnBridge = 0;
102     } else {
103       onBridge[0] = null;
104       onBridge[1] = null;
105       numOnBridge = 0;
106     }
107   }
108
109   public static void initBridge () {
110     onBridge[0] = null;
111     onBridge[1] = null;
112     numOnBridge = 0;
113   }
114
115   public static boolean tryToCross (Person th) {
116     if ((numOnBridge < 2) && (onBridge[0] != th) && (onBridge[1] != th)) {
117       onBridge[numOnBridge++] = th;
118
119       return true;
120     } else {
121       return false;
122     }
123   }
124 }
125
126 class Person {
127   // person to cross the bridge
128 int id;
129   public int time;
130   public boolean side;
131
132   public Person (int i, int t) {
133     time = t;
134     side = Constants.east;
135     id = i;
136   }
137
138   public void move () {
139     if (side == Torch.side) {
140       if (!Verify.randomBool()) {
141         Bridge.tryToCross(this);
142       }
143     }
144   }
145
146   public String JavaDoc toString () {
147     return "" + id;
148   }
149 }
150
151 public class Crossing {
152   public static native void setTotal (int time);
153
154   // due to these natives the code only runs in JPF
155 public static native int getTotal ();
156
157   public static void main (String JavaDoc[] args) {
158     //Verify.beginAtomic();
159
160     // when natives are used one can record the minimal value found so
161 // far to get a better one on the next execution - this
162 // requires the -mulitple-errors option and then the last error
163 // found must be replayed
164 boolean isNative = false;
165
166     if (isNative) {
167       setTotal(30); // set to value larger than solution (17)
168 }
169
170     int total = 0;
171     boolean finished = false;
172     Bridge.initBridge();
173
174     Person p1 = new Person(1, 1);
175     Person p2 = new Person(2, 2);
176     Person p3 = new Person(3, 5);
177     Person p4 = new Person(4, 10);
178     //Verify.endAtomic();
179
180     while (!finished) {
181       //Verify.beginAtomic();
182 p1.move();
183       p2.move();
184       p3.move();
185       p4.move();
186
187       if (Bridge.isFull()) {
188         total += Bridge.Cross();
189
190         if (isNative) {
191           Verify.ignoreIf(total > getTotal());
192         } else {
193           Verify.ignoreIf(total > 17); //with this DFS will also find error
194 }
195
196         Bridge.clearBridge();
197
198         //printConfig(p1,p2,p3,p4,total);
199 finished = !(p1.side || p2.side || p3.side || p4.side);
200       }
201
202       //Verify.endAtomic();
203 }
204
205     //Verify.beginAtomic();
206
207     if (isNative) {
208       if (total < getTotal()) {
209         System.out.println("new total " + total);
210         setTotal(total);
211         assert (total > getTotal());
212       }
213     } else {
214       System.out.println("total time = " + total);
215       assert (total > 17);
216     }
217
218     //Verify.endAtomic();
219 }
220
221   static void printConfig (Person p1, Person p2, Person p3, Person p4,
222                            int total) {
223     if (p1.side == Constants.east) {
224       System.out.print("p1(" + p1.time + ")");
225     }
226
227     if (p2.side == Constants.east) {
228       System.out.print("p2(" + p2.time + ")");
229     }
230
231     if (p3.side == Constants.east) {
232       System.out.print("p3(" + p3.time + ")");
233     }
234
235     if (p4.side == Constants.east) {
236       System.out.print("p4(" + p4.time + ")");
237     }
238
239     System.out.print(" - " + total + " -> ");
240
241     if (p1.side == Constants.west) {
242       System.out.print("p1(" + p1.time + ")");
243     }
244
245     if (p2.side == Constants.west) {
246       System.out.print("p2(" + p2.time + ")");
247     }
248
249     if (p3.side == Constants.west) {
250       System.out.print("p3(" + p3.time + ")");
251     }
252
253     if (p4.side == Constants.west) {
254       System.out.print("p4(" + p4.time + ")");
255     }
256
257     System.out.println();
258   }
259 }
260
Popular Tags