Hi
I won’t comment on the correctness as I don’t know the algorithm and I don’t really have time to delve into the model. But, overall, it seems absolutely fine (I’m just surprised by the last fact which contains eventually INode.color = Green: is it normal that you impose an outcome rather than verifying it?).
Then, if I were you, I would just perform a few improvements (in this order):
- Introduce an
unchanged(let unchanged[r] { (r) = (r)' }) macro and use it to show more explicitly unchanging relations. - Instead of using existential quantifications in events, I’d rather move the quantified variables to pred parameters.
- Then I would apply the event reification idiom for a nice visualization. Having done the previous step, you will be able to see clearly the value given to the quantified variables that were moved to parameters.