I wonder if exclusive and disjoint would be more ergonomic if expressible on view atoms instead of views, e.g.
view exclusive holdLock(); // autogenerates 'constraint holdLock() * holdLock() -> false;'
view disjoint thread(int id); // autogenerates 'constraint thread(id_0) * thread(id_1) -> id_0 != id_1;'
This wouldn't work well with exclusive/disjoint constraints over different view atoms, though, unless it was a shorthand (and I'm torn as to whether Starling should have lots of syntactic sugar, or little syntactic sugar).
I wonder if
exclusiveanddisjointwould be more ergonomic if expressible on view atoms instead of views, e.g.This wouldn't work well with exclusive/disjoint constraints over different view atoms, though, unless it was a shorthand (and I'm torn as to whether Starling should have lots of syntactic sugar, or little syntactic sugar).