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.