แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แ‹ญแˆ… แŒฝแˆ‘แ แ‰ตแˆญแŒ‰แˆ แŠแ‹แข แ‹จแˆตแ‰ณแŠ•แŽแˆญแ‹ต แˆดแˆšแŠ“แˆญ. แŒแŠ• แŠจแŠฅแˆท แ‰ตแŠ•แˆฝ แˆ˜แŒแ‰ขแ‹ซ แ‰ แŠแ‰ตแข แ‹žแˆแ‰ขแ‹Žแ‰ฝ แŠฅแŠ•แ‹ดแ‰ต แ‹ญแˆแŒ แˆซแˆ‰? แˆแˆ‰แˆ แˆฐแ‹ แŒ“แ‹ฐแŠ›แ‹แŠ• แ‹ˆแ‹ญแˆ แ‰ฃแˆแ‹ฐแˆจแ‰ฃแ‹แŠ• แ‹ˆแ‹ฐ แ‹ฐแˆจแŒƒแ‹ แˆˆแˆ˜แˆณแ‰ฅ แ‰ แˆšแˆแˆแŒแ‰ แ‰ต แˆแŠ”แ‰ณ แ‹แˆตแŒฅ แŒˆแ‰ฅแ‰ทแˆ, แŠแŒˆแˆญ แŒแŠ• แŠ แ‹ญแˆฐแˆซแˆ. แŠฅแŠ“ แŠจแŠฅแˆฑ แŒ‹แˆญ แŠฅแŠ•แ‹ฐ "แŠ แ‹ญแˆฐแˆซแˆ" แŠจแŠฅแˆญแˆตแ‹Ž แŒ‹แˆญ แ‰ แŒฃแˆ แ‰ฅแ‹™ แŠ แ‹ญแ‹ฐแˆˆแˆ: แ‰ แŠ แŠ•แ‹ฐแŠ›แ‹ แ‹จแˆ˜แˆˆแŠชแ‹ซ แŠญแแˆ แˆ‹แ‹ญ แˆ˜แ‹ฐแ‰ แŠ› แ‹ฐแˆ˜แ‹ˆแ‹, แ‰ฐแŒแ‰ฃแˆซแ‰ต แŠฅแŠ“ แˆŒแˆŽแ‰ฝแˆ, แŠฅแŠ“ แ‰ แˆŒแˆ‹แŠ›แ‹ แ‹ฐแŒแˆž แˆ›แˆฐแ‰ฅ แ‹ซแˆตแˆแˆแŒ‹แˆ. แˆ›แˆฐแ‰ฅ แ‹ฐแˆต แ‹จแˆ›แ‹ญแˆ แŠฅแŠ“ แˆ…แˆ˜แˆ แŠแ‹. แ‰ แแŒฅแŠแ‰ต แ‰ฐแˆตแ‹ แ‰†แˆญแŒฆ แŠ แŠฅแˆแˆฎแ‹แŠ• แˆณแ‹ซแ‰ แˆซ แŠฎแ‹ต แˆ˜แŒปแ‰แŠ• แ‰€แŒ แˆˆแข แ‹จแ‰ฐแˆ›แˆจแ‹แŠ• แŠ แ‰…แˆ˜ แ‰ขแˆตแŠแ‰ต แŠฅแŠ•แ‰…แ‹แ‰ต แˆˆแˆ›แˆธแŠแ แˆแŠ• แ‹ซแˆ…แˆ แŒฅแˆจแ‰ต แŠฅแŠ•แ‹ฐแˆšแ‹ซแˆตแˆแˆแŒ แ‰ณแˆตแ‰ฃแˆˆแˆ…แฃ แŠฅแŠ“ แ‹แˆ แ‰ฅแˆˆแˆ… แŠ แ‰ณแ‹ฐแˆญแŒˆแ‹แˆแข แ‹žแˆแ‰ขแ‹Žแ‰ฝ แ‹จแˆšแˆแŒ แˆฉแ‰ต แ‰ แ‹šแˆ… แˆ˜แŠ•แŒˆแ‹ต แŠแ‹, แˆŠแ‰ณแŠจแˆ แ‹จแˆšแ‰ฝแˆ แ‹ญแˆ˜แˆตแˆ‹แˆ, แŠแŒˆแˆญ แŒแŠ• แˆ›แŠ•แˆ แ‹จแˆšแ‹ซแ‹ฐแˆญแŒˆแ‹ แŠ แ‹ญแˆ˜แˆตแˆแˆ.

แ‹ซแŠ• แˆณแ‹จแ‹ แˆŒแˆตแˆŠ แˆ‹แˆแ–แˆญแ‰ต (แŠ แ‹Žแฃ แŠจแˆ˜แˆ›แˆชแ‹ซ แˆ˜แŒฝแˆƒแแ‰ต แ‹ซแ‹ แŒ“แ‹ฐแŠ›) แ‹ˆแ‹ฐ แˆฉแˆฒแ‹ซ แ‹ญแˆ˜แŒฃแˆ แŠฅแŠ“ แˆชแ–แˆญแ‰ต แŠ แˆแˆฐแˆซแˆ แฃ แŒแŠ• แ‹จแŒฅแ‹ซแ‰„ แŠฅแŠ“ แˆ˜แˆแˆต แŠญแแˆˆ แŒŠแ‹œ แฃ โ€‹โ€‹แ‰ตแŠ•แˆฝ แ‰ฐแŒ แŠแ‰€แ‰…แŠฉแข แˆแŠญ แŠฅแŠ•แ‹ฐ แˆแŠ”แ‰ณแ‹ โ€‹โ€‹โ€‹โ€‹แˆŒแˆตแˆŠ แ‰ แ‹“แˆˆแˆ แˆ‹แ‹ญ แ‰ณแ‹‹แ‰‚แ‹ แˆณแ‹ญแŠ•แ‰ฒแˆตแ‰ต แฃ แ‰ แ‰ฐแˆฐแˆซแŒจ แŠฎแˆแ’แ‹ฉแ‰ฒแŠ•แŒ แ‹แˆตแŒฅ แ‹จแˆ˜แˆ แˆจแ‰ณแ‹Š แˆฅแˆซแ‹Žแ‰ฝ แ‹ฐแˆซแˆฒ แŠแ‹ แฃ แŠฅแŠ“ แŠฅแˆฑแŠ• แ‰  LaTeX - โ€œLamport TeXโ€ แ‰ แˆšแˆˆแ‹ แ‰ƒแˆ แ‰  แˆ‹ แŠแ‹ฐแˆŽแ‰ฝ แˆแ‰ณแ‹แ‰€แ‹ แ‰ตแ‰ฝแˆ‹แˆˆแˆ…แข แˆแˆˆแ‰ฐแŠ›แ‹ แŠ แˆณแˆณแ‰ขแ‹ แŠแŒˆแˆญ แ‹จแˆฑ แˆ˜แˆตแˆแˆญแ‰ต แŠแ‹แก แ‹จแˆšแˆ˜แŒฃ แˆแˆ‰ (แแแˆ แŠจแŠญแแ‹ซ แŠแƒ) แˆแˆˆแ‰ต แˆชแ–แˆญแ‰ถแ‰นแŠ• แŠ แˆตแ‰€แ‹ตแˆž แˆ›แ‹ณแˆ˜แŒฅ แŠ แˆˆแ‰ แ‰ตแฃ แ‰ขแ‹ซแŠ•แˆต แŠ แŠ•แ‹ต แŒฅแ‹ซแ‰„ แ‰ แŠฅแŠแˆฑ แˆ‹แ‹ญ แ‹ญแˆแŒฃ แŠฅแŠ“ แŠจแ‹šแ‹ซ แ‰ฅแ‰ป แˆ˜แˆแŒฃแ‰ต แŠ แˆˆแ‰ แ‰ตแข แˆ‹แˆแ–แˆญแ‰ต แŠฅแ‹šแ‹ซ แ‹จแˆšแ‹ซแˆตแ‰ฐแˆ‹แˆแˆแ‹แŠ• แˆˆแˆ›แ‹จแ‰ต แ‹ˆแˆฐแŠ•แŠฉ - แŠฅแŠ“ แ‰ แŒฃแˆ แŒฅแˆฉ แŠแ‹! แˆแŠญ แ‹ซ แŠแŒˆแˆญ แŠแ‹แฃ แ‹žแˆแ‰ขแ‹Žแ‰ฝแŠ• แˆˆแˆ˜แˆแ‹ˆแˆต แ‹จแŠ แˆตแˆ›แ‰ต แŠ แŒˆแŠ“แŠ-แŠญแŠ’แŠ•แข แŠ แˆตแŒ แŠแ‰…แ‰ƒแ‰ฝแŠ‹แˆˆแˆ-แŠจแŒฝแˆ‘แ‰ แŠฅแŒ…แŒ แ‰ แŒฃแˆ แ‰ฐแˆˆแ‹‹แ‹‹แŒญ แ‹˜แ‹ดแ‹Žแ‰ฝแŠ• แ‹จแˆšแ‹ˆแ‹ฑ แŠฅแŠ“ แ‹จแ‰ฐแƒแˆแ‹แŠ• แˆˆแˆ˜แˆแ‰ฐแˆฝ แ‹จแˆ›แ‹ญแ‹ˆแ‹ฑ แ‰ แ‰ฐแˆˆแ‹ญแˆ แˆŠแ‰ƒแŒ แˆ‰ แ‹ญแ‰ฝแˆ‹แˆ‰ แข

แŠจแˆƒแ‰ฅแˆฎแŠซแ‰ต แ‰ แŠ‹แˆ‹ แŠฅแŠ•แ‹ฐแ‹แˆ แ‹จแˆดแˆšแŠ“แˆฉ แ‰ตแˆญแŒ‰แˆ แ‹ญแŒ€แˆแˆซแˆแข แ‰ แˆ›แŠ•แ‰ แ‰ฅ แ‹ญแ‹ฐแˆฐแ‰ฑ!

แˆแŠ•แˆ แŠ แ‹ญแŠแ‰ต แˆตแˆซ แ‰ขแˆฐแˆฉ แˆแˆ แŒŠแ‹œ แˆถแˆตแ‰ต แ‹ฐแˆจแŒƒแ‹Žแ‰ฝแŠ• แˆ›แˆˆแ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆแก-

  • แˆแŠ• แŒแ‰ฅ แˆ‹แ‹ญ แˆˆแˆ˜แ‹ตแˆจแˆต แŠฅแŠ•แ‹ฐแˆšแˆแˆแŒ‰ แ‹ญแ‹ˆแˆตแŠ‘;
  • แŒแ‰ฅแ‹ŽแŠ• แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแ‹ซแˆณแŠฉ แ‹ญแ‹ˆแˆตแŠ‘;
  • แ‹ˆแ‹ฐ แŒแ‰ฅแ‹Ž แ‹ญแˆแŒก.

แ‹ญแˆ… แ‰ แ•แˆฎแŒแˆซแˆ แŠ แ‹ˆแŒฃแŒฅ แˆ‹แ‹ญแˆ แ‹ญแˆ แˆซแˆแข แŠฎแ‹ต แˆตแŠ•แŒฝแ แ‹จแˆšแŠจแ‰ฐแˆ‰แ‰ตแŠ• แˆ›แ‹ตแˆจแŒ แŠ แˆˆแ‰ฅแŠ•แก-

  • แ•แˆฎแŒแˆซแˆ™ แˆแŠ• แˆ›แ‹ตแˆจแŒ แŠฅแŠ•แ‹ณแˆˆแ‰ แ‰ต แˆ˜แ‹ˆแˆฐแŠ•;
  • แ‰ฐแŒแ‰ฃแˆฉแŠ• แŠฅแŠ•แ‹ดแ‰ต แˆ›แŠจแŠ“แ‹ˆแŠ• แŠฅแŠ•แ‹ณแˆˆแ‰ แ‰ต แˆ˜แ‹ˆแˆฐแŠ•;
  • แ‰ฐแŒ“แ‹ณแŠ แŠฎแ‹ต แ‹ญแƒแ‰.

แ‹จแˆ˜แŒจแˆจแˆปแ‹ แ‹ฐแˆจแŒƒ, แ‰ แŠฅแˆญแŒแŒฅ, แ‰ แŒฃแˆ แŠ แˆตแˆแˆ‹แŒŠ แŠแ‹, แŒแŠ• แ‹›แˆฌ แˆตแˆˆแˆฑ แŠ แˆแŠ“แŒˆแˆญแˆ. แ‹ญแˆแ‰แŠ•แˆต แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซแ‹Žแ‰นแŠ• แˆแˆˆแ‰ฑแŠ• แŠฅแŠ•แŠแŒ‹แŒˆแˆซแˆˆแŠ•. แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แ•แˆฎแŒแˆซแˆ แŠ แ‹แŒช แ‹ˆแ‹ฐ แˆฅแˆซ แŠจแˆ˜แŒ€แˆ˜แˆฉ แ‰ แŠแ‰ต แ‹ซแŠจแŠ“แ‹แŠ“แ‰ธแ‹‹แˆ. แŠ แˆณแˆฝ แ‹ˆแ‹ญแˆ แ‹ณแ‰ณแ‰คแ‹ แŠฅแ‹จแŒปแแŠญ แŠฅแŠ•แ‹ฐแˆ†แŠ แŠฅแˆตแŠซแˆแ‹ˆแˆฐแŠ•แŠญ แ‹ตแˆจแˆต แˆˆแˆ˜แŒปแ แŠ แ‰ตแ‰€แˆ˜แŒฅแˆแข แˆตแˆˆ แŒแ‰ก แ‹จแ‰ฐแ‹ˆแˆฐแŠ แˆ€แˆณแ‰ฅ แˆ˜แŠ–แˆญ แŠ แˆˆแ‰ แ‰ตแข แŠฅแŠ“ แ‰ แŠฅแˆญแŒแŒ แŠแŠแ‰ต แ•แˆฎแŒแˆซแˆ™ แ‰ แ‰ตแŠญแŠญแˆ แˆแŠ• แŠฅแŠ•แ‹ฐแˆšแˆฐแˆซ แ‹ซแˆตแ‰ฃแˆ‰ แฃ แŠฅแŠ“ แŠฎแ‹ฑ แ‰ แˆ†แŠ แˆ˜แŠ•แŒˆแ‹ต แ‹ˆแ‹ฐ แŠ แˆณแˆฝ แŠฅแŠ•แ‹ฐแˆšแ‰€แ‹จแˆญ แ‰ฐแˆตแ‹ แ‰ แˆ›แ‹ตแˆจแŒ แ‰ แˆ†แŠ แˆ˜แŠ•แŒˆแ‹ต แŠ แ‹ญแŒปแ‰แข

แ‹ญแˆ… แŠฎแ‹ต แŠ แˆตแ‰€แ‹ตแˆž แˆ›แˆฐแ‰ฅ แŠฅแŠ•แ‹ดแ‰ต แ‰ แ‰ตแŠญแŠญแˆ แ‹ญแŠจแˆฐแ‰ณแˆ? แ‰ แ‹šแˆ… แˆจแŒˆแ‹ต แˆแŠ• แ‹ซแˆ…แˆ แŒฅแˆจแ‰ต แˆ›แ‹ตแˆจแŒ แŠ แˆˆแ‰ฅแŠ•? แˆแˆ‰แˆ แŠฅแŠ› แ‰ แˆแŠ•แˆแ‰ณแ‹ แ‰ฝแŒแˆญ แˆ‹แ‹ญ แ‹จแ‰ฐแˆ˜แŠซ แŠแ‹แข แˆตแˆ…แ‰ฐแ‰ตแŠ• แ‹จแˆšแ‰‹แ‰‹แˆ แ‹จแ‰ฐแŠจแ‹แˆแˆˆ แˆตแˆญแ‹“แ‰ต แˆ˜แƒแ แŠฅแŠ•แˆแˆแŒ‹แˆˆแŠ• แŠฅแŠ•แ‰ แˆแข แ‰ แ‹šแˆ… แˆแŠ”แ‰ณ, แŠฎแ‹ต แˆˆแˆ˜แŒปแ แŠจแˆ˜แ‰€แˆ˜แŒก แ‰ แŠแ‰ต แŠแŒˆแˆฎแ‰ฝแŠ• แ‰ แŒฅแŠ•แ‰ƒแ‰„ แˆ›แˆฐแ‰ฅ แŠ แˆˆแ‰ฅแŠ•. แ‹จแŠขแŠ•แ‰ฒแŒ€แˆญ แ‰ฐแˆˆแ‹‹แ‹‹แŒญแŠ• แ‰ 1 แˆˆแˆ˜แŒจแˆ˜แˆญ แ‰ฅแ‰ป แ‰ฅแŠ•แˆแˆแŒแˆต? แ‰ แ‰…แ‹ตแˆ˜-แŠฅแ‹ญแ‰ณ, แŠฅแ‹šแˆ… แˆแˆ‰แˆ แŠแŒˆแˆญ แ‰€แˆ‹แˆ แŠแ‹, แŠฅแŠ“ แˆแŠ•แˆ แˆ€แˆณแ‰ฅ แŠ แ‹ซแˆตแˆแˆแŒแˆ, แŠแŒˆแˆญ แŒแŠ• แŠจแ‹šแ‹ซ แ‰ แŠ‹แˆ‹ แŠจแˆ˜แŒ แŠ• แ‰ แˆ‹แ‹ญ แˆ˜แŒจแˆ˜แˆญ แˆŠแŠจแˆฐแ‰ต แŠฅแŠ•แ‹ฐแˆšแ‰ฝแˆ แŠฅแŠ“แˆตแ‰ณแ‹แˆณแˆˆแŠ•. แˆตแˆˆแ‹šแˆ…, แŠ แŠ•แ‹ต แ‰ฝแŒแˆญ แ‰€แˆ‹แˆ แ‹ˆแ‹ญแˆ แ‹แˆตแ‰ฅแˆตแ‰ฅ แˆ˜แˆ†แŠ‘แŠ• แˆˆแˆ˜แˆจแ‹ณแ‰ต แŠฅแŠ•แŠณแŠ•, แ‰ แˆ˜แŒ€แˆ˜แˆชแ‹ซ แˆ›แˆฐแ‰ฅ แŠ แˆˆแ‰ฅแ‹Žแ‰ต.

แˆˆแ‰ฝแŒแˆฉ แˆ˜แแ‰ตแˆ„แ‹Žแ‰ฝ แŠ แˆตแ‰€แ‹ตแˆ˜แ‹ แŠซแˆฐแ‰ก, แˆตแˆ…แ‰ฐแ‰ถแ‰ฝแŠ• แˆ›แˆตแ‹ˆแŒˆแ‹ต แ‹ญแ‰ฝแˆ‹แˆ‰. แ‹ญแˆ… แŒแŠ• แŠ แˆตแ‰ฐแˆณแˆฐแ‰ฅแˆ… แŒแˆแŒฝ แŠฅแŠ•แ‹ฒแˆ†แŠ• แ‹ญแŒ แ‹ญแ‰ƒแˆแข แ‹ญแˆ…แŠ•แŠ• แˆˆแˆ›แŒแŠ˜แ‰ต, แˆƒแˆณแ‰ฅแ‹ŽแŠ• แˆ˜แŒปแ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ. แ‹จแ‹ฒแŠญ แŒŠแŠ•แ‹ฐแŠ•แŠ• แŒฅแ‰…แˆต แ‰ แŒฃแˆ แ‹ˆแ‹ตแŒ„แ‹‹แˆˆแˆแก โ€œ แˆตแ‰ตแŒฝแ แ‰ฐแˆแŒฅแˆฎ แˆแŠ• แ‹ซแˆ…แˆ แŠ แˆตแ‰ฐแˆณแˆฐแ‰ฅแˆ… แ‹ฐแŠซแˆ› แŠฅแŠ•แ‹ฐแˆ†แŠ แ‹ซแˆณแ‹ซแˆแข แŠซแˆแŒปแแŠญแฃ แŠฅแ‹ซแˆฐแ‰ฅแŠญ แŠฅแŠ•แ‹ฐแˆ†แŠ แ‰ฅแ‰ป แŠแ‹ แ‹จแˆแ‰ณแˆตแ‰ แ‹แข แŠฅแŠ“ แˆƒแˆณแ‰ฆแ‰ฝแ‹ŽแŠ• แ‰ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝ แˆ˜แˆแŠญ แˆ˜แŒปแ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ.

