alloy 相关问题

MIT的合金是一种声明性规范语言,用于表达软件系统中复杂的结构约束和行为,以及用于探索和检查结果结构属性的工具。

如何可视化合金中具有多种边类型的图

虽然Alloy有图模块,但该模块不区分不同的边类型。 我在合金中制作了一个具有多种边缘类型的图表。但可视化是违背直觉的。 sig 节点 { 到 ...

回答 1 投票 0

如果结果不符合预期,如何调试Alloy?

当 Alloy 说“未找到实例”时。我怎样才能找到更多细节来了解为什么结果不符合预期? 我正在使用合金分析仪 6.1.0 我的代码是, sig 状态,节点 {} 信号列表 { 头...

回答 1 投票 0

如何设置事件式模型的可视化

我正在阅读这本书并尝试合金 6 中的示例。对于第 6.2.4 节“基于事件的变化”,我无法真正理解结果。特别删除NoIntervening fact

回答 1 投票 0

书中的示例是否应该完善以避免结果不一致

当书中示例的现有合金模型用于合金6.1时, 评估结果给出了加法运算的直观表示: 在书籍实例中 Book$0 Name$1 与 ...

回答 1 投票 0

如何将正则表达式集成到合金分析仪中?

我目前正在使用 Alloy 为容器编排器建模。事实证明,我需要写的很多事实都涉及到正则表达式(regex)。由于 All 默认情况下不支持正则表达式...

回答 1 投票 0

合金分析仪 - 仅自然数 - 无整数集

有没有办法像Alloy中的Int那样声明自然数? 目前我有 util/integer,如果我运行 run 6 Int 我得到: 整数={-32, -31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -...

回答 1 投票 0

合金中从谓词演算风格到关系演算风格

我有两个合金事实: 事实 A5 { 所有 a、b:填充,s、t:槽 | (s.slot_of 中的 b 和 a.fills 中的 s 以及 t.slot_of 中的 a)意味着 t.slot_of 中的 b } 事实 A6 { 所有 a、b:填充,s、t:槽 | ...

回答 1 投票 0

在大于 7 的整数声明中找不到实例

我正在尝试模拟一个关于泳池上一些女孩的问题。有一些必须遵循的前提。 Maio: amarelo, azul, branco, verde 姓名:安娜、布鲁娜、拉奎尔、薇薇安 伊达德:8、9、10,...

回答 0 投票 0

合金书例子错了?

阅读丹尼尔杰克逊的软件抽象。尝试创建一个简单的模型,意识到它没有按我预期的方式工作。回到书中最基本的模型,和我自己的1:1,还有

回答 2 投票 0

在 Mac OS X 上使用 JPype 的问题:我尝试启动 JVM,但找不到 DLL,但它就在那里

我的 Python 代码是: 导入jpype jvm_path = "/Library/Java/JavaVirtualMachines/microsoft-11.jdk/Contents/Home/lib/jli/libjli.dylib" jpype.startJVM( jvm_path, 类路径=['~/org.

回答 0 投票 0

用合金进行动态建模

我正在评估一个同事的投稿,使用Alloy对问题进行建模,并深入了解满足规范所需的额外问题约束。我相信Alloy是...

回答 1 投票 0

Alloy-如何启用Unsat Core求解器?

我目前正试图在Alloy上使用Unsat Core,但我的求解器选项仅限于PLingeling和Sat4J。我也得到了一个警告,说基于JNI的求解器在我的 ...

回答 1 投票 2

Alloy : 限制一个字符串字段的值

让下面简单的Alloy代码:sig somme{ f : one Ax1, g: one Ax2, } let Ax1= String let Ax2= "Spain" + "Italy" 我想把字段f的值限制在 "Italy "范围内,所以我写了一个谓词: ...

回答 1 投票 0

合金:如何理解Alloy演示中的反例?

出于好奇,我写了一个奇怪的Alloy演示,关于“断言”。假设有一个“程序”,“程序”有2个“变量”,每个“变量”都有“数据”集中的“值”。然后我还设置了一个“事实” ...

回答 2 投票 0

使用用于Java的Alloy API动态修改Alloy模块

我正在使用Alloy API for Java,从文件中读取模块,执行其命令,并检查其可满足性。如果不满意,我想对模块进行更改,特别是放宽...

回答 1 投票 0

评估此合金表达

如何评估这种合金表达? ^ {y0-> y1-> y1,y0-> y2-> y0,y1-> y0-> y1,y2-> y0-> y0,y2-> y1-> y2,y2-> y2-> y1} [y]

回答 1 投票 0

合金分析仪作为常数求解器

朋友是一个社交网络,成员之间可以通过友谊关系建立联系。成员可以发布帖子(仅包含文字)和可选照片。每张照片都有标题,可以...

回答 1 投票 -2

Alloy:如何定义两个模块之间的关系而没有模块依赖性错误?

[以前,我定义了两个简单的签名,以便可以知道该车轮属于哪辆车。 sig Car {车轮:某些车轮} sig Wheel {BelongCar:一辆汽车,} {BelongCar = this。〜@ ...

回答 1 投票 0

合金pred声明:方括号和括号之间是否有区别?

该问题可能回答是/否。考虑代码段:sig A {my:lone B} sig B {} pred single1 [x:A] {//使用[]定义#x.my = 0} pred single2(x:A){//使用( )#...

回答 2 投票 0

合金中的挑战锁>>

我想使用Alloy解决以下锁定挑战。我的主要问题是如何对代表数字键的整数建模。我创建了一个快速草稿:sig Digit,Position {} sig Lock {d:...

回答 3 投票 0

© www.soinside.com 2019 - 2024. All rights reserved.