Alloy 中带有量词的传递闭包

Question

对于设置，我有一组定理，每个定理都有一组值作为前提、标签和它证明的值。

1. A /\ B => C
2. C => D
2. A => D // note same label as C => D
3. B /\ C => V
4. ...

我还有以下限制：

每个定理的标签和前提都是固定的。一个定理总是属于标签 1 并且总是以 A /\ B 作为前提，定理 C => ? 和 D => ? 总是属于标签 2，等等。可能有不同的定理具有相同的前提属于到不同的标签。例如，我可能有 4. C => A，即使我们已经有 2. C => D.
所有前提的形式都是A /\ B /\ ... /\ N。我永远不会以A /\ (B \/ C)为前提，也不会有~A。但是我可以有两个共享标签的定理，一个以 A /\ B 作为前提，一个以 A /\ C.
每个定理证明的值是可变的，事实上是唯一可变的。每个定理最多可以证明一个值。
所有具有相同标签的定理必须证明相同的值。如果2. C =>（不能证明什么），那么我一定也有2. A =>。最多一个标签可以证明一个给定的值。这意味着将此示例编写为 1. C 2. D 3. V ...
如果没有定理证明，则值为 "free"。 V 从来都不是免费的。
一个值是 "provable" 如果它是 A) 自由的，B) 属于一个定理，其中前提可以用可证明的值来满足。

如果 V 是可证明的，则模型是有效的。在这种情况下，因为 A 和 B 是免费的，所以我们得到 C，我们得到 V。但是，1. A 2. C 3. V 是无效的。我想做的是弄清楚需要哪些额外的事实才能使所有可能的模型都有效。例如，如果我们添加一个事实“证明值不能是它自己的前提。

，那么这个反例就会消失。

这是代表这个的 alloy 模型：

abstract sig Label { 
    proves: disj lone Value
}
one sig L1, L2, LV extends Label{}

abstract sig Value{}
one sig A, B, C, D, V extends Value {}

sig Theorem {
    premise: Value set -> Label
}

fun free: set Value {
    Value - Label.proves
}

pred solvable(v: Value) {
    v in free or // ???    
}

pred Valid {
  solvable[V]
}


pred DefaultTheorems {
    one disj T1, T2, T3, T4: Theorem | {
        #Theorem = 4
        T1.premise = (A + B) -> L1
        T2.premise = C -> L2
        T3.premise = A -> L2
        T4.premise = (B + C) -> LV  
    }
    LV.proves = V
}

check { DefaultTheorems => Valid } for 7

我遇到的问题是 solvable 谓词。我需要它服从连词并在任意深度工作。一种可能的解决方案是使用传递闭包。但如果我这样做 v in free or v in free.*(Theorem.(premise.proves))，模型就会变得过于宽容。它会说如果 C 是自由的，那么 A /\ C -> A 是可证明的。这是因为 Alloy 不允许集内集，所以它将 {A C} -> A 折叠为 A -> C 和 A -> A.

另一方面，我可以把它写成

pred solvable(v: Value) {
  v in free or some t: Theorem |
    let premise' = (t.premise).(proves.v) |
      some v' and all v': premise' | solvable[v']

但这非常慢，并且最大递归深度为 3。有没有办法获得使用闭包的速度和任意深度以及使用量词的准确性？我想我可以添加一个跟踪，其中每个步骤都连续证明更多的值，但是在不需要它的系统上强制执行排序似乎很奇怪。

Answer 1

经过大量试验，我认为唯一好的方法是使用跟踪。如果有人感兴趣，这是最终规范：打开util/ordering[步骤]

sig Step {}
    abstract sig Label { 
    proves: disj lone Value
}
one sig L1, L2, LV extends Label{}

abstract sig Value {
    proven_at: set Step
}
one sig A, B, C, D, V extends Value {}

sig Theorem {
    premise: Value set -> Label
}

fun free: set Value {
    Value - Label.proves
}

pred solvable(v: Value, s: Step) {
    v in proven_at.s or
    some t: Theorem |
        let premise' = (t.premise).(proves.v) |
            some premise' and all v': premise' |
                v' in proven_at.s
}

pred Valid {
    solvable[V, last]
}

fact Trace {
free = proven_at.first
all s: Step - last | 
    let s' = s.next |
    proven_at.s' = proven_at.s + {v: Value | solvable[v, s]}
}

pred DefaultTheorems {
    one disj T1, T2, T3, T4: Theorem | {
        #Theorem = 4
        T1.premise = (A + B) -> L1
        T2.premise = C -> L2
        T3.premise = A -> L2
        T4.premise = (B + C) -> LV  
    }
    LV.proves = V
}

check { DefaultTheorems => Valid } for 8 but 4 Step

Alloy 中带有量词的传递闭包

Transitive closure with quantifiers in Alloy

alloy