I’m modelling a credit card system (using Electrum). The idea is that I can cancel a card and get it replaced. My current status is that with tracing cancellation or noOp, it always choses noOp, so it’s a bit dull If I remove the noOp it cannot find an instance. Suggestions? Obviously, there is much to improve…
module cardCancellationElectrum
abstract sig Card {}
sig DebitCard extends Card {}
sig CreditCard extends Card {}
var sig issued in Card {}
var sig cancelled in Card {}
var sig unissued in Card {}
sig Customer {
, var cards: set Card,
, var debitCard: DebitCard
} {
always debitCard in cards
}
fact card_state {
always Card in issued + cancelled + unissued
always disj[issued, cancelled, unissued]
}
fact cards_issued_to_one_customer {
always all disj c1, c2: Customer | no (c1.cards & c2.cards)
always no Customer.cards & (cancelled + unissued)
}
pred cancelled[toCancel, replacement: Card] {
issued' = issued - toCancel + replacement
unissued' = unissued - replacement
cancelled' = cancelled + toCancel
let customer = ~cards[toCancel] {
customer.cards' = customer.cards - toCancel + replacement
}
}
pred init {
some issued
some unissued
some DebitCard
some CreditCard
no cancelled
}
fact traces {
init
always (can_cancel => cancellation) or no_change
}
pred can_cancel {
some unissued
}
pred cancellation {
one toCancel: issued | one replacement: unissued | cancelled[toCancel, replacement]
}
pred no_change {}
pred show {
}
run show for 2 Customer, 6 Card
I;m a bit in a hurry so I hadn’t time (!) to look at your model in details but this may be useful: the solver yields a trace where nothing happens because it’s the simplest one it found that satisfies show. You can try two things:
Click “Fork” in the Visualizer and the solver will try to synthesize another possible trace
Add some constraints in show that force changes, e.g. eventually some (issued' - issued)
The always in signature facts is redundant - Electrum automatically adds an always in that case: all signature facts are invariants.
You have no facts forcing issued cards to belong to some customer. Not sure if it is intentional.
I think this restriction on the next value of cards will not have the desired effect. By projecting cards' on the customer this restriction is only saying what happens to the cards of that customer, meaning the cards of other customers can change freely. I would write this instead
which restricts the value of the all cards relation in the next state. With this new formulation you do need to had a guard to ensure the card toCancel belongs to some customer, for example, by adding some customer inside the let. Your formulation actually ensured this because customer.cards' = customer.cards - toCancel + replacement is a contradiction when customer is empty (meaning customer.cards is also empty).
Also, predicate cancelled allows debitCard to change freely. I’m not sure if this was intentional.
I believe that what you want here is always (can_cancel => cancellation else no_change), meaning no_change will only occur if can_cancel is false.
Finally, in the no_change predicate you need to specify that variable relations do not change, otherwise they can change freely.
Thanks helping out. I had since made some of the changes you suggest, having discovered the obvious problems, but the rest is very helpful. The line about manipulating cards’ with relationships is especially useful.
My next question is that there’s an implied lifecycle of cards: unissued->issued->cancelled. Is there a conventional way to represent that?
You could write a temporal logic assertion to check the lifecycle - I think the following would work.
assert lifecycle {
always all c : issued | always c in issued+cancelled
always all c : cancelled | always c in cancelled
}
You could then issue a check lifecycle command to verify if your system actually respects the lifecycle.
You could also model the status of a card differently, using an enumeration signature for the lifecycle and imposing a total order on it. Then, the property could be written more elegantly (and it would be the same even if you had more phases in the lifecycle). For the signature declarations we would have something like:
open util/ordering[Status]
enum Status {issued, unissued, cancelled}
abstract sig Card {
var status : one Status
}
The remaining facts and predicates would have to be adapted, but notice that with this model you would not need fact card_state as those constraints would hold naturally here.
Then the assertion for the lifecycle could be specified as follows:
assert lifecycle {
always all c : Card, s : c.status | always gte[c.status,s]
}
That is, for all cards it is always true the future statuses are greater or equal to the present one (according the total order).
Here’s the next version. It’s a bit more compact. I had to fix the lifecycle fact to avoid cards skipping a step.
My current problem is that I have a case where a Customer with two Cards (and two unissued) has cancelled both in a single step. I don’t understand this, given my one clause in the cancelled predicate. I’ve also seen unissued cards arbitrarily being issued, even though that increases the number of cards held by a customer.
Thanks
module cardCancellationElectrum
open util/ordering[Status]
enum Status { unissued, issued, cancelled }
abstract sig Card {
var status : one Status
}
sig DebitCard, CreditCard extends Card {}
sig Customer {
, var cards: set Card,
, var debitCard: DebitCard
} {
debitCard in cards
}
fact cards_issued_to_customers {
always all disj c1, c2: Customer | no (c1.cards & c2.cards)
always Customer.cards = status.issued
}
fact card_lifecycle {
always all card : Card | card.status' = card.status or card.status' = card.status.next
}
pred cancelled[toCancel, replacement: Card] {
let customer = cards.toCancel {
toCancel.status' = cancelled
replacement.status' = issued
cards' = cards - customer->toCancel + customer->replacement
debitCard' = (toCancel = customer.debitCard
implies debitCard - customer->toCancel + customer->replacement else debitCard)
}
}
fact traces {
init
always cancellation or no_change
}
pred init {
some u: status.unissued | u in DebitCard
some u: status.unissued | u in CreditCard
no status.cancelled
all customer: Customer | some customer.cards
}
pred cancellation {
one toCancel: Customer.cards | one replacement: status.unissued {
cancelled[toCancel, replacement]
}
}
pred no_change {
status' = status
cards' = cards
debitCard' = debitCard
}
pred show {
eventually some status.cancelled
}
run show for 2 Customer, 6 Card, 3 Time
Similar problem as before: these only restrict the next state value of status for toCancel and replacement. All other cards are free to change status. Instead you could write status' = (status ++ toCancel->cancelled) ++ replacement->issued or add a frame condition such as all c : Card - (toCancel+replacement) | c.status' = c.status.
always has stronger precedence than or, so you need parentheses here.
With this changes I don’s see any of the issues you refer. And card_lifecycle can be changed from a fact to an assert and verified to hold, as expected.
I love this problems so I could not resist. I skipped the diff between credit and debit since I figured the event handling was the crucial aspect. I changed it to my style, so maybe you can pickup some useful aspects:
enum Status { unissued, issued, cancelled }
let unchanged[s,r] = all x : s | x.(r)'=x.(r)
sig Card { var status : Status }
sig Customer { var cards: disj some Card }
var lone sig Cancel {
var card : Card,
var repl : Card
}
var lone sig Stutter {}
pred univ.exec {
this = Cancel => this.cancel else no_change
}
pred Cancel.cancel {
this.card.status = issued
this.repl.status = unissued
let customer = cards.(this.card) {
customer.cards' = customer.cards - this.card + this.repl
this.card.status' = cancelled
this.repl.status' = issued
unchanged[Card - this.repl - this.card,status]
unchanged[Customer - customer,cards]
}
}
pred traces {
#(Stutter + Cancel) = 1
Customer.cards.status = issued
(Card - Customer.cards).status = unissued
always some e : Cancel+Stutter | e.exec
}
pred no_change {
unchanged[Card,status]
unchanged[Customer,cards]
}
check {
traces => always no c : Card | c.status'.lt[c.status]
} for 6 but exactly 2 Customer
run {
traces
eventually # status.cancelled = 3
} for 6 but exactly 2 Customer
I went with the relationship style updates, rather than changing fields on signatures.
I can see why you want the Stutter, but is it necessary?
even though there’s a check at the beginning of the Cancel.cancel, I sometimes get a Cancel object where the two fields point to the same card in the visualisation. I suspect this is because the check doesn’t kick in until the cancel is actually triggered.
enum Status { unissued, issued, cancelled }
let unchanged[s,r] = all x : s | x.(r)'=x.(r)
sig Card { var status : Status }
sig Customer { var cards: disj some Card }
var lone sig Stutter {}
var lone sig Cancel {
var toCancel : Card,
var replacement : Card
}
pred univ.exec {
this = Cancel => this.cancel else no_change
}
pred Cancel.cancel {
this.toCancel.status = issued
this.replacement.status = unissued
let customer = cards.(this.toCancel) {
status' = (status ++ this.toCancel->cancelled) ++ this.replacement->issued
cards' = cards - customer->this.toCancel + customer->this.replacement
}
}
pred traces {
#(Stutter + Cancel) = 1
no status.cancelled
some status.unissued
all customer: Customer | some customer.cards
status.issued = Customer.cards
always some e : Cancel+Stutter | e.exec
}
pred no_change {
unchanged[Card, status]
unchanged[Customer, cards]
}
check {
traces => always all card : Card | card.status' = card.status or card.status' = card.status.next
} for 6 but exactly 2 Customer
run {
traces
eventually no status.unissued
} for 6 but exactly 2 Customer
There was a discussion why you need stutter step on this list on the Pluscal topic. Electrum needs to loop on something to make a lasso trace and it can be used to detect deadlocks. In this case, I also used to make the model ‘extensible’ for more commands. I.e. it is now easy to add a third command like ‘Register’.
I try to prevent this with:
#(Stutter + Cancel) = 1
I.e. the command for each state is either Stutter or Cancel. When looking into this I realized it should be:
This is a great example for me, but I couldn’t figure out something :
why are there “var lone sig” for Cancel and Stutter? what behaviour does that bring to the table?
when I just remove those then no instance found, so it must be something crucial.
A second thought, I think “lone” ensures either Cancel or Stutter is selected and “var” ensures it is a different Cancel or Stutter instance each time. Is that correct?
Well, Cancel and Stutter are the operations/events, so at each step you need to pick one. In traces we enforce this unicity with #(Stutter + Cancel) = 1. The idea is that you can add more operations. They are var so we can let each operation can have its own parameters.
IMO, using cardinality constraints to ensure unicity of events at each step is risky in general, even if safe for particular cases (using signatures is also risky as, depending on how they’re used, it sometimes imposes further implicit cardinality constraints). The worst risk is losing some behaviors (traces).
I think it is safer to follow Lamport’s approach where the unicity of (the observable effect of) actions is a theorem (assert) rather than an axiom (fact). The way to get this in Alloy is to rely on preds for actions, with adequate frame conditions (which will usually induce the said unicity). If you need signatures for visualization of events, this is doable with preds as here.
I observe an undesired behaviour in this style of model that is like
if you have this model and you want to define some restriction on the Cancel. Let’s say Cancel has other relations something and anotherthing and you define a fact saying
Is it true that this will never take effect in this model because there are never two disjoint Cancels in each step because of the ‘var lone sig Cancel’? Or am I doing something wrong here? What is the way to take “all steps” into account and say that all Cancels throughout the model execution should have this behaviour not in each step? Defining the ‘anotherthing’ relation with “disj” doesn’t also take effect. The ‘anotherthing’ relation is the same with another Cancel’s ‘anotherthing’ in another step.
If I remove the noOp it cannot find an instance. Suggestions? Obviously, there is much to improve…