alloy

3热度

2回答

在Alloy网站的the Alloy grammar spec中，我发现自己被方括号使用困惑。在像下面这样的制作中，事情看起来很清楚。 specification ::= [module] open* paragraph* 我猜的方括号表示可选性和星号是克莱尼关闭，所以刚才所引述的规则意味着一个规范包括最多一个module声明，零项或多个open条款，以及零个或多个paragraph秒。这对

0热度

1回答

在合金中有没有像任何循环，而等等？

我可以写这样的事：为（I = 1;我< = 1000;我++）而（）

3热度

2回答

没有GUI的合金模型

我想用Python编写一个可扩展的程序，根据用户输入创建Alloy模型。特别是，我希望用户输入图形并使用Alloy来告诉用户图形是否具有欧拉路径。我在Alloy中为模型的特定实例准备好模型。但是，我正在考虑通过Python代码生成.als文件，然后通过Python启动Alloy来评估模型。是否有我可以使用的Alloy API或任何命令行参数可以帮助我确定某个谓词是否一致？感谢

0热度

1回答

扩展签名和原子实例化

我正在使用Alloy 4.2，并且我有使用继承的复杂性问题。很明显，签名之间的继承不像我以前在面向对象编程中面对的那样（或者至少如我所期待的那样）。显然，当运行命令中没有设置完全关键字时，即使根抽象类是抽象的，原子也会实例化为根抽象签名的原子。当精确关键字用于指定一个命令时，原子被指定为实例化：叶具体类。我希望能够搜索具有从另一个抽象继承的可变性的解决方案。它允许我指定叶签名中存在的抽象签

1热度

1回答

约束语法谓词和声明

我想知道如果在谓词中使用约束语法，而不是在断言中使用约束语法。约束all disj x1，x2：X | x1 = x2在谓词和断言中执行时会给出不同的结果。例如，假定下面的模型： sig A {} sig B {x: one A} assert S1 {all x1,x2: x | x1 = x2} 检查S1 2 - 作为反例x1和x2 assert S2 {! (all x1

0热度

1回答

合金类型错误

我有一个Alloy规范来表示java编程语言的子集。下面我们就这个模型的某些部分： abstract sig Type {} one sig void_ extends Type {} abstract sig PrimitiveType extends Type {} one sig Int_, Long_ extends PrimitiveType {}

1热度

3回答

不具有浮动类型的合金解算器

我想写一个合金问题，其中我有一组状态和它们之间的转换。我的目标是找到各州之间的转换。此外，每个状态s都有一个称为X（s）的值，可以使用其邻居的X值来计算，并且我需要X的所有值都小于特定值。我的问题是Alloy不支持float，并且我的X值可能不是Int。所以，如果我想定义一个从状态到某个数字类型的函数X，该类型只能是Int。你能想办法解决这个问题吗？非常感谢你的帮助，真诚， Fathiye

2热度

1回答

合金：事实等等关于诠释

我最近与合金工作。我可以这样说： fact{ all i: Int | i >= 0 } 我想说：所有整数合金的用途应该是积极的。合金不失败，但也不给我实例。问候

1热度

1回答

重构合金模型

在一个模式，我开始在合金勾画有一天，我收到以下消息时，我试图找到一个特定的谓词的一个实例：翻译能力突破。在这个范围内，宇宙包含34个原子，并且12的关系不能被表示。访问http://alloy.mit.edu/以获取有关重构的建议。对网站alloy.mit.edu看哪里的任何建议？我没有发现任何带有明显标签的东西，例如“重构超出翻译容量的模型”。这是关键问题。 [后记：我的问题的原因似乎

1热度

3回答

剩余类型的合金语法？

是否有直接的方式来表示Alloy中的余数类型，而不是必须显式减去union all的所有子类型？例如，在： sig Test {} one sig A, B extends Test {} 我希望能够通过速记并不需要改变每次Test获得由新SIG延伸到指表达Test-(A+B)。虽然这只会是语法糖，但它可以帮助我在重构模型时避免错误。