แ‹แˆญแ‹แˆฎแ‰ฝ แ‰ฅแ‹™ แ‰ฐแŒแ‰ฃแˆซแ‰ตแŠ• แ‹ซแŠจแŠ“แ‹แŠ“แˆ‰, แ‰ แ‰ฐแˆˆแ‹ญแˆ แ‰ แ‰ตแˆ‹แˆแ‰… แ•แˆฎแŒ€แŠญแ‰ถแ‰ฝ แ‹แˆตแŒฅ. แŒแŠ• แˆตแˆˆ แŠ แŠ•แ‹ฑ แ‰ฅแ‰ป แŠฅแŠ“แŒˆแˆซแˆˆแˆ: แ‰ แŒแˆแŒฝ แŠฅแŠ•แ‹ตแŠ“แˆตแ‰ฅ แ‹ญแˆจแ‹ฑแŠ“แˆ. แ‰ แŒแˆแŒฝ แˆ›แˆฐแ‰ฅ แ‰ แŒฃแˆ แŠ แˆตแˆแˆ‹แŒŠ แŠฅแŠ“ แ‰ แŒฃแˆ แŠจแ‰ฃแ‹ต แŠแ‹, แˆตแˆˆแ‹šแˆ… แŠฅแ‹šแˆ… แˆ›แŠ•แŠ›แ‹แŠ•แˆ แŠฅแˆญแ‹ณแ‰ณ แŠฅแŠ•แˆแˆแŒ‹แˆˆแŠ•. แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แ‰ แ‹จแ‰ตแŠ›แ‹ แ‰‹แŠ•แ‰‹ แˆ˜แŒปแ แŠ แˆˆแ‰ฅแŠ•? แ‰ แŠ แŒ แ‰ƒแˆ‹แ‹ญ แ‹ญแˆ… แˆแˆแŒŠแ‹œ แˆˆแ•แˆฎแŒแˆซแˆ แŠ แ‹แŒชแ‹Žแ‰ฝ แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซแ‹ แŒฅแ‹ซแ‰„ แŠแ‹-แ‰ แˆแŠ• แ‰‹แŠ•แ‰‹ แŠฅแŠ•แŒฝแ‹แˆˆแŠ•. แˆˆแŠฅแˆฑ แˆแŠ•แˆ แ‰ตแŠญแŠญแˆˆแŠ› แˆ˜แˆแˆต แ‹จแˆˆแˆ: แŠฅแ‹จแˆแ‰ณแŠ“แ‰ธแ‹ แ‹ซแˆ‰ แ‰ฝแŒแˆฎแ‰ฝ แ‰ แŒฃแˆ แ‹จแ‰ฐแˆˆแ‹ซแ‹ฉ แŠ“แ‰ธแ‹. แˆˆแŠ แŠ•แ‹ณแŠ•แ‹ถแ‰ฝแฃ TLA+ แ‹ซแ‹˜แŒ‹แŒ€แˆแ‰ต แ‹จแˆตแ”แˆฒแŠแŠฌแˆฝแŠ• แ‰‹แŠ•แ‰‹ แŠแ‹แข แˆˆแˆŒแˆŽแ‰ฝ, แ‰ปแ‹ญแŠ•แŠ› แˆ˜แŒ แ‰€แˆ แ‹จแ‰ แˆˆแŒ  แŠ แˆ˜แ‰บ แŠแ‹. แˆแˆ‰แˆ แŠแŒˆแˆญ แŠฅแŠ•แ‹ฐ แˆแŠ”แ‰ณแ‹ โ€‹โ€‹แ‹ญแ‹ˆแˆฐแŠ“แˆ.

แ‰ แŒฃแˆ แŠ แˆตแˆแˆ‹แŒŠแ‹ แˆŒแˆ‹ แŒฅแ‹ซแ‰„ แŠแ‹-แ‹จแŒ แˆซ แŠ แˆตแ‰ฐแˆณแˆฐแ‰ฅแŠ• แŠฅแŠ•แ‹ดแ‰ต แˆ›แŒแŠ˜แ‰ต แ‹ญแ‰ปแˆ‹แˆ? แˆ˜แˆแˆตแก- แŠฅแŠ•แ‹ฐ แˆณแ‹ญแŠ•แ‰ฒแˆตแ‰ถแ‰ฝ แˆ›แˆฐแ‰ฅ แŠ แˆˆแ‰ฅแŠ•แข แ‹ญแˆ… แ‰ฃแˆˆแ‰แ‰ต 500 แ‹“แˆ˜แ‰ณแ‰ต แ‹แˆตแŒฅ แŠฅแˆซแˆฑแŠ• แ‹ซแˆจแŒ‹แŒˆแŒ  แ‹จแŠ แˆตแ‰ฐแˆณแˆฐแ‰ฅ แˆ˜แŠ•แŒˆแ‹ต แŠแ‹แข แ‰ แˆณแ‹ญแŠ•แˆต แ‹แˆตแŒฅแฃ แ‹จแŠฅแ‹แŠแ‰ณแ‹แŠ• แ‹จแˆ‚แˆณแ‰ฅ แˆžแ‹ดแˆŽแ‰ฝ แŠฅแŠ•แŒˆแŠแ‰ฃแˆˆแŠ•แข แŠ แˆตแ‰ตแˆฎแŠ–แˆš แˆแŠ“แˆแ‰ฃแ‰ต แ‰ แ‰ƒแˆ‰ แŒฅแ‰ฅแ‰… แ‰ตแˆญแŒ‰แˆ แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซแ‹ แˆณแ‹ญแŠ•แˆต แŠแ‹แข แ‰ แˆฅแŠ แˆแˆˆแŠญ แŒฅแŠ“แ‰ต แ‹แˆตแŒฅ แŒฅแ‰…แˆ แˆ‹แ‹ญ แ‰ แˆšแ‹แˆˆแ‹ แ‹จแˆ‚แˆณแ‰ฅ แˆžแ‹ดแˆ แ‹แˆตแŒฅ แ‹จแˆฐแˆ›แ‹ญ แŠ แŠซแˆ‹แ‰ต แ‰ แŒ…แˆแˆ‹ แฃ แ‰ แŠ แ‰€แˆ›แˆ˜แŒฅ แŠฅแŠ“ แ‰ แแŒฅแŠแ‰ต แŠฅแŠ•แ‹ฐ แŠแŒฅแ‰ฆแ‰ฝ แ‹ญแ‰ณแ‹ซแˆ‰ แฃ แˆแŠ•แˆ แŠฅแŠ•แŠณแŠ• แ‰ แŠฅแ‹แŠแ‰ฑ แŠฅแŠแˆฑ แ‰ แ‰ฐแˆซแˆฎแ‰ฝ แŠฅแŠ“ แ‹แ‰…แ‹ซแŠ–แˆถแ‰ฝ แฃ แˆ›แ‹•แ‰ แˆ แŠฅแŠ“ แˆ›แ‹•แ‰ แˆ แ‹แˆตแŒฅ แŠฅแŒ…แŒ แ‰ แŒฃแˆ แ‹แˆตแ‰ฅแˆตแ‰ฅ แŠแŒˆแˆฎแ‰ฝ แŠ“แ‰ธแ‹แข แ‹ญแˆ… แˆžแ‹ดแˆ, แˆแŠญ แŠฅแŠ•แ‹ฐแˆŒแˆ‹แ‹, แ‹จแ‰ฐแ‹ˆแˆฐแŠ‘ แ‰ฝแŒแˆฎแ‰ฝแŠ• แˆˆแˆ˜แแ‰ณแ‰ต แ‹จแ‰ฐแˆแŒ แˆจ แŠแ‹. แ•แˆ‹แŠ”แ‰ต แˆˆแˆ›แŒแŠ˜แ‰ต แŠจแˆแˆˆแŒ‰ แ‰ดแˆŒแˆตแŠฎแ•แŠ• แ‹จแ‰ต แŠฅแŠ•แ‹ฐแˆšแŒ แ‰แˆ™ แˆˆแˆ˜แ‹ˆแˆฐแŠ• แ‰ แŒฃแˆ แŒฅแˆฉ แŠแ‹. แŠแŒˆแˆญ แŒแŠ• แ‰ แ‹šแˆ… แ•แˆ‹แŠ”แ‰ต แˆ‹แ‹ญ แ‹ซแˆˆแ‹แŠ• แ‹จแŠ แ‹จแˆญ แˆแŠ”แ‰ณ แˆˆแˆ˜แ‰ฐแŠ•แ‰ แ‹ญ แŠจแˆแˆˆแŒ‰, แ‹ญแˆ… แˆžแ‹ดแˆ แŠ แ‹ญแˆฐแˆซแˆ.

แ‹จแˆ‚แˆณแ‰ฅ แ‰ตแˆแˆ…แˆญแ‰ต แ‹จแŠ แˆแˆณแ‹ซแ‹ แ‰ฃแˆ…แˆชแ‹ซแ‰ตแŠ• แˆˆแˆ˜แ‹ˆแˆฐแŠ• แ‹ซแˆตแ‰ฝแˆˆแŠ“แˆ. แŠฅแŠ“ แˆณแ‹ญแŠ•แˆต แŠฅแŠแ‹šแˆ… แŠ•แ‰ฅแˆจแ‰ถแ‰ฝ แŠจแŠฅแ‹แŠแ‰ณแ‹ แŒ‹แˆญ แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแ‹›แˆ˜แ‹ฑ แ‹ซแˆณแ‹ซแˆ. แˆตแˆˆ แˆณแ‹ญแŠ•แˆตแฃ แˆตแˆˆ แŠฎแˆแ’แ‹แ‰ฐแˆญ แˆณแ‹ญแŠ•แˆต แŠฅแŠ•แŠแŒ‹แŒˆแˆญแข แ‹จแˆแŠ•แˆฐแˆซแ‰ แ‰ต แŠฅแ‹แŠแ‰ณ แ‹จแ‰ฐแˆˆแ‹ซแ‹ฉ แŠ แ‹ญแŠแ‰ต แ‹จแŠฎแˆแ’แ‹ฉแ‰ฐแˆญ แˆตแˆญแ‹“แ‰ถแ‰ฝแŠ• แŠแ‹แก แ•แˆฎแˆฐแˆฐแˆญแฃ แŒŒแˆ แŠฎแŠ•แˆถแˆŽแ‰ฝแฃ แŠฎแˆแ’แ‹แ‰ฐแˆฎแ‰ฝแฃ แˆแŒปแˆš แ•แˆฎแŒแˆซแˆžแ‰ฝ แŠฅแŠ“ แ‹จแˆ˜แˆณแˆฐแˆ‰แ‰ตแข แ‰ แŠฎแˆแ’แ‹ฉแ‰ฐแˆญ แˆ‹แ‹ญ แˆตแˆˆ แŠ แŠ•แ‹ต แ•แˆฎแŒแˆซแˆ แˆตแˆˆแˆ›แˆตแŠฌแ‹ต แŠฅแŠ“แŒˆแˆซแˆˆแˆ, แŠแŒˆแˆญ แŒแŠ• แ‰ แŠ แŒ แ‰ƒแˆ‹แ‹ญ แŠฅแŠแ‹šแˆ… แˆแˆ‰ แˆ˜แ‹ฐแˆแ‹ฐแˆšแ‹ซแ‹Žแ‰ฝ แˆˆแˆ›แŠ•แŠ›แ‹แˆ แ‹จแŠฎแˆแ’แ‹ฉแ‰ฐแˆญ แˆฒแˆตแ‰ฐแˆ แ‹ญแˆ แˆซแˆ‰. แ‰ แŠฅแŠ› แˆณแ‹ญแŠ•แˆต แ‹แˆตแŒฅ แ‰ฅแ‹™ แ‹จแ‰ฐแˆˆแ‹ซแ‹ฉ แˆžแ‹ดแˆŽแ‰ฝแŠ• แŠฅแŠ•แŒ แ‰€แˆ›แˆˆแŠ•-แ‰ฑแˆชแŠ•แŒ แˆ›แˆฝแŠ• แฃ แ‰ แŠจแŠแˆ แ‹จแ‰ณแ‹˜แ‹™ แ‹จแŠญแˆตแ‰ฐแ‰ถแ‰ฝ แˆตแ‰ฅแˆตแ‰ฆแ‰ฝ แŠฅแŠ“ แˆŒแˆŽแ‰ฝ แ‰ฅแ‹™แข

แ•แˆฎแŒแˆซแˆ แˆแŠ•แ‹ตแŠ• แŠแ‹? แ‹ญแˆ… แ‰ แŒแˆ แˆŠแ‰ณแˆฐแ‰ฅ แ‹จแˆšแ‰ฝแˆ แˆ›แŠ•แŠ›แ‹แˆ แŠฎแ‹ต แŠแ‹แข แŠ แˆณแˆฝ แˆ˜แŒปแ แ‹ซแˆตแˆแˆแŒˆแŠ“แˆ แŠฅแŠ•แ‰ แˆ. แˆถแˆตแ‰ต แ‰ฐแŒแ‰ฃแˆซแ‰ตแŠ• แŠฅแŠ“แŠจแŠ“แ‹แŠ“แˆˆแŠ•-แ‹จแ‰ฐแŒ แ‰ƒแˆšแ‹แŠ• แ‹จแ•แˆฎแŒแˆซแˆ™ แŠฅแ‹ญแ‰ณ แŠฅแŠ•แ‰€แˆญแŒปแˆˆแŠ•, แŠจแ‹šแ‹ซแˆ แ‹จแ•แˆฎแŒแˆซแˆ™แŠ• แŠจแแ‰ฐแŠ› แ‹ฐแˆจแŒƒ แŠ•แ‹ตแ แŠฅแŠ•แŒฝแ‹แˆˆแŠ• แŠฅแŠ“ แ‰ แˆ˜แŒจแˆจแˆปแˆ แŠฎแ‹ฑแŠ• แŠฅแŠ•แŒฝแ‹แˆˆแŠ•. แŠฎแ‹ฑแŠ• แ‰ แˆแŠ•แŒฝแแ‰ แ‰ต แŒŠแ‹œ, แ‹จแŒฝแˆ‘แ แ‰…แˆญแŒธแ‰ต แˆ˜แƒแ แŠฅแŠ•แ‹ณแˆˆแ‰ฅแŠ• แŠฅแŠ•แŒˆแŠแ‹˜แ‰ฃแˆˆแŠ•. แŠฅแ‹šแˆ… แŠฅแŠ•แ‹ฐแŒˆแŠ“ แˆถแˆตแ‰ต แ‰ฝแŒแˆฎแ‰ฝแŠ• แˆ˜แแ‰ณแ‰ต แŠ แˆˆแ‰ฅแŠ•: แ‹ญแˆ… แˆ˜แˆณแˆชแ‹ซ แˆแŠ• แ‹“แ‹ญแŠแ‰ต แŒฝแˆ‘แ แŠฅแŠ•แ‹ฐแˆšแˆ˜แˆˆแˆต แ‹ญแ‹ˆแˆตแŠ‘; แˆˆแˆ˜แ‰…แˆจแŒฝ แˆตแˆแ‰ฐ แ‰€แˆ˜แˆญ แ‹ญแˆแˆจแŒก; แŠฎแ‹ต แŒปแ. แ‹ญแˆ… แ‰ฐแŒแ‰ฃแˆญ แ‹จแˆซแˆฑ แ‹จแˆ†แŠ แŠ•แ‹‘แˆต แ‰ฐแŒแ‰ฃแˆญ แŠ แˆˆแ‹แก แˆฐแˆจแ‹แŠ• แ‰ แ‰ƒแˆ‹แ‰ต แ‹แˆตแŒฅ แ‰ แ‰ตแŠญแŠญแˆ แŠ แˆตแŒˆแ‰ฃแข แ‹ญแˆ…แŠ•แŠ• แŠ•แŠกแˆต แ‰ฐแŒแ‰ฃแˆญ แ‰ แˆฆแˆตแ‰ต แŠฅแˆญแŠจแŠ–แ‰ฝ แŠฅแŠ•แˆแ‰ณแ‹‹แˆˆแŠ• - แŠฅแŠ•แ‹ฐแˆแ‰ณแ‹ฉแ‰ต แŠฅแŠแˆฑ แ‰ แ‰ฅแ‹™ แ‹ฐแˆจแŒƒแ‹Žแ‰ฝ แ‹ญแ‹ฐแŒ‹แŒˆแˆ›แˆ‰แข

แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซแ‹แŠ• แ‹ฐแˆจแŒƒ แ‰ แ‰ แˆˆแŒ  แ‹แˆญแ‹แˆญ แŠฅแŠ•แˆ˜แˆแŠจแ‰ต-แ•แˆฎแŒแˆซแˆ™ แˆแŠ• แ‰ฝแŒแˆญ แŠฅแŠ•แ‹ฐแˆšแˆแ‰ณ. แŠฅแ‹šแˆ… แฃ แŠฅแŠ› แ‰ฅแ‹™แ‹แŠ• แŒŠแ‹œ แŠ แŠ•แ‹ตแŠ• แ•แˆฎแŒแˆซแˆ แŠ แŠ•แ‹ณแŠ•แ‹ต แŒแ‰ฅแ‹“แ‰ต แ‹จแˆšแ‹ˆแˆตแ‹ต แŠฅแŠ“ แ‹จแ‰ฐแ‹ˆแˆฐแŠ แ‹แŒคแ‰ต แ‹จแˆšแ‹ซแˆ˜แŒฃ แ‰ฐแŒแ‰ฃแˆญ แŠ แ‹ตแˆญแŒˆแŠ• แŠฅแŠ•แ‰€แˆญแŒปแˆˆแŠ•แข แ‰ แˆ‚แˆณแ‰ฅ แ‹แˆตแŒฅ แŠ แŠ•แ‹ต แ‰ฐแŒแ‰ฃแˆญ แ‰ฅแ‹™แ‹แŠ• แŒŠแ‹œ แŠฅแŠ•แ‹ฐ แ‹จแ‰ณแ‹˜แ‹˜ แŒฅแŠ•แ‹ต แˆตแ‰ฅแˆตแ‰ฅ แ‹ญแŒˆแˆˆแŒปแˆแข แˆˆแˆแˆณแˆŒแฃ แˆˆแ‰ฐแˆแŒฅแˆฎ แ‰แŒฅแˆฎแ‰ฝ แ‹จแˆตแŠฉแ‹ŠแŠ•แŒ แ‰ฐแŒแ‰ฃแˆญ แŠฅแŠ•แ‹ฐ แˆตแ‰ฅแˆตแ‰ฅ {<0,0>, <1,1>, <2,4>, <3,9>, โ€ฆ} แ‰ฐแŒˆแˆแŒฟแˆ. แ‹จแŠฅแŠ•แ‹ฐแ‹šแˆ… แŠ แ‹ญแŠแ‰ต แ‰ฐแŒแ‰ฃแˆญ แŒŽแˆซ แ‹จแŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แŒฅแŠ•แ‹ต แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซ แŠ แŠซแˆ‹แ‰ต แˆตแ‰ฅแˆตแ‰ฅ แŠแ‹, แˆ›แˆˆแ‰ตแˆ แ‹จแ‰ฐแˆแŒฅแˆฎ แ‰แŒฅแˆฎแ‰ฝ. แŠ แŠ•แ‹ตแŠ• แ‰ฐแŒแ‰ฃแˆญ แˆˆแˆ˜แ‹ˆแˆฐแŠ• แ‹ˆแˆฐแŠ• แŠฅแŠ“ แ‰€แˆ˜แˆฉแŠ• แˆ˜แŒแˆˆแ… แŠ แˆˆแ‰ฅแŠ•แข

