43 Student Enrolment Courses Example

This example keeps the model deliberately small. The main design choices are:

• Enrolment is the source of truth for which student is taking which course.
• Student.enrolled is derived from the student's enrolments.
• Course.prerequisite is the source of truth for course ordering.
• There is no separate dependent attribute, so the model cannot drift into two inconsistent views of the same prerequisite relationship.

enum Day
{
    monday,
    tuesday,
    wednesday,
    thursday,
    friday,
    saturday,
    sunday
}

value TimeSlot
{
    Day day;
    Integer startMinute;
    Integer endMinute;
}

func Boolean overlaps(TimeSlot a, TimeSlot b) =
    a.day = b.day
    ∧ a.startMinute < b.endMinute
    ∧ b.startMinute < a.endMinute;

entity Course
{
    String code;
    Boolean advanced;
    TimeSlot timeslot;

    Course prerequisite*;

    // Navigation back to enrolments is derived from Enrolment.course.
    Enrolment enrolment* where enrolment.course = this;

    key { code };
}

entity Student
{
    String name;
    Course completed*;

    // Navigation to enrolments is derived from Enrolment.student.
    Enrolment enrolment* where enrolment.student = this;

    // A student's current courses come from the enrolment records.
    → Course enrolled* = enrolment.course;

    key { name };

    constraints
    {
        // A course cannot be both completed and currently enrolled.
        [completed = enrolled].Σempty;

        // If an enrolled course is advanced, all its prerequisites
        // must already be completed by this student.
        let s=this in
            enrolled.(advanced → prerequisite.Σ ⊆ s.completed.Σ);

        // No two currently enrolled courses may overlap in time.
        let s=this in
            enrolled.(let c=this in
                s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall);

        // Do not enrol in a prerequisite after completing a course
        // that already depends on it.
        let s=this in
            enrolled.(let c=this in
                s.completed.[c ∈ prerequisite.Σ].Σempty);
    }
}

entity Enrolment
{
    Student student;
    Course course;
}

entity University
{
    Student student*;
    Course course*;
}

Reading the constraints

The first constraint uses an intensional filter as a relation. It says there is no course value that is both in completed and in enrolled.

[completed = enrolled].Σempty

The second constraint keeps the current student in s before entering enrolled.(...). Inside that path tail, this is the enrolled course, so prerequisite.Σ is the set of prerequisites of that course, while s.completed.Σ is the set of courses completed by the original student.

let s=this in
    enrolled.(advanced → prerequisite.Σ ⊆ s.completed.Σ)

The third constraint compares each enrolled course c with the other enrolled courses for the same student. The filter .[this ≠ c] removes the course from its own comparison set.

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

The final constraint checks the opposite direction of the prerequisite relationship without storing a separate dependent attribute. For each currently enrolled course c, it rejects any completed course whose prerequisite set contains c.

let s=this in
    enrolled.(let c=this in
        s.completed.[c ∈ prerequisite.Σ].Σempty)

The student constraints above translate to the following logic:

// A course cannot be both completed and currently enrolled.
∀C:Course
    this.completed(C) → ¬this.enrolled(C)

// Advanced enrolled courses require completed prerequisites.
∀A:Boolean ∀E:Course ∀P:Course
    (this.enrolled(E) ∧ E.advanced(A) ∧ A ∧ E.prerequisite(P))
  → this.completed(P)

// Currently enrolled courses must not overlap.
∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

// Do not enrol in a prerequisite after completing a dependent course.
∀C:Course ∀E:Course
    (this.completed(C) ∧ this.enrolled(E))
  → ¬(E ∈ { P:Course | C.prerequisite(P) })

Common wrong turns

The following examples are deliberately concrete. Each one shows a tempting expression, what it actually denotes, and the form that matches the intended constraint.

1. Comparing scalar paths as if they were sets

A common first attempt is to write the prerequisite rule without folds:

enrolled.(advanced → prerequisite ⊆ completed)

This has no logic denotation, because it is not well typed. Inside enrolled.(...), both prerequisite and completed denote individual Course values in the current path context. The operator ⊆ expects sets, so the type checker rejects the expression:

ERROR: No overload of ⊆ matches operand types ['Course', 'Course']

The correct expression explicitly folds both sides to sets. It also saves the original student in s, because inside enrolled.(...) the receiver this is the enrolled course.

