为什么没有找到谓词的实例？（合金）答案

【问题标题】：Why there is no instance found for the predicate? (Alloy)为什么没有找到谓词的实例？（合金）
【发布时间】：2014-05-17 23:47:37
【问题描述】：

我是 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

【问题讨论】：

标签： instance predicate alloy

【解决方案1】：

你在正确的轨道上。

您的示例表明您已经尝试了一种简单的方法来确定为什么没有找到实例：放松约束以查看导致模型无法实例化的约束。具体来说，您已经注释掉了show 谓词的一部分。

如果你再多做一点，你会发现如果你注释掉show 中的所有约束，让它变得空虚，Alloy 会找到实例。如果您将约束一一带回，您会发现show 是可满足的，当且仅当约束#Election > 1 被注释掉时。

这应将您的注意力引向选举声明，其形式为one sig Election { ... }。您现在明白为什么找不到show 的实例了吗？任何实例都不能同时满足选举不止一次的约束和选举只有一次的约束。

总的来说，如果您学会减少对整数的唯一性和事件排序的依赖，我认为您会更喜欢 Alloy。合金原子具有有时称为对象标识的东西，因此它们不需要具有唯一标识符来记账。

【讨论】：