Transitive closure with quantifiers in Alloy

Question

For the setup, I have a set of theorems, each with a set of values as a premise, a label, and a value it proves.

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

I also have the following constraints:

Labels and premises are fixed for each theorem. One theorem always belongs to label 1 and always has A /\ B as a premise, theorems C => ? and D => ? both always belong to label 2, etc. There may be distinct theorems with the same premise belonging to different labels. For example, it's possible that I could have 4. C => A, even thought we already have 2. C => D.
All premises are of the form A /\ B /\ ... /\ N. I will never have A /\ (B \/ C) as a premise, nor will I have ~A. But I could have two theorems that share a label, one with A /\ B as a premise and one with A /\ C.
The values each theorem proves is variable, and in fact is the only thing that varies. Each theorem may prove at most one value.
All theorems with the same label must prove the same value. If 2. C => (does not prove anything), then I must also have 2. A =>. At most one label can prove a given value. This means it makes sense to write this example as 1. C 2. D 3. V ...
A value is "free" if no theorem proves it. V is never free.
A value is "provable" if it is A) free, B) belongs to a theorem where the premise is satisfiable with provable values.

A model is valid if V is provable. In this case it is, since A and B are free, which gets us C, which gets us V. However, 1. A 2. C 3. V is invalid. What I'm trying to do is figure out which additional facts are required to make all possible models valid. For example, that counterexample disappears if we add a fact that says "A proved value can't be its own premise.

Here's an alloy model representing this:

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

The problem I have is in the solvable predicate. I need it to obey the conjunctions and work for an arbitrary depth. One possible solution would be to use the transitive closure. But if I do v in free or v in free.*(Theorem.(premise.proves)), the model becomes too permissive. It would say that if C is free, then A /\ C -> A is provable. This is because Alloy does not permit sets inside sets, so it collapses {A C} -> A into A -> C and A -> A.

On the other hand, I could write it as

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']

But this is very slow and also has a maximum recursion depth of 3. Is there a way to get the speed and arbitrary depth of using a closure with the accuracy of using a quantifier? I suppose I could add a trace, where each step successively proves more values, but it seems odd to enforce an ordering on a system that doesn't need it.

Hovercouch Hovercouch · Accepted Answer · 2018-01-13T03:40:44

After a lot of experimentation, I've decided that the only good way to do this is with a trace. Here's the final spec if anybody's interested: open util/ordering[Step]

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

Transitive closure with quantifiers in Alloy

1 Answers