1277.190 TLA+를 이용한 형식 명세