Решатель сплавов не имеет плавающего типа

Я пытаюсь написать задачу Alloy, в которой у меня есть набор состояний и переходов между ними. Моя цель — найти переходы между состояниями. Кроме того, каждое состояние s имеет значение, называемое X(s), которое можно вычислить, используя значение X его соседей, и мне нужно, чтобы все значения X были меньше определенного значения. Моя проблема в том, что Alloy не поддерживает float, и мои значения X могут не быть Int. Итак, если я хочу определить функцию X из состояний в некоторый числовой тип, этот тип может быть только Int. Можете ли вы придумать какой-нибудь способ обойти это?

Большое спасибо за вашу помощь, С уважением, Фатхие


int solver alloy
person Fathiyeh    schedule 07.02.2014    source источник

Ответы (3)


arrow_upward
1
arrow_downward

Это действительно зависит от того, что вы подразумеваете под вычислением X из его соседей.

Потребуется ли вам применять операции с плавающей запятой над X? Если это так, вы, вероятно, не сможете смоделировать свою задачу в Alloy.

Если вместо этого вы просто ожидаете применения простых арифметических операций, вы можете попытаться отобразить ваши числа с плавающей запятой в целочисленное представление в Alloy. С этим также следует обращаться осторожно, поскольку диапазон целых чисел в Alloy ограничен.

Еще лучше, если вам просто нужно сравнить порядки между X, вам лучше всего абстрагировать X от общей подписи Alloy и определить порядок его атомов с помощью модуля util/ordering.

person Nuno Macedo    schedule 11.02.2014

arrow_upward
0
arrow_downward

Я не знаком с Alloy, но одним из общих решений является использование арифметики с фиксированной точкой для представлять дробные числа с помощью целых чисел. Например, значение 1,23 можно представить как целое число 1230 с использованием коэффициента масштабирования 1/1000. Конечно, вам нужно будет учитывать этот коэффициент масштабирования в своих расчетах, умножая его на 1000, где это необходимо.

person vitaut    schedule 07.02.2014

arrow_upward
0
arrow_downward

Ну, первый подход, упомянутый vitaut, заключается в использовании семантики чисел с плавающей запятой, которая представляет собой число_с плавающей запятой = мантисса x показатель степени.

Другой способ моделирования — создание подписи с двумя «полями» — двумя целыми числами, представляющими числа слева и справа. Это может выглядеть так

sig Float{
    leftPart: one Int,
    rightPart: one Int
}
person Sp3c7r00M    schedule 10.06.2014