CODEWITHSUNDEEP
alloy
tamjidturjo
tamjidturjo

Reputation: 11

Why does the Alloy API not use the default scope for one signature if the scope for a different signature is specified?

I am currently attempting to run the following Alloy model on the Alloy Analyzer 5.1.0:

sig parent {}
sig var {}
pred testPred{}
run testPred for 3 parent

However, attempting to run this model results in the following syntax error:

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

Why is it not using the default scope for var? If the model is run with the command:

run testPred

It will find an instance using the default scope for both the signatures. Therefore, why would specifying the scope for signature parent stop the Alloy API from using the default scope for signature var and result in the syntax-error. Any help with this would be greatly appreciated!

Upvotes: 0

Views: 82

Answers (1)

Peter Kriens
Peter Kriens

Reputation: 15372

Well, the syntax is that you specify the default scope and then use but [exactly] to specify the scope of the sigs you want to have a different value for. For example:

run testPred for 3 but exactly 2 parent

The way you use the scope leaves the analyzer at loss for what you want.

  1. in Alloy 6 var will be a keyword so you might want to use an alternative name.
  2. the convention is to let sigs start with an upper case. If you're starting with this, it is usually best to follow the conventions.

Upvotes: 0

Related Questions