Temporal model: add an instance to a set of instances inside a field

Questions
1

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?

2

oh, and to clarify: the reason I want to start with all empty courses is because the particular thing I’m modeling this in aid of specifies behavior that happens when a student joins a course… but I’m not there yet! :sweat_smile:

3

ah ha! I think I’ve figured it out. roster has to be var, like this:

sig Course { var roster : set Student }
4

Yes, that was the issue. Maybe it would be nice if the Analyzer raised a warning if the prime is used on a non-variable expression. That would help finding the problem.

1 Like