没有浮动类型的合金求解器答案

【问题标题】：Alloy solver not having float type没有浮动类型的合金求解器
【发布时间】：2014-02-07 02:42:15
【问题描述】：

我正在尝试编写一个合金问题，其中我有一组状态和它们之间的转换。我的目标是找到状态之间的转换。此外，每个状态 s 都有一个称为 X(s) 的值，可以使用其邻居的 X 值来计算，我需要 X 的所有值都小于特定值。我的问题是合金不支持浮点数，我的 X 值可能不是 Int。所以，如果我想定义一个从状态到某个数值类型的函数 X，那么该类型只能是 Int。你能想出什么办法来解决这个问题吗？

非常感谢您的帮助，真挚地，法蒂耶

【问题讨论】：

标签： int solver alloy

【解决方案1】：

这真的取决于你从邻居计算 X 的意思。

您是否需要对 X 应用特定于浮点数的操作？如果是这样，您可能无法在 Alloy 中模拟您的问题。

如果您只是希望应用简单的算术运算，则可以尝试将浮点数映射到 Alloy 中的整数表示。这也应该小心处理，因为 Alloy 中的整数范围是有界的。

更好的是，如果您只需要比较 X 之间的数量级，最好将 X 抽象为通用合金签名，并使用模块 util/ordering 定义其原子的顺序。

【讨论】：

【解决方案2】：

我对合金不熟悉，但一种通用的解决方案是使用fixed-point arithmetic 用整数表示小数。例如，值 1.23 可以使用 1/1000 的比例因子表示为整数 1230。当然，您需要在计算中考虑这个比例因子，必要时乘以 1000。

【讨论】：

【解决方案3】：

vitaut 提到的第一种方法是利用浮点数的语义，即 floating_point_number = mantissa x exponent。

另一种建模方法是创建一个具有 2 个“字段”的签名 - 2 个整数代表左侧和右侧的数字。它可以是这样的

sig Float{
    leftPart: one Int,
    rightPart: one Int
}

【讨论】：