Alloy - scope for this/Univ, ordering, "open" statement

Question

I am having errors in Alloy (4.2) specifications of the following kind:

You must specify a scope for sig "this/Univ"

The issue is easy to reproduce with a toy example:

open util/ordering[State]
open util/integer

sig State { value : Int }

fact {
  first.value = 0
  all s:State, s': s.next | s'.value = plus[s.value, 1]
}

run { } for 5 State, 3 Int

All of the above is fine. Now, when I define State in an external file and import it with an open statement, I get the "Univ scope" error:

open util/ordering[State]
open util/integer
open State

fact {
  first.value = 0
  all s:State, s': s.next | s'.value = plus[s.value, 1]
}

run { } for 5 State, 3 Int

I tried several variations of the above without success. Why does this happen and how can it be solved? In my project, it would be useful for me to define the target sig of the ordering module in a different file.

Thanks, Eduardo

score 2 · Accepted Answer · edited May 23 '17 at 10:33

This is an Alloy "design bug". It was decided that a Univ signature would appear when no signatures are defined in the module in order to check some property over built-in relations (e.g., unit, iden, none).

You have many ways of going around this problem, here is a selection :

You can add ",0 Univ" at the end of your run command
You can add a signature in your Alloy module
You can specify a global scope of zero (run { } for 0 but 5 State, 3 Int )

See this question for additional informations

Alloy - scope for this/Univ, ordering, "open" statement

1 Answers1