integer¶
Emulates integers.
A collection of utility functions for using Integers in Alloy. Note that integer overflows are silently truncated to the current bitwidth using the 2’s complement arithmetic, unless the ‘’forbid overflows’’ option is turned on, in which case only models that do not have any overflows are analyzed.
Warning
The main challenge with this module is the distinction between Int and int. Int is the set of integers that have been instantiated, whereas int returns the value of an Int. You have to explicitly write int i to be able to add, subtract, and compare Ints.
open util/integer
fact ThreeExists { // there is some integer whose value is 3
some x: Int | int x = 3
}
fun add[a, b: Int]: Int {
{i: Int | int i = int a + int b}
}
run add for 10 but 3 int expect 1
To try this module out, in Alloy Analyzer’s evaluator, you may also issue the
following commands (suppose that allow generated a set with numbers ranging
from -8 to 7):
1 + 3
4
7 + 1
-8
Functions¶
-
fun
integer.add [n1, n2: Int]¶ - Return type
one Int
Returns
n1 + n2.
-
fun
integer.plus [n1, n2: Int]¶ - Return type
one Int
Returns
n1 + n2.
-
fun
integer.sub [n1, n2: Int]¶ - Return type
one Int
Returns
n1 - n2.
-
fun
integer.minus [n1, n2: Int]¶ - Return type
one Int
Returns
n1 - n2.
-
fun
integer.mul [n1, n2: Int]¶ - Return type
one Int
Returns
n1 * n2.
-
fun
integer.div [n1, n2: Int]¶ - Return type
one Int
Returns the division with ‘’round to zero’’ semantics, except the following 3 cases:
if a is 0, then it returns 0
else if b is 0, then it returns 1 if a is negative and -1 if a is positive
else if a is the smallest negative integer, and b is -1, then it returns a
-
fun
integer.rem [n1, n2: Int]¶ - Return type
one Int
Returns the unique integer that satisfies
a = ((a/b)*b) + remainder.
-
fun
integer.negate [n: Int]¶ - Return type
one Int
Returns the negation of n.
-
fun
integer.signum [n: Int]¶ - Return type
one Int
Returns the signum of n (aka sign or sgn). In particular,
n < 0 => ( 0 - 1 ) else ( n > 0 => 1 else 0 ).
-
fun
integer.int2elem [i: Int, next: univ->univ, s: set univ]¶ - Return type
lone s
Returns the ith element (zero-based) from the
set sin the ordering ofnext, which is a linear ordering relation like that provided byordering.
-
fun
integer.elem2int [e: univ, next: univ->univ]¶ - Return type
lone Int
Returns the index of the element (zero-based) in the ordering of next, which is a linear ordering relation like that provided by
ordering.
-
fun
integer.max¶ - Return type
one Int
Returns the largest integer in the current bitwidth.
-
fun
integer.min¶ - Return type
one Int
Returns the smallest integer in the current bitwidth.
-
fun
integer.next¶ - Return type
Int -> Int
Maps each integer (except max) to the integer after it.
-
fun
integer.prev¶ - Return type
Int -> Int
Maps each integer (except min) to the integer before it.
-
fun
integer.max [es: set Int]¶ - Return type
lone Int
Given a set of integers, return the largest element.
-
fun
integer.min [es: set Int]¶ - Return type
lone Int
Given a set of integers, return the smallest element.
-
fun
integer.prevs [e: Int]¶ - Return type
set Int
Given an integer, return all integers prior to it.
-
fun
integer.nexts [e: Int]¶ - Return type
set Int
Given an integer, return all integers following it.
-
fun
integer.larger [e1, e2: Int]¶ - Return type
Int
Returns the larger of the two integers.
-
fun
integer.smaller [e1, e2: Int]¶ - Return type
Int
Returns the smaller of the two integers.
Predicates¶
-
pred
integer.eq [n1, n2: Int]¶ Trueiff n1 is equal to n2.
-
pred
integer.gt [n1, n2: Int]¶ Trueiff n1 is greater than n2.
-
pred
integer.gte [n1, n2: Int]¶ Trueiff n1 is greater than or equal to n2.
-
pred
integer.lt [n1, n2: Int]¶ Trueiff n1 is less than n2.
-
pred
integer.lte [n1, n2: Int]¶ Trueiff n1 is less than or equal to n2.
-
pred
integer.zero [n: Int]¶ Trueiff n is equal to0.
-
pred
integer.pos [n: Int]¶ Trueiff n is positive.
-
pred
integer.neg [n: Int]¶ Trueiff n is negative.
-
pred
integer.nonpos [n: Int]¶ Trueiff n is non-positive.
-
pred
integer.nonneg [n: Int]¶ Trueiff n is non-negative.