Milner's Vending Machine

This file formalises Milner's vending machine example for CCS.

We formalise two versions:

• A machine with a deterministic LTS: coin.(tea.VM + coffee.VM).
• A machine with a nondeterministic LTS: coin.tea.VM + coin.coffee.VM.

We then prove the classical example that the two are not bisimilar. We also show the distinction with HML: only the deterministic machine offers the choice of drink after a coin is inserted.

Future work on proving that the two vending machines are trace equivalent would be welcome.

Action names.

@[reducible, inline]

abbrev Cslib.Algorithms.CCS.VendingMachine.Coin : CCS.Act String

Insert a coin.

Equations

• Cslib.Algorithms.CCS.VendingMachine.Coin = Cslib.CCS.Act.name "coin"

@[reducible, inline]

abbrev Cslib.Algorithms.CCS.VendingMachine.Tea : CCS.Act String

Tea request.

Equations

• Cslib.Algorithms.CCS.VendingMachine.Tea = Cslib.CCS.Act.name "tea"

@[reducible, inline]

abbrev Cslib.Algorithms.CCS.VendingMachine.Coffee : CCS.Act String

Coffee request.

Equations

• Cslib.Algorithms.CCS.VendingMachine.Coffee = Cslib.CCS.Act.name "coffee"

inductive Cslib.Algorithms.CCS.VendingMachine.Constant : Type

Constants.

• vm : Constant

def Cslib.Algorithms.CCS.VendingMachine.vm : CCS.Process String Constant

The vending machine process.

Equations

• Cslib.Algorithms.CCS.VendingMachine.vm = Cslib.CCS.Process.const Cslib.Algorithms.CCS.VendingMachine.Constant.vm

Deterministic vending machine

def Cslib.Algorithms.CCS.VendingMachine.vendingDefs : Constant → Option (CCS.Process String Constant)

Constant definitions: vm = coin.(tea.VM + coffee.VM)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cslib.Algorithms.CCS.VendingMachine.ltsD : LTS (CCS.Process String Constant) (CCS.Act String)

The LTS of CCS for the deterministic vending machine.

Equations

• Cslib.Algorithms.CCS.VendingMachine.ltsD = Cslib.CCS.lts

Nondeterministic vending machine

def Cslib.Algorithms.CCS.VendingMachine.vendingDefsND : Constant → Option (CCS.Process String Constant)

vm = coin.tea.VM + coin.coffee.VM

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cslib.Algorithms.CCS.VendingMachine.ltsND : LTS (CCS.Process String Constant) (CCS.Act String)

The LTS of CCS for the nondeterministic vending machine.

Equations

• Cslib.Algorithms.CCS.VendingMachine.ltsND = Cslib.CCS.lts

theorem Cslib.Algorithms.CCS.VendingMachine.vm_ltsD_ltsND_not_bisim : ¬ltsD.Bisimilarity ltsND vm vm

The deterministic and nondeterministic vending machines are not bisimilar.

HML properties of the two vending machines

def Cslib.Algorithms.CCS.VendingMachine.modelD : Logic.Modal.HML.Model (CCS.Process String Constant) (CCS.Act String) Empty

HML model for the deterministic machine with no atomic propositions.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Algorithms.CCS.VendingMachine.modelND : Logic.Modal.HML.Model (CCS.Process String Constant) (CCS.Act String) Empty

HML model for the nondeterministic machine with no atomic propositions.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Algorithms.CCS.VendingMachine.choiceAfterCoin : Logic.Modal.HML.Proposition (CCS.Act String) Empty

After inserting a coin, it is possible to choose between tea and coffee.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Algorithms.CCS.VendingMachine.vm_modelD_choiceAfterCoin : ⇓{ m := modelD.toModal, w := vm, φ := choiceAfterCoin }

theorem Cslib.Algorithms.CCS.VendingMachine.vm_modelND_not_choiceAfterCoin : ¬⇓{ m := modelND.toModal, w := vm, φ := choiceAfterCoin }