Как добавить ограничения на поля подписи, когда в модели два экземпляра

У меня есть следующая модель Alloy, которая описывает группу людей. упростить задачу. Вот пример фрагмента кода.

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_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"))
    }

Но с прогнозом явно что-то не так, и модель не может генерировать для меня правильные решения. Не могли бы вы помочь мне определить проблему в моей модели?


alloy
person user2744486    schedule 11.10.2013    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Модель, которую вы разместили здесь, не компилируется, поэтому я не могу точно определить проблему (поскольку их много, и это могут быть просто опечатки). Что кажется неверным, так это 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
person Aleksandar Milicevic    schedule 11.10.2013

arrow_upward
1
arrow_downward

Не лучше ли было бы заменить вышеприведенное определение 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)
person user1513683    schedule 12.10.2013