이유 술어에 인스턴스가 없습니다. (Alloy)

Question

저는 Alloy에 익숙하지 않습니다.이 술어를 작동 시키려고 노력하고 있지만 어디에 문제가 있는지 알 수 없습니다. 사용자는 당선에 참여할 때 당에 가입하거나 만들 때 총재가 선거 및 입후보 기간을 알리는 사람이며 사용자는 한 사람에게 투표하고 그 사람의 후보자에 대해 세 가지 기본 설정을 지정할 수 있습니다. 왜 그것이 인스턴스를 찾을 수 없는지 나는 모른다. 나 좀 도와 줄 수있어?

module Politics 

abstract sig Document{ } 
abstract sig Photo{ } 


sig Party{ 
id:one Int, 
name:one String, 
program:one Document, 
symbol :one Photo, 
CreateDate: one Int 
}{CreateDate>Election.startCandidacy 
CreateDate<Election.EndCandidacy} 

sig User{ 
id: one Int, 
name: one String, 
surname: one String, 
email: one String, 
password: one String, 
dateBirth: one Int, 
vote: lone Vote 
} 

sig Governor extends User{ 
election:one Election, 
}{vote != none} 

abstract sig Candidate extends User{ 
cv: one Document, 
motLetter: one Document, 
party: one Party, 
dateCand : one Int 
}{cv !=motLetter 
vote != none 
dateCand > Election.startCandidacy 
dateCand < Election.EndCandidacy} 


one sig Election{ 
startCandidacy:one Int, 
EndCandidacy:one Int, 
dateElection: one Int 
}{startCandidacy < EndCandidacy 
dateElection>EndCandidacy} 

sig Vote{ 
dateVote: one Int, 
preference1: one Candidate, 
preference2: lone Candidate, 
preference3: lone Candidate 
}{preference1 != preference2 
preference1 != preference3 
preference2 != preference3 
dateVote = Election.dateElection} 

// Facts 
// Every user has a unique ID and username 
fact noTwoUsersWithSameID{ 
no disj u1, u2 : User | u1.id = u2.id || u1.email = u2.email 
} 

// Every party is unique, with unique name, program and symbol 
fact noTwoSameParties{ 
no disj p1, p2 : Party | p1.name = p2.name || p1.program = p2.program || p1.symbol  = p2.symbol 
} 

// Every candidate has a unique cv and motivation letter 
fact noTwoSameCandidates{ 
no disj c1, c2 : Candidate | c1.cv = c2.cv || c1.motLetter = c2.motLetter 
} 


// All preferences in the vote are on the same party 
fact AllPreferencesSameParty{ 
all v: Vote | v.preference1.party = v.preference2.party and v.preference1.party = v.preference3.party 
} 


fact noSameVotes{ 
no disj u1, u2:User | u1.vote = u2.vote 
all v:Vote | one u:User | u.vote = v 
} 


assert NoSameUsers{ 
no disj u1, u2 : User | u1.id = u2.id || u1.email = u2.email 
} 


check NoSameUsers for 4 

pred show() 
{ 
#Election > 1 
//#Party > 3 
#Candidate > 8 
#User > 10 
} 


run show for 12 

Answer 1

올바른 길을 가고 있습니다.

이 예제에서는 이미 인스턴스가없는 이유를 파악하는 간단한 방법을 시도해 보았습니다. 즉 제약 조건을 완화하여 모델을 인스턴스화하지 못하게하는 제약 조건을 확인합니다. 특히 show 술어의 일부를 주석 처리했습니다.

당신이 조금 더 많은 일을 할 경우, 당신은 당신이 show의 모든 제약 조건을 주석, 그래서 공허하게되면, 합금 인스턴스를 찾을 수 있음을 확인할 수 있습니다. 제약 조건을 하나씩 가져 오면 #Election > 1이 주석 처리 된 경우에만 show이 만족스러운 것으로 나타납니다.

이것은 선거 선언에주의를 기울여야합니다. 양식은 one sig Election { ... }입니다. show의 인스턴스가없는 이유를 지금 보셨습니까? 하나의 선거가 존재한다는 제약과 정확히 하나의 선거가 있다는 제약을 동시에 만족시킬 수있는 사례는 없다.

일반적으로 정수에 의존하지 않고 이벤트를 시퀀싱하는 데 익숙하지 않은 사용자라면 Alloy를 사용하면 더 행복해집니다. 합금 원자는 때로는 객체 신원이라고 불리는 것을 가지므로, 부기 관리를 위해 고유 한 식별자를 가질 필요가 없습니다.