0

私は、人々のグループを説明する次の Alloy モデルを持っています。問題を単純化します。これがサンプルコードスニップです。

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

sig people {
teamleader: Bool,
position: String
}

これで、グループに 2 人が参加しました。次に、グループ内の人々にいくつかの制限を追加したいと思います。たとえば、グループ内の 2 人には、常に 1 人のチーム リーダーと 1 人のチーム メンバーが必要です。これを行うには、次の事実を使用します。

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

今、私は前進を妨げる問題に遭遇しました。私が探している望ましいモデルは、グループの国が「US」の場合、チームリーダーの役職は「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量指定子の 2 つの意味の間です。タスクの説明に基づいて、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 に答える