Having events ordered in event reification

models
1

Hi,

I converted the Customer-Cards model of peter.kriens in here Can't get a model to change with time [Electrum] - #10 by peter.kriens to event reification style as below.

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 }

enum Operation {Cancel, Stutter}

fun _cancel : Operation -> Card -> Card {
	Cancel -> {card1: Card, card2 : Card | cancel[card1, card2] }
}
fun _no_change : Operation {
	{ s : Stutter |  no_change}
}

fun events : set Operation {
	(_cancel).Card.Card + _no_change
}

pred cancel[card : Card, repl : Card] {
  card.status = issued
  repl.status = unissued

  let customer = cards.(card) {
      customer.cards'  = customer.cards - card + repl
      card.status'   = cancelled
      repl.status'   = issued
      unchanged[Card - repl -  card, status]
      unchanged[Customer - customer, cards]
  }
}

pred traces {
  Customer.cards.status = issued
  (Card - Customer.cards).status = unissued
  once no_change -- to make sure a Stutter event occurs
  always (no_change or (one c1: Card | one c2 : Card | cancel[c1, c2] )) 
}

pred no_change {
  unchanged[Card, status]
  unchanged[Customer, cards]
}

But I want to have the order of events, for example I want to create a predicate saying “if ever a stutter event has occured in the previous steps”. I tried the following :

pred events_ever_stutter {
	historically (Stutter in events.prevs )
}

run {
	traces
	eventually (# status.cancelled = 3) and events_ever_stutter
} for 6 but exactly 2 Customer

It won’t find an instance for Stutter in this model, however, it will find an instance when I write for Cancel:

historically (Cancel in events.prevs )

I am not sure if the method is correct, but how can I do this for Stutter?

2

Some comments:

  • Operation is an enum so it’s ordered, but this order is arbitrary, it doesn’t correspond to anything happening temporally.
  • Writing some and disj for the multiplicity of cards is (in general) risky: by imposing these facts, you rule out some behaviors that the state machine (implemented by cancel and no_change) may in principle allow, It’s better to just put set and then check that it’s in fact disj some in all runs.
  • quoting the reference manual, once F is true in state i iff F is true in some state ≤ i. once no_change is stated in the initial state (no previous state) so you’re imposing no_change to happen in the first step of any trace.
  • using one is once again risky: you’re imposing constraints on events in all traces instead of checking that they hold for any trace.
  • remark in passing that one c1 ... one c2 ... is different from one c1, c2...
3

Thank you very much for the comments, they are very useful.
I ended up something like below in the end. I actually wanted the ‘events’ could be navigated using a Customer, but I am still working on to get ‘one event was strictly happened before another event and there is no other event in between’. Something like a->b->c, I know b happened before c and there is no other event in between.

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: set Card }

enum Operation {Add, Cancel, Stutter}

fun _cancel : Operation -> Customer -> Card -> Card {
	Cancel -> {c: Customer, card1: Card, card2 : Card | c.cancel[card1, card2] }
}
fun _add : Operation -> Customer -> Card {
	Add -> {c : Customer , card : Card | c.add[card] }
}
fun _no_change : Operation {
	{ s : Stutter |  no_change}
}

fun events[c : Customer] : set Operation {
	(_cancel).Card.Card.c + (_add).Card.c + _no_change
}

pred Customer::cancel[card : Card, repl : Card] {

      card.status = issued
      repl.status = unissued
      this.cards'  = this.cards - card + repl
      card.status'   = cancelled
      repl.status'   = issued
      unchanged[Card - repl -  card, status]
      unchanged[Customer - this, cards]

}

pred Customer::add[ card : Card] {
	card.status = unissued
	this.cards' = this.cards + card
	card.status' = issued
	unchanged[Card-card, status]
	unchanged[Customer-this, cards]
}

pred traces {

 #Customer.cards = 0
  (Card - Customer.cards).status = unissued
  always (no_change or ( one c : Customer | one c1 : c.cards, c2 : Card | c.cancel[c1, c2] ) or (one c : Customer | one c3: Card | c.add[c3] ) )
}

pred no_change {
  unchanged[Card, status]
  unchanged[Customer, cards]
}

pred events_ever_canceled[c: Customer] {
	 Cancel in c.events 
}

pred disj_cards [c1: Customer]{
	c1.cards !in (Customer-c1).cards
}

run {
	traces
	eventually (one c1, c2 : Customer | #c1.cards > 2 and events_ever_canceled[c1] and disj_cards[c1] and #c2.cards = 2 and c2.cards.status = issued )
} for 6 but exactly 2 Customer
4

“Philosophically”, I think expressing strict and precise ordering constraints is leaving the realm of temporal specification; for the most part, temporal spec shouldn’t be a step-by-step thing.

Technically now, expressing very precise ordering constraints in LTL can be difficult, if you have several states or events. You may rule out far too many possible runs. E.g. if you extend your spec, you may realize that it’s ok for event B not too precede event C just before, but possibly also if some events D or E happened… but D must be before E… and so on and so forth.

Anyway, here, you’re describing a precedence constraint which is easily described with before: B precedes C = always (C implies before B).

To learn/reflect more on spec with LTL, you may refer to the work of Dwyer et al on temporal specification patterns. I don’t think they considered past-time LTL but it’s very handy. Cabrera et al have extended (and fixed some of) Dwyer et al’s work.