Я написал следующий блок кода в Alloy:
one h: Human | h in s.start => {
s'.currentCall = h.from
}
Я хочу выбрать одного «человека» из набора людей (s.start) и установить переменную (s'.currentCall) равной h.from. Однако я думаю, что этот код говорит: в s.start есть только один человек, где
s'.currentCall = h.from
правда. Верно ли мое предположение? И как мне это исправить?
Вы абсолютно правы, значение квантификатора one состоит в том, что в данном домене (наборе) есть ровно один элемент, для которого выполняется тело квантификатора.
Что касается вашей первоначальной цели - выбрать один элемент из набора и установить значение его поля для чего-то: это звучит как обязательное обновление, и вы не можете сделать это непосредственно в Alloy; Alloy полностью декларативен, поэтому вы можете утверждать только логические утверждения о множествах и отношениях для ограниченного универсума дискурса.
Если вы просто измените one на some и также измените импликацию на соединение, а затем запустите анализ (простая команда run для поиска действительного экземпляра), анализатор сплава найдет модель, в которой значение s'.currentCall равно h.from для некоторых (произвольно) h из s.start:
pred p[s, s': S] {
some h: s.start | s'.currentCall = h.from
}
run p
Я надеюсь, что это то, чего вы хотите достичь.
