Fails to find instances with unconstrained Strings

[mjcollins10]

Alloy appears to have a bug when relations include unconstrained Strings. No instance is found for the following:

sig foo{ bar: String, yak: Int } pred show[]{one f:foo | f.yak=0} run show for 1

If we change this tobar: Int, Alloy finds an instance with an arbitrary value. Same behavior in 4.2 and 5.1

[pkriens]

The issue is that currently the only String atoms in the universe are the literals in the code.

I never liked this because the solutions then often have very strange strings in their solution. I've been experimenting with sigs and regular expressions.

sig DutchZip  in /[A-Z]{2}-\d{4}/ {}

Regular expressions work two way. They can be used to validate inputs (or specifying the validation rules) but they can also be used to generate test data. In general, better string support will make it a lot easier to use Alloy specs together with actual code.

It worked very interesting but never had the time to finish this. It could make the visualizations a lot more interesting and I think the lack of specifying this kind of stuff in a specification really hinders Alloy in a lot of use cases.

Just an idea.

[aleksandarmilicevic]

It's by design.

Alloy is not a string solver, and hence cannot come up with strings out of the blue.

The only use for strings in Alloy is to make models look prettier when visualized (e.g., by asserting that a certain field has a literal string value, e.g.,

sig Foo { bar: String, yak: Int } 

run {
  one f: Foo | f.yak=0 and f.bar = "First"
  one f: Foo | f.yak = 1 and f.bar = "Second"
} for 2

[pkriens]

@aleksandarmilicevic Strings can be created out of the blue with regular expressions. These regular expressions could be associated with sigs. I think this would be a very valuable extension since it can be used in mapping atoms to objects and objects to atoms in testing actual code.