为何引用Alloy模块时出现“div未找到”错误？如何解决？

Let's break down what's happening here and how to fix it.

The Root Cause #

Alloy's built-in functions like div belong to the util/integer utility module. When you run your test module directly, Alloy implicitly loads this utility module for the "top-level" module you're executing—so div works without needing an explicit import.

But when you open test from another module (hope), the scope doesn't carry over those implicit dependencies. The test module uses div assuming the utility module is available, but hope has no knowledge of util/integer unless you explicitly tell it to load it. That's why you get the error:

“The name "div" cannot be found.”

Fixes You Can Use #

There are two clean ways to resolve this:

1. Explicitly import util/integer in the test module
   This makes the dependency on the integer utility module explicit, so any module that opens test will inherit this dependency automatically. Here's the updated test module:

   module test
   open util/integer  // Declare the dependency explicitly
   
   one sig Test { t: Int } {
     t = div[4,2]
   }
   
   run {}
   

   Now your original hope module will work without any changes.

2. Import util/integer directly in the hope module
   If you don't want to modify the test module, you can add the import to hope instead:

   module hope
   open test
   open util/integer  // Load the utility module here
   
   sig A {}
   
   run {}
   

Either approach will make the div function available in the hope module's scope.

内容的提问来源于stack exchange，提问作者Roger Costello