function - 多くの要件を持つ合金機能

Question

sig Student, Tutor, Mark {} 
sig Course { 
    reg : set Student, 
    alloc : Student -> Tutor, 
    result : Student -> Mark 
   } 

コースcを入力として受講できるようにしたいと思います。まだマークを持っていないcに登録された1人以上の学生を担当するチューターのセットを出力します。

誰か助けてくれませんか？

Answer 1

今回は、Alloyで集合内包表記を書く方法について質問しているようです。次に、集合の内包的性質を使用して、特定のコースについて、そのコースに登録したすべての学生にマークが割り当てられていないように返す関数を作成できます。その後、alloc関係から直接、それらの学生に割り当てられたチューターを選択するのは簡単です。

Alloyの集合内包表記の構文は次のとおりです。

{x: expr | condition(x)}

そしてそれは「保持するようなセットに属するすべてを選択xexprcondition(x)する」という意味です。

これがあなたの問題のためにこれを書く方法です：

sig Student, Tutor, Mark {}

sig Course {
  reg: set Student, 
  alloc: Student -> Tutor,
  result: Student -> Mark
}

fun studentsWithNoMarks[c: Course]: set Student {
  {s: c.reg | no c.result[s]}
}

fun tutorsForStudentsWithNoMarks[c: Course]: set Tutor {
  c.alloc[studentsWithNoMarks[c]]
}