टीएलए + के साथ एक बिल्ली को कैसे पकड़ना है

कई प्रोग्रामर संघर्ष करते हैं जब औपचारिक तरीकों का उपयोग करके अपने कार्यक्रमों के भीतर समस्याओं को हल करने के लिए, उन तरीकों के रूप में, जबकि प्रभावी, अनुचित रूप से जटिल हो सकता है। ऐसा क्यों होता है यह समझने के लिए, आइए अपेक्षाकृत आसान पहेली को हल करने के लिए मॉडल जाँच विधि का उपयोग करें:

स्थितियां

आप एक दालान में हैं, जिसमें एक तरफ सात दरवाजे हैं और सात कमरे हैं। इनमें से एक कमरे में एक बिल्ली छिपी हुई है। आपका काम बिल्ली को पकड़ना है। एक दरवाजा खोलना एक कदम है। यदि आप सही दरवाजे का अनुमान लगाते हैं, तो आप बिल्ली को पकड़ते हैं। यदि आप सही दरवाजे का अनुमान नहीं लगाते हैं, तो बिल्ली अगले कमरे में भाग जाती है।

टीएलए + और लौकिक तर्क

कुछ उपकरण इस तरह की समस्याओं को हल कर सकते हैं। उदाहरण के लिए, एसएमटी सॉल्वर , जो इन मामलों में अक्सर उपयोग किया जाता है, समस्या को हल करने के लिए विधेय तर्क का उपयोग करते हैं, लेकिन इसके लिए एक सरणी का उपयोग करने की आवश्यकता होती है, जो प्रोग्रामर के लिए असुविधाजनक है और अक्सर परिणामस्वरूप कार्यों का अनावश्यक रूप से जटिल अनुक्रम होता है। दूसरी ओर, TLA + , लौकिक तर्क का उपयोग करता है, जो एक प्रोग्राम को वर्तमान और अगले चरण दोनों में एक स्टेटमेंट में सिस्टम की स्थिति का उपयोग करने की अनुमति देता है।

CatDistr' = CatDistr \ {n} 

यह स्थिति बताती है कि दरवाजे एन के पीछे की जाँच करने के बाद, दरवाजे की संख्या जहाँ बिल्ली स्थित हो सकती है, उन कमरों के सेट से मेल खाती है जहाँ से एन लिया गया था। (यदि बिल्ली दरवाजा एन के पीछे थी, तो निश्चित रूप से, वह पकड़ा गया है।)

एक अनिवार्य प्रोग्रामिंग भाषा में, यह पुराने से गणना की गई एक नया चर बनाता है।

सेट के बारे में

बिल्ली की स्थिति एक विशिष्ट मॉडलिंग कक्ष प्रणाली के रूप में विशिष्ट कमरे के बजाय, सभी संभव कमरों के सेट के भीतर एक चर द्वारा निर्धारित की जाती है। प्रोग्रामिंग के औपचारिक तरीके वर्तमान मूल्य के बजाय संभावित मूल्यों की बहुलता को ध्यान में रखते हैं। यह अक्सर डेवलपर्स की शुरुआत के लिए बहुत जटिल है, इसलिए इस प्रणाली को सरल बनाने से उन डेवलपर्स को अधिक तेज़ी से काम करने में मदद मिलेगी।

टीएलए + में कार्यक्रम की संरचना

कार्यक्रम में घोषणाएँ और कथन (भविष्यवक्ता) होते हैं, जो वर्णन करते हैं:

• प्रारंभिक अवस्था
• वास्तविक राज्यों के बीच की कड़ी
• अगला राज्य
• एक आक्रमणकारी जो सभी उपलब्ध राज्यों में चलता है।

इसमें सहायक विधेय (जैसे पैरामीटर) शामिल हो सकते हैं।

 ---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} ============================================================================= 

उस उदाहरण में:

