Provide Alloy with a “pool” of custom Strings

问题:

I'm interested in using the String type of Alloy, (especially due to the fact it allows the use of special character). I noticed that in order to add a given String to an instance, it is sufficient to include it in an expression. e.g.

fact stringInsert{
   none!="a"+"b"+"c"
}

will lead to the creation of atoms "a","b" and "c" in any generated instances.

Now my question is, is there a way to declare a pool of strings,defining all possible string atoms that might occur in satisfiable instances, BUT whose number respect the scope given and can be further constrained ?

As an example, if we consider the above fact as declaring a pool of string atom {"a","b","c"}, I would like instances obtained from the execution of a model using this pool with a global scope of 2 to only contain two of those three strings "a","b", and "c".

回答1:

You can only declare an exact scope for String, e.g.,

run {} for 3 but exactly 5 String

It is currently not possible to only give an upper bound for Strings, e.g., for 5 String, and ask Alloy to find a solution (with respect to other constraints) with up to 5 strings. So if you try to set the scope for String to 2 in your example above, you will still get all 3 string literals declared in your model ("a", "b", "c"), which is consistent with string literals being "one sigs" extending the abstract String sig; if on the other hand you set the scope to 5, Alloy will generate 2 additional string atoms, "String$0" and "String$1".