1

私は、いずれかの学生にマークが入力されると、その学生は常にそのコースのマークを持っているというアサーションステートメントを書き込もうとしています（マークが変更される可能性はありますが）。生徒がマークを持っているかどうかを確認する方法はすでに知っていますが、そもそも生徒がマークを持っていない場合の確認方法がわかりません。また、このassertステートメントのチェックステートメントを作成するにはどうすればよいですか？

sig Student, Tutor, Mark {} 

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

これは私が試したものです

assert chekmark
  {all c:Course | let c' = CO/next[c] |
     some Student.(c.Result) => some Student.(c.Result)}

check checkmark for 3

しかし、どういうわけかそれは言います：この式はタイプチェックされませんでした。私は正しいか間違っていますか、そして私が正しい場合はどうすれば修正できますか？

4

1 に答える 1

1

問題は、コースでの注文が問題の解決策にならないことです。順序付けモジュールを使用すると、すべてのコースに合計順序が付けられるだけです (つまり、CO/next[c] はその順序で c の直後のコースを返すだけです)。ただし、(Course, Student) ペアごとに一連のマークが必要になる場合があります。 .

たぶん、このようなもの

sig Student, Tutor, Mark {}

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

sig Grade {
  student: one Student,
  marks: seq Mark
}

Alloy シーケンスを使用すると、必要なプロパティが自動的に得られます。つまり、marksフィールドが空でない場合は、マークのシーケンスが含まれるため、途中でヌルになることはありません。

このモデルでは、コースごとに学生ごとに最大 1 つの成績を強制するファクトを追加することができます。

fact oneGradePerStudentPerCourse {
  all c: Course {
    all s: c.reg |   
      lone {g: c.result | g.student = s}
  }
}
于 2013-03-11T14:29:27.050 に答える