แŠแŒˆแˆญ แŒแŠ• แ‰ แˆ‚แˆณแ‰ฅ แ‹แˆตแŒฅ แ‹ซแˆ‰ แ‰ฐแŒแ‰ฃแˆซแ‰ต แ‰ แ•แˆฎแŒแˆซแˆšแŠ•แŒ แ‰‹แŠ•แ‰‹แ‹Žแ‰ฝ แ‹แˆตแŒฅ แŠซแˆ‰ แ‰ฐแŒแ‰ฃแˆซแ‰ต แŒ‹แˆญ แŠ แŠ•แ‹ต แŠ แ‹ญแŠแ‰ต แŠ แ‹ญแ‹ฐแˆ‰แˆแข แˆ’แˆณแ‰ก แ‰ แŒฃแˆ แ‰€แˆ‹แˆ แŠแ‹แข แˆˆแ‰ฐแ‹ˆแˆณแˆฐแ‰ก แˆแˆณแˆŒแ‹Žแ‰ฝ แŒŠแ‹œ แˆตแˆˆแˆŒแˆˆแŠแฃ แ‰€แˆ‹แˆ แ‹จแˆ†แŠแ‹แŠ• แŠฅแŠ•แˆ˜แˆแŠจแ‰ตแก แ‰ C แ‹แˆตแŒฅ แ‹ซแˆˆ แ‰ฐแŒแ‰ฃแˆญ แ‹ˆแ‹ญแˆ แ‰ แŒƒแ‰ซ แ‹แˆตแŒฅ แ‹จแˆแˆˆแ‰ต แŠขแŠ•แ‰ฒแŒ€แˆญ แ‰ตแˆแ‰แŠ• แ‹จแŒ‹แˆซ แŠ แŠซแ‹แ‹ญ แ‹จแˆšแˆ˜แˆแˆต แ‹จแˆ›แ‹ญแŠ•แ‰€แˆณแ‰€แˆต แ‹˜แ‹ดแข แ‰ แ‹šแˆ… แ‹˜แ‹ด แ‹แˆญแ‹แˆญ แ‹แˆตแŒฅ, แŠฅแŠ•แŒฝแ‹แˆˆแŠ•: แ‹ซแˆฐแˆ‹แˆ GCD(M,N) แˆˆแŠญแˆญแŠญแˆญ M ะธ Nแ‹จแ‰ต GCD(M,N) - แŒŽแˆซแ‹ แ‹จแŠขแŠ•แ‰ฒแŒ€แˆญ แŒฅแŠ•แ‹ถแ‰ฝ แˆตแ‰ฅแˆตแ‰ฅ แ‹จแˆ†แŠ แ‰ฐแŒแ‰ฃแˆญแฃ แŠฅแŠ“ แ‹จแˆ˜แˆ˜แˆˆแˆป แŠฅแˆดแ‰ฑ แ‹จแˆšแŠจแ‹แˆแˆˆแ‹ แ‰ตแˆแ‰ แŠขแŠ•แ‰ฒแŒ€แˆญ แŠแ‹แข M ะธ N. แ‹ญแˆ… แˆžแ‹ดแˆ แŠจแŠฅแ‹แŠแ‰ณแ‹ แŒ‹แˆญ แŠฅแŠ•แ‹ดแ‰ต แ‹ญแ‹›แˆ˜แ‹ณแˆ? แˆžแ‹ดแˆ‰ แŠขแŠ•แ‰ฒแŒ€แˆญ แˆ‹แ‹ญ แ‹ญแˆฐแˆซแˆแฃ แ‰ แˆฒ แ‹ˆแ‹ญแˆ แ‰ แŒƒแ‰ซ 32-แ‰ขแ‰ต แŠ แˆˆแŠ•แข int. แ‹ญแˆ… แˆžแ‹ดแˆ แŠ แˆแŒŽแˆชแ‹แˆ แ‰ตแŠญแŠญแˆ แˆ˜แˆ†แŠ‘แŠ• แˆˆแˆ˜แ‹ˆแˆฐแŠ• แ‹ซแˆตแ‰ฝแˆˆแŠ“แˆ GCDแŠแŒˆแˆญ แŒแŠ• แ‹จแ‰ตแˆญแ แˆ˜แŒ แŠ• แˆตแˆ…แ‰ฐแ‰ถแ‰ฝแŠ• แŠ แ‹ญแŠจแˆ‹แŠจแˆแˆแข แ‹ญแˆ… แ‹จแ‰ แˆˆแŒ  แ‹แˆตแ‰ฅแˆตแ‰ฅ แˆžแ‹ดแˆ แ‹ซแˆตแˆแˆแŒˆแ‹‹แˆ, แˆˆแ‹šแˆ…แˆ แˆแŠ•แˆ แŒŠแ‹œ แ‹จแˆˆแˆ.

แŠฅแŠ•แ‹ฐ แˆžแ‹ดแˆ แˆตแˆˆ แŠ แŠ•แ‹ต แ‰ฐแŒแ‰ฃแˆญ แ‹แˆตแŠ•แŠแ‰ต แŠฅแŠ•แŠแŒ‹แŒˆแˆญ. แŠ แŠ•แ‹ณแŠ•แ‹ต แ•แˆฎแŒแˆซแˆžแ‰ฝ (แŠฅแŠ•แ‹ฐ แŠฆแ•แˆฌแ‰ฒแŠ•แŒ แˆฒแˆตแ‰ฐแˆžแ‰ฝ แ‹ซแˆ‰) แˆˆแ‰ฐแ‹ˆแˆฐแŠ‘ แŒแ‰คแ‰ถแ‰ฝ แ‹จแ‰ฐแ‹ˆแˆฐแŠ แŠฅแˆดแ‰ต แ‰ฅแ‰ป แŠ แ‹ญแˆ˜แˆแˆฑแˆแฃ แ‹ซแˆˆแˆ›แ‰‹แˆจแŒฅ แˆŠแˆ„แ‹ฑ แ‹ญแ‰ฝแˆ‹แˆ‰แข แ‰ แ‰ฐแŒจแˆ›แˆชแˆ, แŠฅแŠ•แ‹ฐ แˆžแ‹ดแˆ แ‹ซแˆˆแ‹ แ‰ฐแŒแ‰ฃแˆญ แˆˆแˆแˆˆแ‰ฐแŠ›แ‹ แ‹ฐแˆจแŒƒ แ‰ฐแˆตแˆ›แˆš แŠ แ‹ญแ‹ฐแˆˆแˆ: แ‰ฝแŒแˆฉแŠ• แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแˆแ‰ณ แˆ›แ‰€แ‹ต. แˆแŒฃแŠ• แˆ˜แ‹ฐแˆญแ‹ฐแˆญ แŠฅแŠ“ แ‹จแŠ แˆจแ‹ แˆ˜แ‹ฐแˆญแ‹ฐแˆญ แŠ แŠ•แ‹ต แŠ แ‹ญแŠแ‰ต แ‰ฐแŒแ‰ฃแˆญ แ‹ซแˆฐแˆ‹แˆ‰แฃ แŒแŠ• แˆ™แˆ‰ แˆˆแˆ™แˆ‰ แ‹จแ‰ฐแˆˆแ‹ซแ‹ฉ แˆตแˆแ‰ฐ แ‰€แˆ˜แˆฎแ‰ฝ แŠ“แ‰ธแ‹แข แˆตแˆˆแ‹šแˆ…, แ‹จแ•แˆฎแŒแˆซแˆ™ แŒแ‰ฅ แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแˆณแŠซ แˆˆแˆ˜แŒแˆˆแŒฝ, แ‹จแ‰ฐแˆˆแ‹จ แˆžแ‹ดแˆ แŠฅแŒ แ‰€แˆ›แˆˆแˆ, แ‹ฐแˆจแŒƒแ‹แŠ• แ‹จแŒ แ‰ แ‰€ แ‹จแ‰ฃแˆ…แˆญแ‹ญ แˆžแ‹ดแˆ แŠฅแŠ•แ‰ แˆˆแ‹. แ‰ แ‹แˆตแŒก แ‹ซแˆˆแ‹ แ•แˆฎแŒแˆซแˆ แŠฅแŠ•แ‹ฐ แˆแˆ‰แˆ แ‹จแ‰ฐแˆแ‰€แ‹ฑ แ‰ฃแˆ…แˆชแ‹ซแ‰ต แˆตแ‰ฅแˆตแ‰ฅ แŠแ‹ แ‹จแˆšแ‹ˆแŠจแˆˆแ‹, แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑแˆ แ‰ แ‰ฐแˆซแ‹, แ‹จแŒแ‹›แ‰ถแ‰ฝ แ‰…แ‹ฐแˆ แ‰ฐแŠจแ‰ฐแˆ แŠแ‹, แŠฅแŠ“ แŒแ‹›แ‰ฑ แˆˆแ‰ฐแˆˆแ‹‹แ‹‹แŒฎแ‰ฝ แŠฅแˆดแ‰ถแ‰ฝแŠ• แˆ˜แˆตแŒ แ‰ต แŠแ‹.

แ‹จ Euclid แˆตแˆแ‰ฐ แ‰€แˆ˜แˆญ แˆแˆˆแ‰ฐแŠ› แ‹ฐแˆจแŒƒ แˆแŠ• แŠฅแŠ•แ‹ฐแˆšแˆ˜แˆตแˆ แŠฅแŠ•แ‹ญแข แˆ›แˆตแˆ‹แ‰ต แŠ แˆˆแ‰ฅแŠ• GCD(M, N). แŠฅแŠ“แˆตแŒ€แˆแˆซแˆˆแŠ• M แŠฅแŠ•แ‹ดแ‰ต xแŠ“ N แŠฅแŠ•แ‹ดแ‰ต y, แŠจแ‹šแ‹ซแˆ แ‰ แ‰ฐแ‹ฐแŒ‹แŒ‹แˆš แ‹จแŠฅแŠแ‹šแˆ…แŠ• แ‰ฐแˆˆแ‹‹แ‹‹แŒฎแ‰ฝ แ‰ตแŠ•แˆนแŠ• แŠจแ‰ตแˆแ‰… แŠฅแˆตแŠจ แŠฅแŠฉแˆ แ‹ตแˆจแˆต แ‹ญแ‰€แŠ•แˆฑ. แˆˆแˆแˆณแˆŒ, แŠจแˆ†แŠ M = 12แŠ“ N = 18, แ‹จแˆšแŠจแ‰ฐแˆˆแ‹แŠ• แ‰ฃแˆ…แˆช แˆ˜แŒแˆˆแŒฝ แŠฅแŠ•แ‰ฝแˆ‹แˆˆแŠ•:

[x = 12, y = 18] โ†’ [x = 12, y = 6] โ†’ [x = 6, y = 6]

แŠฅแŠ“ M = 0 ะธ N = 0? แ‹œแˆฎ แ‰ แˆแˆ‰แˆ แ‰แŒฅแˆฎแ‰ฝ แ‹จแ‰ฐแŠจแ‹แˆแˆˆ แŠแ‹, แˆตแˆˆแ‹šแˆ… แ‰ แ‹šแˆ… แŒ‰แ‹ณแ‹ญ แˆ‹แ‹ญ แˆแŠ•แˆ แ‰ณแˆ‹แ‰… แŠ แŠซแ‹แ‹ญ แ‹จแˆˆแˆ. แ‰ แ‹šแˆ… แˆแŠ”แ‰ณ แ‹ˆแ‹ฐ แˆ˜แŒ€แˆ˜แˆชแ‹ซแ‹ แ‹ฐแˆจแŒƒ แ‰ฐแˆ˜แˆแˆฐแŠ• แˆ˜แŒ แ‹จแ‰… แŠ แˆˆแ‰ฅแŠ•แก-แŠ แ‹ŽแŠ•แ‰ณแ‹Š แ‹ซแˆแˆ†แŠ‘ แ‰แŒฅแˆฎแ‰ฝ GCD แ‰ แ‰ตแŠญแŠญแˆ แˆ›แˆตแˆ‹แ‰ต แŠ แˆˆแ‰ฅแŠ•? แ‹ญแˆ… แŠ แˆตแˆแˆ‹แŒŠ แŠซแˆแˆ†แŠ, แˆ˜แŒแˆˆแŒซแ‹แŠ• แˆ˜แ‰€แ‹จแˆญ แ‰ฅแ‰ป แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ.

แŠฅแ‹šแˆ… แˆตแˆˆ แˆแˆญแ‰ณแˆ›แŠแ‰ต แ‰ตแŠ•แˆฝ แŒˆแˆˆแŒป แˆ›แ‹ตแˆจแŒ แŠ แˆˆแ‰ฅแŠ•. แ‰ฅแ‹™แ‹แŠ• แŒŠแ‹œ แ‹จแˆšแˆˆแŠซแ‹ แ‰ แ‰€แŠ• แ‰ แ‰ฐแƒแ‰ แ‹จแŠฎแ‹ต แˆ˜แˆตแˆ˜แˆฎแ‰ฝ แ‰ฅแ‹›แ‰ต แŠแ‹แข แŠแŒˆแˆญ แŒแŠ• แ‹จแ‰ฐแ‹ˆแˆฐแŠ‘ แ‹จแˆ˜แˆตแˆ˜แˆฎแ‰ฝ แ‰ฅแ‹›แ‰ต แŠซแˆตแ‹ˆแŒˆแ‹ฑ แˆตแˆซแ‹Ž แ‹จแ‰ แˆˆแŒ  แŒ แ‰ƒแˆš แŠแ‹, แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แˆˆแŒฅแ‰ƒแ‰…แŠ• แ‰ฆแ‰ณ แ‰ตแŠ•แˆฝ แŠแ‹. แŠฅแŠ“ แŠฎแ‹ฑแŠ• แˆˆแˆ›แˆตแ‹ˆแŒˆแ‹ต แ‰€แˆ‹แˆ‰ แˆ˜แŠ•แŒˆแ‹ต แ‰ แˆ˜แŒ€แˆ˜แˆชแ‹ซ แ‹ฐแˆจแŒƒ แˆ‹แ‹ญ แŠแ‹. แŠฅแˆญแˆตแ‹Ž แˆˆแˆ˜แ‰ฐแŒแ‰ แˆญ แ‹จแˆšแˆžแŠญแˆฉแ‰ตแŠ• แˆแˆ‰แŠ•แˆ แ‹ฐแ‹ˆแˆŽแ‰ฝ แŠฅแŠ“ แŒฉแŠธแ‰ถแ‰ฝ แˆณแ‹ซแˆตแˆแˆแŒแ‹Ž แˆ™แˆ‰ แ‰ แˆ™แˆ‰ แˆŠแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆแข แ•แˆฎแŒแˆซแˆแŠ• แˆˆแˆ›แ‰…แˆˆแˆ แŠฅแŠ“ แŒŠแ‹œ แˆˆแˆ˜แ‰†แŒ แ‰ฅ แˆแŒฃแŠ‘ แˆ˜แŠ•แŒˆแ‹ต แˆ˜แ‹ฐแˆจแŒ แ‹จแˆŒแˆˆแ‰ฃแ‰ธแ‹แŠ• แŠแŒˆแˆฎแ‰ฝ แŠ แˆˆแˆ›แ‹ตแˆจแŒ แŠแ‹แข แˆแˆˆแ‰ฐแŠ›แ‹ แŠฅแˆญแˆแŒƒ แˆแˆˆแ‰ฐแŠ›แ‹ แ‰ แŒฃแˆ แŒŠแ‹œ แ‰†แŒฃแ‰ข แŠ แ‰…แˆ แŠแ‹แข แˆแˆญแ‰ณแˆ›แŠแ‰ตแŠ• แŠจแ‰ฐแƒแ‰ แˆ˜แˆตแˆ˜แˆฎแ‰ฝ แŠ แŠ•แƒแˆญ แŠจแˆˆแŠซแˆ… แŠ แŠ•แ‹ตแŠ• แ‰ฐแŒแ‰ฃแˆญ แŠฅแŠ•แ‹ดแ‰ต แˆ›แŠจแŠ“แ‹ˆแŠ• แŠฅแŠ•แ‹ฐแˆแ‰ตแ‰ฝแˆ แˆ›แˆฐแ‰ฅแˆ… แ‹ซแ‹ฐแˆญแŒแˆƒแˆ แŠ แŠแˆตแ‰ฐแŠ› แˆแˆญแ‰ณแˆ›แŠแ‰ต, แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แ‰ แ‰ตแŠ•แˆฝ แŠฎแ‹ต แ‰ฐแˆ˜แˆณแˆณแ‹ญ แ‰ฝแŒแˆญ แˆ˜แแ‰ณแ‰ต แ‹ญแ‰ฝแˆ‹แˆ‰. แŠฅแ‹šแˆ… แ‰ตแŠญแŠญแˆˆแŠ› แˆตแ‰ณแ‰ฒแˆตแ‰ฒแŠญแˆตแŠ• แˆ˜แˆตแŒ แ‰ต แŠ แˆแ‰ฝแˆแˆ, แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แ‰ แˆ˜แŒแˆˆแŒซแ‹ แˆ‹แ‹ญ แŒŠแ‹œแŠ• แ‰ แˆ›แˆณแˆˆแ, แˆ›แˆˆแ‰ตแˆ แ‰ แˆ˜แŒ€แˆ˜แˆชแ‹ซ แŠฅแŠ“ แ‰ แˆแˆˆแ‰ฐแŠ›แ‹ แ‹ฐแˆจแŒƒแ‹Žแ‰ฝ แˆ‹แ‹ญ, แ‹ซแˆแŒปแแŠฉแ‰ตแŠ• แ‹จแˆ˜แˆตแˆ˜แˆฎแ‰ฝ แ‰ฅแ‹›แ‰ต แˆˆแˆ˜แ‰แŒ แˆญ แˆแŠ•แˆ แˆ˜แŠ•แŒˆแ‹ต แ‹จแˆˆแŠแˆ. แŠฅแŠ“ แˆ™แŠจแˆซแ‹ แŠฅแ‹šแˆ…แˆ แˆŠแ‹˜แŒ‹แŒ… แŠ แ‹ญแ‰ฝแˆแˆ, แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แ‰ แˆ™แŠจแˆซแ‹ แ‹แˆตแŒฅ แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซแ‹แŠ• แ‹ฐแˆจแŒƒ แ‹จแˆ›แŒ แŠ“แ‰€แ‰… แˆ˜แ‰ฅแ‰ต แ‹จแˆˆแŠ•แˆ, แ‰ฐแŒแ‰ฃแˆฉ แŠ แˆตแ‰€แ‹ตแˆž แ‰ฐแ‹ˆแˆตแŠ—แˆ.

