There are some documentation errors for sequences (seq keyword), found at the following page:
http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html
Preconditions for sequence operations are stated in the documentation, but the meaning of a precondition in terms of model finding is not consistent. A formula which contains a seq operator with a false precondition is sometimes unsatisfiable, sometimes satisfiable.
Ideally, Alloy should not return a model where the precondition is false (ie, a predicate applied to a seq operator whose precondition is false should be valued as false also). However, this is certainly an issue to discuss individually.
For now, the documentation should be updated to reflect the current behavior.
Here is a list of preconditioned operators with their behaviour and an Alloy model test_seq_1.txt to illustrate them.
s.setAt [i, x]
Precondition: 0 <= i < #s
It should be : 0 <= i <= #s
Unsatisfiable if precondition not satisfied
s.insert [i, x]
Precondition: 0 <= i <= #s
Unsatisfiable if precondition not satisfied
s.delete [i]
Precondition: 0 <= i < #s
Unsatisfiable if i < 0
Satisfiable if i >= #s, returns the input sequence
Precondition should be : i >= 0
s.subseq [from, to]
Precondition: 0 <= from <= to < #s
Satisfiable if precondition is false, returns the empty sequence
Should not state a precondition
Pull request to follow.
There are some documentation errors for sequences (seq keyword), found at the following page:
http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html
Preconditions for sequence operations are stated in the documentation, but the meaning of a precondition in terms of model finding is not consistent. A formula which contains a seq operator with a false precondition is sometimes unsatisfiable, sometimes satisfiable.
Ideally, Alloy should not return a model where the precondition is false (ie, a predicate applied to a seq operator whose precondition is false should be valued as false also). However, this is certainly an issue to discuss individually.
For now, the documentation should be updated to reflect the current behavior.
Here is a list of preconditioned operators with their behaviour and an Alloy model test_seq_1.txt to illustrate them.
s.setAt [i, x]
Precondition: 0 <= i < #s
It should be : 0 <= i <= #s
Unsatisfiable if precondition not satisfied
s.insert [i, x]
Precondition: 0 <= i <= #s
Unsatisfiable if precondition not satisfied
s.delete [i]
Precondition: 0 <= i < #s
Unsatisfiable if i < 0
Satisfiable if i >= #s, returns the input sequence
Precondition should be : i >= 0
s.subseq [from, to]
Precondition: 0 <= from <= to < #s
Satisfiable if precondition is false, returns the empty sequence
Should not state a precondition
Pull request to follow.