java - 指定合金中 Sig 的范围

标签 java oop alloy

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

A Syntax error has occurred: You must specify a scope for "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

有人可以帮我指出这个错误吗?

最佳答案

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

第一个方法是为模型的每个签名分配范围。 例如:为 4 人、3 个名字运行 ownGrandpa

第二个是给出一个将应用于所有签名的全局范围。 例如运行 4 岁的自己的爷爷

最后一个是前两个的混合,由一个全局作用域和一个或多个单独的作用域定义组成。 例如为 5 人但 4 人运行自己的爷爷。 全局范围将应用于缺少单个范围声明的所有签名。

因此,在您的示例中,run ownGrandpa for 5 but 4 Person 相当于run ownGrandpa for 5 Name, 4 Person

请注意,提供这样的范围仅给出从签名派生的原子数量的上限。

如果您想表达您的任何实例都应恰好包含 4 个人(不多也不少),那么您应该使用关键字 exactly。 例如为 5 人运行自己的爷爷,但正好 4 人

关于java - 指定合金中 Sig 的范围,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30360214/

相关文章:

java - 在 Java 语言层次结构中添加自定义树类

alloy - 如何在 Alloy API 中实现以下 Alloy 模型?

java - 反向@OneToMany 不可更新

Java 抽象字段模式

java - jaxb:将属性绑定(bind)到元素

javascript - 将 .apply() 与 'new' 运算符一起使用。这可能吗?

alloy - 用合金制作井字棋模型

logic - 合金约束规范

java - 使用 Spring Security,我如何使用 HTTP 方法(例如 GET、PUT、POST)来区分特定 URL 模式的安全性?

java - Java 的文件路径或文件位置 - new file()