问题标签 [alloy]

下面是我最近为手机短信完成的一个马马虎虎的合金规格。这只是基本的发短信要求，因为这是一种做法，我没有严格的要求要坚持。但是，我有一些尴尬的问题，例如为什么我不能获得超过 1 对 Name-Mobile 对？为什么 2 个 MessageSets 坚持指向一个 Name？除了问题之外，事实和谓词非常直截了当。请随意批评，因为我需要反馈来学习合金本身。

我在做以下事情时的想法；

一个 Message Box 有 0 个或多个 MessageSet。一套只属于一个人，没有一套是免费的。每组有 1 个或多个消息，由消息行、开始和结束键和行以及光标位置组成。多条消息可以属于同一个人，但一条消息不能同时属于 2 个人。每行有 1 个或多个键，并有它们的开始键和结束键。此外，一行可能有也可能没有新行。每个键可能有也可能没有下一个键。通过触摸板按下按键。每个名字都有一个手机号码，并记录在 ContactList 中。没有两个名字可以有相同的手机，但一个人可以有多个电话号码。

谢谢。

我几乎开始研究合金来做一些验证。我正在尝试练习制作一些代表编程语言的简单结构。

映射实体具有程序和依赖关系

程序具有功能

函数有几行代码

依赖关系是一个实体，将程序中某个函数中的两行代码相互映射

这是我尝试做的，但输出图显示了一行代码，它链接到依赖元组但与函数不匹配。我需要所有代码行都在一个函数中，它们可以是依赖关系，也可以不是......

我有一个合金模块

当我三合会运行此模式时，它给了我这个消息：“第 2 行第 5 列的语法错误：此处可能出现 3 个可能的标记：NAME seq this”

不知道是什么意思？

2\ 如果我有 2 个合金模型，每个模型都有相同的元素，即 mode1/name、model2/name。如何创建一个可以说 mode1/name = model2/name 的事实或 pred？

问候

任何人都可以在这里解释传递闭包运算符如何根据矩阵在合金中工作。我的意思是将闭包运算符转换为实际矩阵运算的转换规则。

我有一个小的合金规格如下：

首先，我认为合金会将 f1 转换为布尔矩阵，然后对其执行闭包操作。但它似乎没有进行这种翻译（看起来它在创建布尔矩阵之前运行了一些东西。）。那么这个 f1 究竟是如何翻译的呢？它使用关系谓词吗？我只是对合金的翻译很好奇。

我目前正在制作一个程序，该程序在 java 中处理一些注释，然后构建一个合金模型，使用合金 api 对其进行解析，然后运行一些合金命令。当我在合金应用程序中测试生成的合金模型时，它工作正常并给了我预期的结果。但是，当我通过 API 运行生成的合金模型时，它告诉我：“您必须为 sig this/ObjectName 指定范围”。我从这样的字符串中读取合金代码。

我使用的唯一选项是 SAT4J 求解器和 1 的 skolemdepth。

然后我遍历来自世界的命令，将它们转换为 kodkod，然后执行它们。

我更新的合金代码如下所示：

那么有没有人知道我该如何解决这个问题，因为我认为 for 1 Configuration, 8 Elements 将为所有扩展信号设置范围？

编辑*

我用建议更新了我的合金模型，但仍然收到相同的错误：“您必须为 sig “this/Controller”指定一个范围以上合金代码在合金分析器中工作并给出以下结果：

My question is whether the semantics of () in the declaration of fields had changed in Alloy 4.2.

I read in "Software Abstractions" that

means that the relation addr associates at most one address with each address book and name pair but this does not hold when running Alloy 4.2

For instance, for

Alloy 4.2 finds a model instance which has for instance AddBX$2 with

If I use instead

then no instance for the same run is found. This seems to indicate that in Alloy 4.2 this is how to declare that the relation addr associates at most one address with each address book and name pair but I would like to have a confirmation for this.

考虑以下地址簿示例的简单变体

在某些模型实例中，我可以在评估器中得到以下结果

如果 show 是一个关系，那么人们可能会期望得到如下答案：{ true, false }。假设它是一个谓词，则返回一个布尔值。我本来希望 show[Book] 是上面普遍量化的表达式的简写。相反，它似乎是在使用存在量化来折叠结果。任何人都知道这可能是什么原因，或者对 show[Book] 的含义有另一种解释？

在合金考虑

信号队列{链接：队列，元素：整数}

考虑到我有一些谓词 predicate-1，当我为 Queue <=1、int ={-3,-2,0,2} 运行 predicate-1 时，我将如何定义范围。我没有在这里列出谓词

为 1 个队列运行 predicate-1，此处为 int 范围

不知道 int 范围的语法是什么

如果我有一组特定的信号，例如我制定了一组 closed_Switches。我可以得到一组open_switches（或所有未关闭的开关）如下

刚开始使用合金，这是解决这个问题的正确方法吗？