Constructing a relation in Alloy

Question

In the dining philosophers problem we have a table with Philosophers and Forks.

sig P {}
sig F {}

For this problem I want the following relation that represents the table:

P1 -> F1
F1 -> P2
P2 -> F2
F2 -> P3
P3 -> F3
F3 -> P1

I.e. each P would point to an F and each F to a P, and this would form a circle. I would like to call a function to get this relation:

fun table : (P+F) one -> one (P+F) { ... }         

I've been trying hard to make this work but it feels like I am missing something fundamental that also is relevant for other problems I am having. Somehow I miss a 'constructor'.

Any pointers?

Additional

@Hovercouch gave an working solution with a helper sig. However, this required a non-natural extension to the P and F and introduced a new sig. This can also be solved by:

sig P, F {}
one sig Table {
    setting : (P+F) one -> one (P+F)
} {
    # P = # F
    all p : P, f : F | P in p.^setting and F in f.^setting
}
run {} for 6

Which addresses the non-natural inheritance concerns.

However, it still seems very global and a lot of work for an imho very simple problem. Still keeping the question open to see if there are other solutions.

Answer 1

If you're willing to add a helper object, we can do this by making an abstract sig Thing and then making both P and F instances of Thing:

abstract sig Thing {
    next: Thing
} {
    Thing = this.^@next
}

sig F extends Thing {} {
    next in P
}

sig P extends Thing {} {
    next in F
}

fact SameNumberOfThings {
    #P = #F
}

run {} for 6

Answer 2

There may be a design tradeoff involved here, between expressive power and tractability.

There is certainly an issue of what counts as clean or intuitive; you say that the 'next'-ness of P and F is "an aspect of the table setting" and not "an aspect of P or F". I think I understand your thinking, but I don't think you are likely to have any more success defining a principled way to distinguish between "aspects" of P and F and relations in whose domain or range they appear, any more than any of the philosophers who have tried, over the last couple thousand years, to distinguish reliably between essence and accidence.

And if we accept that the distinction is unreliable, but we nevertheless find it useful, then the question becomes "who made the rule that a relation defined as part of a signature must relate to an (intrinsic) aspect of the individuals involved, and not to an extrinsic relation which is not an aspect of the individuals?" The answer is: you did, not [the creators of] Alloy. If one insists too strongly on one's intuitions about the constructs one wants to use to express something, there is a certain risk of insisting not just that the thing should be expressible but that we should be able to express it using a particular construct. That kind of insistence can teach us a lot about a notation, but sometimes it's easier to accept that the designers of the notation also had intuitions.

This general topic is discussed in Daniel Jackson's Software Abstractions under the questions Does Alloy allow freestanding declarations? (in discussion following section 3.5.3 on higher-order quantification) and Must all relations be declared as fields? (in discussion following section 4.2.2 on basic field declarations). The nut of the discussion is "If you want to declare some relations that don't belong naturally to any existing signatures, you can simply declare them as fields of a singleton signature." Mutatis mutandis, the example given looks a lot the Table sig in your addendum.

TL;DR yes, you may find it a bit cumbersome, but the singleton sig to contain a relation you don't want to define on its first member really is as close to an established idiom as there is, for this sort of thing.