如何在Alloy中为函数返回单个值？

Question

找到很多困难的资源来寻找合金的功能。我成功地制作了一个返回一组值的函数（即具有“设置”返回类型），但是我无法弄清楚如何编写一个返回单个值的函数。一世。我有

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 {
     {one t : Time | some f : F | all g : F | f.time = t && gte[f.time,g.time]}
}

函数getTime获取一组文件并返回最新的文件戳（F中所有文件的最大时间属性）但是，无论我用哪种方式编写，都会不断地返回错误的返回类型（原始布尔值）错误或其他错误。如何返回时间类型的东西？

Answer 1

由于关键字one，您将获得布尔返回类型。仅当正好有一个满足以下谓词的时间t时，此量词才强制返回true。

没有任何量词，函数中的表达式就是我们所谓的集合理解，也就是说，将包含一个包含每次满足以下谓词的原子的集合]]

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