1

我正在尝试编写一个断言语句，大意是一旦为任何学生输入了一个分数，那么该学生总是对该课程有一个分数（尽管分数可能会改变）。我已经知道如何检查学生是否有分数，但是如果学生没有任何分数，我不知道该怎么做。另外，我怎样才能为这个断言语句写一个检查语句？

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

问题是 Courses 的排序并不能解决您的问题。使用 ordering 模块只需对所有课程进行总排序（因此 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字段是非空的，那么它将包含一系列标记，因此中间不可能出现空值。

使用此模型，您可能希望添加一个事实，即每门课程每个学生最多执行一个等级。

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