แˆ˜แ‹ฐแ‰ แŠ› แ‰ฃแˆแˆ†แŠ‘ แ‹แˆญแ‹แˆฎแ‰ฝ แ‹แˆตแŒฅ แ‰ฅแ‹™ แ‰ฝแŒแˆฎแ‰ฝแŠ• แ‰ฝแˆ‹ แˆ›แˆˆแ‰ต แ‰€แˆ‹แˆ แŠแ‹แข แˆˆแ‰ฐแŒแ‰ฃแˆฎแ‰ฝ แŒฅแ‰ฅแ‰… แ‹แˆญแ‹แˆฎแ‰ฝแŠ• แˆˆแˆ˜แŒปแ แˆแŠ•แˆ แŠ แˆตแ‰ธแŒ‹แˆช แŠแŒˆแˆญ แ‹จแˆˆแˆ, แˆตแˆˆแ‹šแˆ… แŒ‰แ‹ณแ‹ญ แŠ แˆแŠ“แŒˆแˆญแˆ. แ‰ แˆแ‰ตแŠฉแฃ แˆˆแˆ˜แ‹ฐแ‰ แŠ› แ‰ฃแˆ…แˆชแ‹ซแ‰ต แŒ แŠ•แŠซแˆซ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แˆตแˆˆแˆ˜แŒปแ แŠฅแŠ•แŠแŒ‹แŒˆแˆซแˆˆแŠ•แข แ‹จแ‹ฐแˆ…แŠ•แŠแ‰ต แŠ•แ‰ฅแˆจแ‰ฑแŠ• แ‰ แˆ˜แŒ แ‰€แˆ แ‹จแ‰ตแŠ›แ‹แŠ•แˆ แ‹จแ‰ฃแˆ…แˆช แˆตแ‰ฅแˆตแ‰ฅ แˆŠแŒˆแˆˆแŒฝ แŠฅแŠ•แ‹ฐแˆšแ‰ฝแˆ แ‹จแˆšแŒˆแˆแŒฝ แ‰ฒแ‹Žแˆฌแˆ แŠ แˆˆแข (แ‹ฐแˆ…แŠ•แŠแ‰ต) แŠฅแŠ“ แ‹จแˆ˜แ‹ณแŠ• แ‰ฃแˆ…แˆชแ‹ซแ‰ต (แˆ•แ‹ซแ‹แŠแ‰ต). แ‹ฐแˆ…แŠ•แŠแ‰ต แˆ›แˆˆแ‰ต แˆแŠ•แˆ แˆ˜แŒฅแŽ แŠแŒˆแˆญ แŠ แ‹ญแŠจแˆฐแ‰ตแˆ, แ•แˆฎแŒแˆซแˆ™ แ‹จแ‰ฐแˆณแˆณแ‰ฐ แˆ˜แˆแˆต แŠ แ‹ญแˆฐแŒฅแˆ. แˆ˜แ‰ตแˆจแ แˆ›แˆˆแ‰ต แ‹ญแ‹‹แˆ แ‹ญแ‹ฐแˆญ แŠฅแŠ•แŒ‚ แŠ แŠ•แ‹ต แŒฅแˆฉ แŠแŒˆแˆญ แ‹ญแŠจแˆฐแ‰ณแˆ แˆ›แˆˆแ‰ตแˆ แ•แˆฎแŒแˆซแˆ™ แˆแŒฅแŠ–แˆ แˆ†แŠ แ‹˜แŒแ‹ญแ‰ถ แ‰ตแŠญแŠญแˆˆแŠ›แ‹แŠ• แˆ˜แˆแˆต แ‹ญแˆฐแŒฃแˆ. แŠฅแŠ•แ‹ฐ แ‹ฐแŠ•แ‰ก, แ‹ฐแˆ…แŠ•แŠแ‰ต แ‹จแ‰ แˆˆแŒ  แŠ แˆตแˆแˆ‹แŒŠ แŠ แˆ˜แˆ‹แŠซแ‰ฝ แŠแ‹, แˆตแˆ…แ‰ฐแ‰ถแ‰ฝ แ‰ฅแ‹™แ‹แŠ• แŒŠแ‹œ แŠฅแ‹šแˆ… แ‹ญแŠจแˆฐแ‰ณแˆ‰. แˆตแˆˆแ‹šแˆ…, แŒŠแ‹œแŠ• แˆˆแˆ˜แ‰†แŒ แ‰ฅ, แˆตแˆˆ แˆ˜แ‰ตแˆจแ แŠ แˆแŠ“แŒˆแˆญแˆ, แˆแŠ•แˆ แŠฅแŠ•แŠณแŠ• แ‰ แŠฅแˆญแŒแŒฅ แŠ แˆตแˆแˆ‹แŒŠ แ‰ขแˆ†แŠ•แˆ.

แ‰ แˆ˜แŒ€แˆ˜แˆชแ‹ซ แ‹ฐแˆจแŒƒ แˆŠแˆ†แŠ‘ แ‹จแˆšแ‰ฝแˆ‰ แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซ แŒแ‹›แ‰ถแ‰ฝแŠ• แ‰ แˆ›แ‹˜แ‹ แ‹ฐแˆ…แŠ•แŠแ‰ตแŠ• แŠฅแŠ“แˆณแŠซแˆˆแŠ•แข แˆแˆˆแ‰ฐแŠ›แฃ แˆˆแŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แŒแ‹›แ‰ต แŠจแˆšแˆ˜แŒกแ‰ต แˆแˆ‰แˆ แŒแ‹›แ‰ถแ‰ฝ แŒ‹แˆญ แ‹ซแˆ‰ แŒแŠ•แŠ™แŠแ‰ถแ‰ฝแข แŠฅแŠ•แ‹ฐ แˆณแ‹ญแŠ•แ‰ฒแˆตแ‰ถแ‰ฝ แŠฅแŠ•แˆตแˆซ แŠฅแŠ“ แŒแ‹›แ‰ถแ‰ฝแŠ• แ‰ แˆ‚แˆณแ‰ฅ แŠฅแŠ•แŒˆแˆแƒแˆˆแŠ•แข แ‹จแˆ˜แŠแˆป แŒแ‹›แ‰ถแ‰ฝ แˆตแ‰ฅแˆตแ‰ฅ แ‰ แ‰€แˆ˜แˆญ แ‹ญแŒˆแˆˆแŒปแˆ แฃ แˆˆแˆแˆณแˆŒ แฃ แ‰ แ‹ฉแŠญแˆŠแ‹ต แŠ แˆแŒŽแˆชแ‹แˆ แˆแŠ”แ‰ณ แ‹แˆตแŒฅ- (x = M) โˆง (y = N). แˆˆแ‰ฐแ‹ˆแˆฐแŠ‘ แŠฅแˆดแ‰ถแ‰ฝ M ะธ N แŠ แŠ•แ‹ต แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซ แˆแŠ”แ‰ณ แ‰ฅแ‰ป แŠ แˆˆ. แŠจแ‰€แŒฃแ‹ฉ แŒแ‹›แ‰ต แŒ‹แˆญ แ‹ซแˆˆแ‹ แŒแŠ•แŠ™แŠแ‰ต แ‹จแ‰€แŒฃแ‹ฉ แŒแ‹›แ‰ต แ‰ฐแˆˆแ‹‹แ‹‹แŒฎแ‰ฝ แŠจแ‹‹แŠ“ แŒ‹แˆญ แ‰ แ‰ฐแƒแ‰แ‰ แ‰ต แ‰€แˆ˜แˆญ แ‹ญแŒˆแˆˆแŒปแˆ, แŠฅแŠ“ แ‹จแŠ แˆแŠ‘ แˆแŠ”แ‰ณ แ‰ฐแˆˆแ‹‹แ‹‹แŒฎแ‰ฝ แ‹ซแˆˆ แ•แˆซแ‹ญแˆ แ‹จแ‰ฐแƒแ‰ แŠ“แ‰ธแ‹. แ‹จแ‹ฉแŠญแˆŠแ‹ต แŠ แˆแŒŽแˆชแ‹แˆแŠ• แ‰ แ‰ฐแˆ˜แˆˆแŠจแ‰ฐ แ‹จแˆแˆˆแ‰ฑแŠ• แ‰€แˆ˜แˆฎแ‰ฝ แˆ˜แŒฃแˆ˜แˆ แŠฅแŠ“แˆตแ‰ฐแŠ“แŒแ‹ณแˆˆแŠ• แฃ แŠจแŠฅแŠแ‹šแˆ…แˆ แ‹แˆตแŒฅ แ‰ แŠ แŠ•แ‹ฑ x แ‰ตแˆแ‰ แ‹‹แŒ‹ แŠแ‹, แŠฅแŠ“ แ‰ แˆแˆˆแ‰ฐแŠ›แ‹ แ‹แˆตแŒฅ - y:

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แ‰ แˆ˜แŒ€แˆ˜แˆชแ‹ซแ‹ แˆแŠ”แ‰ณ แŠ แ‹ฒแˆฑ แ‹จy แŠฅแˆดแ‰ต แŠจแ‰€แ‹ตแˆžแ‹ แ‹จy แŠฅแˆดแ‰ต แŒ‹แˆญ แŠฅแŠฉแˆ แŠแ‹, แŠฅแŠ“ แ‰ตแŠ•แˆนแŠ• แ‰ฐแˆˆแ‹‹แ‹‹แŒญ แŠจแ‰ตแˆแ‰… แ‰ฐแˆˆแ‹‹แ‹‹แŒญ แ‰ แˆ˜แ‰€แŠแˆต แŠ แ‹ฒแˆฑแŠ• แ‹จ x แŠฅแˆดแ‰ต แŠฅแŠ“แŒˆแŠ›แˆˆแŠ•. แ‰ แˆแˆˆแ‰ฐแŠ›แ‹ แŒ‰แ‹ณแ‹ญ แ‰ฐแ‰ƒแˆซแŠ’แ‹แŠ• แŠฅแŠ“แ‹ฐแˆญแŒ‹แˆˆแŠ•.

แ‹ˆแ‹ฐ แ‹ฉแŠญแˆŠแ‹ต แˆตแˆแ‰ฐ แ‰€แˆ˜แˆญ แŠฅแŠ•แˆ˜แˆˆแˆตแข แŠฅแŠ•แ‹ฐ แŒˆแŠ“ แŠฅแŠ“แˆตแ‰ฅ M = 12, N = 18. แ‹ญแˆ… แŠแŒ แˆ‹ แ‹จแˆ˜แŒ€แˆ˜แˆชแ‹ซ แˆแŠ”แ‰ณแŠ• แ‹ญแŒˆแˆแŒปแˆ แฃ (x = 12) โˆง (y = 18). แŠจแ‹šแ‹ซ แŠฅแŠแ‹šแ‹ซแŠ• แŠฅแˆดแ‰ถแ‰ฝ แŠจแˆ‹แ‹ญ แ‰ฃแˆˆแ‹ แ‰€แˆ˜แˆญ แ‹แˆตแŒฅ แŠฅแŠ•แˆฐแŠซแ‰ธแ‹‹แˆˆแŠ• แŠฅแŠ“ แŠฅแŠ“แŒˆแŠ›แˆˆแŠ•แก-

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แ‰ฅแ‰ธแŠ›แ‹ แˆ˜แแ‰ตแˆ” แ‹ญแŠธแ‹แŠ“แก- x' = 18 - 12 โˆง y' = 12แŠฅแŠ“ แ‰ฃแˆ…แˆชแ‹แŠ• แŠฅแŠ“แŒˆแŠ›แˆˆแŠ•- [x = 12, y = 18]. แ‰ แ‰ฐแˆ˜แˆณแˆณแ‹ญแฃ แ‰ แ‰ฃแˆ…แˆชแ‹ซแ‰ฝแŠ• แ‹ซแˆ‰แ‰ตแŠ• แˆแˆ‰แŠ•แˆ แŒแ‹›แ‰ถแ‰ฝ แˆ˜แŒแˆˆแ… แŠฅแŠ•แ‰ฝแˆ‹แˆˆแŠ•แก- [x = 12, y = 18] โ†’ [x = 12, y = 6] โ†’ [x = 6, y = 6].

แ‰ แˆ˜แŒจแˆจแˆปแ‹ แŒแ‹›แ‰ต [x = 6, y = 6] แˆแˆˆแ‰ฑแˆ แ‹จแŒˆแˆˆแŒปแ‹ แŠญแแˆŽแ‰ฝ แˆแˆฐแ‰ต แˆตแˆˆแˆšแˆ†แŠ‘ แ‰€แŒฃแ‹ญ แˆแŠ”แ‰ณ แ‹จแˆˆแ‹แˆแข แˆตแˆˆแ‹šแˆ… แฃ แ‹จแˆแˆˆแ‰ฐแŠ›แ‹ แ‹ฐแˆจแŒƒ แˆ™แˆ‰ แ‹แˆญแ‹แˆญ แŠ แˆˆแŠ• - แŠฅแˆญแˆตแ‹Ž แŠฅแŠ•แ‹ฐแˆšแˆ˜แˆˆแŠจแ‰ฑแ‰ต แฃ แ‹ญแˆ… แŠฅแŠ•แ‹ฐ แˆ˜แˆแŠ•แ‹ฒแˆถแ‰ฝ แŠฅแŠ“ แˆณแ‹ญแŠ•แ‰ฒแˆตแ‰ถแ‰ฝ แ‰ แŒฃแˆ แ‰ฐแˆซ แˆ‚แˆณแ‰ฅ แŠแ‹ แฃ แŠฅแŠ“ แŠฅแŠ•แ‹ฐ แŠฎแˆแ’แ‹ฉแ‰ฐแˆญ แˆณแ‹ญแŠ•แˆต แŠฅแŠ•แŒแ‹ณ แŠ แ‹ญแ‹ฐแˆˆแˆแข

แŠฅแŠแ‹šแˆ… แˆแˆˆแ‰ต แ‰€แˆ˜แˆฎแ‰ฝ แ‹ˆแ‹ฐ แŠ แŠ•แ‹ต แ‹จแŒŠแ‹œแ‹ซแ‹Š แŠ แˆ˜แŠญแŠ•แ‹ฎ แ‰€แˆ˜แˆญ แˆŠแŒฃแˆ˜แˆฉ แ‹ญแ‰ฝแˆ‹แˆ‰แข แŠฅแˆท แ‰†แŠ•แŒ† แŠฅแŠ“ แˆˆแˆ›แ‰ฅแˆซแˆซแ‰ต แ‰€แˆ‹แˆ แŠแ‰ฝ แฃ แŒแŠ• แŠ แˆแŠ• แˆˆแŠฅแˆท แˆแŠ•แˆ แŒŠแ‹œ แ‹จแˆˆแˆแข แˆˆแŠ‘แˆฎ แŠ•แ‰ฅแˆจแ‰ต แ‰ฅแ‰ป แŒŠแ‹œแ‹ซแ‹Š แŠ แˆ˜แŠญแŠ•แ‹ฎ แˆŠแ‹ซแˆตแˆแˆแŒˆแŠ• แ‹ญแ‰ฝแˆ‹แˆแฃ แˆˆแ‹ฐแˆ…แŠ•แŠแ‰ต แˆฒแ‰ฃแˆ แŠ แ‹ซแˆตแˆแˆแŒแˆแข แŒŠแ‹œแ‹ซแ‹Š แŠ แˆ˜แŠญแŠ•แ‹ฎ แŠ แˆแ‹ˆแ‹ตแˆ แฃ แŠฅแˆฑ แ‰ แŒฃแˆ แ‰ฐแˆซ แˆ‚แˆณแ‰ฅ แŠ แ‹ญแ‹ฐแˆˆแˆ แฃ แŒแŠ• แ‰ แŠ แŠ—แŠ—แˆญ แˆแŠ”แ‰ณ แŠ แˆตแˆแˆ‹แŒŠ แŠญแ‹แ‰ต แŠแ‹แข

แ‰ แ‹ฉแŠญแˆŠแ‹ต แˆตแˆแ‰ฐ แ‰€แˆ˜แˆญ แˆˆแŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แŠฅแˆดแ‰ต x ะธ y แˆแ‹ฉ แŠฅแˆดแ‰ถแ‰ฝ แŠ แˆแ‰ธแ‹ x' ะธ y', แ‹ญแˆ…แˆ แŠจแˆšแ‰€แŒฅแˆˆแ‹ แŒแ‹›แ‰ต แŒ‹แˆญ แ‹ซแˆˆแ‹แŠ• แŒแŠ•แŠ™แŠแ‰ต แŠฅแ‹แŠแ‰ต แ‹ซแ‹ฐแˆญแŒˆแ‹‹แˆ. แ‰ แˆŒแˆ‹ แŠ แŠแŒ‹แŒˆแˆญ แ‹จแ‹ฉแŠญแˆŠแ‹ต แŠ แˆแŒŽแˆชแ‹แˆ แ‰†แˆซแŒฅ แŠแ‹แข แ‹จแˆ›แ‹ญแ‹ˆแˆตแŠ• แŠ แˆแŒŽแˆชแ‹แˆแŠ• แˆˆแˆ˜แ‰…แˆจแŒฝแฃ แŠ แˆแŠ• แ‹ซแˆˆแ‹ แˆแŠ”แ‰ณ แ‰ฅแ‹™ แˆŠแˆ†แŠ‘ แ‹จแˆšแ‰ฝแˆ‰ แ‹จแ‹ˆแ‹ฐแŠแ‰ต แŒแ‹›แ‰ถแ‰ฝ แˆŠแŠ–แˆฉแ‰ต แ‹ญแŒˆแ‰ฃแˆแฃ แŠฅแŠ“ แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แ‹ซแˆแ‰ฐแŠจแ‹แˆแˆˆ แ‰ฐแˆˆแ‹‹แ‹‹แŒญ แŠฅแˆดแ‰ต แ‰ฅแ‹™ แ‹‹แŠ“ แ‰ฐแˆˆแ‹‹แ‹‹แŒญ แŠฅแˆดแ‰ถแ‰ฝ แŠ แˆ‰แ‰ต แฃ แˆˆแˆแˆณแˆŒ แŠจแˆšแ‰€แŒฅแˆˆแ‹ แŒแ‹›แ‰ต แŒ‹แˆญ แ‹ซแˆˆแ‹ แŒแŠ•แŠ™แŠแ‰ต แŠฅแ‹แŠแ‰ต แŠแ‹แข แ‹ญแˆ…แŠ• แˆ›แ‹ตแˆจแŒ แ‰€แˆ‹แˆ แŠแ‹แฃ แŒแŠ• แŠ แˆแŠ• แˆแˆณแˆŒแ‹Žแ‰ฝแŠ• แŠ แˆแˆฐแŒฅแˆแข

แ‹จแˆšแˆฐแˆซ แˆ˜แˆณแˆชแ‹ซ แˆˆแˆ˜แˆตแˆซแ‰ต แˆ˜แ‹ฐแ‰ แŠ› แˆ‚แˆณแ‰ฅ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆแข แˆ˜แŒแˆˆแŒซแ‹แŠ• แŠฅแŠ•แ‹ดแ‰ต แˆ˜แ‹ฐแ‰ แŠ› แˆ›แ‹ตแˆจแŒ แ‹ญแ‰ปแˆ‹แˆ? แ‹ญแˆ…แŠ•แŠ• แˆˆแˆ›แ‹ตแˆจแŒ, แˆ˜แ‹ฐแ‰ แŠ› แ‰‹แŠ•แ‰‹ แ‹ซแˆตแˆแˆแŒˆแŠ“แˆ, แˆˆแˆแˆณแˆŒ, TLA+. แ‹จแ‹ฉแŠญแˆŠแ‹ต แŠ แˆแŒŽแˆชแ‹แˆ แˆ˜แŒแˆˆแŒซ แ‰ แ‹šแˆ… แ‰‹แŠ•แ‰‹ แ‹ญแˆ…แŠ•แŠ• แ‹ญแˆ˜แˆตแˆ‹แˆแข

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แ‹จแˆถแˆตแ‰ต แˆ›แ‹•แ‹˜แŠ• แˆแˆแŠญแ‰ต แ‹ซแˆˆแ‹ แ‹จแŠฅแŠฉแˆ แˆแˆแŠญแ‰ต แˆแˆแŠญแ‰ต แˆ›แˆˆแ‰ต แ‰ แˆตแ‰ฐแŒแˆซ แ‹ซแˆˆแ‹ แ‹‹แŒ‹ แŠจแˆแˆแŠญแ‰ฑ แ‰ แˆตแ‰ฐแ‰€แŠ แŠซแˆˆแ‹ แŠฅแˆดแ‰ต แŒ‹แˆญ แŠฅแŠฉแˆ แŠแ‹ แˆ›แˆˆแ‰ต แŠแ‹. แ‰ แˆ˜แˆ แˆจแ‰ฑ, แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแ‹ แแ‰บ แŠแ‹, แ‰ แŠฅแŠ› แˆแŠ”แ‰ณ แˆแˆˆแ‰ต แ‰ตแˆญแŒ“แˆœแ‹Žแ‰ฝ. แ‰ TLA+ แ‹แˆตแŒฅ แˆ‹แˆˆแ‹ แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแฃ แˆแŠญ แŠจแˆ‹แ‹ญ แ‰ฃแˆˆแ‹ แˆตแˆ‹แ‹ญแ‹ต แˆ‹แ‹ญ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แŠฅแŠ“ แŠ แŠ•แ‹ณแŠ•แ‹ต แŠ แŒˆแ‰ฃแ‰ฆแ‰ฝแŠ• แˆ›แŠจแˆ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆแข แ‰  ASCII แ‹แˆตแŒฅ แ‹ญแˆ… แ‹ญแˆ˜แˆตแˆ‹แˆ

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แŠฅแŠ•แ‹ฐแˆšแˆ˜แˆˆแŠจแ‰ฑแ‰ต, แˆแŠ•แˆ แ‹จแ‰ฐแ‹ˆแˆณแˆฐแ‰  แŠแŒˆแˆญ แ‹จแˆˆแˆ. แ‹จTLA+ แˆ˜แŒแˆˆแŒซแ‹ แˆŠแˆžแŠจแˆญ แ‹ญแ‰ฝแˆ‹แˆแฃ แˆ›แˆˆแ‰ตแˆ แ‰ แ‰ตแŠ•แˆฝ แˆžแ‹ดแˆ แˆแˆ‰แŠ•แˆ แˆŠแˆ†แŠ‘ แ‹จแˆšแ‰ฝแˆ‰ แ‰ฃแˆ…แˆชแ‹Žแ‰ฝแŠ• แˆ›แˆˆแแข แ‰ แŠฅแŠ› แˆแŠ”แ‰ณ, แ‹ญแˆ… แˆžแ‹ดแˆ แ‹จแ‰ฐแ‹ˆแˆฐแŠ‘ แŠฅแˆดแ‰ถแ‰ฝ แ‹ญแˆ†แŠ“แˆ M ะธ N. แ‹ญแˆ… แˆ™แˆ‰ แ‰ แˆ™แˆ‰ แŠ แ‹แ‰ถแˆ›แ‰ฒแŠญ แ‹จแˆ†แŠ แ‰ แŒฃแˆ แ‰€แˆแŒฃแ‹ แŠฅแŠ“ แ‰€แˆ‹แˆ แ‹จแˆ›แˆจแŒ‹แŒˆแŒซ แ‹˜แ‹ด แŠแ‹แข แˆ˜แ‹ฐแ‰ แŠ› แ‹จแŠฅแ‹แŠแ‰ต แˆ›แˆจแŒ‹แŒˆแŒซแ‹Žแ‰ฝแŠ• แˆ˜แƒแ แŠฅแŠ“ แ‰ แˆœแŠซแŠ’แŠซแˆ แˆ˜แˆแ‰ฐแˆฝแˆ แ‹ญแ‰ปแˆ‹แˆ แŠแŒˆแˆญแŒแŠ• แ‹ญแˆ… แ‰ฅแ‹™ แŒŠแ‹œ แ‹จแˆšแ‹ˆแˆตแ‹ต แ‰ แˆ˜แˆ†แŠ‘ แˆ›แŠ•แˆ แ‹ญแˆ…แŠ• แ‹จแˆšแ‹ซแ‹ฐแˆญแŒˆแ‹ แ‹จแˆˆแˆ แˆ›แˆˆแ‰ต แ‹ญแ‰ปแˆ‹แˆแข

