合金：使用断言检查约束时的arity问题

Question

我最近开始为一个项目试验合金，但遇到了一个不平等的问题。这是一个简化的例子。我有四个签名：

• 字
• 定义
• 文档：文档包含文本（单词序列）
• 字典：字典将一个单词序列映射到一个定义序列（为简单起见，假设一个单词应该只有一个定义）

这是一个最小的代码示例：

module dictionaries

open util/relation as relation

sig Word {}

sig Definition {}

sig Document {
    text: seq Word
}

sig Dictionary {
    entries: seq Word,
    defseq: seq Definition,
    define: Word->Definition,
}{
    //dictionary maps word to def only for the word present in dictionary
    dom[define] = elems [entries] function [define, elems [entries]]
    //content of the list of defintions
    defseq = entries.define
}

//assert all word in a  dictionary have a definition
assert all_word_defined {
    all w: Word | all dict: Dictionary | some def: Definition |
    //w in dict.entries implies w->def in dict.define
}

check all_word_defined

所以我的问题是：

1. 如何限制字典，以使字典中的每个单词都准确映射到一个定义？像上面的代码那样做对吗？

2. 如何检查断言是否遵守此约束？显然代码w in dict.entries implies w->def in dict.define 不起作用，因为w in dict.entries和w->def in dict.define 没有相同的元数，我收到错误消息“in can be used only between 2 expression of the same arity”...

Answer 1

我认为你在seq 和assertions 上比arity 更苦恼。

• seq 在 Alloy 中并不常见，只有在需要更改元素顺序时才使用它。在此示例中，我认为当前描述中不需要订购。
• 断言验证整个模型的不变量。你试图断言的更多是你在模型中陈述的事实，而不是你断言的。如果您已经定义了操作并且想要验证某些事情永远不会发生，无论这些操作如何执行以及以什么顺序执行，断言很有用。 IE。断言验证模型的后果，而不是事实。 （尽管有时验证某些东西是有用的。）
• Alloy 在浏览全局 表方面非常强大。尽管看起来是面向对象的，但诀窍在于了解字段实际上是连接的全局表。 （这是我花了很长时间才得到的。）
• 模型中不应包含冗余信息。 entries、defseq 和 define 可以使用 define 表上的函数进行建模。
• 基础语言非常强大。对于这种规模的问题，您通常不需要任何实用程序。尤其是在你感受了Alloy的关系模型之后，relation就显得很多余了。

好的，一步一步来：

一个文档是一个单词序列：

我只会将文档制作成一组 Word，因为这样更自然且更易于使用。在 this 问题中，单词的顺序不起作用，所以使用普通集合似乎可以吗？ （计算单词需要一个seq。）

 sig Word {}
 sig Document {
   text: Word
 }

字典将一个单词序列映射到一个定义序列（为了简单起见，假设一个单词应该只有一个定义）

我认为您的意思是字典可以将 a 单词映射到一个定义？每个单词都有一个条目吗？还是有一些词有条目？你说“a”，我认为它是一些具有一个定义的词？如果是这样：

 sig Definition {}
 sig Dictionary {
   define : Word -> one Definition,
 } 

define 表（即Dictionary->Word->Definition）有一个约束，即对于给定的 Dictionary->Word 组合，必须有 one 定义。这意味着并非所有单词都必须在表中，但如果单词在表中，则必须恰好有一个定义。 （您也可以使用其他约束对其进行建模。最好是写出一个表并查看列。）

您将entries 定义为字典中的单词集。您可以将其更好地建模为函数：

 fun Dictionary.entries : set Word {
   this.define.univ
 }

第一个连接选择define 表中的this 字典并删除第一列。第二个连接删除最后一列。

defseq 也类似：

 fun Dictionary.defseq : set Definition {
    this.define[univ]
 }

框连接[] 只是将方括号的内部与它之前的表格的第一列 连接起来，留下定义列。那就是：

 (univ).(this.define)

如何检查断言是否遵守此约束

我认为不清楚你试图断言什么。 （这是您发现这一点的正式语言的力量！）在 Alloy 中，您声明为字典中的单词映射到一个定义的事实。断言你已经定义为事实的东西是没有用的。在您可以断言之前，您首先需要更多定义。

通常，您开始编写谓词，然后查找模型的示例。例如，如果我们想查看无限字典之一，那么我们可以这样写：

pred show( d : Dictionary ) {
     d.define.univ = Word
}
run show for 5

在此示例中，您将看到一个字典，其中每个单词都有一个定义。

我写了一篇可能对你有用的博客：http://aqute.biz/2017/07/15/Alloy.html