Can't get a model to change with time [Electrum]

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 :slight_smile: 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:

  1. Click “Fork” in the Visualizer and the solver will try to synthesize another possible trace
  2. Add some constraints in show that force changes, e.g. eventually some (issued' - issued)

Both useful, thanks.

eventually some cancelled

seems like a good move

Hi,

A couple of comments about your model:

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

let customer = ~cards[toCancel] {
  cards' = cards - customer->toCancel + customer->replacement
}

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.

pred no_change {
	issued' = issued
	cancelled' = cancelled
	unissued' = unissued
	cards' = cards
	debitCard' = debitCard
}

Best,
Alcino

1 Like

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).

Best,
Alcino

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

Hi,

There are two issues with your model.

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.

Best,
Alcino

This works. I’m slowly getting the idea of seeing relationships rather than objects with fields. The clue was the symmetry around the

status' =
cards' = 
debitCard' = 

pattern, which should occur in every possible branch for a step. I might pull that into a function to make the point.

Also, I can use the union operator to simplify the debitCard update to

debitCard' = (toCancel = customer.debitCard
    implies debitCard ++ customer->replacement else debitCard)

Thanks for your help.

S

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

Here’s my response. A couple of differences.

  • 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:

 always #(Stutter + Cancel) = 1