Adding reachability analysis when state matching occurs.
[jpf-core.git] / examples / DiningPhil.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 public class DiningPhil {
20
21   static class Fork {
22   }
23
24   static class Philosopher extends Thread {
25
26     Fork left;
27     Fork right;
28
29     public Philosopher(Fork left, Fork right) {
30       this.left = left;
31       this.right = right;
32       //start();
33     }
34
35     @Override
36         public void run() {
37       // think!
38       synchronized (left) {
39         synchronized (right) {
40           // eat!
41         }
42       }
43     }
44   }
45   
46   static int nPhilosophers = 6;
47
48   public static void main(String[] args) {
49     if (args.length > 0){
50       nPhilosophers = Integer.parseInt(args[0]);
51     }
52     
53     //Verify.beginAtomic();
54     Fork[] forks = new Fork[nPhilosophers];
55     for (int i = 0; i < nPhilosophers; i++) {
56       forks[i] = new Fork();
57     }
58     for (int i = 0; i < nPhilosophers; i++) {
59       Philosopher p = new Philosopher(forks[i], forks[(i + 1) % nPhilosophers]);
60       p.start();
61     }
62     //Verify.endAtomic();
63   }
64 }