合金规格中的类型错误答案

【问题标题】：Type Error in Alloy specification合金规格中的类型错误
【发布时间】：2015-07-08 21:06:47
【问题描述】：

在需求工程 (2007) 文章“问题框架中的需求进展”中，有一个关于交通灯问题的工作示例，我已将其转录到 Alloy 编辑器中。不幸的是，我在测试代码时收到以下错误。

正在启动求解器...

发生了类型错误：这必须是一个集合或关系。相反，它具有以下可能的类型： {PrimitiveBoolean}

错误由以下谓词触发：

pred LightUnitBreadcrumb [] {
    all t: Time | 
        NGObserve [t] <=> 
            odd [NGPulse [t]] and
        SGObserve [t] <=> 
            odd [SGPulse [t]] }

引用下面的 NGPulse 谓词：

sig NGP, SGP, NRP, SRP in Time {}
pred NGPulse [t: Time] {t in NGP}
pred SGPulse [t: Time] {t in SGP}
pred NRPulse [t: Time] {t in NRP}
pred SRPulse [t: Time] {t in SRP}

【问题讨论】：

没错。我在book 的第 137 页解释了为什么 boolean 不是 Alloy 中的类型。
感谢 Loic 和 Daniel 的跟进和澄清 - 非常感谢。

标签： requirements alloy

【解决方案1】：

我的猜测是，在 odd 的方括号之间需要一个集合值表达式，而不是调用 NGPulse 或 SGPulse 谓词。实际上，谓词是布尔值而不是集合/关系值表达式，因此会出现错误。

【讨论】：