Почему возможен сплав отрицательной кардинальности

Я описываю некоторые модели на языке Alloy. Чтобы описать конечный автомат, я предоставил несколько строк кода:

sig FSA_state {
    transitions: some FSA_state,
    initial: lone InitialState
}

sig InitialState {}

fact i {
    all f: FSA_state | #(f.transitions) <= 0
}

pred show {
}

run show for 5 but 1 InitialState

Теперь я пытаюсь понять, почему он делает более нуля переходов в одном состоянии. С помощью инструмента "Эвалюатор" я обнаружил, что некоторый мир имеет отрицательную кардинальность при переходах множеств, как это возможно (множество не может иметь меньше нуля элементов)? Инструкция, которую я использовал в Оценщике, это #(FSA_state.transitions)


set cardinality alloy
person Gianluca Venturini    schedule 10.01.2014    source источник

Ответы (2)


arrow_upward
0
arrow_downward

На самом деле вы обеспечиваете, чтобы количество переходов для каждого FSA_state было отрицательным. В вашей подписи FSA_state использование ключевого слова «некоторые» обеспечивает, чтобы количество переходов было по крайней мере один.

В экземпляре, который вам удалось сгенерировать, Alloy воспользовался ограниченной областью действия подписи Integer, чтобы удовлетворить оба противоречащих друг другу ограничения.

Действительно, если целые числа находятся в диапазоне, например, от -2 до 3, то если количество переходов для каждого состояния равно 4, #(f.transition) будет равно -2.

TL;DR: удалите факт i (ключевое слово some уже обеспечивает наличие хотя бы одного перехода на FSA_state)

person Loïc Gammaitoni    schedule 11.01.2014

arrow_upward
1
arrow_downward

Если вы хотите исключить все модели с переполнением, вы можете установить «запретить переполнение», доступное в версии 4.2.

person Aleksandar Milicevic    schedule 14.01.2014