Some Simple Vending Machines

There is a tradition in concurrency theory of using vending machines to illustrate various formalisms, perhaps because vending machines are such familiar and prototypical reactive systems. Here we illustrate some behavioral features of BOBJ, by specifying some simple vending machines, and then proving some of their behavioral properties. Although a different formulation might use streams of inputs, the less complex approach of this page may bring out the relevant features of BOBJ more clearly. These examples were done by Joseph Goguen, with help from Kai Lin and Grigore Rosu.

1. The First Vending Machine

The machine specified below accepts quarters and dollars (Q and D, respectively) as well as requests for coffee and tea (C and T, respectively); so these are its methods. States are represented as pairs, consisting of a running total of money deposited but so far unspent (respresented by an integer number of quarters), and a message displayed on (say) an LCD screen; these two are its only attributes. We have chosen not to include an "output" where coffee and tea "actually" accumulate, but instead let the display attribute tell when a beverage is delivered. bth VENDM is pr (INT || QID)*(sort Tuple to S) . ops (Q_) (D_) (T_) (C_) : S -> S . op $_ : S -> Nat . op o_ : S -> Id . op I : -> S . eq I = < 0,'Hello > . var N : Nat . var L : Id . var S : S . eq $ <N, L > = N . eq o <N, L > = L . eq Q <N, L> = <N + 1, 'Thank-you > . eq D <N, L> = <N + 4, 'Thank-you > . cq T <N, L > = <N, 'Please-deposit-more > if N < 4 . cq T <N, L > = <N - 4, 'T > if N >= 4 . cq C <N, L > = <N, 'Please-deposit-more > if N < 6 . cq C <N, L > = <N - 6, 'C > if N >= 6 . end Notice that a beverage request disappears if there are insufficient funds for it. The proofs below will use three simple lemmas about natural numbers: obj LEMMAS is pr VENDM . vars M N : Nat . var L : Id . eq N + M >= N = true . eq (N + M) - N = M . cq N < M = true if N < M - 1 . endo Now we check some simple behavioral equations. Thse first three are all true: cred Q Q Q Q <N, L> == D <N, L> . cred Q D <N, L> == D Q <N, L> . cred Q <0, 'C > == Q <0, 'T > . The equations in the next group are all false, and we will see that BOBJ gets the right answer, although it is also possible that some of these results are true, but cannot be proved with just circular coinductive rewriting, because some case analysis is needed. cred <0, 'C > == <0, 'T > . cred T C <N, L> == C T <N, L> . cred Q T <N, L> == Q C <N, L> . We now try to prove a more difficult result, that C Q T Q Q Q <N, L> = C Q C Q D <N, L> We first try to prove it directly with circular coinductive rewriting. Since this fails (see the BOBJ output in Section 2), we rewrite each side separately, to get some help in understanding what the obstacle is. The resulting normal forms suggest that the result is false when N = 0, and so we do circular coinductive rewriting with case analysis to verify this intuition. The algorithm proves the equation for N > 0 (see Section 2) even though the answer is false, because the case N = 0 fails, as expected. cred C Q T Q Q Q <N, L> == C Q C Q D <N, L> . red C Q T Q Q Q <N, L> . red C Q C Q D <N, L> . cases VCASES for LEMMAS is vars M N : Nat . var L : Id . context <M + N, L> . case op m : -> Nat . eq N = m + 1 . case eq N = 0 . end cred with VCASES C Q T Q Q Q <N, L> == C Q C Q D <N, L> . The case declaration VCASE defines two cases; they are given in the opposite order from the usual, because we expect N = 0 to fail, which would prevent us from seeing the output of the other case. The term given after the keyword context determines when case analysis will be applied. Notice that BOBJ allows new operations to be declared within case definitions. In the first case, a new constant m is introduced, to "Skolemize" the condition N > 0. Case analysis can be used not only for proofs, but also for testing and debugging specifications.

We can show that the result for positive N really is a behavioral result, by reducing the two sides separately, under appropriate assumptions.

open . ops n m : -> Nat . eq n = m + 1 . red C Q T Q Q Q <n, L> . red C Q C Q D <n, L> . close The output in Section 2 shows that the two reduced forms are indeed different.

Just for fun, here are some simple but typical user scenarios, for which we let BOBJ compute the result:

