Сравнение элементов Alloy Analyzer из набора

Во-первых, вам нужно смоделировать свои операции до, после и. Функции ужасны для этого, потому что они не могут не возвращать что-то, что указывает на сбой. Поэтому вам необходимо смоделировать операцию как предикат. Значение предиката указывает, выполняются ли условия pre/post, аргументы и возвращаемые значения могут быть смоделированы как параметры.

Насколько я понимаю вашу операцию:

pred add[ x : Int, x' : Int ] {
  x > 0             -- pre condition
  x = 2 => 
    x'=x.plus[1] 
  else 
    x'=x
  x' > 0            -- post condition
}

В Alloy нет переменных для записи (в отличие от Electrum), поэтому вам нужно смоделировать состояние до и после с помощью символа штрих (').

Теперь мы можем использовать этот предикат для расчета набора решений вашей проблемы:

fun solutions : set Int {
  { x' : Int | some x : Int | add[ x,x' ] }
}

Мы создаем набор с целыми числами, для которых у нас есть результат. Главный символ не представляет собой ничего особенного в Alloy, это всего лишь условность для пост-состояния. Я немного злоупотребляю этим.

Этого источника Alloy более чем достаточно, чтобы делать ошибки, так что давайте проверим это.

run { some solutions }

Если вы запустите это, вы увидите в представлении Txt:

skolem $solutions={1, 3, 4, 5, 6, 7}

Это ожидаемо. Операция add работает только для положительных чисел. Проверить. Если вход равен 2, результат равен 3. Следовательно, 2 никогда не может быть решением. Проверить.

Признаюсь, меня немного смущает то, что вы делаете в своих утверждениях. Я пытался воспроизвести их точно, хотя я удалил ненужные вещи, по крайней мере, я думаю, что мы не нужны. Сначала ваше дело some. Ваш код выполнял all, но затем выбирал 2. Поэтому удалил внешнюю количественную оценку и жестко закодировал 2.

check  somen {
    some x' : solutions | 2.plus[1] = x'
}

Это действительно не дает нам никакого контрпримера. Так как solutions было {1, 3, 4, 5, 6, 7}, то в наборе 2+1=3, т.е. условие some выполнено.

check  alln {
    all x' : solutions  | 2.plus[1] = x'
}

Однако не все решения имеют 3 в качестве ответа. Если вы проверите это, я получу следующий контрпример:

skolem $alln_x'={7}
skolem $solutions={1, 3, 4, 5, 6, 7}

Заключение. Дэниел Джексон советует не учить Alloy с Ints. Глядя на свой класс Number, вы поняли его буквально: вы по-прежнему основываете свою проблему на Ints. Он имел в виду не использовать Int, не прятать их под ковер в поле. Я понимаю, откуда взялся Даниэль, но Ints очень привлекательны, поскольку мы так хорошо с ними знакомы. Однако, если вы используете Ints, позвольте им хотя бы использовать всю свою славу и не прячьте их.

Надеюсь это поможет.

И вся модель:

pred add[ x : Int, x' : Int ] {
    x > 0               -- pre condition
    x = 2 => 
        x'=x.plus[1] 
    else 
        x'=x
    x' > 0              -- post condition
}   
fun solutions : set Int { { x' : Int | some x : Int | add[ x,x' ] } }

run { some solutions }
check  somen { some x' : solutions | x' = 3 }   
check  alln { all x' : solutions  | x' = 3 }