如何查看 Alloy 中函数的返回值？

Question

我试图了解函数在 Alloy 中的工作原理，其中一个重要部分是测试它们。例如我有这个代码：

open util/ordering[Time]   // enforces total order on Time

sig Time {}                // instances denote timestamps

sig File {
   time : Time             // every file has exactly one timestamp
}

fun getTime[F : set File] : Time {
    {t : Time | some f : F | all x : F | f.time = t && gte[f.time,x.time]}
}

getTime 函数用于 return 给定文件集中具有最大时间戳的文件的时间值。我已经完成了这个功能，我相信它应该能按预期工作，但我不知道如何实际测试它。我知道我可以 运行 在 Alloy 中运行，但我不知道如何创建一组示例文件以用作输入。每当我设法得到一些东西到 运行 时，结果可视化中的任何地方都没有显示函数输出的内容。

Answer 1

在可视化中，您可以使用工具栏中的按钮打开“Evaluator”。

在那里你可以输入如下内容：

univ

获取所有原子的列表。并且：

getTime[File[=11=]]

计算函数。