0

我有以下描述一群人的合金模型。简化问题。这是一个示例代码片段。

sig groupofpeople {
member: set person,
country: Country
}{
 #person=2
} 

sig people {
teamleader: Bool,
position: String
}

所以现在我们在一个组中有两个人。接下来我想对组中的人添加一些限制。例如，我希望一个小组中的两个人始终有一个团队负责人和一个团队成员。我使用以下事实来做到这一点：

fact {
all n: people , m: people - n {
        n.teamleader not in m.teamleader
    }
}

现在我遇到了一个阻碍我前进的问题。我正在寻找的理想模型是，如果一个小组的国家是“美国”，那么团队负责人的职位是“US_TL”，团队成员的职位是“US_TM”。如果国家是“UK”，那么队长的位置是“UK_TL”，团队成员的位置是“UK_TM”，以此类推。

我试图添加类似的东西：

all n: groupofpeople {
        (n.country in US => (
        n.member.position="US_TL" or 
        n.member.position= "US_TM"))  or
        (n.country in UK => (
        n.member.position ="UK_TL" or 
        n.member.position = "UK_TM"))
    }

但是预测显然有问题，模型无法为我生成正确的解决方案。您能帮我找出模型中的问题吗？

4

2 回答 2

2

您在此处发布的模型无法编译，因此我无法真正确定问题所在（因为有很多，所以其中可能只是拼写错误）。or最后一个量词中的两个含义之间似乎不正确的是all：根据您对任务的描述，它应该是and。

如果我了解您的模型所需的属性，这就是我将如何重写它（如果这不是您想要实现的目标，请澄清您的问题并发布一个语法正确的模型）：

open util/boolean

abstract sig Country {}
one sig US extends Country {}
one sig UK extends Country {}

sig GroupOfPeople {
  member: set Person,
  country: one Country
}{
  #member=2
} 

sig Person {
  teamleader: Bool,
  position: String
}

fact {
  all g: GroupOfPeople {
    all n: g.member, m: g.member - n {
      n.teamleader not in m.teamleader
    }
  }
}

run {
  all n: GroupOfPeople {
    (n.country in US => (
        n.member.position="US_TL" or 
        n.member.position= "US_TM"))
    (n.country in UK => (
        n.member.position ="UK_TL" or 
        n.member.position = "UK_TM"))
    }
} for 5
于 2013-10-11T22:34:17.457 回答
1

将上面 sig Person 的定义替换为

abstract sig Person{position : String}
sig Leader, Follower extends Person

fact one_leader {
  all g : GroupOfPeople | one (g.member & Leader)
}

甚至更好地将这个事实放在 GroupOfPeople 的不变量中：

one (member & Leader)
于 2013-10-12T16:20:49.810 回答