How to reduce temporal update boilerplate for state-rich models?

A few years ago I made an attempt to support a Pluscal like language in Alloy. One of the features was that it traversed all the logical paths and automatically ensured the non-used variables were kept constant if not mentioned in a branch.

PlusCal in Alloy

It never generated a lot of interest so I stopped pursuing it. I made a deplorable joke that seemed to have upset some sensitive souls and that dominated the discussion :slight_smile: but reviving the part that keeps unused variables constant might be an idea.

I agree that doing it manually is very error prone and tedious.

1 Like