我是 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/