let s=this in
    enrolled.(advanced → prerequisite.Σ ⊆ s.completed.Σ)

∀A:Boolean ∀E:Course ∀P:Course
    (this.enrolled(E) ∧ E.advanced(A) ∧ A ∧ E.prerequisite(P))
  → this.completed(P)

Principle: use .Σ when the constraint is about a set of values. Use let before a path composition when the inner expression still needs the outer receiver.

2. Forgetting that this changes inside a path tail

This schedule rule looks plausible, but it accidentally compares each enrolled course only with itself:

enrolled.(let c=this in
    enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

Its denotation exposes the problem. The antecedent contains E ≠ E, which is impossible:

∀T:TimeSlot ∀T1:TimeSlot ∀E:Course
    (this.enrolled(E) ∧ E ≠ E ∧ E.timeslot(T) ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

The issue is that the unqualified inner enrolled is evaluated relative to the current enrolled course, not relative to the student. Save the student first, then navigate back through s.enrolled.

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

Principle: after x.(...), unqualified paths in the parentheses are evaluated from each value of x. Use let outer=this in ... when a nested path still needs the outer object.

3. Using value inequality when the domain has a richer predicate

If TimeSlot is an interval, this rule is too weak:

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].timeslot ≠ c.timeslot)

It only says the two enrolled courses cannot have exactly equal TimeSlot values:

∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → T ≠ T1

For interval times, equality is not the important domain concept. Use the domain predicate:

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

Principle: write constraints in the vocabulary of the domain. If the domain concept is overlap, encode overlap directly instead of relying on value inequality.

4. Misusing universal navigation for a universal condition

This example refers to a variant of the model that stores a reverse navigation Course dependent*. The tempting expression is:

course.(dependent ⇒ advanced)

It does not mean "all dependent courses are advanced". Universal navigation returns values that all dependents agree on. Used as a Boolean constraint, it says that if every dependent agrees on some advanced value A, then A must be true:

∀A:Boolean ∀C:Course
    (this.course(C) ∧ (∀D:Course (C.dependent(D) → D.advanced(A))))
  → A

The direct constraint is to look for counterexamples: dependent courses that are not advanced. Then require that set to be empty.

course.dependent.[¬advanced].Σempty

∀D:Course ∀C:Course ∀A:Boolean
    (this.course(C) ∧ C.dependent(D) ∧ D.advanced(A))
  → A

Principle: to say "all X satisfy P", filter X by the negation of P and require .Σempty. This is often clearer than reaching for ⇒.

5. Traversing the relationship in the wrong direction

Again suppose the model stores dependent. This expression is easy to write backwards:

student.completed.dependent ≠ course

Its denotation says that the enrolment course must not be a dependent of any completed course:

∀D:Course ∀C1:Course ∀C:Course ∀S:Student
    (this.student(S) ∧ S.completed(C) ∧ C.dependent(D) ∧ this.course(C1))
  → D ≠ C1

That is the reverse of "do not enrol in a prerequisite after completing a course that depends on it". With a stored dependent navigation, the direction should be:

course.dependent ≠ student.completed

∀D:Course ∀C1:Course ∀C:Course ∀S:Student
    (this.course(C) ∧ C.dependent(D) ∧ this.student(S) ∧ S.completed(C1))
  → D ≠ C1

The revised model avoids storing dependent at all. It asks whether the currently enrolled course c appears in the prerequisite set of any completed course:

let s=this in
    enrolled.(let c=this in
        s.completed.[c ∈ prerequisite.Σ].Σempty)

∀C:Course ∀E:Course
    (this.completed(C) ∧ this.enrolled(E))
  → ¬(E ∈ { P:Course | C.prerequisite(P) })

Principle: read a path left to right and name the relationship direction. If the prose says "completed courses that depend on the enrolled course", either navigate from the enrolled course to its dependents, or test whether the enrolled course appears in a completed course's prerequisite set.

Constraint-writing principles

• Decide which entity should own the constraint. If a rule is naturally about one student's courses, put it on Student.
• Keep one source of truth for each relationship. Prefer deriving reverse navigation instead of storing both directions independently.
• Use .Σ when comparing sets of path values; otherwise a path usually denotes individual values.
• Use let to preserve an outer receiver before entering a path composition that changes this.
• For universal requirements, look for bad cases and require .Σempty.
• Use domain predicates such as overlaps when equality or inequality does not capture the real business rule.