• पहली और आखिरी लाइनें घोषित करती हैं कि यह एक स्रोत मॉड्यूल है।
• == का अर्थ है 'समान रूप से परिभाषा'।
• = का अर्थ है कि गणना की गई अभिव्यक्ति मान बराबर हैं
• कॉन्फ़िगरेशन फ़ाइल में दरवाजे एक निरंतर सेट है।
• कैटडिसर उस कमरे को निर्धारित करता है जिसमें बिल्ली स्थित है।
• LastDoor चर, जो अंतिम चेक किए गए कमरे का प्रतिनिधित्व करता है, आसानी से कार्यक्रम के आउटपुट को पढ़ता है। बड़े मॉडल के लिए, इस तरह के चर प्रोग्राम वर्कफ़्लो को धीमा कर सकते हैं और उन राज्यों की संख्या बढ़ा सकते हैं जिनका विश्लेषण करने की आवश्यकता है। इस मॉडल में, हालांकि, राज्य में अब इतिहास शामिल है कि कौन से दरवाजे खोले गए थे। इस प्रकार, अलग-अलग तरीकों से बनाए गए समान राज्य अब अलग-अलग हैं।
• इनिट प्रेडिक्टर कार्यक्रम की प्रारंभिक स्थिति का वर्णन करता है - इस मामले में, अभी तक कोई दरवाजे नहीं खोले गए हैं।
• OpenDoor (n) बताता है कि जब दरवाजा n खोला जाता है तो क्या होता है - या तो आपने बिल्ली को पकड़ लिया, या आपने नहीं लिया।
• अगला भविष्यवक्ता मौजूद है क्योंकि TLA + यह नहीं जानता है कि हम किस कमरे में प्रवेश कर सकते हैं, इसलिए यह देखने के लिए जाँच करेगा कि क्या प्रत्येक मामले में आक्रमणकारी सही हैं या नहीं।
  
  यहाँ एक और अधिक स्पष्ट संस्करण है:
  
  

   Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors) 

  
  इस मामले में, कोड एक निश्चित संख्या में कमरों के साथ काम करता है, जिससे कोड को मानकीकृत किया जाता है।
• अंत में, कैटवॉक आक्रमणकारी निर्धारित करता है कि बिल्ली कहाँ छिप रही है। एक अपरिवर्तनीय उल्लंघन का मतलब है कि बिल्ली को जहां भी छिपाया गया था, वह पकड़ा गया था। विनिर्देशन की पुष्टि करते समय, एक अपरिवर्तनीय उल्लंघन एक त्रुटि है, लेकिन चूंकि हम अपने इच्छित उद्देश्य के लिए उपकरण का उपयोग नहीं कर रहे हैं, इसलिए इस मामले में त्रुटि प्राप्त करने का अर्थ है समस्या को हल करना।

मॉडल कॉन्फ़िगरेशन

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

इस कॉन्फ़िगरेशन में प्रारंभिक स्थिति, कमरों की संख्या, एक राज्य परिवर्तन की स्थिति और एक सत्यापन योग्य परीक्षा शामिल है।

आप इस कमांड का उपयोग करके कमांड लाइन से इस मॉडल को चला सकते हैं:
tlc2 -config cat.cfg cat.tla ।

TLA + में एक उन्नत GUI है और इसे tla-toolbox कमांड द्वारा लॉन्च किया गया है। दुर्भाग्य से, यह .cfg फ़ाइलों को नहीं समझता है, इसलिए मेनू के माध्यम से मॉडल मापदंडों को कॉन्फ़िगर करना होगा।

निष्कर्ष

इस विशेष कार्यक्रम को बनाना काफी सरल था, लेकिन कई मामलों में, औपचारिक तरीकों को लागू करने के लिए बहुत बड़े मॉडल और विभिन्न भाषा निर्माणों के उपयोग की आवश्यकता होगी। हम आशा करते हैं कि इस तरह की सरल पहेलियों को हल करना, कार्य परियोजनाओं को औपचारिक तरीके लागू करने का एक आसान और दिलचस्प तरीका प्रदान करेगा।

• इंटरैक्टिव समाधान सत्यापन के लिए एक सरल कार्यक्रम यहां पाया जा सकता है ।
• TLA + के बारे में अधिक जानें यहां ।