NetBill

-- The data types DATAxy are the set of data
-- that are transmitted from the principal x
-- to the principal y;
DATAmc = {noPayment, paymentSlip,
          encryptedGoods} 
DATAbc = {noPayment, paymentSlip, noRecord}
DATAcm = {goodsReq, epo}
DATAcb = {transactionEnquiry}
DATAbm = {paymentSlip, noPayment}
DATAmb = {endorsedEpo}

-- The names of the channels are of the form
-- x(in/out)y, where in/out refers to the
-- direction (relative to x), and y is the
-- other party of the communication;
pragma channel coutm : DATAcm
pragma channel coutb : DATAcb
pragma channel moutc : DATAmc
pragma channel moutb : DATAmb
pragma channel boutc : DATAbc
pragma channel boutm : DATAbm
pragma channel minc : DATAcm
pragma channel binc : DATAcb
pragma channel cinm : DATAmc
pragma channel binm : DATAmb
pragma channel cinb : DATAbc
pragma channel minb : DATAbm

pragma channel creditM, debitC, timeoutEvent

[The consumer process CONSUMER:
 as given in the paper.]

[The merchant process MERCHANT:
 as given in the paper.]

[The bank process BANK:
 as given in the paper.]

SUCCESS = STOP
ERROR = STOP
NO_FUNDS = STOP
NO_TRANSACTION = STOP
END = STOP
ABORT = STOP
FAIL = STOP

-- The communication channels: only those
-- involving the bank are reliable.

COMMcm = []x: DATAcm @
              (coutm ?x ->
                 (COMMcm []
                  (minc !x -> COMMcm)))
COMMcb = []x: DATAcb @
              (coutb ?x ->
                 ((binc !x -> COMMcb)))
COMMmc = []x: DATAmc @
              (moutc ?x ->
                 (COMMmc []
                  (cinm !x -> COMMmc)))
COMMmb = []x: DATAmb @
              (moutb ?x ->
                 ((binm !x -> COMMmb)))
COMMbc = []x: DATAbc @
              (boutc ?x ->
                 ((cinb !x -> COMMbc)))
COMMbm = []x: DATAbm @
              (boutm ?x ->
                 ((minb !x -> COMMbm)))

COMM = COMMcm [|{}|] COMMcb [|{}|] COMMmc
       [|{}|] COMMmb [|{}|] COMMbc
       [|{}|] COMMbm

-- The Whole Netbill System
CIO = {| coutm, coutb, cinm, cinb |}
MIO = {| moutc, moutb, minc, minb |}
BIO = {| boutc, boutm, binc, binm |}
BINT = {debitC, creditM}
BTOT = union(BIO, BINT)
COMMIO = union(CIO, union(MIO, BIO))
COMMIO' = diff(COMMIO,
               {cinm.encryptedGoods,
                cinm.paymentSlip,
                cinb.paymentSlip})

SYSTEM1 =
   ((CONSUMER [|{}|] MERCHANT [|{}|] BANK)
    [| COMMIO |] COMM)
   \ union(COMMIO, {timeoutEvent})

SYSTEM2 =
   ((CONSUMER [|{}|] MERCHANT [|{}|] BANK)
    [| COMMIO |] COMM)
   \ union(MIO,
       union(BIO,
         union({|coutm, coutb |},
               {cinm.noPayment,
                cinb.noPayment,
                cinb.noRecord,
                timeoutEvent})))

SPEC1 = STOP |~|
       ((debitC -> creditM -> STOP) []
        (creditM -> debitC -> STOP))

SPEC2 = (STOP |~|
        (cinm.encryptedGoods -> (STOP |~|
           (debitC -> creditM -> 
           ((cinb.paymentSlip -> STOP) |~|
            (cinm.paymentSlip -> STOP))))))

The check of SPEC1 generated the following FDR output:

fdr> Check1 "SPEC1" "SYSTEM1";
SPEC1 ....(5 states)
CONSUMER ..........(10 states)
MERCHANT ...............(15 states)
BANK .........(10 states)
COMMcm .(3 states)
COMMcb .(2 states)
COMMmc .(4 states)
COMMmb .(2 states)
COMMbc .(4 states)
COMMbm .(3 states)
readalphabet:
  Alphabet contains 3 events [up to 998]
6 configuration masks in 6 transitions
3 
5 reachable configurations         
0 
nfcompact :
  compacting 4 state normal form:
    now 4 states
87 configuration masks in 67 transitions
139 
199 reachable configurations         
1 The implementation does indeed
  refine the normal form.
Checked 199 pairs.
Refinement check succeeded
No failure in this context!
val it = - : (label,selector,cause) Context
fdr>