search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
695 stars 124 forks source link

Single quote in names results in syntax error #159

Closed link2xt closed 2 years ago

link2xt commented 2 years ago

I'm trying to run example http://softwareabstractions.org/models/a4-models/chapter2/addressBook1f.als

Executing the example fails with the error

Syntax error at line 9 column 15:
There are 3 possible tokens that can appear here:
, : =

Of course I can replace b' with b2 or something like this, but it seems strange that ' in the name is not allowed in Alloy Analyzer 6.1.0 if it was allowed before. http://alloytools.org/spec.html does not say what a valid name is and the link to "lex" on http://alloytools.org/documentation.html is 404. Found https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.core/parser/Alloy.lex (seems flex was renamed to lex), it looks like only a double quote is allowed (so I can use b", but ' is interpreted as something called "prime", no idea what it is.

link2xt commented 2 years ago

There are similar problems for examples from the models repository: https://github.com/AlloyTools/models/blob/master/software-abstractions-book/chapter2/addressBook1g.als

grayswandyr commented 2 years ago

Yes indeed, it's related to the new temporal feature in Alloy 6. It's incompatible with former models, but we used this symbol because it's also used in other formal methods addressing temporal reasoning. See https://alloytools.org/spec.html for the Alloy 6 spec. More palatable documentation for end users is also on its way, you may read a draft at https://haslab.github.io/formal-software-design/ .

link2xt commented 2 years ago

Thanks! I also found https://alloy.readthedocs.io/ but it looks more like a reference, will try to read https://haslab.github.io/formal-software-design/ first.