如何查看 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 函数旨在返回给定文件集中具有最大时间戳的文件的时间值。我已经完成了这个功能，我相信它应该可以按预期工作，但我不知道如何实际测试它。我知道我可以在 Alloy 中运行函数，但我不知道如何创建一组样本文件以用作输入。每当我设法让某些东西运行时，在生成的可视化中都没有显示函数输出的内容。

Answer 1

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

您可以在此处输入以下内容：

univ

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

getTime[File$0]

评估函数。