I'm evaluating a co-worker's pitch using Alloy to model the problem and gain insight into additional questions/constraints that are required to meet the specification.
I believe that Alloy is the right tool for this scope. I also believe I need a dynamic model to illustrate the sequence of actions and identify cases where additional constraints are needed.
Problem: A Member can spend points to purchase Vouchers for an Offer, and redeem or return them. The member cannot net out more points than spent by returning. The member cannot receive more benefits than vouchers.
Model:
open util/ordering[Time]
sig Time {}
// A membership may have a point balance
sig Membership {
vouchers: Voucher
}
sig Voucher {
, voucher_for: one VoucheredOffer
, voucher_from: one PurchasableOffer
}
// Purchasable offers may have some point cost
sig PurchasableOffer {
, grants_for: one VoucheredOffer
}
sig VoucheredOffer {}
// Events
abstract sig Event {
, time: Time
, memberships: Membership
}
one sig init extends Event {} {
first = time
}
// PurchaseVoucher
// A membership receives a voucher
// Additionally, membership may spend points
sig purchaseVoucher extends Event {
, membership: Membership
, offer: PurchasableOffer
, voucher: Voucher
} {
voucher = voucher_from.offer
memberships.vouchers = [email protected] + voucher
}
// ReturnVoucher
// A membership returns a voucher, and if points were spent, the points are returned
// ReserveVoucher
// A membership reserves a voucher
// RedeemVoucher
// Membership redeems a voucher, receiving a benefit.
// Assertions/Invariants/Checks
// A membership's points returned does not exceed points spent.
// A membership does not receive more benefits than total vouchers purchased minus vouchers returned.
I can't figure out how to model purchaseVoucher such that it adds a voucher to the membership's vouchers relation. Or I'm just doing it wrong. I am trying to use signatures to model the events because it presents a better visualization and simpler construction than using predicates. Further, if I am going to use predicates, I would just model this in TLA+.
