问题标签 [alloy]

一段时间以来，我一直对形式化方法感兴趣。我已经使用正式的方法来推理我一直在从事的几个项目的一些非常具体的子领域。我永远无法说服其他团队成员尝试相同的方法，更不用说使用正式的方法指定整个域了。

我发现一种特别有趣的方法是Alloy。我认为它可以更好地“扩展”作为整个项目的基础，因为它在概念上和符号上非常接近实际的编程语言。此外，这些工具非常可靠，因此模型验证的好处很容易获得。

我很想听听你们在项目中使用 Alloy 的实际经验。你觉得它帮助你设计了一个更好的领域模型吗？验证期间是否在您的域模型中发现错误？你会再次使用它吗？

我被困在这个正式的方法作业问题上，我不确定我做错了什么。

我有两个签名，Item 和 ToDo，它们的定义如下：

我必须定义一个函数，它将具有给定日期和类别的项目插入到待办事项列表集中。诀窍是列表集应该按项目的到期日期排序。步骤和日期都有排序。

我的问题是：如何在 ToDo.list 中获取具有特定日期的项目集？我有这个功能：

我尝试使用以下代码（及其变体）来获取项目集：

这不起作用，我理解为什么，因为 t.due.st 留下了一组日期。然而，从那时起的其他尝试并没有让我到达那里。在到达 t 之前，我尝试使用括号来评估“due.st”和“d”之间的连接，但这不起作用，我尝试使用方括号来更改顺序，但是不起作用。我知道我在这里做错了什么，但我不知道是什么。

考虑一个upgrades关系：

我需要确保它upgrades不能是循环的。我怎样才能在合金中做到这一点？

所以我在Alloy中有以下代码：

但这不会产生任何包含队列的实例，我想知道为什么。它只显示带有节点的实例。我试过等效的谓词

但输出是一样的。

我错过了什么吗？

我想将alloy4 用于自动化测试用例生成研究项目。谁能帮我解决这个问题？如何使用合金生成的实例来创建 java 实例对象？

这是家庭作业，我遇到了很多麻烦。我正在使用Alloy对库进行建模。以下是对象的定义：

然后我们需要有一个事实，即每本书要么在书架上，要么被赞助人取出。但是，它们不能同时出现在这两个地方。

我试过这个...

但它不起作用……书总是在书架上。想说，“每一本书，如果不借，就上架。否则，就出去了。”

非常感谢更正、示例和提示。

我在 ALLOY 中有一段代码我正在尝试做一个餐厅预订系统，我有这个信号和它们之间的关系。

我想说明一个事实，早餐可以预订或免费，午餐和晚餐都一样，有什么想法吗？

我是 Alloy（规范语言）的初学者，需要根据案例研究做一些进一步的工作，可以在这里找到（代码在第 5 页）。相关代码：

更正一些语法后，我收到此错误消息：“此表达式无法进行类型检查”，并t'在let t' = T0/t.next. 如何进行类型检查t'？

我正在尝试用 Alloy 对代数群的结构进行建模。

一个组只有一组元素和具有某些属性的二元关系，所以我认为它非常适合合金。

这就是我开始的

将以下约束添加到 cafe.als：

• 您可以从任何一家咖啡馆开车到任何其他咖啡馆（尽管可能没有直达路线）。
• 咖啡馆之间的步行道是双向的。
• 每家咖啡馆都可以从其他咖啡馆直接到达，只需一两步。
• 公共汽车在一条非分支路线上访问每家咖啡馆。（注意：您可能希望为此稍微更改总线关系的声明。）

我从未与 Alloy 合作过，我的教授也几乎没有接触过它。我真的迷路了，任何人都可以帮助解释发生了什么或帮助我解决任何问题吗？