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 ``Int``s.

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 add [n1, n2: Int]
Return type

one Int

Returns n1 + n2.

fun plus [n1, n2: Int]
Return type

one Int

Returns n1 + n2.

fun sub [n1, n2: Int]
Return type

one Int

Returns n1 - n2.

fun minus [n1, n2: Int]
Return type

one Int

Returns n1 - n2.

fun mul [n1, n2: Int]
Return type

one Int

Returns n1 * n2.

fun 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 rem [n1, n2: Int]
Return type

one Int

Returns the unique integer that satisfies a = ((a/b)*b) + remainder.

fun negate [n: Int]
Return type

one Int

Returns the negation of n.

fun 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 int2elem [i: Int, next: univ->univ, s: set univ]
Return type

lone s

Returns the ith element (zero-based) from the set s in the ordering of next, which is a linear ordering relation like that provided by ordering.

fun 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 max
Return type

one Int

Returns the largest integer in the current bitwidth.

fun min
Return type

one Int

Returns the smallest integer in the current bitwidth.

fun next
Return type

Int -> Int

Maps each integer (except max) to the integer after it.

fun prev
Return type

Int -> Int

Maps each integer (except min) to the integer before it.

fun max [es: set Int]
Return type

lone Int

Given a set of integers, return the largest element.

fun min [es: set Int]
Return type

lone Int

Given a set of integers, return the smallest element.

fun prevs [e: Int]
Return type

set Int

Given an integer, return all integers prior to it.

fun nexts [e: Int]
Return type

set Int

Given an integer, return all integers following it.

fun larger [e1, e2: Int]
Return type

Int

Returns the larger of the two integers.

fun smaller [e1, e2: Int]
Return type

Int

Returns the smaller of the two integers.

Predicates

pred eq [n1, n2: Int]

True iff n1 is equal to n2.

pred gt [n1, n2: Int]

True iff n1 is greater than n2.

pred gte [n1, n2: Int]

True iff n1 is greater than or equal to n2.

pred lt [n1, n2: Int]

True iff n1 is less than n2.

pred lte [n1, n2: Int]

True iff n1 is less than or equal to n2.

pred zero [n: Int]

True iff n is equal to 0.

pred pos [n: Int]

True iff n is positive.

pred neg [n: Int]

True iff n is negative.

pred nonpos [n: Int]

True iff n is non-positive.

pred nonneg [n: Int]

True iff n is non-negative.