Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TLSF identifiers can contain @ #7

Closed
johnyf opened this issue May 14, 2016 · 3 comments
Closed

TLSF identifiers can contain @ #7

johnyf opened this issue May 14, 2016 · 3 comments

Comments

@johnyf
Copy link
Contributor

johnyf commented May 14, 2016

The parser that I am using in omega interprets @ as an operator. In general, it is expected that symbols other than _ and - may be assigned meaning in various formats. It would therefore be desirable to either not use @ in identifiers in the competition, or exclude it from the TLSF grammar.

@kleinreact
Copy link
Collaborator

@-symbols can be used to express positions, e.g, lift@floor1 or robot@position_2_3, which is useful for various types of benchmarks. Beside that, I also don't know any LTL related languages that actively uses the @-symbol for some specific kind of operator. Nevertheless, I agree that the symbol itself may not be allowed by all possible tools.

As a fix I would suggest to add an operation flag to the tool, which allows to change the symbol to some alternative (similar to the delemiter-flag), which is then set to @ per default.

@johnyf
Copy link
Contributor Author

johnyf commented May 17, 2016

SPIN's Promela uses @ to describe remote references, and so openpromela too. In omega, I've been experimenting with another use for it.

In any case, @ is somewhat unusual within identifiers in programming languages.

Implicitly, @ is used in a translator in the slugs distribution that takes a fragment of structured slugs (restricted to integer addition) and outputs slugsin syntax. There, it is used to incorporate integer range information (essentially part of the symbol table) within bit identifiers. I don't think that that approach of tracking information is robust, so I manage the symbol table throughout within the synthesizer frontend, and avoid @ within identifiers.

I agree that character substitution by syfco is the best next alternative to consider, if it cannot be avoided. Again, the new variable names need be taken into account during model checking, cf. #11.

kleinreact pushed a commit that referenced this issue May 30, 2016
@kleinreact
Copy link
Collaborator

You can now replace the symbols by using the -as option.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants