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].