01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
11: // Universitaet Koblenz-Landau, Germany
12: // Chalmers University of Technology, Sweden
13: //
14: // The KeY system is protected by the GNU General Public License.
15: // See LICENSE.TXT for details.
16: /** $Id: PersistentCondition.java 1.4.1.1 Tue, 26 Jun 2007 10:47:12 +0200 christian $
17: * @(#)$RCSfile$ 1.1 2003-02-10 Andre Platzer
18: *
19: * Copyright (c) 2003 Andre Platzer. All Rights Reserved.
20: */package de.uka.ilkd.key.cspec;
21:
22: /**
23: * Implementation of persistent conditions, i.e. conditions that do
24: * not suffer from signal loss. Note that this concept can be
25: * generalized beyond the limitations of our current implementation.
26: * However, we do not yet have any needs for more sophisticated
27: * conditions.
28: *
29: * @author André Platzer
30: * @version 1.1, 2003-02-10
31: * @version-revision $Revision: 1.4.1.1 $, $Date: Tue, 26 Jun 2007 10:47:12 +0200 $
32: */
33: public class PersistentCondition {
34: private final Object synchronization;
35: private int count;
36:
37: /**
38: * Create a new condition.
39: */
40: public PersistentCondition() {
41: //@internal note that we do not need synchronization, here, since the constructor has not yet returned
42: count = 0;
43: synchronization = new Object();
44: }
45:
46: /**
47: * Signal that this condition has become true.
48: * @see Object#notifyAll()
49: */
50: public void signal() {
51: synchronized (synchronization) {
52: count = count + 1;
53: synchronization.notifyAll();
54: }
55: }
56:
57: /**
58: * Wait until the condition is true.
59: * If the condition has not yet become true due to an earlier call to
60: * {@link #signal()}, this method will wait until {@link #signal()} gets called.
61: * @throws InterruptedException if another thread has interrupted
62: * the current thread. The interrupted status of the current
63: * thread is cleared when this exception is thrown.
64: * @see Object#wait()
65: */
66: public void waitFor() throws InterruptedException {
67: synchronized (synchronization) {
68: if (count > 0)
69: return;
70: else
71: synchronization.wait();
72: }
73: }
74: }// PersistentCondition
|