使用合金进行动态建模答案

【问题标题】：Dynamic modeling with Alloy使用合金进行动态建模
【发布时间】：2020-04-24 22:35:34
【问题描述】：

我正在评估一位同事的宣传，使用 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 = time.prev.@memberships.vouchers + 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.

我不知道如何对 purchaseVoucher 建模，以便将优惠券添加到会员的优惠券关系中。或者我只是做错了。我正在尝试使用签名对事件进行建模，因为它提供了比使用谓词更好的可视化和更简单的构造。此外，如果我要使用谓词，我会在 TLA+ 中对其进行建模。

【问题讨论】：

您可能想查看 Electrum，它是具有内置动态结构的合金克隆。就个人而言，我非常不喜欢时间模式。

标签： alloy

【解决方案1】：

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

vouchers: Voucher

变成

vouchers: Voucher -> Time

正如 Peter 指出的，您还可以使用 Electrum，它通过为随时间变化的组件提供关键字来简化此操作。

【讨论】：