Alloy Function with many requirement

Question

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

I want to be able to takes course c as input; outputs the set of tutors who are responsible for one or more students registered for c who do not yet have a mark.

Can anyone help me please?

Answer 1

This time it seems your are asking about how to write set comprehensions in Alloy. You can then use a set comprehension to write a function that for a given course returns all students who registered for that course such that they don't have a mark assigned. After that it is easy to select tutors assigned to those students, directly from the alloc relation.

Syntax for set comprehensions in Alloy is the following

{x: expr | condition(x)}

and it means "select all x that belong to set expr such that condition(x) holds".

Here is how to write this for your problem:

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]]
}