You are absolutely correct, the meaning of the one
quantifier is that there is exactly one element in the given domain (set) such that the quantifier body holds true.
Regarding your original goal of picking one element from a set and setting its field value to something: that sounds like an imperative update, and you can't really do that directly in Alloy; Alloy is fully declarative, so you can only assert logical statements about the sets and relations for a bounded universe of discourse.
If you just change one
to some
and also change the implication to conjunction, and then run the analysis (a simple run
command to find a valid instance), the Alloy Analyzer will find a model in which the value s'.currentCall
is equal to h.from
for some (arbitrary) h
from s.start
:
pred p[s, s': S] {
some h: s.start | s'.currentCall = h.from
}
run p
I hope this is what you want to achieve.