This archetype is a very basic miles management system with add and consume transactions. It may be considered as a simplified version of ERC20.
miles.arlarchetype milesvariable validator : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jgasset account identified by owner {owner : role;amount : int;}entry add (ow : role, value : int) {called by validatoreffect {if account.contains(ow) thenaccount.update (ow, { amount += value })elseaccount.add({ owner = ow; amount = 0 })}}entry consume (ow : role, value : int) {specification {postcondition s1 {let some ba = before.account[ow] inlet some a = account[ow] inba.amount = a.amount + valueotherwise trueotherwise true}}called by validatorrequire {c1 : account[ow].amount >= value;}effect {account.update (ow, { amount -= value })}}