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 .
eq o = L .
eq Q = .
eq D = .
cq T = if N < 4 .
cq T = if N >= 4 .
cq C = if N < 6 .
cq 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 == D .
cred Q D == D Q .
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 == C T .
cred Q T == Q C .
We now try to prove a more difficult result, that
C Q T Q Q Q = C Q C Q D
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 == C Q C Q D .
red C Q T Q Q Q .
red C Q C Q D .
cases VCASES for LEMMAS is
vars M N : Nat . var L : Id .
context .
case op m : -> Nat .
eq N = m + 1 .
case eq N = 0 .
end
cred with VCASES C Q T Q Q Q == C Q C Q D .
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 .
red C Q C Q D .
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 .
red Q C Q D .
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 .
cq $ C S = $ S if $ S < 6 .
cq $ T S = $ S if $ S < 4 .
eq o = L .
eq R S = <$ S, 'Hello > .
cq C = C if N < 6 and L =/= msg1 .
cq T = T if N < 4 and L =/= msg1 .
eq D = .
eq Q = .
cq T = if N >= 4 .
cq 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 == D .
cred Q D == D Q .
cred Q <0, 'C > == Q <0, 'T > .
cred R C I == R T I .
cred Q R Q == Q Q R .
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 == C T .
cred Q T == Q C .
cred R C == R T .
We now try to prove the same more difficult result as before, that
C Q T Q Q Q = C Q C Q D
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 == C Q C Q D .
red C Q T Q Q Q .
red C Q C Q D .
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 .
case eq N = 0 .
case op m : -> Nat .
eq N = m + 1 .
end
cred with VCASES C Q T Q Q Q == C Q C Q D .
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 .
red C Q T Q Q Q .
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 .
red Q C Q D .
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