Alloy constraint specification

Question

I wrote the following code block in Alloy:

one h: Human | h in s.start => {
    s'.currentCall = h.from
}

I want to pick one 'human' from a set of humans (s.start) and set a variable (s'.currentCall) equal to h.from. However I think this code is saying: There is only one human in s.start, where

s'.currentCall = h.from

is true. Is my assumption correct? And how should I fix this?

Answer 1

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.