该签名包含两个字段，每个保持的整数： sig Test {
a: Int,
b: Int
}
该断言包含一系列约束： pred Show (t: Test) {
t.a = 0
t.b = 1
}
这些约束被隐式AND关系结合在一起。所以，这谓词相当于这个谓词： pred Show (t: Test) {
t.a = 0 and
中一套的所有子集我正在努力如何定义一个事件可以发布每个步骤，但多个删除的状态更改。我有这样的模式： open util/ordering[State]
sig Event {}
sig State {
queue : set Event
}
pred State.post(next' : State, event : Event) {
next'.queue = th
我最近开始尝试用于一个项目的合金，并且遇到了一个问题不均匀的问题。这是一个简单的例子。我有四个特征： 字 定义 文件：文件有一个文本（单词序列） 字典：字典单词序列映射到一个定义序列（保持简单，让我们说，一个词应该有一个确切的定义） 这里是一个最小的代码示例： module dictionaries
open util/relation as relation
sig Word {}
是否约束为了在这个pred件事： pred Example {
A
B
C
}
A，B，C表示约束。 那是pred与此相同pred： pred Example {
B
A
C
}
处于IF-THEN-ELSE下令限制？例如，是ReadMemory和WriteMemory在此IF-THEN-ELSE下令： pred Exampl
我有以下模式： sig A1 {
// ...
}
sig A2 {
// ...
}
sig S {
s_a1: one A1,
s_a2: one A2
}
我想“生产”的子集S1：基于S0的元件S：S受以下约束： S1具有相同数目的原子作为S0 那些原子在S0满足条件C1 [s_valid.s_a1] s_valid还必须包含在S1 每个这些原子s_i
页Software Abstractions 293说，这两者是等价的： all x: X, y: Y | F
all x: X | all y: Y | F
但是这两个是不相等的： one x: X, y: Y | F
one x: X | one y: Y | F
为什么是后两者并不等同？ 我用最具体的例子来学习，所以我们举一个具体的例子。 上周我乘坐邮轮去了阿拉斯加。晚餐时，
我经常听到类似这样的论点：传统测试的一个缺点是它是不完整的，而Alloy分析是详尽而完整的（在一个界限内）。但是，第一个是谈论软件，第二个是谈论模型。这不是一个苹果与橘子的比较吗？ 更新：我错了。比较不是这样的：testing code versus analyzing models。这是一个苹果与橙子的比较。相反，比较是这些： Testing models versus analysis of