Alloy shorthand for range to always contain certain value

Question

I have done a little bit of work on Alloy so I understand a fair bit about it. A lot of the shorthand however is not really covered anywhere. What I was wondering was in the example below:

open util/relation

abstract sig Proc { prv : lone (Proc - Remove) 
}{
}

fact {acyclic[prv,Proc] // no cycles 
}
sig Remove extends Proc{}
sig Begin extends Proc{}{no prv}
sig Action extends Proc{}

pred show() {} 
run show for 3

I want to ensure that the final Proc is always going to be a Begin (at the moment it can be a Action too).

There are many ways to write it longhand. I have included one below, which when included ensures that the final Proc (ie one not in a domain) will always be a Begin.

fact {
all p : Proc  |   p not in dom[prv] implies p in Begin
}

However I like using the shorthand along the lines of (Proc - Remove), for example as makes things so much easier to read, which means that Remove cannot be linked to from another Proc. I hope I have explained that well. I assume there is going to be a really obvious answer but I can't think what it is. Any ideas please?

Answer 1

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.

Answer 2

It sounds as if you could achieve your goal by writing

sig Remove extends Proc{}{some prv}
sig Begin extends Proc{}{no prv}
sig Action extends Proc{}{some prv}

This ensures that no Begin has a prv node, and all non-Begin nodes do.