Pool custom strings
I'm interested in using the String type of Alloy (especially since it allows a special character). I noticed that to add a given string to an instance, it is enough to include it in an expression. eg
fact stringInsert{
none!="a"+"b"+"c"
}
will result in the creation of atoms "a", "b", and "c" in any generated instances.
Now my question is, is there a way to declare a row pool, defining all possible row atoms that can occur in satisfactory instances, BUT whose number matches the scope provided and can be further limited?
As an example, if we consider the above fact as an atomic pool declaration of a row {"a", "b", "c"}, I would like the instances obtained from executing the model using this pool with a global scope of 2 only contain two of these three lines: "a", "b" and "c".
source to share
You can declare the scope to be exact for String
, for example
run {} for 3 but exactly 5 String
It is currently not possible to give just an upper bound for rows, for example, for 5 String
and ask Alloy to find a solution (relative to other constraints) with up to 5 rows. So if you try to set the scope for String
to 2 in the above example, you will still get all 3 string literals declared in your model ("a", "b", "c"), which matches string literals being "one signem ", extending abstract String
sig; if, on the other hand, you specify a scope of 5, the fusion will generate 2 extra string atoms, "String $ 0" and "String $ 1".
source to share