How about this
fact { ^prv.Begin = Proc - Begin }
It's not super short, but at least it doesn't use a quantifier. I'm not sure if you can do any better than that.
In a graph terminology, it basically says: if you fully expand the prv
graph by following all the edges in it as many times as possible (i.e., take transitive closure of prv, ^prv
), then select source nodes of those edges that point to a Begin node (^prv.Begin
), that set must contain all nodes except the Begin nodes. With the fact you already have which says that Begin nodes have no prv, it implies that starting from any non Begin node and following only the prv
links, a Begin node will be reached, and the chain will end there. This fact disallows Action nodes to and such chains.
You can check this claim in Alloy by asserting
check {
// there is no non-Begin node that does not lead to a Begin node
no p: Proc-Begin | no (Begin & p.^prv)
} for 6
and checking that it doesn't find any counterexamples.