问题标签 [alloy]

我正在学习 Alloy 教程，并且刚刚开始这一章。我的问题是本章开头的那句话：

现在我们已经建立了一个模型来确保我们的文件系统的结构正确性......

当我运行到目前为止构建的模型时，我仍然会发现文件系统断开连接，这似乎与这句话相矛盾。

这是Alloy 4.2，几天前从网站下载的构建日期2012-9-25。我做错了什么还是故意的？据我了解，我在模型中看不到任何可以防止这种断开连接的东西。但是我的理解还是有点模糊。

相关模型复制如下：

我可以看到live: set FSObject可能需要连接的线路，但这不是我目前对该线路语义的理解。

谁能告诉我如何使用 Alloy 中的函数输出二元关系？例如，学生与老师链接，学生也与课程链接。如何将学生作为输入，然后输出教师与课程之间的二元关系？

我正在尝试编写一个断言语句，大意是一旦为任何学生输入了一个分数，那么该学生总是对该课程有一个分数（尽管分数可能会改变）。我已经知道如何检查学生是否有分数，但是如果学生没有任何分数，我不知道该怎么做。另外，我怎样才能为这个断言语句写一个检查语句？

这是我试过的

但不知何故，它说：这个表达式没有经过类型检查。我是对还是错，如果我是对的，我该如何解决？

我希望能够将课程 c 作为输入；输出一组导师，他们负责一个或多个在 c 注册但还没有分数的学生。

任何人都可以帮助我吗？

具有以下内容：

任何人都可以帮助实施 Enq 和 Deq 吗？

任何帮助表示赞赏。

我需要使用合金模拟碳氢化合物结构基本上我需要设计烷烃、烯烃和炔烃基团我创建了以下签名（烯烃示例）

这适用于烯烃，但是当我尝试通过改变所有 a:alkynegrp|#ah=minus[mul[#(ac),2],2]的事实来为烷烃或炔烃设计相同的东西时，它不起作用。谁能建议我如何实现它？

我的问题陈述是在有机化学中饱和碳氢化合物是完全由单键组成的有机化合物，并被氢饱和。饱和烃的通式是 C _n H _2n+2（假设非环状结构）。也称为烷烃。不饱和烃在碳原子之间具有一个或多个双键或三键。具有双键的称为烯烃。具有一个双键的那些具有式 C _n H _2n（假设非环状结构）。含有三键的称为炔烃，通式为C _n H _2n-2。模拟碳氢化合物并给出谓词以生成烷烃、烯烃和炔烃的实例。我们尝试过：

e

烷烃的一般公式是 C _n H _2n+2，对于乘法，我们可以使用 mul 内置函数，但我们不能写加法，因为我们必须做 C _n H _2n+2。我们应该写什么才能使它适用于烷烃

I was trying to reverse a doubly linked list in alloy, I created a signature for it. This is the signature

The problem is that it gives desired result when i run for exactly 8 elemnts. After that it shows instances where one element has more than 3 indegree and 3 outdegree.

假设我在合金 4.2 中有以下签名声明：

运行时，生成的实例将具有从 everyB到 someTarget和 fromC到 some的箭头Target。

我怎么能只隐藏箭头B？
起初，我尝试了以下方法：

这将使我能够控制rin B，但是在编写属性时会引入很多歧义。我想让这些尽可能简单。例如：

上面说a'sTargets是a'children's的集合Targets。
对于后面的声明，我将不得不将其重写为

这是不可取的。

是否有任何解决方法可以拥有一个通用字段，但仍然可以控制显示的箭头？

我正在尝试使用alloy 对自动售货机程序进行建模。我希望创建一个模型，我可以在其中插入一些钱并为机器提供一个项目的选择选项，它会为我提供相同的功能，如果提供的钱少，则不会提供任何东西。在这里，我尝试输入一个硬币和一个按钮作为输入，它应该从自动售货机返回所需的物品，提供值即。分配给每个项目的金额作为输入提供。所以这里按钮 a 应该需要 10 个 Rs，按钮 b 需要 5 个 rs， c 需要 1 并且 d 需要 2 。op 实例是插入所需资金后返回的项目。opc 是要退回的硬币余额。ip 是输入按钮，x 是钱输入。我如何提供一个实例，使其接收多个硬币作为输入，并且如果金额大于项目成本，那么它应该返回一个硬币数量。如果我能得到一些帮助，将不胜感激。

我目前在我的项目中使用 Alloy api，我需要显示 A4Solutions。我可以使用 vizualiser Alloy 提供的 (vizGUI) 轻松做到这一点，但它对我的目的来说有点太有限了。所以我愿意从 A4Solution 对象生成我自己的图（使用任何其他图 api）。

我能够毫无问题地获得原子（这非常简单），但我真的不知道如何检索这些原子之间的关系。

我在网上查看了一些关于如何解析 A4Solution 的示例，但不幸的是什么也没找到。