แ‹จแ‰ฒแŠคแˆแŠค+ แ‹‹แŠแŠ› แŒ‰แ‹ณแ‰ฑ แˆ‚แˆณแ‰ฅ แˆ˜แˆ†แŠ‘ แŠแ‹แฃ แŠฅแŠ“ แ•แˆฎแŒแˆซแˆ˜แˆฎแ‰ฝ แŠฅแŠ“ แ‹จแŠฎแˆแ’แ‹แ‰ฐแˆญ แˆณแ‹ญแŠ•แ‰ฒแˆตแ‰ถแ‰ฝ แˆ‚แˆณแ‰ฅแŠ• แ‹ญแˆแˆซแˆ‰แข แ‰ แˆ˜แŒ€แˆ˜แˆชแ‹ซ แˆฒแ‰ณแ‹ญ, แ‹ญแˆ… แŠฅแŠ•แ‹ฐ แ‰€แˆแ‹ต แ‹ญแˆ˜แˆตแˆ‹แˆ, แŒแŠ• แ‰ แˆšแ‹ซแˆณแ‹แŠ• แˆแŠ”แ‰ณ, แ‰ แ‰แˆ แŠแŒˆแˆญ แˆ›แˆˆแ‰ด แŠแ‹. แ‹จแˆฅแˆซ แ‰ฃแˆแ‹ฐแˆจแ‰ฃแ‹ฌ TLA+แŠ• แˆˆแ‰ฅแ‹™ แŒˆแŠ•แ‰ขแ‹Žแ‰ฝ แˆˆแˆ›แˆตแˆจแ‹ณแ‰ต แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆžแŠจแˆจ แŠฅแ‹จแŠแŒˆแˆจแŠ แŠแ‰ แˆญแข แ‰€แˆ˜แˆฎแ‰น แ‰ แˆตแŠญแˆชแŠ‘ แˆ‹แ‹ญ แŠฅแŠ•แ‹ฐแ‰ณแ‹ฉ แ‹ˆแ‹ฒแ‹ซแ‹แŠ‘ แ‹จแ‰ฅแˆญแŒญแ‰† แ‹“แ‹ญแŠ–แ‰ฝ แˆ†แŠ‘แข แˆตแˆˆแ‹šแˆ… TLA+ แŠซแˆตแˆแˆซแ‹Žแ‰ต แˆ˜แŒ แ‰€แˆ แ‹ญแ‰ฝแˆ‹แˆ‰แข แ•แˆ‹แˆตแŠซแˆแฃ แ‹จแŠ แˆปแŠ•แŒ‰แˆŠแ‰ต แ•แˆฎแŒแˆซแˆšแŠ•แŒ แ‰‹แŠ•แ‰‹ แŠ แ‹ญแŠแ‰ต แŠแ‹แข แ‰ แ•แˆ‹แˆตแŠซแˆ แ‹แˆตแŒฅ แ‹ซแˆˆ แŠ แŒˆแˆ‹แˆˆแŒฝ แˆ›แŠ•แŠ›แ‹แˆ TLA+ แŠ แŒˆแˆ‹แˆˆแŒฝ แˆ›แˆˆแ‰ตแˆ แ‰ แŠ แŒ แ‰ƒแˆ‹แ‹ญ แˆ›แŠ•แŠ›แ‹แˆ แ‹จแˆ‚แˆณแ‰ฅ แŠ แŒˆแˆ‹แˆˆแŒฝ แˆŠแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆแข แ‰ แ‰ฐแŒจแˆ›แˆชแˆ แ•แˆ‹แˆตแŠซแˆ แˆ‹แˆแ‰ฐแ‹ˆแˆฐแŠ แˆตแˆแ‰ฐ แ‰€แˆ˜แˆฎแ‰ฝ แŠ แŒˆแ‰ฃแ‰ฅ แŠ แˆˆแ‹แข แ•แˆ‹แˆตแŠซแˆ แˆ›แŠ•แŠ›แ‹แŠ•แˆ แ‹จTLA+ แŠ แŒˆแˆ‹แˆˆแŒฝ แˆŠแŒฝแ แˆตแˆˆแˆšแ‰ฝแˆแฃ PlusCal แŠจแˆ›แŠ•แŠ›แ‹แˆ แ‰ตแŠญแŠญแˆˆแŠ› แ‹จแ•แˆฎแŒแˆซแˆ แŠ แ‹ˆแŒฃแŒฅ แ‰‹แŠ•แ‰‹ แ‹จแ‰ แˆˆแŒ  แŒˆแˆ‹แŒญ แŠแ‹แข แ‰ แˆ˜แ‰€แŒ แˆ แ•แˆ‹แˆตแŠซแˆ แ‰ แ‰€แˆ‹แˆ‰ แˆŠแŠแ‰ แ‰ฅ แ‹ˆแ‹ฐแˆšแ‰ฝแˆ แ‹จTLA+ แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แ‰ฐแˆฐแ‰ฅแˆตแ‰งแˆแข แ‹ญแˆ… แˆ›แˆˆแ‰ต แŒแŠ• แ‹แˆตแ‰ฅแˆตแ‰ฅ แ‹จแ•แˆ‹แˆตแŠซแˆ แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แ‰  TLA + แˆ‹แ‹ญ แ‹ˆแ‹ฐ แ‰€แˆ‹แˆ แ‹ญแ‰€แ‹จแˆซแˆ แˆ›แˆˆแ‰ต แŠ แ‹ญแ‹ฐแˆˆแˆ - แ‰ แˆ˜แŠซแŠจแˆ‹แ‰ธแ‹ แ‹ซแˆˆแ‹ แ‹ฐแ‰ฅแ‹ณแ‰ค แŒแˆแŒฝ แŠแ‹, แˆแŠ•แˆ แ‰ฐแŒจแˆ›แˆช แ‹แˆตแ‰ฅแˆตแ‰ฅแŠแ‰ต แŠ แ‹ญแŠ–แˆญแˆ. แ‰ แˆ˜แŒจแˆจแˆปแˆแฃ แ‹ญแˆ… แˆ˜แŒแˆˆแŒซ แ‰ TLA+ แˆ˜แˆณแˆชแ‹ซแ‹Žแ‰ฝ แˆŠแˆจแŒ‹แŒˆแŒฅ แ‹ญแ‰ฝแˆ‹แˆแข แ‰ แŠ แŒ แ‰ƒแˆ‹แ‹ญ แ•แˆ‹แˆตแŠซแˆ แ‹จแˆ‚แˆณแ‰ฅ แŽแ‰ขแ‹ซแŠ• แˆˆแˆ›แˆธแŠแ แ‹ญแˆจแ‹ณแˆ แŠฅแŠ“ แˆˆแ•แˆฎแŒแˆซแˆ แŠ แ‹แŒชแ‹Žแ‰ฝ แŠฅแŠ“ แˆˆแŠฎแˆแ’แ‹ฉแ‰ฐแˆญ แˆณแ‹ญแŠ•แ‰ฒแˆตแ‰ถแ‰ฝ แŠฅแŠ•แŠณแŠ• แˆˆแˆ˜แˆจแ‹ณแ‰ต แ‰€แˆ‹แˆ แŠแ‹แข แ‰€แ‹ฐแˆ แˆฒแˆ, แ‰ แŠฅแˆฑ แˆ‹แ‹ญ แˆตแˆแ‰ฐ แ‰€แˆ˜แˆฎแ‰ฝแŠ• แŠ แˆณแ‰ตแˆœแ‹ซแˆˆแˆ แˆˆแ‰ฐแ‹ˆแˆฐแŠ แŒŠแ‹œ (แ‹ˆแ‹ฐ 10 แ‹“แˆ˜แ‰ณแ‰ต แŒˆแ‹ฐแˆ›).

แˆแŠ“แˆแ‰ฃแ‰ต แŠ แŠ•แ‹ต แˆฐแ‹ TLA + แŠฅแŠ“ PlusCal แˆ‚แˆณแ‰ฅ แŠ“แ‰ธแ‹ แ‰ฅแˆˆแ‹ แ‹ญแ‰ƒแ‹ˆแˆ›แˆ‰แฃ แŠฅแŠ“ แˆ‚แˆณแ‰ฅ แ‹ฐแŒแˆž แ‰ แ‰ฐแˆแŒ แˆฉ แˆแˆณแˆŒแ‹Žแ‰ฝ แˆ‹แ‹ญ แ‰ฅแ‰ป แ‹ญแˆฐแˆซแˆแข แ‰ แ‰ฐแŒแ‰ฃแˆญ, แŠจแ‹“แ‹ญแŠแ‰ถแ‰ฝ, แˆ‚แ‹ฐแ‰ถแ‰ฝ, แŠฅแ‰ƒแ‹Žแ‰ฝ, แ‹ˆแ‹˜แ‰ฐ แŒ‹แˆญ แŠฅแ‹แŠแ‰ฐแŠ› แ‰‹แŠ•แ‰‹ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ. แ‹ญแˆ… แˆตแˆ…แ‰ฐแ‰ต แŠแ‹แข แ‰ แŠ แˆ›แ‹žแŠ• แ‹แˆตแŒฅ แ‹ญแˆ แˆซ แ‹จแŠแ‰ แˆจแ‹ แŠญแˆชแˆต แŠ’แ‹แŠฎแˆแ‰ฅ แ‹จแŒปแˆแ‹ แŠฅแŠแˆ†แก- โ€œTLA+แŠ• แ‰ แŠ แˆฅแˆญ แ‹‹แŠ“ แ‹‹แŠ“ แ•แˆฎแŒ€แŠญแ‰ถแ‰ฝ แˆ‹แ‹ญ แ‰ฐแŒ แ‰…แˆ˜แŠ“แˆแฃแ‰ แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แˆแŠ”แ‰ณ แˆ˜แŒ แ‰€แˆ›แ‰ฝแŠ• แˆˆแˆแˆ›แ‰ต แ‰ตแˆแ‰… แˆˆแ‹แŒฅ แŠ แˆแŒฅแ‰ทแˆ แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แˆแˆญแ‰ฑแŠ• แŠจแˆ˜แˆแ‰ณแ‰ณแ‰ฝแŠ• แ‰ แŠแ‰ต แŠ แ‹ฐแŒˆแŠ› แˆณแŠ•แŠซแ‹Žแ‰ฝแŠ• แˆˆแˆ˜แ‹ซแ‹ แˆตแˆˆแ‰ปแˆแŠ• แŠฅแŠ“ แŠฅแŠ•แ‹ตแŠ•แ‰ฝแˆ แ‹จแˆšแ‹ซแˆตแˆแˆแŒˆแŠ•แŠ• แŒแŠ•แ‹›แ‰ค แŠฅแŠ“ แŠฅแˆแŠแ‰ต แˆตแˆˆแˆฐแŒ แŠ• แŠแ‹แข แ‹จแ•แˆฎแŒแˆซแˆ™แŠ• แŠฅแ‹แŠแ‰ต แˆณแ‹ญแŠแŠฉ แŠƒแ‹ญแˆˆแŠ› แ‹จแŠ แˆแƒแ€แˆ แˆ›แˆปแˆปแ‹ซแ‹Žแ‰ฝแŠ• แ‹ซแ‹ตแˆญแŒ‰". แ‰ฅแ‹™แ‹แŠ• แŒŠแ‹œ แˆ˜แ‹ฐแ‰ แŠ› แ‹˜แ‹ดแ‹Žแ‰ฝแŠ• แˆตแŠ•แŒ แ‰€แˆ แ‹แŒคแ‰ณแˆ› แ‹ซแˆแˆ†แŠ แŠฎแ‹ต แŠฅแŠ“แŒˆแŠ›แˆˆแŠ• - แ‰ แ‰ฐแŒแ‰ฃแˆญ แˆแˆ‰แˆ แŠแŒˆแˆญ แ‰ แ‰ตแŠญแŠญแˆ แ‰ฐแ‰ƒแˆซแŠ’ แŠแ‹. แ‰ แ‰ฐแŒจแˆ›แˆชแˆ, แ‹จแ•แˆฎแŒแˆซแˆ แŠ แ‹˜แŒ‹แŒ†แ‰ฝ แŒ แ‰ƒแˆšแŠแ‰ณแ‰ธแ‹แŠ• แ‰ขแ‹ซแˆแŠ‘แˆ, แŠ แˆตแ‰ฐแ‹ณแ‹ณแˆชแ‹Žแ‰ฝ แ‹จแˆ˜แ‹ฐแ‰ แŠ› แ‹˜แ‹ดแ‹Žแ‰ฝแŠ• แŠ แˆตแˆแˆ‹แŒŠแŠแ‰ต แˆ›แˆณแˆ˜แŠ• แŠฅแŠ•แ‹ฐแˆ›แ‹ญแ‰ฝแˆ‰ แŠ แˆตแ‰ฐแ‹ซแ‹จแ‰ต แŠ แˆˆ. แŠฅแŠ“ แŠ’แ‹แŠฎแˆแ‰ฅ แŠฅแŠ•แ‹ฒแˆ… แˆฒแˆ แŒฝแแˆ: "แŠ แˆตแ‰ฐแ‹ณแ‹ณแˆชแ‹Žแ‰ฝ แŠ แˆแŠ• แˆˆTLA + แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แˆˆแˆ˜แƒแ แŠฅแŠ“ แ‰ แ‰ฐแˆˆแ‹ญแˆ แˆˆแ‹šแˆ… แŒŠแ‹œ แˆˆแˆ˜แˆ˜แ‹ฐแ‰ฅ แ‰ แŒฃแˆ แŠฅแ‹จแŒฃแˆฉ แŠแ‹". แˆตแˆˆแ‹šแˆ… แŠ แˆตแ‰ฐแ‹ณแ‹ณแˆชแ‹Žแ‰ฝ TLA+ แŠฅแ‹จแˆฐแˆซ แˆ˜แˆ†แŠ‘แŠ• แˆฒแ‹ซแ‹ฉแฃ แ‰ แ‹ฐแˆตแ‰ณ แ‹ญแ‰€แ‰ แˆ‹แˆ‰แข แŠญแˆชแˆต แŠ’แ‹แŠฎแˆแ‰ฅ แ‹ญแˆ…แŠ•แŠ• แ‹จแŒปแˆแ‹ แŠจแˆตแ‹ตแˆตแ‰ต แ‹ˆแˆญ แ‰ แŠแ‰ต (แŒฅแ‰…แˆแ‰ต 2014) แˆฒแˆ†แŠ• แŠ แˆแŠ• แŒแŠ• แŠฅแŠ” แŠฅแˆตแŠจแˆ›แ‹แ‰€แ‹ แ‹ตแˆจแˆต TLA+ แ‰  14 แ•แˆฎแŒ€แŠญแ‰ถแ‰ฝ แ‹แˆตแŒฅ แŒฅแ‰…แˆ แˆ‹แ‹ญ แ‹ญแ‹แˆ‹แˆ แŠฅแŠ•แŒ‚ 10 แŠ แ‹ญแ‹ฐแˆˆแˆ. แˆŒแˆ‹แ‹ แˆแˆณแˆŒ แŠจ XBox 360 แŠ•แ‹ตแ แŒ‹แˆญ แ‹จแ‰ฐแ‹ซแ‹ซแ‹˜ แŠแ‹. แŠ แŠ•แ‹ต แ‰ฐแˆˆแˆ›แˆ›แŒ… แ‹ˆแ‹ฐ แ‰ปแˆญแˆแˆต แ‰ณแŠจแˆญ แˆ˜แŒฃ แŠฅแŠ“ แ‹จแˆ›แˆ…แ‹ฐแˆจ แ‰ตแ‹แˆตแ‰ณ แˆตแˆญแ‹“แ‰ต แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แŒฝแแˆ. แˆˆแ‹šแˆ… แŒˆแˆˆแŒป แˆแˆตแŒ‹แŠ“ แ‹ญแŒแ‰ฃแ‹แŠ“แฃ แ‹ซแˆˆแ‰ แˆˆแ‹šแ‹ซ แˆณแ‹ญแˆตแ‰ฐแ‹‹แˆ แ‹จแˆ›แ‹ญแ‰€แˆญ แˆตแˆ…แ‰ฐแ‰ต แ‰ฐแŒˆแŠ˜แฃ แŠฅแŠ“ แ‰ แ‹šแˆ… แˆแŠญแŠ•แ‹ซแ‰ต แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ XBox 360 แŠจแŠ แˆซแ‰ต แˆฐแŠ แ‰ณแ‰ต แŠ แŒ แ‰ƒแ‰€แˆ แ‰ แŠ‹แˆ‹ แ‹ญแ‹ˆแ‹ตแ‰ƒแˆแข แ‹จIBM แˆ˜แˆแŠ•แ‹ฒแˆถแ‰ฝ แˆ™แŠจแˆซแ‰ธแ‹ แ‹ญแˆ…แŠ•แŠ• แˆตแˆ…แ‰ฐแ‰ต แŠฅแŠ•แ‹ณแˆ‹แŒˆแŠ™แ‰ต แŠ แˆจแŒ‹แŒแŒ แ‹‹แˆแข

