001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019:
020: /**
021: * This is the famous Bridge-crossing puzzle. The aim is to see what the minimum
022: * amount of time is for 4 people to cross with flash-light (torch): 10.5.2.1.
023: * The answer is 17 for the given configuration.
024: *
025: * One can find this solution with JPF in BFS search mode - DFS will not
026: * work since this is an infinite-state program (time keeps increasing).
027: *
028: * If one uses the ignoreIf(cond) call the branches that will lead to
029: * solutions worst than the current will be cut-off and this will allow
030: * DFS also to complete - and BFS to terminate faster.
031: *
032: * When setting the native flag in main one can also save information
033: * from one run to the next using JPF's native peer methods -
034: * see JPF_Crossing.java for the code of getTotal() and setTotal(int).
035: */package gov.nasa.jpf.mc;
036:
037: import gov.nasa.jpf.jvm.Verify;
038:
039: class Constants {
040: public static final boolean east = true;
041: public static final boolean west = false;
042: }
043:
044: class Torch {
045: public static boolean side = Constants.east;
046:
047: public String toString() {
048: if (side == Constants.east) {
049: return "east";
050: } else {
051: return "west";
052: }
053: }
054: }
055:
056: class Bridge {
057: static Person[] onBridge = new Person[2];
058: static int numOnBridge = 0;
059:
060: public static boolean isFull() {
061: return numOnBridge != 0;
062: }
063:
064: public static int Cross() {
065: int time = 0;
066: Torch.side = !Torch.side;
067:
068: if (numOnBridge == 1) {
069: onBridge[0].side = Torch.side;
070: time = onBridge[0].time;
071:
072: //System.out.println("Person " + onBridge[0] +
073: // " moved to " + Torch.side +
074: // " in time " + time);
075: } else {
076: onBridge[0].side = Torch.side;
077: onBridge[1].side = Torch.side;
078:
079: if (onBridge[0].time > onBridge[1].time) {
080: time = onBridge[0].time;
081: } else {
082: time = onBridge[1].time;
083: }
084:
085: //System.out.println("Person " + onBridge[0] +
086: // " and Person " + onBridge[1] +
087: // " moved to " + Torch.side +
088: // " in time " + time);
089: }
090:
091: return time;
092: }
093:
094: public static void clearBridge() {
095: if (numOnBridge == 0) {
096: return;
097: } else if (numOnBridge == 1) {
098: onBridge[0] = null;
099: numOnBridge = 0;
100: } else {
101: onBridge[0] = null;
102: onBridge[1] = null;
103: numOnBridge = 0;
104: }
105: }
106:
107: public static void initBridge() {
108: onBridge[0] = null;
109: onBridge[1] = null;
110: numOnBridge = 0;
111: }
112:
113: public static boolean tryToCross(Person th) {
114: if ((numOnBridge < 2) && (onBridge[0] != th)
115: && (onBridge[1] != th)) {
116: onBridge[numOnBridge++] = th;
117:
118: return true;
119: } else {
120: return false;
121: }
122: }
123: }
124:
125: class Person {
126: // person to cross the bridge
127: int id;
128: public int time;
129: public boolean side;
130:
131: public Person(int i, int t) {
132: time = t;
133: side = Constants.east;
134: id = i;
135: }
136:
137: public void move() {
138: if (side == Torch.side) {
139: if (!Verify.randomBool()) {
140: Bridge.tryToCross(this );
141: }
142: }
143: }
144:
145: public String toString() {
146: return "" + id;
147: }
148: }
149:
150: public class Crossing {
151: public static native void setTotal(int time);
152:
153: // due to these natives the code only runs in JPF
154: public static native int getTotal();
155:
156: public static void main(String[] args) {
157: //Verify.beginAtomic();
158:
159: // when natives are used one can record the minimal value found so
160: // far to get a better one on the next execution - this
161: // requires the -mulitple-errors option and then the last error
162: // found must be replayed
163: boolean isNative = false;
164:
165: if (isNative) {
166: setTotal(30); // set to value larger than solution (17)
167: }
168:
169: int total = 0;
170: boolean finished = false;
171: Bridge.initBridge();
172:
173: Person p1 = new Person(1, 1);
174: Person p2 = new Person(2, 2);
175: Person p3 = new Person(3, 5);
176: Person p4 = new Person(4, 10);
177: //Verify.endAtomic();
178:
179: while (!finished) {
180: //Verify.beginAtomic();
181: p1.move();
182: p2.move();
183: p3.move();
184: p4.move();
185:
186: if (Bridge.isFull()) {
187: total += Bridge.Cross();
188:
189: if (isNative) {
190: Verify.ignoreIf(total > getTotal());
191: } else {
192: Verify.ignoreIf(total > 17); //with this DFS will also find error
193: }
194:
195: Bridge.clearBridge();
196:
197: //printConfig(p1,p2,p3,p4,total);
198: finished = !(p1.side || p2.side || p3.side || p4.side);
199: }
200:
201: //Verify.endAtomic();
202: }
203:
204: //Verify.beginAtomic();
205:
206: if (isNative) {
207: if (total < getTotal()) {
208: System.out.println("new total " + total);
209: setTotal(total);
210: assert (total > getTotal());
211: }
212: } else {
213: System.out.println("total time = " + total);
214: assert (total > 17);
215: }
216:
217: //Verify.endAtomic();
218: }
219:
220: static void printConfig(Person p1, Person p2, Person p3, Person p4,
221: int total) {
222: if (p1.side == Constants.east) {
223: System.out.print("p1(" + p1.time + ")");
224: }
225:
226: if (p2.side == Constants.east) {
227: System.out.print("p2(" + p2.time + ")");
228: }
229:
230: if (p3.side == Constants.east) {
231: System.out.print("p3(" + p3.time + ")");
232: }
233:
234: if (p4.side == Constants.east) {
235: System.out.print("p4(" + p4.time + ")");
236: }
237:
238: System.out.print(" - " + total + " -> ");
239:
240: if (p1.side == Constants.west) {
241: System.out.print("p1(" + p1.time + ")");
242: }
243:
244: if (p2.side == Constants.west) {
245: System.out.print("p2(" + p2.time + ")");
246: }
247:
248: if (p3.side == Constants.west) {
249: System.out.print("p3(" + p3.time + ")");
250: }
251:
252: if (p4.side == Constants.west) {
253: System.out.print("p4(" + p4.time + ")");
254: }
255:
256: System.out.println();
257: }
258: }
|