Início / user-15446749

ZarakshR's questions

Martin Hope
ZarakshR
Asked: 2025-04-08 13:38:27 +0800 CST
  • 5

Estou tentando resolver o problema do aperto de mão de Halmos (Seção 2.3) usando Alloy 4 (sou obrigado a usar Alloy 4 no meu curso universitário; no entanto, esta folha de problemas não faz parte do meu trabalho de curso, estou tentando resolvê-la como prática).

Este é o modelo que eu criei:

module halmos

abstract sig Person { shook : set Person }
sig Man extends Person { wife : one Woman }
sig Woman extends Person { husband : one Man }
one sig Me in Man { }
one sig MyWife in Woman { }

fact {
    Me.wife = MyWife
    MyWife.husband = Me
}

// hand-shaking is symmetric
fact { all p : Person | p.shook = shook.p }

// "No one shook his or her own hand"
fact { all p : Person | p not in p.shook }

// "no husband shook his wife’s hand"
// this and symmetricity of shook implies no wife shook her husband's hand
fact { all m : Man | m.wife not in m.shook }

fact monogamy {
    all m : Man, w : Woman |
        // these parens are needed for correct precedence
        (m.wife = w implies w.husband = m)
        and
        (w.husband = m implies m.wife = w)
}

// all distinct persons (other than Me) shook a different number of hands
fact {
    all disj p1,p2 : Person - Me |
        #p1.shook != #p2.shook
}

O problema é que o Alloy não consegue encontrar uma instância para o caso com 10 Persons, embora eu saiba pela descrição do problema que deveria haver um modelo com 10 Persons que satisfaça minha especificação.

run { } for exactly 10 Personme dá:

Executing "Run run$1 for exactly 10 Person"
   Solver=glucose 4.1(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   5762 vars. 440 primary vars. 14101 clauses. 10ms.
   No instance found. Predicate may be inconsistent. 1094ms.

Curiosamente, run { } for exactly 8 Personme dá:

Executing "Run run$1 for exactly 8 Person"
   Solver=glucose 4.1(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   3645 vars. 288 primary vars. 8394 clauses. 6ms.
   Instance found. Predicate is consistent. 17ms.

e uma saída como esta, que parece corresponder à descrição de Halmos (nenhuma das duas pessoas -- exceto Mee -- MyWifetem o mesmo número de apertos de mão):

da mesma forma, run { } for exactly 4 Personme dá, como esperado:

Executing "Run run$1 for exactly 4 Person"
   Solver=glucose 4.1(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   980 vars. 80 primary vars. 1931 clauses. 2ms.
   Instance found. Predicate is consistent. 1ms.

e run { } for exactly 5 Personnão consegue encontrar uma instância (já que precisamos de um número par de pessoas para combiná-las como casais), como esperado.

Por que, então, o Alloy não consegue encontrar uma instância para 10 Persons? Estou usando o Alloy errado ou minha especificação está incorreta de alguma forma?

Obrigado,

alloy