แ‰ แ‰ แ‹ญแŠแˆ˜แˆจแ‰ฅ แˆ‹แ‹ญ แˆตแˆˆ TLA + แ‹จแ‰ แˆˆแŒ  แˆ›แŠ•แ‰ แ‰ฅ แ‹ญแ‰ฝแˆ‹แˆ‰ แฃ แŒแŠ• แŠ แˆแŠ• แˆตแˆˆ แˆ˜แ‹ฐแ‰ แŠ› แ‹ซแˆแˆ†แŠ‘ แ‹แˆญแ‹แˆฎแ‰ฝ แŠฅแŠ•แŠแŒ‹แŒˆแˆญ แข แŠ แŠแˆตแ‰ฐแŠ›แ‹แŠ• แ‹จแŒ‹แˆซ แŠ แŠซแ‹แ‹ญ แŠฅแŠ“ แ‹จแˆ˜แˆณแˆฐแˆ‰แ‰ตแŠ• แ‹จแˆšแ‹ซแˆฐแˆ‰ แ•แˆฎแŒแˆซแˆžแ‰ฝแŠ• แˆ˜แƒแ แ‰ฅแ‹™แˆ แŠ แ‹ญแŒ แ‰ แ‰…แ‰ฅแŠ•แˆแข แ‰ฅแ‹™ แŒŠแ‹œ แˆˆ TLA+ แ‹จแŒปแแŠฉแ‰ตแŠ• แ‰†แŠ•แŒ†-แˆ›แ‰ฐแˆšแ‹ซ แˆ˜แˆณแˆชแ‹ซ แ‹จแˆ˜แˆณแˆฐแˆ‰ แ•แˆฎแŒแˆซแˆžแ‰ฝแŠ• แŠฅแŠ•แŒฝแ‹แˆˆแŠ•แข แ‰ แŒฃแˆ แ‰€แˆ‹แˆ แŠจแˆ†แŠแ‹ แˆ‚แ‹ฐแ‰ต แ‰ แŠ‹แˆ‹ แ‹จTLA + แŠฎแ‹ต แ‹ญแˆ…แŠ• แ‹ญแˆ˜แˆตแˆ‹แˆแข

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แŠแŒˆแˆญ แŒแŠ• แŠจแˆ‹แ‹ญ แ‰ฃแˆˆแ‹ แˆแˆณแˆŒแฃ แ‰ฐแŒ แ‰ƒแˆšแ‹ แˆแŠ“แˆแ‰ฃแ‰ต แŒฅแˆแˆจแ‰ฑ แŠฅแŠ“ แŠฅแŠฉแˆ แˆแˆแŠญแ‰ถแ‰ฝ แŠฅแŠ•แ‹ฒแˆตแˆ˜แˆฉ แ‹ญแˆแˆแŒ‰ แŠแ‰ แˆญแข แˆตแˆˆแ‹šแˆ… แ‰ตแŠญแŠญแˆˆแŠ›แ‹ แ‰…แˆญแŒธแ‰ต แ‹ญแˆ…แŠ• แ‹ญแˆ˜แˆตแˆ‹แˆแข

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แˆŒแˆ‹ แˆแˆณแˆŒ แ‹ฐแŒแˆž แŠฅแŠ•แˆ˜แˆแŠจแ‰ต-

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แŠฅแ‹šแˆ…แฃ แ‰ แ‰ฐแ‰ƒแˆซแŠ’แ‹แฃ แ‰ แˆแŠ•แŒฉ แ‹แˆตแŒฅ แ‹จแŠฅแŠฉแˆแฃ แ‹จแˆ˜แ‹ฐแˆ˜แˆญ แŠฅแŠ“ แ‹จแˆ›แ‰ฃแ‹›แ‰ต แˆแˆแŠญแ‰ถแ‰ฝ แŠ แˆฐแˆ‹แˆˆแ แ‰ แ‹˜แˆแ‰€แ‹ฐ แŠแ‰ แˆญแฃ แˆตแˆˆแ‹šแˆ… แ‰€แˆ‹แˆ‰ แŠ แˆฐแˆซแˆญ แ‰ แ‰‚ แŠแ‹แข แ‰ แŠ แŒ แ‰ƒแˆ‹แ‹ญ, แ‰ตแŠญแŠญแˆˆแŠ› แ‰…แˆญแŒธแ‰ต แ‰ตแŠญแŠญแˆˆแŠ› แ‹จแˆ‚แˆณแ‰ฅ แแ‰บ แ‹จแˆˆแˆ, แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แ‰ แ‹šแˆ… แŒ‰แ‹ณแ‹ญ แˆ‹แ‹ญ "แ‰ตแŠญแŠญแˆ" แˆ›แˆˆแ‰ต "แ‰ฐแŒ แ‰ƒแˆšแ‹ แ‹จแˆšแˆแˆแŒˆแ‹" แˆ›แˆˆแ‰ต แŠแ‹, แŠฅแŠ“ แ‹ญแˆ… แ‰ แˆ‚แˆณแ‰ฅ แˆŠแ‰ณแ‹ˆแ‰… แŠ แ‹ญแ‰ฝแˆแˆ.

แ‹จแŠฅแ‹แŠแ‰ต แแ‰บ แŠจแˆŒแˆˆแŠ• แˆตแ”แˆฒแŠแŠฌแˆฝแŠ‘ แŠจแŠ•แ‰ฑ แ‹ญแˆ˜แˆตแˆ‹แˆแข แŒแŠ• แŠ แ‹ญแ‹ฐแˆˆแˆ. แŠ แŠ•แ‹ต แ•แˆฎแŒแˆซแˆ แˆแŠ• แˆ›แ‹ตแˆจแŒ แŠฅแŠ•แ‹ณแˆˆแ‰ แ‰ต แˆตแˆˆแˆ›แŠ“แ‹แ‰… แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแˆฐแˆซ แˆ›แˆฐแ‰ฅ แŠ แ‹ซแˆตแˆแˆแŒˆแŠ•แˆ แˆ›แˆˆแ‰ต แŠ แ‹ญแ‹ฐแˆˆแˆ - แ‰ แ‰ฐแ‰ƒแˆซแŠ’แ‹ แ‹จแ‰ แˆˆแŒ  แŒฅแˆจแ‰ต แˆ›แ‹ตแˆจแŒ แŠ แˆˆแ‰ฅแŠ•. แˆ˜แŒแˆˆแŒซแ‹ แ‰ แ‰ฐแˆˆแ‹ญ แŠฅแ‹šแˆ… แŠ แˆตแˆแˆ‹แŒŠ แŠแ‹. แˆˆแ‰ฐแ‰€แŠแ‰ฃแ‰ แˆจ แˆ…แ‰ตแˆ˜แ‰ต แ‰ แŒฃแˆ แŒฅแˆฉแ‹แŠ• แ•แˆฎแŒแˆซแˆ แˆˆแˆ˜แ‹ˆแˆฐแŠ• แ‹จแˆ›แ‹ญแ‰ปแˆ แŠแ‹, แŠแŒˆแˆญ แŒแŠ• แ‹ญแˆ… แˆ›แˆˆแ‰ต แ‰ แŒญแˆซแˆฝ แˆ˜แ‹แˆฐแ‹ต แ‹จแˆˆแ‰ฅแŠ•แˆ แˆ›แˆˆแ‰ต แŠ แ‹ญแ‹ฐแˆˆแˆ, แŠฅแŠ“ แŠฅแŠ•แ‹ฐ แ‹จแŠ•แ‰ƒแ‰ฐ แˆ…แˆŠแŠ“ แ‹ฅแˆจแ‰ต แŠฎแ‹ต แˆ˜แŒปแ แŒฅแˆฉ แŠแŒˆแˆญ แŠ แ‹ญแ‹ฐแˆˆแˆ. แ‰ แˆ˜แŒจแˆจแˆป แฃ แ‹จแˆตแ‹ตแˆตแ‰ต แˆ…แŒŽแ‰ฝแŠ• แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แŠจแ‰ตแˆญแŒ‰แˆžแ‰ฝ แŒ‹แˆญ แŒปแแŠฉ แ‰ แŠ แˆตแ‰ฐแ‹ซแ‹จแ‰ถแ‰ฝ แˆ˜แˆแŠญ แ‰ แŒƒแ‰ซ แ‹แ‹ญแˆ แ‹แˆตแŒฅแข แŠจแˆ…แŒŽแ‰น แ‹แˆตแŒฅ แ‹จแŠ แŠ•แ‹ฑ แˆแˆณแˆŒ แ‹ญแŠธแ‹แŠ“แก- a left-comment token is LeftComment aligned with its covering token. แ‹ญแˆ… แˆ…แŒ แ‹จแ‰ฐแŒปแˆแ‹ แ‰ แˆ‚แˆณแ‰ฅ แŠฅแŠ•แŒแˆŠแ‹แŠ› แŠแ‹ แŠฅแŠ•แ‰ แˆแก- LeftComment aligned, left-comment ะธ covering token - แ‰ตแˆญแŒ“แˆœแ‹Žแ‰ฝ แŒ‹แˆญ แ‹แˆŽแ‰ฝ. แ‹จแˆ‚แˆณแ‰ฅ แˆŠแ‰ƒแ‹แŠ•แ‰ต แˆ’แˆณแ‰ฅแŠ• แ‹จแˆšแŒˆแˆแŒนแ‰ต แ‰ แ‹šแˆ… แˆ˜แŠ•แŒˆแ‹ต แŠแ‹แก แ‹จแ‰ƒแˆ‹แ‰ต แแ‰บแ‹Žแ‰ฝแŠ• แ‹ญแŒฝแ‹แˆ‰ แŠฅแŠ“ แ‰ แŠฅแŠแˆฑ แˆ‹แ‹ญ แ‰ฐแˆ˜แˆตแˆญแ‰ฐแ‹ แˆ•แŒŽแ‰ฝแŠ• แ‹ญแŒฝแ‹แˆ‰แข แ‹จแ‹šแˆ… แ‹“แ‹ญแŠแ‰ฑ แ‹แˆญแ‹แˆญ แŒฅแ‰…แˆ แŠจ 850 แ‹จแŠฎแ‹ต แˆ˜แˆตแˆ˜แˆฎแ‰ฝ แˆตแ‹ตแˆตแ‰ต แ‹ฐแŠ•แ‰ฆแ‰ฝ แˆˆแˆ˜แˆจแ‹ณแ‰ต แŠฅแŠ“ แˆˆแˆ›แˆจแˆ แ‰ แŒฃแˆ แ‰€แˆ‹แˆ แŠ“แ‰ธแ‹. แŠฅแŠแ‹šแˆ…แŠ• แ‹ฐแŠ•แ‰ฆแ‰ฝ แˆ˜แŒปแ แ‰€แˆ‹แˆ แŠ แˆแŠแ‰ แˆจแˆแฃ แŠฅแŠแˆฑแŠ• แˆˆแˆ›แˆจแˆ แ‰ฅแ‹™ แŒŠแ‹œ แ‹ˆแˆตแ‹ทแˆ แˆ›แˆˆแ‰ต แŠ แˆˆแ‰ฅแŠแข แ‰ แ‰ฐแˆˆแ‹ญ แˆˆแ‹šแˆ… แ‹“แˆ‹แˆ› แ‹จแ‰ตแŠ›แ‹ แ‹ฐแŠ•แ‰ฅ แŒฅแ‰…แˆ แˆ‹แ‹ญ แŠฅแŠ•แ‹ฐแ‹‹แˆˆ แ‹จแˆšแŒˆแˆแŒฝ แŠฎแ‹ต แŒปแแŠฉ. แŠฅแŠแ‹šแˆ…แŠ• แˆตแ‹ตแˆตแ‰ต แˆ…แŒŽแ‰ฝ แ‰ แ‰ แˆญแŠซแ‰ณ แˆแˆณแˆŒแ‹Žแ‰ฝ แˆตแˆˆแˆžแŠจแˆญแŠณแ‰ธแ‹ 850 แ‹จแŠฎแ‹ต แˆ˜แˆตแˆ˜แˆฎแ‰ฝแŠ• แˆ›แˆจแˆ แŠ แˆ‹แˆตแˆแˆˆแŒˆแŠแˆ แŠฅแŠ“ แˆตแˆ…แ‰ฐแ‰ถแ‰ฝแŠ• แˆˆแˆ›แŒแŠ˜แ‰ต แ‰ แŒฃแˆ แ‰€แˆ‹แˆ แˆ†แŠ– แ‰ฐแŒˆแŠแ‰ทแˆแข แŒƒแ‰ซ แˆˆแ‹šแˆ… แŒฅแˆฉ แˆ˜แˆณแˆชแ‹ซแ‹Žแ‰ฝ แŠ แˆ‰แ‰ต. แŠฎแ‹ฑแŠ• แŠ แˆแŠ• แ‰ฅแŒฝแ แŠ–แˆฎ แ‰ฅแ‹™ แŒŠแ‹œ แ‹ญแ‹ˆแˆตแ‹ตแ‰ฅแŠ แŠแ‰ แˆญแฃ แŠฅแŠ“ แ‰…แˆญแŒธแ‰ฑ แŒฅแˆซแ‰ต แ‹จแˆŒแˆˆแ‹ แ‹ญแˆ†แŠ• แŠแ‰ แˆญแข

แˆˆแˆแŠ• แˆ˜แ‹ฐแ‰ แŠ› แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แˆ˜แŒ แ‰€แˆ แŠ แˆแ‰ฐแ‰ปแˆˆแˆ? แ‰ แŠ แŠ•แ‹ต แ‰ แŠฉแˆ, แ‰ตแŠญแŠญแˆˆแŠ›แ‹ แŠ แˆแƒแ€แˆ แŠฅแ‹šแˆ… แ‰ แŒฃแˆ แŠ แˆตแˆแˆ‹แŒŠ แŠ แ‹ญแ‹ฐแˆˆแˆ. แˆ˜แ‹‹แ‰…แˆซแ‹Š แˆ…แ‰ตแˆ˜แ‰ถแ‰ฝ แˆ›แŠ•แŠ•แˆ แˆ‹แˆˆแˆ›แˆตแ‹ฐแˆฐแ‰ณแ‰ธแ‹ แ‹จแˆ›แ‹ญแ‰€แˆญ แŠแ‹แฃ แˆตแˆˆแ‹šแˆ… แ‰ แˆแˆ‰แˆ แ‹ซแˆแ‰ฐแˆˆแˆ˜แ‹ฑ แˆแŠ”แ‰ณแ‹Žแ‰ฝ แ‹แˆตแŒฅ แ‰ แ‰ตแŠญแŠญแˆ แŠฅแŠ•แ‹ฒแˆฐแˆซ แˆ›แ‹ตแˆจแŒ แŠ แˆ‹แˆตแˆแˆˆแŒˆแŠแˆแข แ‰ แŒฃแˆ แŠ แˆตแˆแˆ‹แŒŠแ‹ แŠแŒˆแˆญ แ‹ฐแŒแˆž แ‰ แ‰‚ แˆ˜แˆฃแˆชแ‹ซ แˆตแˆ‹แˆแŠแ‰ แˆจแŠ แŠแ‹แข แ‹จแ‰ฒแŠคแˆแŠค+ แˆžแ‹ดแˆ แŠ แˆซแˆš แŠฅแ‹šแˆ… แˆแŠ•แˆ แ‹แ‹ญแ‹ณ แ‹จแˆˆแ‹แˆแฃแˆตแˆˆแ‹šแˆ… แˆแˆณแˆŒแ‹Žแ‰นแŠ• แ‰ แŠฅแŒ… แˆ˜แŒปแ แŠ แˆˆแ‰ฅแŠแข

แŠจแˆ‹แ‹ญ แ‹ซแˆˆแ‹ แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แˆˆแˆแˆ‰แˆ แ‹แˆญแ‹แˆฎแ‰ฝ แ‹จแ‰ฐแˆˆแˆ˜แ‹ฑ แ‰ฃแˆ…แˆชแ‹ซแ‰ต แŠ แˆ‰แ‰ต. แŠจแŠฎแ‹ฑ แŠจแ แ‹ซแˆˆ แ‹ฐแˆจแŒƒ แŠแ‹แข แ‰ แˆ›แŠ•แŠ›แ‹แˆ แ‰‹แŠ•แ‰‹ แˆŠแ‰ฐแŒˆแ‰ แˆญ แ‹ญแ‰ฝแˆ‹แˆ. แˆˆแˆ˜แŒปแ แˆ›แŠ•แŠ›แ‰ธแ‹แˆ แˆ˜แˆณแˆชแ‹ซแ‹Žแ‰ฝ แ‹ˆแ‹ญแˆ แ‹˜แ‹ดแ‹Žแ‰ฝ แˆแŠ•แˆ แ‹แ‹ญแ‹ณ แ‹จแˆ‹แ‰ธแ‹แˆแข แ‹ญแˆ…แŠ•แŠ• แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แˆˆแˆ˜แŒปแ แˆแŠ•แˆ แ‹จแ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠฎแˆญแˆต แŠ แ‹ญแˆจแ‹ณแ‹Žแ‰ตแˆแข แŠฅแŠ“ แŠฅแˆญแˆตแ‹Ž แ‰ TLA+ แ‹แˆตแŒฅ แ‹จแ‰ฐแ‹‹แ‰€แˆฉ แ‹จแˆ•แ‰ตแˆ˜แ‰ต แ•แˆฎแŒแˆซแˆžแ‰ฝแŠ• แˆˆแˆ˜แŒปแ แ‰ แ‰ฐแˆˆแ‹ญ แ‰‹แŠ•แ‰‹ แŠฅแ‹จแŒปแ‰ แŠซแˆแˆ†แŠ แ‰ แˆตแ‰ฐแ‰€แˆญ แ‹ญแˆ…แŠ•แŠ• แˆ˜แŒแˆˆแŒซ แŠ แˆ‹แˆตแˆแˆ‹แŒŠ แˆŠแ‹ซแ‹ฐแˆญแŒ“แ‰ธแ‹ แ‹จแˆšแ‰ฝแˆ‰ แˆแŠ•แˆ แˆ˜แˆฃแˆชแ‹ซแ‹Žแ‰ฝ แ‹จแˆ‰แˆแข แ‰ แˆ˜แŒจแˆจแˆปแˆ, แ‹ญแˆ… แ‹แˆญแ‹แˆญ แŠฎแ‹ต แ‰ แ‰ตแŠญแŠญแˆ แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆแŠ•แŒฝแ แˆแŠ•แˆ แŠ แ‹ญแŠ“แŒˆแˆญแˆ, แ‹ญแˆ… แŠฎแ‹ต แˆแŠ• แŠฅแŠ•แ‹ฐแˆšแˆฐแˆซ แ‰ฅแ‰ป แŠแ‹ แ‹จแˆšแŠ“แŒˆแˆจแ‹. แˆตแˆˆ แŠฎแ‹ฑ แˆ›แˆฐแ‰ฅ แŠจแˆ˜แŒ€แˆ˜แˆซแ‰ฝแŠ• แ‰ แŠแ‰ต แ‰ฝแŒแˆฉแŠ• แˆˆแˆ›แˆฐแ‰ฅ แŠฅแŠ•แ‹ฒแˆจแ‹ณแŠ• แˆ˜แŒแˆˆแŒซแ‹แŠ• แŠฅแŠ•แŒฝแ‹แˆˆแŠ•แข

แŠแŒˆแˆญ แŒแŠ• แ‹ญแˆ… แ‹แˆญแ‹แˆญ แŠจแˆŒแˆŽแ‰ฝ แˆ˜แˆ˜แ‹˜แŠ›แ‹Žแ‰ฝ แ‹จแˆšแˆˆแ‹ฉแ‰ต แ‰ฃแˆ…แˆชแ‹ซแ‰ตแˆ แŠ แˆ‰แ‰ต. 95% แ‹จแˆšแˆ†แŠ‘แ‰ต แˆŒแˆŽแ‰ฝ แ‹แˆญแ‹แˆฎแ‰ฝ แ‰ แŒฃแˆ แŠ แŒญแˆญ แŠฅแŠ“ แ‰€แˆ‹แˆ แŠ“แ‰ธแ‹แก

แ•แˆฎแŒแˆซแˆšแŠ•แŒ แŠจแŠฎแ‹ต แ‰ แˆ‹แ‹ญ แŠแ‹แข

