src/examples/Crossing.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 /**
  19  * This is the famous Bridge-crossing puzzle. The aim is to see what the minimum
  20  * amount of time is for 4 people to cross with flash-light (torch): 10.5.2.1.
  21  * The answer is 17 for the given configuration.
  22  *
  23  * Purpose of this example is to show how to use the 'Verify' API in test
  24  * applications (usually drivers)
  25  *
  26  * One can find this solution with JPF in BFS search mode - DFS will not
  27  * work since this is an infinite-state program (time keeps increasing).
  28  *
  29  * If one uses the ignoreIf(cond) call the branches that will lead to
  30  * solutions worst than the current will be cut-off and this will allow
  31  * DFS also to complete - and BFS to terminate faster.
  32  *
  33  * When setting the native flag in main one can also save information
  34  * from one run to the next using JPF's native peer methods -
  35  * see JPF_Crossing.java for the code of getTotal() and setTotal(int).
  36  */
  37
  38 import gov.nasa.jpf.vm.Verify;
  39
  40 enum Side { LEFT, RIGHT }
  41
  42 class Bridge {
  43
  44   Side torchSide;
  45   Person[] onBridge = new Person[2];
  46   int numOnBridge = 0;
  47
  48   public Bridge (Side torchSide){
  49     this.torchSide = torchSide;
  50   }
  51
  52   void moveTorch(){
  53     if (torchSide == Side.LEFT){
  54       torchSide = Side.RIGHT;
  55     } else {
  56       torchSide = Side.LEFT;
  57     }
  58   }
  59
  60   public int cross() {
  61     int time = 0;
  62     moveTorch();
  63
  64     if (numOnBridge == 1) {
  65       onBridge[0].side = torchSide;
  66       time = onBridge[0].timeToCross;
  67
  68     //System.out.println("Person " + onBridge[0] +
  69     //                     " moved to " + Torch.side +
  70     //               " in time " + time);
  71     } else {
  72       onBridge[0].side = torchSide;
  73       onBridge[1].side = torchSide;
  74
  75       if (onBridge[0].timeToCross > onBridge[1].timeToCross) {
  76         time = onBridge[0].timeToCross;
  77       } else {
  78         time = onBridge[1].timeToCross;
  79       }
  80
  81     //System.out.println("Person " + onBridge[0] +
  82     //                 " and Person " + onBridge[1] +
  83     //                 " moved to " + Torch.side +
  84     //                 " in time " + time);
  85     }
  86
  87     return time;
  88   }
  89
  90   public void clearBridge() {
  91     numOnBridge = 0;
  92     onBridge[0] = null;
  93     onBridge[1] = null;
  94   }
  95
  96   boolean isFull(){
  97     return numOnBridge == 2;
  98   }
  99
 100   boolean arePersonsOnBridge(){
 101     return numOnBridge > 0;
 102   }
 103
 104   boolean isPersonOnBridge (Person p){
 105     return (p == onBridge[0] || p == onBridge[1]);
 106   }
 107
 108   void putPersonOnBridge (Person p){
 109     onBridge[numOnBridge++] = p;
 110   }
 111 }
 112
 113 class Person {
 114   String name;
 115   Side side;
 116   int timeToCross;
 117
 118   public Person(String name, int timeToCross) {
 119     this.timeToCross = timeToCross;
 120     this.name = name;
 121   }
 122
 123   public void tryToMove (Bridge bridge) {
 124     if (side == bridge.torchSide) {
 125       if (!Verify.getBoolean()) {
 126         if (! (bridge.isFull() || bridge.isPersonOnBridge(this))){
 127           bridge.putPersonOnBridge(this);
 128         }
 129       }
 130     }
 131   }
 132
 133   @Override
 134   public String toString(){
 135     return name;
 136   }
 137 }
 138
 139 public class Crossing {
 140
 141   Bridge bridge;
 142   Person[] persons;
 143   int elapsedTime;
 144   Side initialSide;
 145
 146   public Crossing (Person[] persons, Side initialSide){
 147     this.persons = persons;
 148     for (Person p : persons){
 149       p.side = initialSide;
 150     }
 151
 152     this.bridge = new Bridge( initialSide);
 153     this.initialSide = initialSide;
 154   }
 155
 156   boolean haveAllPersonsCrossed (){
 157     for (Person p : persons){
 158       if (p.side == initialSide){
 159         return false;
 160       }
 161     }
 162
 163     return true;
 164   }
 165
 166   void solve (){
 167     printPersons();
 168     System.out.println();
 169     printCrossingState();
 170     //Verify.setCounter(0, Integer.MAX_VALUE);
 171
 172     while (!haveAllPersonsCrossed()){
 173       for (Person p : persons){
 174         p.tryToMove(bridge);
 175       }
 176
 177       if (bridge.arePersonsOnBridge()) {
 178         elapsedTime += bridge.cross();
 179
 180         //Verify.ignoreIf(elapsedTime >= Verify.getCounter(0));
 181         //Verify.ignoreIf(elapsedTime > 17); //with this DFS will also find error
 182
 183         bridge.clearBridge();
 184       }
 185
 186       printCrossingState();
 187     }
 188
 189
 190     System.out.println("total time = " + elapsedTime);
 191
 192     //Verify.setCounter(0, elapsedTime); // new minimum
 193     Verify.printPathOutput("done");
 194     Verify.storeTraceAndTerminateIf(elapsedTime == 17, null, null);
 195     //assert (elapsedTime > 17);
 196   }
 197
 198   String personsOnSide (Side side){
 199     int n=0;
 200     StringBuilder sb = new StringBuilder();
 201     for (Person p : persons){
 202       if (p.side == side){
 203         if (n++ > 0){
 204           sb.append(',');
 205         }
 206         sb.append( p);
 207       }
 208     }
 209     return sb.toString();
 210   }
 211
 212   String torchSymbol (Side side){
 213     if (bridge.torchSide == side){
 214       return "*";
 215     } else {
 216       return " ";
 217     }
 218   }
 219
 220   void printPersons(){
 221     for (Person p : persons){
 222       System.out.printf("%10s needs %2d min to cross\n", p.name, p.timeToCross);
 223     }
 224   }
 225
 226   void printCrossingState (){
 227     System.out.printf("%20s %s====%s %-20s : elapsed time=%d\n",
 228             personsOnSide(Side.LEFT), torchSymbol(Side.LEFT),
 229             torchSymbol(Side.RIGHT), personsOnSide(Side.RIGHT), elapsedTime);
 230   }
 231
 232   public static void main(String[] args) {
 233     Person[] persons = {
 234       new Person("Bill", 1),
 235       new Person("Xoe", 2),
 236       new Person("Sue", 5),
 237       new Person("Joe", 10)
 238     };
 239
 240     Crossing crossing = new Crossing( persons, Side.LEFT);
 241     crossing.solve();
 242   }
 243 }