用合金进行动态建模

Question

我正在评估一个同事的投稿，使用Alloy对问题进行建模，并深入了解满足规范所需的额外问题约束。

我相信Alloy是这个范围的正确工具。我还相信我需要一个动态模型来说明行动的顺序，并确定需要额外约束的情况。

问题：一个会员可以花费积分购买优惠券，并兑换或返还它们。该会员通过返还不能净赚到比花费更多的积分。该会员获得的优惠不能多于优惠券。

模式。

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.

我不知道如何建立购买券的模型 使它能在会员的优惠券关系中增加一张优惠券。或者是我做错了。我试图使用签名来对事件进行建模，因为它比使用谓词呈现出更好的可视化和更简单的结构。此外，如果我要使用谓词，我会在TLA+中建模即可。

Answer 1

我的书中给出了如何做到这一点的例子，但事件的一般策略是使状态签名与时间相关。比如说

vouchers: Voucher

成为

vouchers: Voucher -> Time

正如Peter所提到的，你也可以使用Electrum，它通过给你提供一个时间变化组件的关键字来让你更容易。