Search code examples
alloy

The name "div" cannot be found ... Huh? Why?

In this module I use the Alloy "div":

module test

one sig Test {
     t: Int
} {
   t = div[4,2]
}

run {}

Executing that works fine.

I created another module, which uses the first module:

module hope

open test

sig A {}

run {}

Executing that results in the following error message:

The name "div" cannot be found.

Why am I getting the error message? How to fix it?

Solution

  • It's a known bug with a simple workaround. You need to explicitly import the util/integer module in your first model.

    See Alloy built-in integer math functions don't work in imported files