I’m trying to model an interaction in the product I’m working on. To start off, I’m modeling a world where students can join courses. I’m trying to do this with the new temporal features of Alloy 6, but having some difficulty. Here’s my model. I ran this through the minisat with unsat core solver, and marked the formulas it found with `// unsat`

.

```
sig Student {}
sig Course { roster: set Student }
pred init {
some Course
some Student // unsat
no roster // unsat
}
pred stutter {
roster' = roster
}
pred join [s: Student, c: Course] {
// guard: doesn't make sense for the same student to join over and over
s not in c.roster
c.roster' = c.roster + s
}
fact traces {
init
always {
stutter or
(one s: Student, c: Course | join[s, c])
}
}
run traces {
eventually { all s : Student | some c: Course | s in c.roster } // unsat
} for 3
```

I have the intuition that maybe this is not working because I am saying “you have some students, some courses, and eventually all those students will be in at least one course… but you have the option to stutter forever.” I do not know how to express this otherwise, though! Is that intuition correct? How can I fix my mental model to see a consistent predicate whose instances I can explore?