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
, excludinge
.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 ifes
is emptyReturn type: lone elem
See Also: max