为合金中的 Sig 指定范围

【问题标题】：Specifying A Scope for Sig in Alloy为合金中的 Sig 指定范围
【发布时间】：2015-05-20 20:56:26
【问题描述】：

我是 Alloy 的新手，由于出现错误，我的程序无法执行或显示。我遇到的错误是

发生了语法错误：您必须为“this/Name”指定范围

我的代码是

    module language/Family
sig Name { }
abstract sig Person {
  name: one Name,
  siblings: Person,
  father: lone Man,
  mother: lone Woman
  }
sig Man extends Person {
  wife: lone Woman
  } 
sig Woman extends Person {
  husband: lone Man
  }
sig Married extends Person {
  }
fact {
  no p: Person | p in p.^(mother + father)
  wife = ~husband
}
fun grandpas[p: Person] : set Person {
  let parent = mother + father + father.wife + mother.husband | p.parent.parent & Man
  }
pred ownGrandpa[p: Person] {
  p in grandpas[p]
  }

这些是我的运行命令

run ownGrandpa for 4 Person
run ownGrandpa for 2 Person
run ownGrandpa for 1 Person

谁能帮我指出这个错误。

【问题讨论】：

标签： java oop alloy

【解决方案1】：

可以通过三种方式为模型分配范围。

第一个是为模型的每个签名分配一个范围。例如：run ownGrandpa for 4 Person, 3 Name

第二个是通过提供将应用于所有签名的全局范围。例如run ownGrandpa for 4

最后一个是前两个的混合，由一个全局范围和一个或多个单独的范围定义组成。例如run ownGrandpa for 5 but 4 Person. 全局范围将应用于缺少单个范围声明的所有签名。

因此，在您的示例中，run ownGrandpa for 5 but 4 Person 等同于 run ownGrandpa for 5 Name, 4 Person

请注意，提供这样的作用域只会给出从签名派生的原子数的上限。

如果您想表达您的任何实例都应该包含 4 个人（不多也不少），那么您应该使用关键字 exactly。例如run ownGrandpa for 5 but exactly 4 Person

【讨论】：