ordering

Ordering places an ordering on the parameterized signature.

open util/ordering[A]

sig A {}

run {
  some first -- first in ordering
  some last  -- last in ordering
  first.lt[last]
}

ordering can only be instantiated once per signature. You can, however, call it for two different signatures:

open util/module[Thing1] as u1
open util/module[Thing2] as u2

sig Thing1 {}
sig Thing2 {}

Warning

ordering forces the signature to be exact. This means that the following model has no instances:

open util/ordering[S]

sig S {}

run {#S = 2} for 3

In particular, be careful when using ordering as part of an assertion: the assertion may pass because of the implicit constraint!

Functions

fun ordering.first

Returns:

The first element of the ordering

Return type:

elem

See Also:

last

fun ordering.prev

Return type:

elem -> elem

See Also:

next

Returns the relation mapping each element to its previous element. This means it can be used as any other kind of relation:

fun is_first[e: elem] {
  no e.prev
}

fun ordering.prevs[e]

Returns:

All elements before e, excluding e.

Return type:

elem

See Also:

nexts

fun ordering.smaller[e1, e2: elem]

Returns:

the element that comes first in the ordering

See Also:

larger

fun ordering.min[es: set elem]

Returns:

The smallest element in es, or the empty set if es is empty

Return type:

lone elem

See Also:

max

Predicates

pred ordering.lt[e1, e2: elem]

See Also:

gt, lte, gte

True iff e1 in prevs[e2].