01: package U2.T2.examples;
02:
03: /**
04: * An example of a class with a temporal property. This class
05: * implements a simple vote manager. When an instance of this class is
06: * created, we specify how many ballots we have. Users can call
07: * voteYes or voteNo. The manager will manage the counting. There is
08: * also a method to stop the counting.
09: *
10: * <p>We want a temporal specification that says:
11: *
12: * []!open && numberOfBallots=N ==> []numberOfBallots=N
13: *
14: * That is, once the counting is stopped, the number of ballots still
15: * left in the manager should not change anymore. This property is
16: * implemented as a never-claim automaton, coded in the class
17: * invariant.
18: */
19:
20: public class SimpleVotesManager {
21:
22: private int numberOfBallots;
23: private int yes = 0;
24: private int no = 0;
25: private boolean open = true;
26:
27: public SimpleVotesManager(int ballots) {
28: numberOfBallots = ballots;
29: }
30:
31: public void voteYes() {
32: if (open && numberOfBallots > 0) {
33: numberOfBallots--;
34: yes++;
35: }
36: }
37:
38: public void voteNo() {
39: if (open && numberOfBallots > 0) {
40: numberOfBallots--;
41: no++;
42: }
43: }
44:
45: public void close() {
46: open = false;
47: }
48:
49: public void voteYes(int n) {
50: if (numberOfBallots > n) {
51: numberOfBallots = numberOfBallots - n;
52: yes = yes + n;
53: }
54: }
55:
56: private static final int NEVER_STATE_INIT = 0;
57: private static final int NEVER_STATE_1 = 1;
58: private static final int NEVER_STATE_ACCEPT = 2;
59:
60: /**
61: * Defining auxiliary variables for the neverclaim automaton.
62: */
63: private int aux_state = NEVER_STATE_INIT;
64: private int aux_numberOfBallots_frozen;
65:
66: /**
67: * The neverclaim automaton is coded in the class invariant.
68: */
69: public boolean classinv() {
70:
71: if (aux_state == NEVER_STATE_INIT && open)
72: return true;
73:
74: if (aux_state == NEVER_STATE_INIT && !open) {
75: aux_state = NEVER_STATE_1;
76: aux_numberOfBallots_frozen = numberOfBallots;
77: return true;
78: }
79:
80: if (aux_state == NEVER_STATE_1
81: && numberOfBallots != aux_numberOfBallots_frozen) {
82:
83: aux_state = NEVER_STATE_ACCEPT;
84: return false;
85: }
86:
87: if (aux_state == NEVER_STATE_1
88: && numberOfBallots == aux_numberOfBallots_frozen)
89:
90: return true;
91:
92: return false;
93: }
94:
95: }
|