Dynami c моделирование с Alloy - PullRequest
Новая
       20

Dynami c моделирование с Alloy

0 голосов
/ 25 апреля 2020

Я оцениваю шаг коллеги, используя Alloy, чтобы смоделировать проблему и получить представление о дополнительных вопросах / ограничениях, которые необходимы для соответствия спецификации.

Я считаю, что Alloy - правильный инструмент для этого объем. Я также считаю, что мне нужна динамическая модель c, чтобы проиллюстрировать последовательность действий и определить случаи, когда необходимы дополнительные ограничения.

Проблема: Участник может потратить баллы, чтобы купить ваучеры на предложение, а также выкупить или вернуть их. Участник не может net набрать больше очков, чем потратил на возвращение. Участник не может получить больше преимуществ, чем ваучеры.

Модель: 

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.

Я не могу понять, как смоделировать buyVoucher таким образом, чтобы он добавлял ваучер в отношение ваучеров членства. Или я просто делаю это неправильно. Я пытаюсь использовать сигнатуры для моделирования событий, потому что это обеспечивает лучшую визуализацию и более простую конструкцию, чем использование предикатов. Кроме того, если я собираюсь использовать предикаты, я просто смоделирую это в TLA +.

1 Ответ

0 голосов
/ 29 апреля 2020

В моей книге приведены примеры того, как это сделать, но общая стратегия с событиями - сделать подписи состояний зависимыми от времени. Например, 

vouchers: Voucher

становится 

vouchers: Voucher -> Time

Как отметил Питер, вы также можете использовать Electrum, который облегчает это, давая вам ключевое слово для изменяющихся во времени компонентов.

...