prompt_zero.txt

Alloy is a formal modelling language where that uses sets (named signatures in Alloy) and relations (sets of tuples, named fields in Alloy) to represent information in a domain.

In Alloy we can express requirements about a model using facts specified in relational logic, which is an extension of first-order logic with relational operators. Given a requirement it is useful to have both positive and negative instances to serve as test cases for validation. An instance of a model is a valuation to all declared sets and relations. 

Positive and negative instances can be included as test cases in a model using run commands. A run command includes a specification of the instance using relational logic, a scope that states how many elements of each top-level signature exist, and an expectation that states if the run command should be satisfiable (representing a positive instance) or unsatisfiable (representing a negative instance). To specify an instance with logic we can use an existential quantifiers to capture the elements of each signature of the domain, and then state what are the values of each set and relation using an equality with the name of the set or relation in the left hand side and the value in the right hand side. To express that a set or relation is empty we can specify that it is equal to the empty set (none) or empty relation of appropriate arity (for example, none->none if the relation is binary). Since there can be multiple total orders we must disambiguate which next relation is being defined using the <: operator with the signature on the left. The same applies if more that one relation is declared with the same name. The scope of run command only needs to define the number of elements that exist in top-level signatures, those that are not subsets of any other. 

In the following interaction you will act as an Alloy expert. I will ask you to generate positive and negative instances for different requirements for a given model.

Here are some instructions:
- Do not attempt to formalize the requirement with a fact, just output the requested instances as run commands.
- I will clearly state how many positive and negative instances you should output. 
- All instances should be truly different (be aware that the names of the elements are actually irrelevant).
- Try to produce minimal instances with few elements.
- All instances must include a comment explaining in natural language why it is positive or negative.
- All positive instances should have an expect 1 and all negative an expect 0.
- All instances must define the scopes for all top-level signatures in the model. 
- In every instance you must specify the values for all declared sets and relations with an equality restriction.
- To declare the elements of each signature use a some quantifier with the disj keyword to ensure that all elements are different.
- The value of a relation should take into account its arity. For example, if it is a ternary relation its value must be a set of triples.
- If a set or relation is empty you must explicitly state that it is equal to the empty set (none) or empty relation (of the correct arity).
- If there are two relations with the same name you must disambiguate using the <: operator with the domain signature on the left.
- If a model uses ordering on a signature you must also specify the value of the next binary relation using the <: operator to disambiguate. Signatures with ordering cannot be empty so next is never empty.
- If the value of some sets and relations is irrelevant for a given requirement you can just state that they are empty or assign them random values.
- Generate only Alloy code, do not include any explanations outside the code.