แ‰ แ‰ฐแŒจแˆ›แˆชแˆ, แ‹ญแˆ… แ‹แˆญแ‹แˆญ แ‹ฐแŠ•แ‰ฆแ‰ฝ แˆตแ‰ฅแˆตแ‰ฅ แŠแ‹. แŠฅแŠ•แ‹ฐ แŠ แŠ•แ‹ต แ‹ฐแŠ•แ‰ฅ, แ‹ญแˆ… แ‹ฐแŠซแˆ› แ‹แˆญแ‹แˆญ แˆแˆแŠญแ‰ต แŠแ‹. แ‹จแˆ•แŒŽแ‰ฝ แˆตแ‰ฅแˆตแ‰ฅ แ‹จแˆšแ‹ซแˆตแŠจแ‰ตแˆˆแ‹แŠ• แˆ˜แ‹˜แ‹ แˆ˜แˆจแ‹ณแ‰ต แ‰ แŒฃแˆ แŠจแ‰ฃแ‹ต แŠแ‹แฃ แˆˆแ‹šแˆ…แˆ แŠแ‹ แŠฅแŠแˆฑแŠ• แˆˆแˆ›แˆจแˆ แ‰ฅแ‹™ แŒŠแ‹œ แˆ›แˆณแˆˆแ แ‹จแŠแ‰ แˆจแ‰ฅแŠแข แˆ†แŠ–แˆ แŒแŠ•, แ‰ แ‹šแˆ… แˆแŠ”แ‰ณ, แ‹จแ‰ฐแˆปแˆˆ แˆ˜แŠ•แŒˆแ‹ต แˆ›แŒแŠ˜แ‰ต แŠ แˆแ‰ปแˆแŠฉแˆ.

แ‹ซแˆˆแˆ›แ‰‹แˆจแŒฅ แˆตแˆˆแˆšแˆ แˆฉ แ•แˆฎแŒแˆซแˆžแ‰ฝ แŒฅแ‰‚แ‰ต แ‰ƒแˆ‹แ‰ต แˆ˜แŠ“แŒˆแˆญ แ‰ฐแŒˆแ‰ข แŠแ‹แข แŠฅแŠ•แ‹ฐ แŠ แŠ•แ‹ต แ‹ฐแŠ•แ‰ฅ, แ‰ แ‰ตแ‹ญแ‹ฉ แ‹ญแˆฐแˆซแˆ‰, แˆˆแˆแˆณแˆŒ, แˆตแˆญแ‹“แ‰ฐ แŠญแ‹ˆแŠ“แ‹Žแ‰ฝ แ‹ˆแ‹ญแˆ แ‹จแ‰ฐแŠจแ‹แˆแˆ‰ แˆตแˆญแ‹“แ‰ถแ‰ฝ. แ‰ แŒฃแˆ แŒฅแ‰‚แ‰ต แˆฐแ‹Žแ‰ฝ แ‰ แŠ แŠฅแˆแˆฏแ‹Šแˆ แˆ†แŠ แ‰ แ‹ˆแˆจแ‰€แ‰ต แˆŠแˆจแ‹ทแ‰ธแ‹ แ‹ญแ‰ฝแˆ‹แˆ‰, แŠฅแŠ“ แŠฅแŠ” แŠจแŠแˆฑ แŠ แŠ•แ‹ฑ แŠ แ‹ญแ‹ฐแˆˆแˆแˆ, แˆแŠ•แˆ แŠฅแŠ•แŠณแŠ• แŠ แŠ•แ‹ต แŒŠแ‹œ แˆ›แ‹ตแˆจแŒ แ‰ฅแ‰ฝแˆแˆ. แˆตแˆˆแ‹šแˆ… แˆตแˆซแ‰ฝแŠ•แŠ• แ‹จแˆšแˆแ‰ตแˆน แˆ˜แˆณแˆชแ‹ซแ‹Žแ‰ฝ แ‹ซแˆตแˆแˆแŒ‰แŠ“แˆ - แˆˆแˆแˆณแˆŒ TLA + แ‹ˆแ‹ญแˆ PlusCalแข

แŠฎแ‹ฑ แ‰ แ‰ตแŠญแŠญแˆ แˆแŠ• แˆ›แ‹ตแˆจแŒ แŠฅแŠ•แ‹ณแˆˆแ‰ แ‰ต แŠซแ‹ˆแ‰…แŠฉ แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แˆ˜แŒปแ แˆˆแˆแŠ• แŠ แˆตแˆแˆˆแŒˆ? แŠฅแŠ•แ‹ฐแ‹แˆ แ‹จแˆ›แ‹แ‰€แ‹ แˆ˜แˆฐแˆˆแŠแข แ‰ แ‰ฐแŒจแˆ›แˆชแˆแฃ แ‰ แˆ˜แŒแˆˆแŒซแ‹แฃ แŠ แŠ•แ‹ต แ‹จแ‹แŒญ แˆฐแ‹ แ‰ แ‰ตแŠญแŠญแˆ แ‹จแˆšแ‹ซแ‹ฐแˆญแŒˆแ‹แŠ• แˆˆแˆ˜แˆจแ‹ณแ‰ต แŠจแŠ แˆแŠ• แ‰ แŠ‹แˆ‹ แ‹ˆแ‹ฐ แŠฎแ‹ต แˆ˜แŒแ‰ฃแ‰ต แŠ แ‹ซแˆตแˆแˆแŒˆแ‹แˆแข แˆ…แŒ แŠ แˆˆแŠแก แŠ แŒ แ‰ƒแˆ‹แ‹ญ แˆ…แŒŽแ‰ฝ แˆŠแŠ–แˆฉ แŠ แ‹ญแŒˆแ‰ฃแˆแข แˆˆแ‹šแˆ… แˆ…แŒ แ‹จแ‰ฐแˆˆแ‹จ แŠแŒˆแˆญ แŠ แˆˆแฃ แ‰ แŠฅแˆญแŒแŒฅแฃ แŠฅแŠ” แ‹จแˆแŠจแ‰ฐแˆˆแ‹ แŠ แŒ แ‰ƒแˆ‹แ‹ญ แˆ…แŒ แŠฅแˆฑ แ‰ฅแ‰ป แŠแ‹แก แŠฎแ‹ฑ แ‹จแˆšแˆฐแˆซแ‹ แŠแŒˆแˆญ แ‹แˆญแ‹แˆญ แŠฎแ‹ต แˆฒแŒ แ‰€แˆ™ แˆ›แ‹ˆแ‰… แ‹ซแˆˆแ‰ฃแ‰ธแ‹แŠ• แˆแˆ‰ แˆˆแˆฐแ‹Žแ‰ฝ แˆ˜แŠ•แŒˆแˆญ แŠ แˆˆแ‰ แ‰ตแข

แˆตแˆˆแ‹šแˆ… แ•แˆฎแŒแˆซแˆ˜แˆฎแ‰ฝ แˆตแˆˆ แˆ›แˆฐแ‰ฅ แ‰ แ‰ตแŠญแŠญแˆ แˆแŠ• แˆ›แ‹ˆแ‰… แŠ แˆˆแ‰ฃแ‰ธแ‹? แˆˆแŒ€แˆ›แˆชแ‹Žแ‰ฝ แฃ แŠฅแŠ•แ‹ฐแˆ›แŠ•แŠ›แ‹แˆ แˆฐแ‹ แฃ แŠฅแˆญแˆตแ‹Ž แŠซแˆแƒแ‰ แฃ แŠฅแˆญแˆตแ‹Ž แŠฅแ‹ซแˆฐแ‰ก แ‰ฅแ‰ป แŠแ‹ แ‹จแˆšแˆ˜แˆตแˆˆแ‹แข แŠฅแŠ•แ‹ฒแˆแˆ แŠฎแ‹ต แŠจแˆ›แ‹ตแˆจแŒแ‹Ž แ‰ แŠแ‰ต แˆ›แˆฐแ‰ฅ แŠ แˆˆแ‰ฅแ‹Žแ‰ต, แ‹ญแˆ…แˆ แˆ›แˆˆแ‰ต แŠฎแ‹ต แŠจแˆ›แˆตแ‰€แˆ˜แŒฅแ‹Ž แ‰ แŠแ‰ต แˆ˜แŒปแ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ. แˆ˜แŒแˆˆแŒซแ‹ แŠฎแ‹ต แˆ›แ‹ตแˆจแŒ แŠจแˆ˜แŒ€แˆ˜แˆซแ‰ฝแŠ• แ‰ แŠแ‰ต แ‹จแˆแŠ•แŒฝแˆแ‹ แŠแ‹แข แˆ›แŠ•แŠ›แ‹แˆ แˆฐแ‹ แˆŠแŒ แ‰€แˆแ‰ แ‰ต แ‹ˆแ‹ญแˆ แˆŠแˆปแˆปแˆ แˆˆแˆšแ‰ฝแˆ แŠฎแ‹ต แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แ‹ซแˆตแˆแˆแŒ‹แˆแข แŠฅแŠ“ แ‹ญแˆ… "แŠ แŠ•แ‹ต แˆฐแ‹" แŠจแ‰ฐแŒปแˆ แŠจแŠ แŠ•แ‹ต แ‹ˆแˆญ แ‰ แŠ‹แˆ‹ แŠฅแˆซแˆฑ แ‹จแŠฎแ‹ฑ แ‹ฐแˆซแˆฒ แˆŠแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆ. แˆˆแ‰ตแˆ‹แˆแ‰… แ•แˆฎแŒแˆซแˆžแ‰ฝ แŠฅแŠ“ แˆตแˆญแ‹“แ‰ถแ‰ฝ, แˆˆแŠญแแˆŽแ‰ฝ, แˆˆแˆตแˆแ‰ถแ‰ฝ แŠฅแŠ“ แŠ แŠ•แ‹ณแŠ•แ‹ดแˆ แ‹แˆตแ‰ฅแˆตแ‰ฅ แˆˆแˆ†แŠ‘ แ‹จแŠ แŠ•แ‹ต แ‹˜แ‹ด แŠญแแˆŽแ‰ฝ แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แ‹ซแˆตแˆแˆแŒ‹แˆ. แˆตแˆˆ แŠฎแ‹ฑ แ‰ แ‰ตแŠญแŠญแˆ แˆแŠ• แˆ˜แƒแ แŠ แˆˆแ‰ แ‰ต? แˆแŠ• แŠฅแŠ•แ‹ฐแˆšแˆฐแˆซ แˆ›แˆˆแ‰ตแˆ แ‹ญแˆ…แŠ•แŠ• แŠฎแ‹ต แˆˆแˆšแŒ แ‰€แˆ แˆˆแˆ›แŠ•แŠ›แ‹แˆ แˆฐแ‹ แˆแŠ• แˆŠแŒ แ‰…แˆ แŠฅแŠ•แ‹ฐแˆšแ‰ฝแˆ แˆ˜แŒแˆˆแŒฝ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆแข แŠ แŠ•แ‹ณแŠ•แ‹ต แŒŠแ‹œ แŠฎแ‹ฑ แ‹“แˆ‹แˆ›แ‹แŠ• แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแˆแŒฝแˆ แˆ˜แŒแˆˆแŒฝ แŠ แˆตแˆแˆ‹แŒŠ แˆŠแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆ. แ‹ญแˆ…แŠ•แŠ• แ‹˜แ‹ด แ‰ แŠ แˆแŒŽแˆชแ‹แˆ แˆ‚แ‹ฐแ‰ต แ‹แˆตแŒฅ แŠซแˆˆแแŠ•, แŠจแ‹šแ‹ซแˆ แŠ แˆแŒŽแˆชแ‹แˆ แ‰ฅแˆˆแŠ• แŠฅแŠ•แŒ แˆซแ‹‹แˆˆแŠ•. แ‹จแ‰ แˆˆแŒ  แˆแ‹ฉ แŠฅแŠ“ แŠ แ‹ฒแˆต แŠแŒˆแˆญ แŠจแˆ†แŠ, แŠจแแ‰ฐแŠ› แ‹ฐแˆจแŒƒ แŠ•แ‹ตแ แ‰ฅแˆˆแŠ• แŠฅแŠ•แŒ แˆซแ‹‹แˆˆแŠ•. แŠฅแ‹šแˆ… แˆแŠ•แˆ แŠ แ‹ญแŠแ‰ต แˆ˜แ‹ฐแ‰ แŠ› แˆแ‹ฉแŠแ‰ต แ‹จแˆˆแˆแก แˆแˆˆแ‰ฑแˆ แ‹จแ•แˆฎแŒแˆซแˆ แŠ แ‰ฅแˆตแ‰ตแˆซแŠญแ‰ต แˆžแ‹ดแˆ แŠ“แ‰ธแ‹แข

แ‹จแŠฎแ‹ต แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แŠฅแŠ•แ‹ดแ‰ต แ‰ แ‰ตแŠญแŠญแˆ แˆ˜แŒปแ แŠ แˆˆแ‰ฅแ‹Žแ‰ต? แ‹‹แŠ“แ‹ แŠแŒˆแˆญ: แŠจแŠฎแ‹ฑ แˆซแˆฑ แŠ แŠ•แ‹ต แ‹ฐแˆจแŒƒ แŠจแ แ‹ซแˆˆ แˆ˜แˆ†แŠ• แŠ แˆˆแ‰ แ‰ต. แŒแ‹›แ‰ถแ‰ฝแŠ• แŠฅแŠ“ แ‰ฃแˆ…แˆชแ‹ซแ‰ตแŠ• แˆ˜แŒแˆˆแŒฝ แŠ แˆˆแ‰ แ‰ต. แ‰ฐแŒแ‰ฃแˆฉ แ‹จแˆšแˆแˆแŒˆแ‹แŠ• แ‹ซแˆ…แˆ แŒฅแ‰ฅแ‰… แˆ˜แˆ†แŠ• แŠ แˆˆแ‰ แ‰ต. แŠ แŠ•แ‹ต แ‰ฐแŒแ‰ฃแˆญ แŠฅแŠ•แ‹ดแ‰ต แˆ˜แ‰ฐแŒแ‰ แˆญ แŠฅแŠ•แ‹ณแˆˆแ‰ แ‰ต แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แŠฅแ‹จแŒปแ‰ แŠจแˆ†แŠแฃ แ‰ pseudocode แ‹ˆแ‹ญแˆ แ‰ แ•แˆ‹แˆตแŠซแˆ แˆ˜แŒปแ แ‹ญแ‰ฝแˆ‹แˆ‰แข แ‰ แˆ˜แ‹ฐแ‰ แŠ› แ‹แˆญแ‹แˆฎแ‰ฝ แˆ‹แ‹ญ แ‹แˆญแ‹แˆฎแ‰ฝแŠ• แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแŒฝแ‰ แˆ˜แˆ›แˆญ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ. แ‹ญแˆ… แˆ˜แ‹ฐแ‰ แŠ› แ‰ฃแˆแˆ†แŠ‘ แˆฐแ‹Žแ‰ฝ แˆ‹แ‹ญแˆ แ‹จแˆšแˆจแ‹ณแ‹Žแ‰ตแŠ• แŠ แˆตแˆแˆ‹แŒŠ แŠญแˆ…แˆŽแ‰ถแ‰ฝ แ‹ญแˆฐแŒฅแ‹Žแ‰ณแˆ. แˆ˜แ‹ฐแ‰ แŠ› แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แŠฅแŠ•แ‹ดแ‰ต แˆ˜แŒปแ แ‹ญแˆ›แˆซแˆ‰? แ•แˆฎแŒแˆซแˆ แˆ›แ‹ตแˆจแŒแŠ• แˆตแŠ•แˆ›แˆญ แ•แˆฎแŒแˆซแˆžแ‰ฝแŠ• แŒปแแŠ• แŠจแ‹šแ‹ซแˆ แŠ แˆซแˆแŠ•แข แŠฅแ‹šแˆ… แŒ‹แˆญ แ‰ฐแˆ˜แˆณแˆณแ‹ญ แŠแ‹: แˆตแ”แŠญแ‰ฐแˆฉแŠ• แ‹ญแƒแ‰, แ‰ แŠ แˆแˆณแ‹ซแ‹ แŠ แˆจแŒ‹แŒ‹แŒญ แ‹ซแˆจแŒ‹แŒแŒก แŠฅแŠ“ แˆตแˆ…แ‰ฐแ‰ถแ‰ฝแŠ• แ‹ซแˆตแ‰ฐแŠซแŠญแˆ‰. TLA+ แˆˆแˆ˜แ‹ฐแ‰ แŠ› แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝ แˆแˆญแŒก แ‰‹แŠ•แ‰‹ แˆ‹แ‹ญแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆแฃ แŠฅแŠ“ แˆŒแˆ‹ แ‰‹แŠ•แ‰‹ แˆˆแŠฅแˆญแˆตแ‹Ž แˆแ‹ฉ แแˆ‹แŒŽแ‰ต แ‹จแ‰ฐแˆปแˆˆ แˆŠแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆแข แ‹จTLA+ แŒฅแ‰…แˆ™ แ‹จแˆ‚แˆณแ‰ฅ แŠ แˆตแ‰ฐแˆณแˆฐแ‰ฅแŠ• แ‰ แ‹ฐแŠ•แ‰ฅ แˆ›แˆตแ‰ฐแˆ›แˆญ แŠแ‹แข

แˆ˜แŒแˆˆแŒซ แŠฅแŠ“ แŠฎแ‹ต แŠฅแŠ•แ‹ดแ‰ต แˆ›แŒˆแŠ“แŠ˜แ‰ต แ‹ญแ‰ปแˆ‹แˆ? แ‹จแˆ‚แˆณแ‰ฅ แ…แŠ•แˆฐ-แˆ€แˆณแ‰ฆแ‰ฝแŠ• แŠฅแŠ“ แŠ แ‰ฐแŒˆแ‰ฃแ‰ แˆญแŠ• แ‰ แˆšแ‹ซแŒˆแŠ“แŠ™ แŠ แˆตแ‰ฐแ‹ซแ‹จแ‰ถแ‰ฝ แŠฅแŒˆแ‹›แข แŠจแŒแˆซแŽแ‰ฝ แŒ‹แˆญ แ‹จแˆšแˆฐแˆฉ แŠจแˆ†แŠ แ‰ แ•แˆฎแŒแˆซแˆ™ แ‹ฐแˆจแŒƒ แ‹จแŠ แŠ•แŒ“แ‹Žแ‰ฝ แŠฅแŠ“ แ‹จแŠ แŒˆแŠ“แŠžแ‰ฝ แ‹ตแˆญแ‹ตแˆญ แ‹ญแŠ–แˆฉแ‹Žแ‰ณแˆแข แˆตแˆˆแ‹šแˆ…, แŒแˆซแ‰ แ‰ แŠฅแŠแ‹šแˆ… แ‹จแ•แˆฎแŒแˆซแˆ แŠ แ‹ˆแ‰ƒแ‰€แˆฎแ‰ฝ แŠฅแŠ•แ‹ดแ‰ต แŠฅแŠ•แ‹ฐแˆšแ‰ฐแŒˆแ‰ แˆญ แ‰ แ‰ตแŠญแŠญแˆ แˆ˜แŒปแ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ.

