Mercurial > hg > Members > kono > jpf-core

annotate src/tests/gov/nasa/jpf/test/mc/data/CrossingTest.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
1 /*
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
2 * Copyright (C) 2014, United States Government, as represented by the
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
3 * Administrator of the National Aeronautics and Space Administration.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
4 * All rights reserved.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
5 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
8 * in compliance with the License. You may obtain a copy of the License at
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
9 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
10 * http://www.apache.org/licenses/LICENSE-2.0.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
11 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
12 * Unless required by applicable law or agreed to in writing, software
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
13 * distributed under the License is distributed on an "AS IS" BASIS,
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
15 * See the License for the specific language governing permissions and
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
16 * limitations under the License.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
17 */
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
18 /**
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
19 * This is the famous Bridge-crossing puzzle. The aim is to see what the minimum
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
20 * amount of time is for 4 people to cross with flash-light (torch): 10.5.2.1.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
21 * The answer is 17 for the given configuration.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
22 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
23 * One can find this solution with JPF in BFS search mode - DFS will not
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
24 * work since this is an infinite-state program (time keeps increasing).
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
25 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
26 * If one uses the ignoreIf(cond) call the branches that will lead to
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
27 * solutions worst than the current will be cut-off and this will allow
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
28 * DFS also to complete - and BFS to terminate faster.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
29 *
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
30 * When setting the native flag in main one can also save information
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
31 * from one run to the next using JPF's native peer methods -
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
32 * see JPF_Crossing.java for the code of getTotal() and setTotal(int).
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
33 */
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
34 package gov.nasa.jpf.test.mc.data;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
35
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
36 import gov.nasa.jpf.util.test.TestJPF;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
37 import gov.nasa.jpf.vm.Verify;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
38
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
39 import org.junit.Test;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
40
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
41 public class CrossingTest extends TestJPF {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
42
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
43 static class Constants {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
44
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
45 public static final boolean east = true;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
46 public static final boolean west = false;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
47 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
48
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
49 static class Torch {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
50
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
51 public static boolean side = Constants.east;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
52
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
53 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
54 public String toString() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
55 if (side == Constants.east) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
56 return "east";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
57 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
58 return "west";
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
59 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
60 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
61 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
62
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
63 static class Bridge {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
64
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
65 static Person[] onBridge = new Person[2];
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
66 static int numOnBridge = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
67
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
68 public static boolean isFull() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
69 return numOnBridge != 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
70 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
71
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
72 public static int Cross() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
73 int time = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
74 Torch.side = !Torch.side;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
75
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
76 if (numOnBridge == 1) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
77 onBridge[0].side = Torch.side;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
78 time = onBridge[0].time;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
79
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
80 //System.out.println("Person " + onBridge[0] +
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
81 // " moved to " + Torch.side +
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
82 // " in time " + time);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
83 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
84 assert onBridge[0] != null : "Argh, null " + numOnBridge;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
85 assert onBridge[1] != null;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
86
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
87 onBridge[0].side = Torch.side;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
88 onBridge[1].side = Torch.side;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
89
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
90 if (onBridge[0].time > onBridge[1].time) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
91 time = onBridge[0].time;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
92 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
93 time = onBridge[1].time;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
94 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
95
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
96 //System.out.println("Person " + onBridge[0] +
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
97 // " and Person " + onBridge[1] +
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
98 // " moved to " + Torch.side +
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
99 // " in time " + time);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
100 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
101
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
102 return time;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
103 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
104
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
105 public static void clearBridge() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
106 if (numOnBridge == 0) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
107 return;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
108 } else if (numOnBridge == 1) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
109 onBridge[0] = null;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
110 numOnBridge = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
111 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
112 onBridge[0] = null;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
113 onBridge[1] = null;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
114 numOnBridge = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
115 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
116 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
117
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
118 public static void initBridge() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
119 onBridge[0] = null;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
120 onBridge[1] = null;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
121 numOnBridge = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
122 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
123
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
124 public static boolean tryToCross(Person th) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
125 if ((numOnBridge < 2) && (onBridge[0] != th) && (onBridge[1] != th)) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
126 onBridge[numOnBridge++] = th;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
127
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
128 return true;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
129 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
130 return false;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
131 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
132 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
133 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
134
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
135 static class Person {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
136 // person to cross the bridge
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
137
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
138 int id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
139 public int time;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
140 public boolean side;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
141
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
142 public Person(int i, int t) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
143 time = t;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
144 side = Constants.east;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
145 id = i;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
146 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
147
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
148 public void move() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
149 if (side == Torch.side) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
150 if (!Verify.randomBool()) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
151 Bridge.tryToCross(this);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
152 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
153 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
154 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
155
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
156 @Override
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
157 public String toString() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
158 return "" + id;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
159 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
160 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
161
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
162 public static native void setTotal(int time);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
163
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
164 // due to these natives the code only runs in JPF
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
165 public static native int getTotal();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
166
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
167 public void run() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
168 //Verify.beginAtomic();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
169
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
170 // when natives are used one can record the minimal value found so
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
171 // far to get a better one on the next execution - this
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
172 // requires the -mulitple-errors option and then the last error
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
173 // found must be replayed
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
174 boolean isNative = false;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
175
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
176 if (isNative) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
177 setTotal(30); // set to value larger than solution (17)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
178 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
179
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
180 int total = 0;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
181 boolean finished = false;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
182 Bridge.initBridge();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
183
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
184 Person p1 = new Person(1, 1);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
185 Person p2 = new Person(2, 2);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
186 Person p3 = new Person(3, 5);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
187 Person p4 = new Person(4, 10);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
188 //Verify.endAtomic();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
189
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
190 while (!finished) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
191 //Verify.beginAtomic();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
192 p1.move();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
193 p2.move();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
194 p3.move();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
195 p4.move();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
196
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
197 if (Bridge.isFull()) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
198 total += Bridge.Cross();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
199
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
200 if (isNative) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
201 Verify.ignoreIf(total > getTotal());
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
202 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
203 Verify.ignoreIf(total > 17); //with this DFS will also find error
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
204 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
205
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
206 Bridge.clearBridge();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
207
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
208 //printConfig(p1,p2,p3,p4,total);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
209 finished = !(p1.side || p2.side || p3.side || p4.side);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
210 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
211
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
212 //Verify.endAtomic();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
213 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
214
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
215 //Verify.beginAtomic();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
216
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
217 if (isNative) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
218 if (total < getTotal()) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
219 System.out.println("new total " + total);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
220 setTotal(total);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
221 assert (total > getTotal());
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
222 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
223 } else {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
224 System.out.println("total time = " + total);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
225 assert (total > 17) : "total > 17 | total = " + total;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
226 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
227
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
228 //Verify.endAtomic();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
229 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
230
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
231 static void printConfig(Person p1, Person p2, Person p3, Person p4,
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
232 int total) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
233 if (p1.side == Constants.east) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
234 System.out.print("p1(" + p1.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
235 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
236
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
237 if (p2.side == Constants.east) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
238 System.out.print("p2(" + p2.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
239 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
240
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
241 if (p3.side == Constants.east) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
242 System.out.print("p3(" + p3.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
243 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
244
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
245 if (p4.side == Constants.east) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
246 System.out.print("p4(" + p4.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
247 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
248
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
249 System.out.print(" - " + total + " -> ");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
250
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
251 if (p1.side == Constants.west) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
252 System.out.print("p1(" + p1.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
253 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
254
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
255 if (p2.side == Constants.west) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
256 System.out.print("p2(" + p2.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
257 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
258
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
259 if (p3.side == Constants.west) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
260 System.out.print("p3(" + p3.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
261 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
262
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
263 if (p4.side == Constants.west) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
264 System.out.print("p4(" + p4.time + ")");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
265 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
266
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
267 System.out.println();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
268 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
269
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
270
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
271 @Test public void testNoHeuristic () {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
272 if (verifyAssertionError()){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
273 run();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
274 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
275 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
276
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
277 @Test public void testBFSHeuristic() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
278 if (verifyAssertionError("+search.class=gov.nasa.jpf.search.heuristic.BFSHeuristic")){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
279 run();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
280 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
281 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
282 }