CODEWITHSUNDEEP
alloy
edrdo
edrdo

Reputation: 133

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

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

Upvotes: 0

Views: 204

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

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

Upvotes: 2

Related Questions