CODEWITHSUNDEEP
assertalloy
user2154506
user2154506

Reputation: 15

Alloy assert check

I'm trying to write an assert statement to the effect that once a mark is entered for any student then the student always has a mark for that course (although it's possible the mark may change). I already know how to check if the student has the mark or not, but i don't know how to do it in case the student doesn't have any mark to begin with. Also, how can i write a check statement for this assert statement?

sig Student, Tutor, Mark {} 

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

This is what i tried

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

check checkmark for 3

But somehow it says: This expression failed to be typechecked. Am i right or wrong,and how can i fix it if i'm right?

Upvotes: 1

Views: 1638

Answers (1)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3857

The problem is that the ordering on Courses is not going to be a solution for your problem. Using the ordering module simply places a total order on all courses (so CO/next[c] just returns the course immediately following c in that order), whereas you probably want to have a sequence of marks for each (Course, Student) pair.

Maybe something like this

sig Student, Tutor, Mark {}

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

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

Using Alloy sequences automatically gives you the property you want, that is, if the marks field is non-empty, then it is going to contain a sequence of Marks so no nulls in the middle are possible.

With this model, you might want to add a fact that enforces at most one grade per student per course.

fact oneGradePerStudentPerCourse {
  all c: Course {
    all s: c.reg |   
      lone {g: c.result | g.student = s}
  }
}

Upvotes: 1

Related Questions