1277.120 페트리 넷의 형식적 정의