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!

See also

Module time

Adds additional convenience macros for the most common use case of ordering.

Sequences

For writing ordered relations vs placing top-level ordering on signatures.

Functions

fun first
Returns

The first element of the ordering

Return type

elem

See Also

last

fun 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 prevs[e]
Returns

All elements before e, excluding e.

Return type

elem

See Also

nexts

fun smaller[e1, e2: elem]
Returns

the element that comes first in the ordering

See Also

larger

fun 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 lt[e1, e2: elem]
See Also

gt, lte, gte

True iff e1 in prevs[e2].