Search code examples
graphalloyindependent-set

Creating an independent set from a graph in Alloy 4.2

I've created a test graph to try and create an independent set from. I know and independent set is a set of vertices that aren't connected, but I'm not sure how to accomplish this in alloy 4.2. Here's what I have:

abstract sig Vertex {
    e: set Vertex   -- e is the edge relation
}
-- the test graph has vertices A, B, C, D, E, F
one sig A, B, C, D, E, F extends Vertex { }
pred independentSet[e: Vertex->Vertex, s: set Vertex] {
    --code here?
}
pred show {
    -- setting up the edge relation
    (A->A + A->B + A->C + A->D) +
        (B->A + B->B + B->C + B->E) +
            (C->A + C->B + C->C + C->F) = e
}
run show for 6
Solution 
  • all i, j: s | not i -> j in e

    That's the answer I put, I think it's sort of correct and it gives an instance. I think it's missing a point but am not sure how to fully express it. I hope it gives you an idea!