Modélisation d'un graphe complètement connecté en Alliage

Question

J'essaie de mouiller mes pieds avec Alloy (aussi relativement nouveau à la logique formelle), et j'essaie de commencer avec un graphe de nœuds complètement connecté.

sig Node { 
    adj : set Node 
} 

fact { 
    adj = ~adj -- symmetrical 
    no iden & adj  -- no loops 
    all n : Node | Node in n.*adj -- connected 
} 

pred ex { } 
run ex for exactly 3 Node 

Comme vous pouvez le voir sur l'image, les nœuds 0 et 1 ne sont pas connectés. Je pensais que mon fait était suffisant pour le rendre complètement connecté ... mais peut-être que j'ai raté quelque chose.

Answer 1

Que diriez-vous

adj = Node -> Node - iden 

Cela dit essentiellement que adj contient toutes les paires possibles de noeuds, à l'exception des identités (auto-boucles).

La raison pour laquelle il est correct que Node1 et Node2 ne sont pas connectés à votre modèle est la dernière clause de votre fait qui limite que pour chaque noeud, tous les nœuds sont transitive accessibles, mais il me semble que vous les voulez être immédiatement joignable. Comme alternative à ma solution ci-dessus, vous pouvez modifier

all n: Node | Node in n.*adj à all n: Node | (Node - n) in n.adj

pour obtenir le même effet.