-
2 votesanswersviews
合金的配方翻译
我有一点合金规格如下： sig class {parents : set class} fact f1{all p:class | not p in p.^parents} run{} for exactly 4 class 首先，我认为合金会将f1转换为布尔矩阵，然后对其执行闭包操作 . 但似乎它没有做这种翻译（看起来它在布尔矩阵创建之前运行了一些东西 . ） . 那么这个f1究竟是如何翻译的... -
0 votesanswersviews
[合金]没有发现没有事实的实例
我在Alloy中编写了以下代码 . 我想知道为什么它找不到实例，因为代码中根本没有事实 . abstract sig TaskStatus {} one sig Completed extends TaskStatus {} one sig Waiting extends TaskStatus {} one sig OnGoing extends TaskStatus {} sig Capabi... -
6 votesanswersviews
Alloy中'private'关键字的含义是什么？ 'enum'声明的含义是什么？
Alloy 4 grammar允许签名声明（以及其他一些东西）携带 private 关键字 . 它还允许允许规范包含表单的枚举声明 enum nephews { hughie, louis, dewey } enum ducks { donald, daisy, scrooge, nephews } The language reference没有（据我所知）描述 private 关键字或 en... -
2 votesanswersviews
三元关系中的多重性
三元关系中下界多重性 some 和 one 的语义很难掌握 . 根据Software Abstractions（Rev. ed . ）第79-80页，关系 addr: Book -> (Name -> some Addr) 应该等同于 all b: Book | b.addr in Name -> some Addr （另见第97页） . 但后一个公式究竟意味着什么呢？我的想象力... -
3 votesanswersviews
合金4.2的语义变化对合金书的练习A.1.6的影响？
根据Alloy 4.2的release notes，存在与整数相关的语义变化 . 这些变化似乎对Alloy书的练习A.1.6产生了影响 . 在本练习中，以下代码作为基础（我在最后添加了“Int”以显示我的问题） . 当运行“show”谓词时，可视化器显示一个实例，但除了整数之外，该实例还包含两个原子“Univ0”和“Univ1” . module exercises/spanning pred ... -
-4 votesanswersviews
合金和webpro
我是合金的新人，我有一个与Alloy有关的任务 . 我必须用合金建模协议，该协议是一个网络协议 . 我有一个发送者，接收者和一个中间实体 . 我在这些实体上写了签名，但我不知道如何运行这个模型 . 我试图理解电子邮件客户端的地址簿示例，但是当我执行该示例时，它会生成一个简单书籍的大量实例，这些书籍将名称映射到一个地址 . 我认为模型中有3个签名是Book，Name和Addr . 如果我们运行此模型... -
0 votesanswersviews
“addFront”函数看起来非常程序化（即，不是声明性的）
在Software Abstractions一书的第10页，它强调了Alloy的声明性质： Alloy是声明性的，并通过比较before和after值来描述如何检查状态更改是否有效 . 第9页是添加新电子邮件地址簿的示例 . 该示例显示了“添加”之后的书籍状态与添加之前的书籍状态的不同之处 . 很好 - 确实很有说服力！ 在页135上是参数化“列表”模块的示例 . 该示例具有“addFront... -
0 votesanswersviews
为什么我为两个关系的连接和三个关系的连接得到相同的图形？
下面我创建三组：名称，地址和主机 . addr字段将Name映射到Address . 主机字段将地址映射到主机 . sig Name { addr: Address } sig Address { host: Host } sig Host {} 在这里，我要求Alloy Analyzer为两个关系的连接创建一个实例：addr和host . run {one addr.ho... -
1 votesanswersviews
“设置”是默认的多重性吗？
这两个是等价的： r: A -> B r: A set -> set B 那就是 set 的默认多重性？ 如果是，那么我将在Software Abstractions一书中对箭头操作符的定义进行狡辩 . 这本书在第55页说： 两个关系p和q的箭头乘积（或只是乘积）p-> q是通过从p中取出元组和q中的元组的每个组合并将它们连接起来得到的关系 . 我将该定义解释为p->... -
0 votesanswersviews
理解合金中的签名
我在合金网站上看到签名定义了一套 . 鉴于这个定义，我试图理解下面的合金代码： enum dooroptype { unlocked, locked, opened} enum enginetype {on,off} enum motortype { ismoving, still} enum key_location { in_car, faralone} abstract sig state... -
0 votesanswersviews
理解合金中复杂的特征
在下面 sig building{ abv: Man -> Man } { all m:Man | Above(m,m.abv) } 以下是什么意思？它与签名定义有什么关系？这是签名的关系吗？ { all m:Man | Above(m,m.abv) } -
0 votesanswersviews
Alloy中关系运算的域和范围
是否有任何操作返回Alloy中关系的范围和域 . 假设我在Alloy中定义了一个sig： sig A {r : B } sig B {} 我正在寻找和操作应用于r并给我B（可能像r [B]返回B） 上面的情况可能看起来很愚蠢，因为r [B]会返回B，所以为什么我不首先使用B！实际上我发现有一个范围和域操作（如果它们存在）在编写事实（约束）时非常有用 . 例如 . ： sig O {sup:O}... -
0 votesanswersviews
合金中三元关系中第一个和最后一个元素的投影
如何在Alloy中以三元关系投影第一列和最后一列？ 假设我有 r1: A->B->C 并假设 r1= (A0->B1->C1,A1->B1->C0, A2->B0->C2) ，如何定义 r2: A->C 为 r2= (A0->C1,A1->C0, A2->C2) 更具体的是，如果我有： sig A {r1：B-> C，... -
2 votesanswersviews
合金中的基数运算符（＃）错误结果
我使用#manrator获得笛卡尔积（A-> B）和Union（A B）的基数 . 但它返回奇怪的负数，我不知道它们是什么！？ 请看下面的快照，显示我的模型的A-> B和A B内容以及Alloy给我使用#manrator的基数 . （我希望第一个获得12个，第二个获得8个，但第一个获得-4而第二个获得-8） 任何意见？！ 如果它有帮助，波纹管是我的规格： open util / ... -
0 votesanswersviews
合金：仅定义与正整数的关系
我有一个这个sig的模型： sig Thing {} sig World { quantities: Thing ->one Int, } 我想在 quantities 关系上定义一个约束，这样每个Thing的数量必须是一个正整数 . 我是Alloy的初学者（我没有理论背景可供借鉴，我只是一名Python程序员） . 我按照教程进行了操作，但是我没有看到我想要做的配方 . 我知道如... -
3 votesanswersviews
在Alloy中隐藏一个子类型的字段
假设我在合金4.2中有以下签名声明： sig Target {} abstract sig A { parent: lone A, r: some Target } sig B extends A {} sig C extends A {} 运行时，生成的实例将包含从每个 B 到某些 Target 的箭头，以及从 C 到某些 Target 的箭头 . 我怎么能只隐藏 B 中的... -
2 votesanswersviews
重构合金模型
在模型中，我开始在Alloy中绘制草图，当我尝试查找特定谓词的实例时，我收到以下消息： 超出翻译能力 . 在此范围内，Universe包含34个原子，并且无法表示arity 12的关系 . 访问http://alloy.mit.edu/获取有关重构的建议 . 有关Alloy.mit.edu网站在哪里的任何建议？我找不到像“重构超出翻译能力的模型”这样明显标签的东西 . 这是至关重要的问题 . ... -
0 votesanswersviews
合金中的重构
我有一个具有这种关系的Alloy模型： sig myint {nextX：（myint - > myint - > myint） - > myint，nextT：（myint - > myint - > myint） - > myint} 我收到以下错误消息： 翻译能力超出 . 在此范围内，Universe包含84个原子，并且无法表示arity 5的关系... -
1 votesanswersviews
指定合金中关系的属性
我试图在Alloy中表达关系的某些数学属性，但我不确定我是否有正确的方法，因为我只是一个初学者 . 非常感谢来自专家社区的任何见解！ Specifying the fact that domain of a relation as singleton . 例如以下是一种合理而正确的方法吗？ pred SingletonDomain(r: univ->univ) { one ~r } s... -
0 votesanswersviews
显示派生关系
考虑一个简单的图形结构 G ，它在一组节点上定义了几个关系（ r1 和 r2 ） . 我想谈谈我的图表是否具有某个名为 wf_G 的属性 . 此属性通过从 r1 和 r2 派生另一个关系 r3 ，然后约束 r3 来定义 . sig X {} sig G { r1, r2 : X -> X } pred wf_G [g : G] { let r3 = (g.r1 - iden) . (... -
1 votesanswersviews
如何解释合金事实
我正在读an article that uses Alloy to model some safety and security requirements for aircraft avionics . 我正在努力理解文章中显示的一个"fact constraints" . 数据流入系统 . 数据由系统使用 . 该模型声明了一组Data，一组System和一个consumeBy... -
0 votesanswersviews
合金：使用断言检查约束时的arity问题
我最近开始为一个项目试验合金，我遇到了一个不平等的问题 . 这是一个简化的例子 . 我有四个签名： Word 定义 文件：文件有文字（一系列文字） 字典：字典将一系列单词映射到一系列定义（为了保持简单，让我们说一个单词应该只有一个定义） 这是一个最小的代码示例： module dictionaries open util/relation as relation sig W... -
1 votesanswersviews
集合联合的积累
我有两个类 A 和 B 以及与它们的类 R 的额外数据的关系 . 所以， A 和 B 通过 R 相互关联 . sig A {} sig B {} sig R { a : A, b : B, data : Bool } 在这里，Bool被定义为： sig Bool {} sig True, False extends Bool {} 现在，我像这样扩展 A ： sig ... -
1 votesanswersviews
如何避免在合金分析器窗口中出现额外的箭头
我在Alloy中有以下规格： sig A {} sig Q{isA: one A} fact { all c1,c2:Q | c1.isA=c2.isA => c1=c2 // injective mapping all a1:A | some c1:Q | c1.isA=a1 //surjective } run {} for 4 当我生成此规范的实例时，... -
0 votesanswersviews
在Alloy中为每个关系创建一个对象
我有以下def . 在合金中： sig A {b : set B} sig B{} sig Q {s: A , t: B} 我想添加一组约束，使得对于每个关系b1：b存在一个且仅存在一个Q1：Q，其中Q1.s和Q1.t分别指向b1的源和目标 . 例如，如果我有一个包含A1和B1并且b1连接它们的实例（即b1：A1-> B1），那么我也希望有一个Q1，其中Q1.s = A1，Q1.t = B... -
1 votesanswersviews
合金 - 找不到不满的核心
我有一个“No instance found”Alloy文件，并想调试它 . 文档说要去选项并选择SAT Solver>不满核心 . 然而，我没有看到，只有SAT4J . 我正在运行最新的Alloy 4.2，刚下载 . 当我运行时，有一条关于不支持JNI的说明 . 如果我需要下载不同的配置以查看不满核心，请告诉我该怎么做 . 否则，我该如何调试Alloy文件？ 那是最新的稳定 . 我也尝试... -
0 votesanswersviews
如何表达这种约束：在一个以上的乐队中有一个歌手
我想表达这种约束：在一个以上的乐队中有一个歌手 . 以下是Band和Singer的声明 . 关系“乐队”将歌手映射到乐队 . sig Band {} sig Singer { band: Band } 这似乎表达了期望的约束： some s: Singer | some s.band 反思后，我认为这不正确 . 它说（我相信）有一个歌手在_1841566频段 . （我对么？） 我希望约... -
0 votesanswersviews
处理多个关系（arity~10）
我有一个类似于这个的sig的模型： sig State { ps: set P, cs: set C, o: set C -> set P, m: set M } 像这样的谓词，处理两个 State ： pred my_pred [s, s': State] { ... } 我有一个 State sig，而是在函数和谓词中显式传递这些字段 . 这意味着拥有类似的谓词... -
1 votesanswersviews
使用合金实例创建Java实例并自动生成测试用例
我想将alloy4用于自动化测试用例生成研究项目 . 任何人都可以帮我这个吗？如何使用合金生成实例来使用合金创建java实例对象？ -
4 votesanswersviews
Alloy - 从.als生成.xml实例
我需要在程序中从.als生成随机的.xml实例 . 我设法通过在后台运行合金（不可见的JFrame）并调用doOpen，doExecuteLatest和doShowLatest函数来做到这一点 . 但每次运行我的代码时都要等合金开始是一件痛苦的事 . 我认为如果我简单地使用合成代码部分执行此程序（我想这将是kodkod）会更有效率 . 有谁知道这是怎么做到的吗？我发现合金的代码非常令人困惑.......