代码之家 › 专栏 › 技术社区 › Roger Costello

约束何时隐式AND?约束何时必须显式AND?

alloy

Roger Costello · 技术社区 · 7 年前

此签名包含两个字段,每个字段包含一个整数:

sig Test {
    a: Int,
    b: Int
}

pred Show (t: Test) {
    t.a = 0
    t.b = 1
}

这些约束隐式地和在一起。因此,该谓词等价于该谓词:

pred Show (t: Test) {
    t.a = 0 and
    t.b = 1
}

该断言包含一系列约束,后跟一个蕴涵运算符:

assert ImplicationTest {
    all t: Test {
        t.a = 0
        t.b = 1 => plus[t.a, t.b] = t.b
    }
}

但在这种情况下,约束不是隐式AND'ed在一起。如果我想让他们和ed在一起,我必须明确和他们:

assert ImplicationTest {
    all t: Test {
        t.a = 0 and
        t.b = 1 => plus[t.a, t.b] = t.b
    }
}

1 回复 | 直到 7 年前

Peter Kriens 7 年前

我查看了解析器,据我所知,它将换行符/空格的右侧和左侧视为带括号的表达式。

expr exprs -> expr and exprs

t.a = 0  t.b = 1   t.c =2  => plus[t.a, t.b] = t.b

相当于:

(t.a = 0) and (t.b = 1 and ( t.c => plus[t.a, t.b] = t.b))

以下模型似乎证明了这些表达式是等效的:

sig Test {
    a: Int,
    b: Int,
    c: Int
}

pred simple( t: Test ) {
    t.a = 0 t.b = 1 t.c = 2 => plus[t.a, t.b] = t.b
}

pred full( t: Test ) {
    (t.a = 0) and  ((t.b = 1) and (t.c=2 => plus[t.a, t.b] = t.b))
}

assert Equivalent {
    all t : Test {
        simple[t] <=> full[t]
    }
}

check Equivalent for 10

推荐文章

Roger Costello · 检查两种方法的等效性,以确保所有酒店客人都能获得一套独特的钥匙

7 年前

Lorin Hochstein · 在MacOS上运行IDEA中的bnd结构化应用程序:未解决的需求:导入包:com。苹果eawt公司

7 年前

Roger Costello · 使用关系值创建签名字段是最佳做法吗?

7 年前

Roger Costello · 是否以XML形式查看实例?

7 年前

Roger Costello · 正确的术语:调用订购模块?是否使用订购模块?使用排序模块约束集合?

7 年前

Hovercouch · 合金中带量词的传递闭包

7 年前

Peter Kriens · 在合金中构建关系

7 年前

Paul · 我可以用Alloy来解决线性规划之类的问题吗?

7 年前

Roger Costello · 为什么在箭头表达式中使用的字段不同?

7 年前

johnf · 合金模型-如何在图形可视化中显示循环?

7 年前