แŠจแˆ‹แ‹ญ แŠจแ‰ฐแŒ แ‰€แˆฑแ‰ต แ‹แˆตแŒฅ แŠ แŠ•แ‹ณแ‰ธแ‹แˆ แ‰ขแˆ†แŠ‘ แ‰ตแŠญแŠญแˆˆแŠ›แ‹แŠ• แŠฎแ‹ต แ‹จแˆ˜แŒปแ แˆ‚แ‹ฐแ‰ต แŠฅแŠ•แ‹ฐแˆ›แ‹ญแˆ˜แˆˆแŠจแ‰ฑ แˆแ‰ฅ แˆŠแ‰ฃแˆ แ‹ญแŒˆแ‰ฃแˆ. แŠฎแ‹ฑแŠ• แˆฒแŒฝแ‰, แˆ›แˆˆแ‰ตแˆ, แˆถแˆตแ‰ฐแŠ›แ‹แŠ• แ‹ฐแˆจแŒƒ แ‹ซแŠจแŠ“แ‹แŠ“แˆ‰, แŠฅแŠ•แ‹ฒแˆแˆ แ‰ แ•แˆฎแŒแˆซแˆ™ แ‹แˆตแŒฅ แˆ›แˆฐแ‰ฅ แŠฅแŠ“ แˆ›แˆฐแ‰ฅ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ. แŠ แŠ•แ‹ต แŠ•แ‹‘แˆต แˆฅแˆซ แ‹แˆตแ‰ฅแˆตแ‰ฅ แ‹ˆแ‹ญแˆ แŒแˆแŒฝ แŠซแˆแˆ†แŠ, แˆˆแŠฅแˆฑ แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซ แˆ˜แŒปแ แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ. แŠฅแŠ” แŒแŠ• แŠฅแ‹šแˆ… แˆตแˆˆ แŠฎแ‹ฑ แˆซแˆฑ แŠ แˆ‹แ‹ˆแˆซแˆแข แˆ›แŠ•แŠ›แ‹แŠ•แˆ แ‹จแ•แˆฎแŒแˆซแˆšแŠ•แŒ แ‰‹แŠ•แ‰‹ แฃ แˆ›แŠ•แŠ›แ‹แŠ•แˆ แ‹˜แ‹ด แˆ˜แŒ แ‰€แˆ แ‹ญแ‰ฝแˆ‹แˆ‰ แฃ แŠฅแˆฑ แˆตแˆˆแŠฅแŠแˆฑ แŠ แ‹ญแ‹ฐแˆˆแˆแข แŠฅแŠ•แ‹ฒแˆแˆ, แŠจแˆ‹แ‹ญ แŠจแ‰ฐแŒ แ‰€แˆฑแ‰ต แ‹แˆตแŒฅ แ‹จแ‰ตแŠ›แ‹แˆ แŠฎแ‹ตแŠ• แˆ˜แˆžแŠจแˆญ แŠฅแŠ“ แˆ›แˆจแˆ แŠ แ‹ซแˆตแˆแˆแŒแˆ. แ‹จแŠ แ‰ฅแˆตแ‰ตแˆซแŠญแ‰ต แˆžแ‹ดแˆ แ‰ แ‰ตแŠญแŠญแˆ แ‹จแ‰ฐแŒปแˆ แ‰ขแˆ†แŠ•แˆ แŠฅแŠ•แŠณ แ‰ แŠ แ‰ฐแŒˆแ‰ฃแ‰ แˆฉ แˆ‹แ‹ญ แˆตแˆ…แ‰ฐแ‰ถแ‰ฝ แˆŠแŠ–แˆฉ แ‹ญแ‰ฝแˆ‹แˆ‰.

แ‹แˆญแ‹แˆฎแ‰ฝแŠ• แˆ˜แŒปแ แ‰ แŠฎแ‹ต แˆ‚แ‹ฐแ‰ต แ‹แˆตแŒฅ แ‰ฐแŒจแˆ›แˆช แŠฅแˆญแˆแŒƒ แŠแ‹แข แˆˆแŠฅแˆฑ แˆแˆตแŒ‹แŠ“ แ‹ญแŒแ‰ฃแ‹แŠ“ แ‰ฅแ‹™ แˆตแˆ…แ‰ฐแ‰ถแ‰ฝ แ‰ แ‰ตแŠ•แˆฝ แŒฅแˆจแ‰ต แˆŠแ‹ซแ‹™ แ‹ญแ‰ฝแˆ‹แˆ‰ - แ‹ญแˆ…แŠ•แŠ• แŠจแŠ แˆ›แ‹žแŠ• แ‹จแ•แˆฎแŒแˆซแˆ แŠ แ‹˜แŒ‹แŒ†แ‰ฝ แˆแˆแ‹ต แŠฅแŠ“แ‹แ‰ƒแˆˆแŠ•แข แŠจแ‹แˆญแ‹แˆฎแ‰ฝ แŒ‹แˆญ, แ‹จแ•แˆฎแŒแˆซแˆžแ‰ฝ แŒฅแˆซแ‰ต แŠจแ แ‹ซแˆˆ แ‹ญแˆ†แŠ“แˆ. แ‰ณแ‹ฒแ‹ซ แˆˆแˆแŠ•แ‹ตแŠแ‹ แ‰ฅแ‹™ แŒŠแ‹œ แ‹ซแˆˆ แŠฅแŠแˆญแˆฑ แ‹จแˆแŠ•แˆ„แ‹ฐแ‹? แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แˆ˜แŒปแ แŠจแ‰ฃแ‹ต แŠแ‹แข แŠฅแŠ“ แˆ˜แŒปแ แŠจแ‰ฃแ‹ต แŠแ‹, แˆแŠญแŠ•แ‹ซแ‰ฑแˆ แˆˆแ‹šแˆ… แˆ›แˆฐแ‰ฅ แŠ แˆˆแ‰ฅแ‹Žแ‰ต, แŠฅแŠ“ แˆ›แˆฐแ‰ฅแˆ แŠ แˆตแ‰ธแŒ‹แˆช แŠแ‹. แ‹ซแˆฐแ‰กแ‰ตแŠ• แˆ›แˆตแˆ˜แˆฐแˆ แˆแˆ แŒŠแ‹œ แ‰€แˆ‹แˆ แŠแ‹แข แŠฅแ‹šแˆ… แŠจแˆฉแŒซ แŒ‹แˆญ แ‰ฐแˆ˜แˆณแˆณแ‹ญแŠแ‰ต แˆ˜แˆณแˆ แ‹ญแ‰ฝแˆ‹แˆ‰ - แ‰ฃแŠแˆฐแ‹Žแ‰ต แˆ˜แŒ แŠ• แฃ แŠฅแ‹จแˆฎแŒก แ‹ญแˆ„แ‹ณแˆแข แŒกแŠ•แ‰ปแ‹Žแ‰ตแŠ• แˆ›แˆฐแˆแŒ แŠ• แŠฅแŠ“ แˆ˜แŒปแ แˆ˜แˆˆแˆ›แˆ˜แ‹ต แ‹ซแˆตแˆแˆแŒแ‹Žแ‰ณแˆ. แˆแˆแˆแ‹ต แ‹ซแˆตแˆแˆแŒ‹แˆแข

แˆ˜แŒแˆˆแŒซแ‹ แ‰ตแŠญแŠญแˆ แˆ‹แ‹ญแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆแข แ‹จแˆ†แŠ แ‰ฆแ‰ณ แˆ‹แ‹ญ แˆตแˆ…แ‰ฐแ‰ต แˆฐแˆญแ‰ฐแˆ… แˆŠแˆ†แŠ• แ‹ญแ‰ฝแˆ‹แˆแฃ แ‹ˆแ‹ญแˆ แˆ˜แˆตแˆแˆญแ‰ถแ‰น แ‰ฐแˆˆแ‹แŒ แ‹‹แˆ แ‹ˆแ‹ญแˆ แˆ˜แˆปแˆปแˆ แˆŠแŠ–แˆญแ‰ฅแˆ… แ‹ญแ‰ฝแˆ‹แˆแข แˆ›แŠ•แŠ›แ‹แˆ แˆฐแ‹ แ‹จแˆšแŒ แ‰€แˆแ‰ แ‰ต แŠฎแ‹ต แˆ˜แ‰€แ‹จแˆญ แŠ แˆˆแ‰ แ‰ตแฃ แˆตแˆˆแ‹šแˆ… แ‹ญแ‹‹แˆ แ‹ญแ‹ฐแˆญ แŠฅแŠ•แŒ‚ แˆ˜แŒแˆˆแŒซแ‹ แŠจแ•แˆฎแŒแˆซแˆ™ แŒ‹แˆญ แŠ แ‹ญแ‹›แˆ˜แ‹ตแˆแข แ‰ แˆแˆณแ‰ฅ แ‹ฐแˆจแŒƒ, แ‰ แ‹šแˆ… แˆแŠ”แ‰ณ แ‹แˆตแŒฅ, แŠ แ‹ฒแˆต แ‹แˆญแ‹แˆญ แˆ˜แŒปแ แŠฅแŠ“ แˆ™แˆ‰ แ‰ แˆ™แˆ‰ แ‰ แ‹ตแŒ‹แˆš แˆ˜แŒปแ แŠ แˆˆแ‰ฅแ‹Žแ‰ต. แˆ›แŠ•แˆ แ‹ซแŠ•แŠ• แŠฅแŠ•แ‹ฐแˆ›แ‹ซแ‹ฐแˆญแŒ แŒ แŠ•แ‰…แ‰€แŠ• แŠฅแŠ“แ‹แ‰ƒแˆˆแŠ•แข แ‰ แ‰ฐแŒแ‰ฃแˆญ แฃ แŠฎแ‹ฑแŠ• แŠฅแŠ“แˆตแ‰ฐแŠซแŠญแˆ‹แˆˆแŠ• แŠฅแŠ“ แˆแŠ“แˆแ‰ฃแ‰ต แˆ˜แŒแˆˆแŒซแ‹แŠ• แŠฅแŠ“แ‹˜แˆแŠแ‹‹แˆˆแŠ•แข แ‹ญแˆ… แˆแŒฅแŠ–แˆ แ‹ญแˆแŠ• แ‹˜แŒแ‹ญแ‰ถ แˆ˜แŠจแˆฐแ‰ฑ แ‹จแˆ›แ‹ญแ‰€แˆญ แŠจแˆ†แŠ แˆˆแˆแŠ• แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แ‹ญแƒแ‰? แ‰ แˆ˜แŒ€แˆ˜แˆชแ‹ซแฃ แŠฎแ‹ตแ‹ŽแŠ• แˆˆแˆšแˆˆแ‹แŒฅ แˆฐแ‹แฃ แ‰ แ‹แˆญแ‹แˆฉ แ‹แˆตแŒฅ แ‹ซแˆˆแ‹ แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แ‰ฐแŒจแˆ›แˆช แ‰ƒแˆ แŠญแ‰ฅแ‹ฐแ‰ฑ แ‰ แ‹ˆแˆญแ‰… แŠแ‹แฃ แŠฅแŠ“ แ‹ญแˆ… แˆฐแ‹ แŠฅแˆญแˆตแ‹Ž แŠฅแˆซแˆตแ‹Ž แˆŠแˆ†แŠ‘ แ‹ญแ‰ฝแˆ‹แˆ‰แข แŠฅแŠ” แ‰ฅแ‹™ แŒŠแ‹œ แ‹จแŠฅแŠ”แŠ• แŠฎแ‹ต แŠ แˆญแ‰ตแ‹–แ‰ต แ‰ แˆแˆ†แŠ•แ‰ แ‰ต แŒŠแ‹œ แ‰ แ‰‚ แˆ˜แŒแˆˆแŒซ แˆตแˆ‹แˆ‹แŒˆแŠ˜แˆ แŠฅแˆซแˆดแŠ• แŠฅแˆณแ‹ฐแ‰ฃแˆˆแˆแข แŠฅแŠ“ แŠจแŠฎแ‹ต แ‹จแ‰ แˆˆแŒ  แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แŠฅแŒฝแ‹แˆˆแˆ. แˆตแˆˆแ‹šแˆ…, แŠฎแ‹ฑแŠ• แˆฒแ‹ซแˆญแ‰ตแ‹‘, แˆ˜แŒแˆˆแŒซแ‹ แˆแˆแŒŠแ‹œ แˆ˜แ‹˜แˆ˜แŠ• แ‹ซแˆตแˆแˆแŒˆแ‹‹แˆ. แ‰ แˆแˆˆแ‰ฐแŠ› แ‹ฐแˆจแŒƒ, แ‰ แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แŠญแˆˆแˆณ, แŠฎแ‹ฑ แŠฅแ‹จแ‰ฃแˆฐ แ‹ญแˆ„แ‹ณแˆ, แˆˆแˆ›แŠ•แ‰ แ‰ฅ แŠฅแŠ“ แˆˆแˆ›แ‰†แ‹จแ‰ต แ‹จแ‰ แˆˆแŒ  แŠ แˆตแ‰ธแŒ‹แˆช แ‹ญแˆ†แŠ“แˆ. แ‹ญแˆ… แ‹จแŠขแŠ•แ‰ตแˆฎแ’แŠ• แˆ˜แŒจแˆ˜แˆญ แŠแ‹. แŠแŒˆแˆญ แŒแŠ• แ‰ แ‹แˆญแ‹แˆญ แŠซแˆแŒ€แˆ˜แˆญแŠญ แŠฅแ‹ซแŠ•แ‹ณแŠ•แ‹ฑ แ‹จแˆšแŒฝแˆแ‹ แˆ˜แˆตแˆ˜แˆญ แŠคแ‹ฒแ‰ต แ‹ญแˆ†แŠ“แˆแฃ แŠฅแŠ“ แŠฎแ‹ฑ แ‹จแˆ›แ‹ญแŒ แ‰…แˆ แŠฅแŠ“ แŠจแŒ…แˆแˆฉ แˆˆแˆ›แŠ•แ‰ แ‰ฅ แŠ แˆตแ‰ธแŒ‹แˆช แ‹ญแˆ†แŠ“แˆแข

แŠฅแŠ•แ‹ฐแ‰ฐแŠ“แŒˆแˆจแ‹ แŠ แ‹ญแ‹˜แŠ•แˆƒแ‹ˆแˆญ, แŒฆแˆญแŠแ‰ต แ‰ แŠฅแ‰…แ‹ต แŠ แˆแ‰ฐแˆธแŠแˆแˆแฃ แ‹ซแˆˆ แŠฅแ‰…แ‹ตแˆ แ‹ตแˆ แŠ แˆแ‰ฐแ‹ฐแˆจแŒˆแˆแข. แŠฅแŠ“ แˆตแˆˆ แŒฆแˆญแŠแ‰ถแ‰ฝ แŠ แŠ•แ‹ต แ‹ˆแ‹ญแˆ แˆแˆˆแ‰ต แŠแŒˆแˆญ แ‹ซแ‹แ‰ƒแˆแข แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แˆ˜แŒปแ แŒŠแ‹œ แˆ›แ‰ฃแŠจแŠ• แŠแ‹ แ‹จแˆšแˆ แŠ แˆตแ‰ฐแ‹ซแ‹จแ‰ต แŠ แˆˆ. แŠ แŠ•แ‹ณแŠ•แ‹ต แŒŠแ‹œ แ‹ญแˆ… แŠฅแ‹แŠแ‰ต แŠแ‹, แŠฅแŠ“ แˆตแˆซแ‹ แ‰ แŒฃแˆ แ‰€แˆ‹แˆ แˆตแˆˆแˆ†แŠ แ‰ แŠฅแˆฑ แ‹แˆตแŒฅ แˆˆแˆ›แˆฐแ‰ฅ แˆแŠ•แˆ แŠแŒˆแˆญ แ‹จแˆˆแˆ. แŠแŒˆแˆญ แŒแŠ• แ‹แˆญแ‹แˆญ แˆ˜แŒแˆˆแŒซแ‹Žแ‰ฝแŠ• แŠฅแŠ•แ‹ณแ‰ตแŒฝแ‰ แˆฒแŠแŒˆแˆญแˆ… แŠฅแŠ•แ‹ณแ‰ณแˆตแ‰ฅ แŠฅแŠ•แ‹ฐแ‰ฐแŠแŒˆแˆจแˆ… แˆแˆแŒŠแ‹œ แˆ›แˆตแ‰ณแ‹ˆแˆต แŠ แˆˆแ‰ฅแˆ…แข แŠฅแŠ“ แˆแˆ แŒŠแ‹œ แˆŠแ‹ซแˆตแ‰กแ‰ แ‰ต แ‹ญแŒˆแ‰ฃแˆ. แ‰ แ‰ฐแŒแ‰ฃแˆฉ แˆ‹แ‹ญ แˆ›แˆฐแ‰ฅ แˆตแˆ…แ‰ฐแ‰ต แˆ‹แˆˆแˆ˜แˆฅแˆซแ‰ต แ‹‹แˆตแ‰ตแŠ“ แŠ แ‹ญแˆ†แŠ•แˆ. แŠฅแŠ•แ‹ฐแˆแŠ“แ‹แ‰€แ‹, แˆ›แŠ•แˆ แˆฐแ‹ แŠ แˆตแˆ›แ‰ณแ‹Šแ‹แŠ• แ‹˜แŠ•แŒ แ‹จแˆแŒ แˆจแ‹ แ‹จแˆˆแˆ, แŠฅแŠ“ แ•แˆฎแŒแˆซแˆ แˆ›แ‹แŒฃแ‰ต แŠจแ‰ฃแ‹ต แˆตแˆซ แŠแ‹. แŠแŒˆแˆญ แŒแŠ• แ‰ แ‰ฝแŒแˆฉ แ‹แˆตแŒฅ แŠซแˆ‹แˆฐแ‰กแ‰ต แˆตแˆ…แ‰ฐแ‰ต แˆˆแˆ˜แˆฅแˆซแ‰ต แ‹‹แˆตแ‰ตแŠ“ แ‹ญแˆฐแŒฅแ‹Žแ‰ณแˆ.

แˆตแˆˆ TLA + แŠฅแŠ“ PlusCal แ‰ แˆแ‹ฉ แ‹ตแˆ…แˆจ แŒˆแŒฝ แˆ‹แ‹ญ แ‹จแ‰ แˆˆแŒ  แˆ›แŠ•แ‰ แ‰ฅ แ‰ตแ‰ฝแˆ‹แˆ‹แ‰ฝแˆแฃ แŠจแˆ˜แŠแˆป แŒˆแŒผ แ‹ˆแ‹ฐแ‹šแ‹ซ แˆ˜แˆ„แ‹ต แ‰ตแ‰ฝแˆ‹แˆ‹แ‰ฝแˆ แˆ›แ‹ซแ‹ซแ‹ฃ. แ‹ซ แˆˆแŠฅแŠ” แ‰ฅแ‰ป แŠแ‹แฃ แˆตแˆˆ แ‰ตแŠฉแˆจแ‰ตแˆ… แŠ แˆ˜แˆฐแŒแŠ“แˆˆแˆแข

แŠฅแ‰ฃแŠญแ‹Ž แ‹ญแˆ… แ‰ตแˆญแŒ‰แˆ แˆ˜แˆ†แŠ‘แŠ• แ‹ซแˆตแ‰ฐแ‹แˆ‰. แŠ แˆตแ‰ฐแ‹ซแ‹จแ‰ถแ‰ฝแŠ• แˆตแ‰ตแŒฝแ แ‹ฐแˆซแˆฒแ‹ แŠฅแŠ•แ‹ฐแˆ›แ‹ซแŠแ‰ฃแ‰ธแ‹ แŠ แˆตแ‰ณแ‹แˆตแข แŠจแŒธแˆแŠแ‹ แŒ‹แˆญ แˆˆแˆ˜แ‹ˆแ‹ซแ‹จแ‰ต แ‰ แŠฅแ‹แŠแ‰ต แŠจแˆแˆˆแŒ‰, แŠฅแˆฑ แŠจแŒแˆ‹แ‹ญ 2019-11, 12 แ‰ แˆดแŠ•แ‰ต แ’แ‰ฐแˆญแˆตแ‰ แˆญแŒ แ‰ แˆšแŠซแˆ„แ‹ฐแ‹ แ‹จ Hydra 2019 แŠฎแŠ•แˆแˆจแŠ•แˆต แˆ‹แ‹ญ แ‹ญแˆ†แŠ“แˆ. แ‰ตแŠฌแ‰ถแ‰ฝแŠ• แˆ˜แŒแ‹›แ‰ต แ‹ญแ‰ปแˆ‹แˆ แ‰ แ‹ญแ‹แ‹Šแ‹ แ‹ตแˆญแŒฃแ‰ขแ‹ซ แˆ‹แ‹ญแข.

แˆแŠ•แŒญ: hab.com

แŠ แˆตแ‰ฐแ‹ซแ‹จแ‰ต แ‹ซแŠญแˆ‰