# Having events ordered in event reification

**URL:** <https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321>\
**Category:** models\
**Created:** [January 13, 2023, 6:07pm UTC](https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321 "2023-01-13T18:07:32Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![ilkane](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/ilkane/32/124_2.png) [@ilkane](https://alloytools.discourse.group/u/ilkane)\
**Post date:** [January 13, 2023, 6:07pm UTC](https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321/1 "2023-01-13T18:07:32Z")

</div>

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](https://alloytools.discourse.group/t/cant-get-a-model-to-change-with-time-electrum/85/10) to event reification style as below.

```auto
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 :

```auto
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:

```auto
historically (Cancel in events.prevs )

```

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

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [January 16, 2023, 9:42am UTC](https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321/2 "2023-01-16T09:42:37Z")

</div>

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...`](https://stackoverflow.com/questions/46635327/why-are-multiple-alloy-declarations-not-equivalent-to-nested-alloy-declarations/46703498#46703498)

---

<div class="post-metadata">

**Author:** ![ilkane](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/ilkane/32/124_2.png) [@ilkane](https://alloytools.discourse.group/u/ilkane)\
**Post date:** [January 16, 2023, 10:43am UTC](https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321/3 "2023-01-16T10:43:14Z")

</div>

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.

```auto
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

```

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [January 16, 2023, 3:45pm UTC](https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321/4 "2023-01-16T15:45:17Z")

</div>

“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](https://matthewbdwyer.github.io/psp/). I don’t think they considered past-time LTL but it’s very handy. [Cabrera _et al_](https://hal.science/hal-00931093/document) have extended (and fixed some of) Dwyer _et al_’s work.