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

models
10

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