Continuing the discussion from Optimizing version of Alloy:
Hello everyone!
I am a complete beginner. I’m considering to model a system with alloy 6. Now I’am learning it. When I run the instance of GitHub, I will be prompted with an error “There are 3 possible tokens that can appear here”. Is this because of the version problem?
I don’t think there should be such a problem. Do you have the same problem?
Please copy paste your model target than showing a screenshot, it will be easier for people to test it. Here the issue may be due to the presence of the prime symbol as macro arguments. In general I would advise against using macros as much as you can. There are also issues with the way you update days, I suggest you refer to this post for a nice example of the canonical way to write models.
EDIT: notice that in Alloy 6, the prime symbol cannot be used for identifiers anymore, the prime symbol now denotes the value of the variable in the next instant. We have an on-going book about Alloy 6 here.
Also, don’t use let for defining top level predicates. let, at the top level, is a macro, and doesn’t (among other things) give you typechecking. Use pred instead.
It does type check but at the expansion level. This can be very useful but the error messages can be hard to interpret sometimes. And macros have bugs so it is not wise to use them before you’re more experienced. That said, sometimes I find them a life saver.
