为合金中的 Sig 指定范围 [英] Specifying A Scope for Sig in Alloy

问题描述

我是 Alloy 的新手，并且有一个错误导致我的程序无法执行或显示.我遇到的错误是

i am new to Alloy and there is an error due to which my program can't execute or show. Error iam having is

出现语法错误:您必须为this/Name"指定范围

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

谁能帮我指出这个错误.

Can Any one point out This Error for me Please.

推荐答案

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

There are three ways to assign a scope to your model.

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

The first one is by assigning a scope to each signature of your model. e.g. : run ownGrandpa for 4 Person, 3 Name

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

The second one is by giving a global scope that will be applied to all the signatures. e.g. run ownGrandpa for 4

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

The last one is a mix of the two previous and consists of a global scope accompanied by one or several individual scope definitions. e.g. run ownGrandpa for 5 but 4 Person. The global scope is to be applied to all the signature for which an individual scope declaration is missing.

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

Thus, in your example, run ownGrandpa for 5 but 4 Person is equivalent to run ownGrandpa for 5 Name, 4 Person

请注意，提供这样的范围只会给出从签名派生的原子数量的上限.

Note that providing scopes like this only gives an upper bound to the number of atoms derived from a signature.

如果您想表示您的任何实例都应包含恰好 4 个人(不多也不少)，那么您应该使用关键字 exactly.例如运行ownGrandpa 5但正好4个人

If you want to express that any of your instance should contain exactly 4 persons (no more, no less) then you should use the keyword exactly. e.g. run ownGrandpa for 5 but exactly 4 Person

这篇关于为合金中的 Sig 指定范围的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！