Lightweight utilities to assist model writing and model-based testing activities using the TLA+ ecosystem