问题标签 [alloy]

只是想知道如何在合金中使用我自己的 API？

我已经开发了合金 API，但我不知道如何使用它？

问候

穆迪

我目前正在使用 Alloy Analyzer API 来构建程序，并获得了一些特殊的行为。具体来说，如果我打开一个文件并解析它（使用 CompUtil.parseEverything），然后创建一个新命令并在解析的文件上调用 TranslateAlloyToKodkod.execute_command，并使用带有 UNSAT 核心的 MiniSat 新创建的命令，它运行良好。但是，稍后在执行中，我的程序解析第二个输入文件（也使用 CompUtil.parseEverything），获取另一个世界，发出一个新命令，然后我尝试再次调用 TranslateAlloyToKodkod.execute_command，它会引发以下错误：

ERROR: class edu.mit.csail.sdg.alloy4.ErrorFatal: The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)

有谁知道为什么这是第二次抛出，但不是第一次？

总而言之，我有类似以下内容：

Alloy 4 语法允许签名声明（和其他一些东西）携带private关键字。它还允许允许规范包含形式的枚举声明

语言参考没有（据我所知）描述private关键字或enum结构的含义。

有可用的文档吗？还是它们在语法中是为未来规范保留的结构？

我已经在 wiki 上阅读了这两个概念的定义，但区别仍然不清楚。有人可以举一些例子和一些简单的解释吗？

我正在尝试查看是否可以让 Alloy 返回特定集合的最大可能答案。因此，在此示例中，我希望模型查找器不生成答案x={}、x=A和。x=B

我已经尝试了一些类似的东西：

但我得到一个错误，即无法进行分析，因为它需要高阶量化。

我想知道是否有可能（或更简单）的方法来做到这一点？

下界多重性some和one三元关系的语义很难掌握。根据Software Abstractions (Rev. ed.) pp.79-80，关系addr: Book -> (Name -> some Addr)应该等同于all b: Book | b.addr in Name -> some Addr（另见 p.97）。但是后一个公式究竟是什么意思呢？我的想象力在这里失败了。这就是为什么我在 Alloy Analyzer 4.1.0 中做了一些实验。该模型的含义：

成立（没有找到反例）。因此，如果有任何书籍，则每个名称都应至少在其中一本中注册。允许未记录的地址，并且没有书籍，未记录的名称突然似乎也被允许。

以下模型中的含义：

再次持有。这是之前模型的镜像：禁止无证 Addrs，除非根本没有 Book。并且对于名称的文档没有任何限制。

两种模型都可以组合起来更简洁：

因此，如果有任何 Book，所有Names 都应该参与关系 addr1，所有Addr 都应该参与 addr2。多重one性行为相似。

就下界约束而言，似乎软件抽象和分析器并没有讲述关于R: A -> (B m -> n C)之类的构造的相同故事，但我可能遗漏了一些东西。我发现的含义不是我所期望的，并且可能还有其他我尚未发现的奇怪含义。我越来越觉得嵌套的下界多重性根本没有意义。我能说对吗？

我在 avlTree.als 中有一个合金模型。该模型使用整数运算，特别是加号和减号函数。这个模型中有一些断言，我可以使用 Alloy Analyzer GUI 很好地运行这些断言。

我在 test.als 中有另一个合金模型。该模型导入 avlTree（使用“open avlTree”），然后对 avlTree 模型中的关系进行一些断言。但是当我尝试在 Alloy Analyzer GUI 中运行这些断言时，我收到以下消息：

发生语法错误：

找不到名称“加号”。

语法错误的链接将我带到我的 avlTree 模型。因此，当我自己运行该模型时，似乎 avlTree 模型对整数数学的使用效果很好，但是当我尝试将其导入另一个模型时它会中断。有解决办法吗？

我正在运行合金 4.2。

根据 Alloy 4.2 的发行说明，存在与整数相关的语义更改。这些变化似乎对 Alloy 书的练习 A.1.6 产生了影响。

在本练习中，以以下代码为基础（我在最后添加了“Int”以显示我的问题）。当运行“show”谓词时，可视化器显示一个实例，但这个实例除了整数之外还包含两个原子“Univ0”和“Univ1”。

这两个原子“Univ0”和“Univ1”是什么意思？他们为什么在那里？它们与在 Alloy 4.1.10 上执行的代码不同。

我有两个类A，B并且与它们的额外类数据有关系R。

因此，A和B通过 相互关联R。

这里，Bool 定义为：

现在，我这样扩展A：

其中包含 this和 thatB之间存在关系以及数据类型为 的所有实例。ABTrue

我想将以下逻辑陈述表达为合金事实：

_{（来源：dropproxy.com）}

我在这里假设True == 1andFalse != 1集合A和分别R包含 and 的所有A实例R。

到目前为止，我尝试的是定义 a fun trueR(a : A)which 应该返回所有R's for whichR.a = a and r.data = True和 a fact allbIsRTruewhich 声明 for eachA allb应该是R.b's 返回的总和 by trueR。

但是，这就是我卡住的地方，我找不到正确的构造来对引用中的集合求和，并尝试sum导致语法错误。

我如何将我的正式约束指定为合金事实？

我对合金很陌生，目前正在阅读 mit 的教程。我有点卡在事情的逻辑上。我正在尝试做的一件非常基本的事情如下。

• 一个人最多只能完成一项任务
• 一项任务最多可由 1 人完成
• 一个人只能做他/她能够做的事

当我运行以下命令时，每个人都具有相同的技能（所有技能），并且每项任务都需要相同的技能（再次全部）。每个人至少被分配一项任务，但有时他们会获得相同的任务。

提前致谢