MIT的合金是一种声明性规范语言，用于表达软件系统中复杂的结构约束和行为，以及用于探索和检查结果结构属性的工具。
该问题可能回答是/否。考虑代码段：sig A {my：lone B} sig B {} pred single1 [x：A] {//使用[]定义＃x.my = 0} pred single2（x：A）{//使用（ ）＃...
我想使用Alloy解决以下锁定挑战。我的主要问题是如何对代表数字键的整数建模。我创建了一个快速草稿：sig Digit，Position {} sig Lock {d：...
某些背景：我的项目是制作一个从类似c的语言编译为Alloy的编译器。具有类似c语法的输入语言必须支持合同。现在，我正在尝试实现...
我正在尝试使用Alloy表示条件（if-else）语句。我的理解是我需要使用Hoare三元组。但是，我对软件验证工具和...
我正在尝试写一个谓词，使所有香蕉和新鲜苹果都变得昂贵。我能够达到其中一个条件，但不能同时达到两个条件。我对使用Alloy非常陌生，任何帮助都会非常...
我可以为合金分析仪指定自定义颜色（例如RGB）以在可视化中使用吗？
在主题窗格中，我希望摆脱几乎不可读的黄色，而将其替换为橙色，并可能将红色替换为较深的红色。是否有XML（或某种易于编辑的配置...
我如何将一组实例传递给Alloy Analyzer的Evaluator中的函数或谓词？
BLUF：我有一个谓词，它以一个签名实例和同一签名实例集作为参数。生成模型实例后，我想传递...
我正在学习Alloy建模语言，并且看到了这段代码。 sig人{合伙人：人}事实partnerProperties {合伙人=〜合伙人否p：人| p在p.partner中的}这段代码表示“ Person'...
我正在使用https://profsandhu.com/journals/tissec/p207-ahn.pdf作为启发，开发一个基于角色的简单授权模型。到目前为止的代码是：abstract sig Object {} abstract sig Operation ...
[当我使用Alloy（无论是v4.2还是v5）执行以下示例时，我得到的实例在解决方案空间中出现两次。 sig A {} sig B扩展A {} pred P {}对2个生成的实例运行P：...
模块测试sig Foo {} sig A {b：设置B，foo：一个Foo} sig B {foo：一个Foo} assert foo {all s：（univ-Foo）|全部相关：（univ-Foo）->（univ-Foo）| s不在s。* rel} ...
[我对合金报告使用seq找不到该模型的实例感到困惑：一个sig Const {T：seq（seq Int）} fact const_facts {Const.T = {0-> {0-> 1 + 1-> 9} +1-＆...
我尝试在O365插件加载机制中对错误进行建模，基本上就像书中的地址簿示例一样，该错误发生在您加载一个插件并退出插件模式然后重新打开它时。 ...
如何为Alloy中的信号写出文字？考虑下面的示例。 sig Foo {a：Int}事实{#Foo = 1}这个/ Foo |一个| | ---------- | --- || | Foo⁰| 7 |在...
假设我有以下模型：sig计数器{值：整数，} {值> 0值<3} pred show {}运行show精确地运行1个计数器，我想生成与...对应的als文件。
我总是以相同的方式使用Alloy：要么找到给定约束集（=模型）的实例（解决方案），要么检查可以表示为断言的模型的特定属性...
[我正在尝试编写Alloy函数来检索与该函数的参数有关的某种类型的所有元素（让我说，它们的“ fields / ...”之一具有该值）] >
我想知道，如何在合金中定义一对和一对序列？例如，在Z表示法中，我们可以将像c这样的变量定义作为成对的序列，即“ c：seq（A \ cross B）“ ...
找到很多困难的资源来寻找合金的功能。我成功地制作了一个返回一组值的函数（即具有“设置”返回类型），但是我无法弄清楚如何...