red o D T I . red $ D T I . red o D C I . red $ D C I . red o D D C I . red $ D D C I . red o T D D C I . red $ T D D C I . red o Q I . red $ Q I . red o T C D D D I . red $ T C D D D I . red o T C Q I . red $ T C Q I . red C Q D <N, L> . red Q C Q D <N, L> . The last scenario is a bit tricky: the second quarter cannot be added to the total because it is not possible to determine the value of N, in order to know which rule to apply for C. A case analysis similar to that done above would show that you get a coffee and N quarter dollars in each of the two cases. (This is a good exercise for the interested reader.)

2. Output for the First Vending Machine

Here is the BOBJ output for the code in Section 1: awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.213 built: Tue Nov 26 18:07:27 PST 2002 University of California, San Diego Tue Nov 26 20:58:05 PST 2002 BOBJ> in vend7c ========================================== ***> /net/cs/htdocs/groups/tatami/bobj/examples/vend7c.bob ========================================== bth VENDM ========================================== obj LEMMAS ========================================== ***> the first three should be true: ========================================== c-reduce in LEMMAS : Q (Q (Q (Q (< N , L >)))) == D (< N , L >) using cobasis for LEMMAS: op o _ : S -> Id [prec 15] op $ _ : S -> Nat [prec 15] op Q _ : S -> S [prec 15] op D _ : S -> S [prec 15] op T _ : S -> S [prec 15] op C _ : S -> S [prec 15] --------------------------------------- result: true c-rewrite time: 45ms parse time: 32ms ========================================== c-reduce in LEMMAS : Q (D (< N , L >)) == D (Q (< N , L >)) result: true c-rewrite time: 10ms parse time: 28ms ========================================== c-reduce in LEMMAS : Q (< 0 , 'C >) == Q (< 0 , 'T >) result: true c-rewrite time: 5ms parse time: 16ms ========================================== ***> the next three should be false: ========================================== c-reduce in LEMMAS : < 0 , 'C > == < 0 , 'T > result: false c-rewrite time: 60ms parse time: 9ms ========================================== c-reduce in LEMMAS : T (C (< N , L >)) == C (T (< N , L >)) result: false c-rewrite time: 90ms parse time: 22ms ========================================== c-reduce in LEMMAS : Q (T (< N , L >)) == Q (C (< N , L >)) result: false c-rewrite time: 75ms parse time: 27ms ========================================== c-reduce in LEMMAS : C (Q (T (Q (Q (Q (< N , L >)))))) == C (Q (C (Q (D (< N , L >))))) result: false c-rewrite time: 136ms parse time: 66ms ========================================== reduce in LEMMAS : C (Q (T (Q (Q (Q (< N , L >)))))) result S: C (Q (T < (3 + N) , 'Thank-you >)) rewrite time: 27ms parse time: 11ms ========================================== reduce in LEMMAS : C (Q (C (Q (D (< N , L >))))) result S: C (Q (C < (5 + N) , 'Thank-you >)) rewrite time: 21ms parse time: 9ms ========================================== cases VCASES ========================================== c-reduce in LEMMAS : C (Q (T (Q (Q (Q (< N , L >)))))) == C (Q (C (Q (D (< N , L >))))) use: VCASES ------------------------------------------- case analysis by VCASES ------------------------------------------- introduce constant(s): n for the variable N ------------------------------- case 1 : add: op m : -> Nat assume: n = m + 1 reduce: C (Q (T (< (3 + n) , 'Thank-you >))) == C (Q (C (< (5 + n) , 'Thank-you >))) nf: true ------------------------------- case 2 : assume: n = 0 reduce: C (Q (T (< (3 + n) , 'Thank-you >))) == C (Q (C (< (5 + n) , 'Thank-you >))) nf: < 4 , 'Please-deposit-more > == < 0 , 'C > ------------------------------- result: false c-rewrite time: 424ms parse time: 61ms ========================================== open ========================================== ops n m : -> Nat ========================================== eq n = m + 1 ========================================== reduce in LEMMAS : C (Q (T (Q (Q (Q (< n , L >)))))) result S: C < (1 + m) , 'Thank-you > rewrite time: 49ms parse time: 10ms ========================================== reduce in LEMMAS : C (Q (C (Q (D (< n , L >))))) result S: C < (1 + m) , 'Thank-you > rewrite time: 34ms parse time: 8ms ========================================== close ========================================== reduce in LEMMAS : o (D (T I)) result Id: 'Thank-you rewrite time: 7ms parse time: 1ms ========================================== reduce in LEMMAS : $ (D (T I)) result NzNat: 4 rewrite time: 10ms parse time: 1ms ========================================== reduce in LEMMAS : o (D (C I)) result Id: 'Thank-you rewrite time: 7ms parse time: 2ms ========================================== reduce in LEMMAS : $ (D (C I)) result NzNat: 4 rewrite time: 8ms parse time: 2ms ========================================== reduce in LEMMAS : o (D (D (C I))) result Id: 'Thank-you rewrite time: 9ms parse time: 2ms ========================================== reduce in LEMMAS : $ (D (D (C I))) result NzNat: 8 rewrite time: 10ms parse time: 2ms ========================================== reduce in LEMMAS : o (T (D (D (C I)))) result Id: 'T rewrite time: 15ms parse time: 2ms ========================================== reduce in LEMMAS : $ (T (D (D (C I)))) result NzNat: 4 rewrite time: 18ms parse time: 3ms ========================================== reduce in LEMMAS : o (Q I) result Id: 'Thank-you rewrite time: 4ms parse time: 1ms ========================================== reduce in LEMMAS : $ (Q I) result NzNat: 1 rewrite time: 4ms parse time: 1ms ========================================== reduce in LEMMAS : o (T (C (D (D (D I))))) result Id: 'T rewrite time: 21ms parse time: 3ms ========================================== reduce in LEMMAS : $ (T (C (D (D (D I))))) result NzNat: 2 rewrite time: 23ms parse time: 3ms ========================================== reduce in LEMMAS : o (T (C (Q I))) result Id: 'Please-deposit-more rewrite time: 11ms parse time: 2ms ========================================== reduce in LEMMAS : $ (T (C (Q I))) result NzNat: 1 rewrite time: 12ms parse time: 2ms ========================================== reduce in LEMMAS : C (Q (D (< N , L >))) result S: C < (5 + N) , 'Thank-you > rewrite time: 18ms parse time: 6ms ========================================== reduce in LEMMAS : Q (C (Q (D (< N , L >)))) result S: Q (C < (5 + N) , 'Thank-you >) rewrite time: 22ms parse time: 7ms BOBJ> q Bye. awk%

3. The Second Vending Machine

Our second machine is similar to the first in that it also accepts quarters and dollars (Q and D, respectively) as well as requests for coffee and tea (C and T, respectively); in addition, it has a reset R, which deletes all beverage requests, but still remembers how much has been deposited. So these five are its methods. States are again represented as pairs, of a running total of deposited but unspent money (respresented by an integer number of quarters), and a message; these two are again the only attributes. However, this machine differs from the first in that it queues up requests for coffee or tea, and can then only fulfill those requests in the order that they were made, unless reset by R. bth VEND is pr (INT || QID)*(sort Tuple to S). ops (C_)(T_)(D_)(Q_)(R_) : S -> S [prec 2]. op $_ : S -> Nat . op o_ : S -> Id . let I = <0, 'Hello > . let msg1 = 'Please-Deposit-More . var S : S . vars M N : Nat . var L : Id . eq $ <N, L> = N . cq $ C S = $ S if $ S < 6 . cq $ T S = $ S if $ S < 4 . eq o <N, L> = L . eq R S = <$ S, 'Hello > . cq C <N, L> = C <N, msg1> if N < 6 and L =/= msg1 . cq T <N, L> = T <N, msg1> if N < 4 and L =/= msg1 . eq D <N, L> = <N + 4, 'Thanks > . eq Q <N, L> = <N + 1, 'Thanks > . cq T <N, L> = <N - 4, 'T > if N >= 4 . cq C <N, L> = <N - 6, 'C > if N >= 6 . cq Q C S = C Q S if $ S < 6 . cq D C S = C D S if $ S < 6 . cq Q T S = T Q S if $ S < 4 . cq D T S = T D S if $ S < 4 . end Without the reset method, a malicious anti-coffee activist could request a huge number of teas without depositing any money, and then depart, forcing a subsequent coffee addict to buy all that tea before consuming any coffee.

The proofs below use two simple lemmas about natural numbers:

obj LEMMAS is pr VEND . vars M N : Nat . var L : Id . eq N + M >= N = true . eq (N + M) - N = M . endo We again check some simple equations. Those in the first group are all true: cred Q Q Q Q <N, L> == D <N, L> . cred Q D <N, L> == D Q <N, L> . cred Q <0, 'C > == Q <0, 'T > . cred R C I == R T I . cred Q R Q <N, L> == Q Q R <N, L> . The next group of equations are all false, and as before, although BOBJ gets the right answer, it is possible that some results fail, because case analysis is needed. cred <0, 'C > == <0, 'T > . cred T C <N, L> == C T <N, L> . cred Q T <N, L> == Q C <N, L> . cred R C <N, L> == R T <N, L> . We now try to prove the same more difficult result as before, that C Q T Q Q Q <N, L> = C Q C Q D <N, L> first directly by circular coinductive rewriting. Since this fails, we rewrite each side separately, hoping for some insight. cred C Q T Q Q Q <N, L> == C Q C Q D <N, L> . red C Q T Q Q Q <N, L> . red C Q C Q D <N, L> . The normal forms suggest that as before, case analysis on N = 0 and N > 0 is needed. cases VCASES for LEMMAS is vars M N : Nat . var L : Id . context <M + N, L> . case eq N = 0 . case op m : -> Nat . eq N = m + 1 . end cred with VCASES C Q T Q Q Q <N, L> == C Q C Q D <N, L> . This time, both cases succeed, and the result is proved. As before, we can also check that the result is truly behavioral by reducing the two sides. open . ops n m : -> Nat . eq n = m + 1 . red C Q C Q D <n, L> . red C Q T Q Q Q <n, L> . close We now run the same simple but typical user scenarios as in the first example, and let BOBJ compute the results: red o D T I . red $ D T I . red o D C I . red $ D C I . red o D D C I . red $ D D C I . red o T D D C I . red $ T D D C I . red o Q I . red $ Q I . red o T C D D D I . red $ T C D D D I . red o T C Q I . red $ T C Q I . red C Q D <N, L> . red Q C Q D <N, L> . As before, in the last reduction the second quarter cannot be added to the total because it is impossible to know whether N is positive. The reader is urged to run a case analysis to show that you get coffee and N quarter dollars in each case.

4. Output for the Second Vending Machine

Here is the BOBJ output from the code in Section 3: awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.213 built: Tue Nov 26 18:07:27 PST 2002 University of California, San Diego Tue Nov 26 21:12:29 PST 2002 BOBJ> in vend4c ========================================== ***> /net/cs/htdocs/groups/tatami/bobj/examples/vend4.bob ========================================== bth VEND ========================================== obj LEMMAS ========================================== ***> the first five should be true: ========================================== c-reduce in LEMMAS : Q (Q (Q (Q (< N , L >)))) == D (< N , L >) using cobasis for LEMMAS: op o _ : S -> Id [prec 15] op $ _ : S -> Nat [prec 15] op C _ : S -> S [prec 2] op T _ : S -> S [prec 2] op D _ : S -> S [prec 2] op Q _ : S -> S [prec 2] op R _ : S -> S [prec 2] --------------------------------------- result: true c-rewrite time: 32ms parse time: 29ms ========================================== c-reduce in LEMMAS : Q (D (< N , L >)) == D (Q (< N , L >)) result: true c-rewrite time: 10ms parse time: 23ms ========================================== c-reduce in LEMMAS : Q (< 0 , 'C >) == Q (< 0 , 'T >) result: true c-rewrite time: 6ms parse time: 16ms ========================================== c-reduce in LEMMAS : R (C I) == R (T I) result: true c-rewrite time: 21ms parse time: 4ms ========================================== c-reduce in LEMMAS : Q (R (Q (< N , L >))) == Q (Q (R (< N , L >))) result: true c-rewrite time: 17ms parse time: 29ms ========================================== ***> the next four should be false: ========================================== c-reduce in LEMMAS : < 0 , 'C > == < 0 , 'T > result: false c-rewrite time: 111ms parse time: 10ms ========================================== c-reduce in LEMMAS : T (C (< N , L >)) == C (T (< N , L >)) result: false c-rewrite time: 112ms parse time: 22ms ========================================== c-reduce in LEMMAS : Q (T (< N , L >)) == Q (C (< N , L >)) result: false c-rewrite time: 131ms parse time: 23ms ========================================== c-reduce in LEMMAS : R (C (< N , L >)) == R (T (< N , L >)) result: false c-rewrite time: 146ms parse time: 23ms ========================================== c-reduce in LEMMAS : C (Q (T (Q (Q (Q (< N , L >)))))) == C (Q (C (Q (D (< N , L >))))) result: false c-rewrite time: 219ms parse time: 63ms ========================================== reduce in LEMMAS : C (Q (T (Q (Q (Q (< N , L >)))))) result S: C (Q (T < (3 + N) , 'Thanks >)) rewrite time: 54ms parse time: 11ms ========================================== reduce in LEMMAS : C (Q (C (Q (D (< N , L >))))) result S: C (Q (C < (5 + N) , 'Thanks >)) rewrite time: 39ms parse time: 9ms ========================================== cases N0POS ========================================== c-reduce in LEMMAS : C (Q (T (Q (Q (Q (< N , L >)))))) == C (Q (C (Q (D (< N , L >))))) use: N0POS ------------------------------------------- case analysis by N0POS ------------------------------------------- introduce constant(s): n for the variable N ------------------------------- case 1 : assume: n = 0 reduce: C (Q (T (< (3 + n) , 'Thanks >))) == C (Q (C (< (5 + n) , 'Thanks >))) nf: true ------------------------------- case 2 : add: op m : -> Nat assume: n = 1 + m reduce: C (Q (T (< (3 + n) , 'Thanks >))) == C (Q (C (< (5 + n) , 'Thanks >))) nf: true ----------------------------------------- analyzed 2 cases, all cases succeeded result: true c-rewrite time: 321ms parse time: 55ms ========================================== open ========================================== ops n m : -> Nat ========================================== eq n = m + 1 ========================================== ***> the following should be true: ========================================== c-reduce in LEMMAS : C (Q (T (Q (Q (Q (< n , L >)))))) == C (Q (C (Q (D (< n , L >))))) using cobasis for LEMMAS: op o _ : S -> Id [prec 15] op $ _ : S -> Nat [prec 15] op C _ : S -> S [prec 2] op T _ : S -> S [prec 2] op D _ : S -> S [prec 2] op Q _ : S -> S [prec 2] op R _ : S -> S [prec 2] --------------------------------------- result: true c-rewrite time: 119ms parse time: 59ms ========================================== reduce in LEMMAS : C (Q (C (Q (D (< n , L >))))) result S: C < (1 + m) , 'Thanks > rewrite time: 49ms parse time: 9ms ========================================== reduce in LEMMAS : C (Q (T (Q (Q (Q (< n , L >)))))) result S: C < (1 + m) , 'Thanks > rewrite time: 67ms parse time: 11ms ========================================== close ========================================== reduce in LEMMAS : o (D (T I)) result Id: 'T rewrite time: 17ms parse time: 2ms ========================================== reduce in LEMMAS : $ (D (T I)) result Zero: 0 rewrite time: 14ms parse time: 1ms ========================================== reduce in LEMMAS : o (D (C I)) result Id: o C < 4 , 'Please-Deposit-More > rewrite time: 25ms parse time: 1ms ========================================== reduce in LEMMAS : $ (D (C I)) result NzNat: 4 rewrite time: 29ms parse time: 2ms ========================================== reduce in LEMMAS : o (D (D (C I))) result Id: 'C rewrite time: 33ms parse time: 2ms ========================================== reduce in LEMMAS : $ (D (D (C I))) result NzNat: 2 rewrite time: 33ms parse time: 2ms ========================================== reduce in LEMMAS : o (T (D (D (C I)))) result Id: o T < 2 , 'Please-Deposit-More > rewrite time: 51ms parse time: 2ms ========================================== reduce in LEMMAS : $ (T (D (D (C I)))) result NzNat: 2 rewrite time: 48ms parse time: 3ms ========================================== reduce in LEMMAS : o (Q I) result Id: 'Thanks rewrite time: 4ms parse time: 1ms ========================================== reduce in LEMMAS : $ (Q I) result NzNat: 1 rewrite time: 4ms parse time: 1ms ========================================== reduce in LEMMAS : o (T (C (D (D (D I))))) result Id: 'T rewrite time: 23ms parse time: 3ms ========================================== reduce in LEMMAS : $ (T (C (D (D (D I))))) result NzNat: 2 rewrite time: 129ms parse time: 3ms ========================================== reduce in LEMMAS : o (T (C (Q I))) result Id: o T (C < 1 , 'Please-Deposit-More >) rewrite time: 20ms parse time: 4ms ========================================== reduce in LEMMAS : $ (T (C (Q I))) result NzNat: 1 rewrite time: 14ms parse time: 2ms ========================================== reduce in LEMMAS : C (Q (D (< N , L >))) result S: C < (5 + N) , 'Thanks > rewrite time: 19ms parse time: 5ms ========================================== reduce in LEMMAS : Q (C (Q (D (< N , L >)))) result S: Q (C < (5 + N) , 'Thanks >) rewrite time: 37ms parse time: 18ms BOBJ> q Bye. awk%
To BOBJ examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Thu Nov 28 22:12:55 PST 2002