The XSD schema can be downloaded here
A sample XML example can be downloaded here, and is
also shown at the bottom of this page for easy reference.
First of all, the toplevel node should be <alloy>, and it should contain at least one <instance> element; currently the Alloy Analyzer will ignore additional instances you put into a file, but a future version might decide to embed multiple instances into a single XML file to represent a sequence of successive solutions.
The <instance> element's bitwidth must be between 1 and 30.
The <instance> element's maxseq must be between 0 and (2^(bitwidth-1))-1.
The <instance> element can then contain 0 or more sigs, fields, and skolems.
There are two important things to understand about the document structure:
1) Each unique sig, field, and skolem must have a unique integer ID. So you cannot have two sigs both with ID="2". You cannot even have a sig and a field both with ID="2". However, their labels do not need to be unique. So you can <sig label="a" ID="7"> and <sig label="a" ID="8"> in the same instance, and they will be two distinct sigs that just happen to have identical labels.
2) Each unique atom must have a unique label. So you cannot have two distinct atoms with the same label. However, the atom labels have nothing to do with sig labels or field labels.
Now that we've established the above, we can talk about sigs, fields, and skolems in more detail.
Each sig must have a unique ID and a list of zero or more atoms.
If you wish to say sig B extends sig A, just add a parentID attribute to B's definition.
However, there are three builtin sigs that are special and must always exist in every instance:
<sig label="univ" ID="0" builtin="yes">,
<sig label="Int" ID="1" parentID="0" builtin="yes">, and
<sig label="seq/Int" ID="2" parentID="1" builtin="yes">
univ is at the root of the inheritance hierachy;
every normal sig extends univ, or extends someone who extends univ, etc.
When you write out the univ sig, you must make sure it contains every atom in this particular instance.
Int is the set of all integers.
It must contain every integer allowed by your bitwidth.
For example, if your bitwidth is 3, then Int must contain exactly {-4, -3, -2, -1, 0, 1, 2, 3}.
seq/Int is the set of all sequence index.
It must contain every nonnegative integer smaller than your maxseq.
For example, if your maxseq is 3, then seq/Int must contain exactly {0, 1, 2}.
Each field must have a unique ID and a list of zero or more tuples.
It must also contain one or more list of types.
For example, if you have a relation x from B to (A+B) where A's ID is 4 and B's ID is 8.
then under Alloy's union type system, x's type is the union B->A + B->B.
We would say x's parentID is B's ID, and x has two types: B->A and B->B.
Like this:
<field label="x" ID="9" parentID="8"> <tuple> <atom label="atom1"/> <atom label="atom2"/> </tuple> <types> <type ID="8"/> <type ID="4"/> </types> <types> <type ID="8"/> <type ID="8"/> </types> </field>
Each skolem is just like a field, except you never give it a parentID.
Below is a complete example, where we have the three builtin sigs (univ, Int, and seq/Int)
plus three user-defined sigs (p, a, b) and a user-defined field (x).
In this instance, bitwidth is 4 therefore Int={-8..7}; maxseq=4 therefore seq/Int={0,1,2,3}
On top of that, univ contained two other atoms a$0 and b$0. Therefore univ={a$0, b$0, -8..7}
sig p extends univ, and contains a$0 and b$0.
sig a extends p, and contains a$0.
sig b extends p, and contains b$0.
field x is a relation from b->(a+b), containing just one tuple in this case: (b$0, a$0).
<alloy> <instance bitwidth="4" maxseq="4" command="Run addEntry" filename="/User/my.als"> <sig label="univ" ID="0" builtin="yes"> <atom label="a$0"/> <atom label="b$0"/> <atom label="-8"/> <atom label="-7"/> <atom label="-6"/> <atom label="-5"/> <atom label="-4"/> <atom label="-3"/> <atom label="-2"/> <atom label="-1"/> <atom label="0"/> <atom label="1"/> <atom label="2"/> <atom label="3"/> <atom label="4"/> <atom label="5"/> <atom label="6"/> <atom label="7"/> </sig> <sig label="Int" ID="1" parentID="0" builtin="yes"> <atom label="-8"/> <atom label="-7"/> <atom label="-6"/> <atom label="-5"/> <atom label="-4"/> <atom label="-3"/> <atom label="-2"/> <atom label="-1"/> <atom label="0"/> <atom label="1"/> <atom label="2"/> <atom label="3"/> <atom label="4"/> <atom label="5"/> <atom label="6"/> <atom label="7"/> </sig> <sig label="seq/Int" ID="2" parentID="1" builtin="yes"> <atom label="0"/> <atom label="1"/> <atom label="2"/> <atom label="3"/> </sig> <sig label="p" ID="3" parentID="0"> <atom label="a$0"/> <atom label="b$0"/> </sig> <sig label="a" ID="4" parentID="3"> <atom label="a$0"/> </sig> <sig label="b" ID="8" parentID="3"> <atom label="b$0"/> </sig> <field label="x" ID="9" parentID="8"> <tuple> <atom label="b$0"/> <atom label="a$0"/> </tuple> <types> <type ID="8"/> <type ID="4"/> </types> <types> <type ID="8"/> <type ID="8"/> </types> </field> </instance> </alloy>