I am currently modeling a container orchestrator using Alloy. It turns out that many of the facts I need to write involve regular expressions (regex). Since regex is not supported by default in Alloy, I would like to know how to go about adding this support. Does anyone know the steps to follow? Which part of the code to modify, for example?
I looked into the documentation and the Java repository, but I'm having trouble identifying the parts of the code to modify.
I'm an old gen Alloy user, from a time where Alloy used to be a very simple, yet expressive semi formal modelling language. I know that a lot of modifications have been brought to the language since version 4.2 and it could be that the original elegance of the language has been further sacrificed to expand the usability of the language.
That being said, I truly feel that Alloy is by essence not suited to reason about regexp. More broadly, it isn't suited to reason about String operations, arithmetics, or any other non-abstract domain with potentially infinite values.
Of course you could make a toy example that work with those things to some extent but any real worthwhile use case will hurt itself against the scalability issues of Alloy.
Indeed, having an exhaustive regexp validation would entail that you do have a very large pool of strings at disposition, which by itself goes against the small scope hypothesis.
It simply goes against what Alloy used to stand for, that is making abstractions of complex systems to unveil the subtlest of flaws.
Again, I'm a dinosaur. It very well could be that I'm all wrong and that Alloy 7 will also do coffee.