TLA modeling tips

cs functional