TLA + के साथ एक बिल्ली पकड़ो

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

आप एक तरफ के सात कमरों के साथ एक सीधे गलियारे में हैं। उनमें से एक में एक बिल्ली है। एक कदम में, आप एक कमरे में देख सकते हैं, अगर कोई बिल्ली है, तो वह पकड़ा जाता है। जैसे ही दरवाजा बंद होता है, बिल्ली पड़ोसी कमरों में से एक में चली जाएगी जिसमें वह था। कार्य बिल्ली को पकड़ना है।

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

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

CatDistr' = CatDistr \ {n} 

यह स्थिति बताती है कि जिन कमरों में बिल्ली n कमरे की जाँच के बाद स्थित हो सकती है, उन कमरों के सेट के साथ मेल खाता है जहाँ से उन्होंने 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 वैरिएबल, अंतिम चेक किया गया कमरा, प्रोग्राम आउटपुट की पठनीयता के लिए दर्ज किया गया है। बड़े मॉडल के लिए, इस तरह के चर विश्लेषण किए गए राज्यों की संख्या में वृद्धि करके कार्यक्रम को काफी धीमा कर सकते हैं (चूंकि राज्य में अब यह कैसे होता है और अलग-अलग तरीकों से बनाए गए एक ही राज्य का इतिहास होगा)।

विधेय Init प्रारंभिक स्थिति का वर्णन करता है (0. कमरे सभी कमरों का सेट है)। OpenDoor (n) बताता है कि जब आप रूम एन का दरवाजा खोलते हैं तो क्या होता है (सबसे खराब स्थिति में, बिल्ली वहां नहीं है - अन्यथा हमने उसे पकड़ लिया)।

अगला विधेय थोड़ा अजीब लगता है - देखने के लिए एक कमरा है। तथ्य यह है कि कुछ के अस्तित्व का मतलब है कि टीएलए + को यह नहीं पता है कि हम किस कमरे में देखेंगे, इसलिए, यह सभी मामलों में अपरिवर्तनीयता की शुद्धता की जांच करेगा।

यह लिखना अधिक स्पष्ट होगा

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

लेकिन तब हमारा कोड केवल एक निश्चित संख्या में कमरों के साथ काम करेगा, और इसे बेहतर बनाने के लिए इसे मानकीकृत किया जाएगा।

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

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

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

यहां सब कुछ सरल है - हमने कमरों की संख्या, प्रारंभिक स्थितियों, राज्य के परिवर्तन की शर्तों और परीक्षण के तहत अपरिवर्तनीय का संकेत दिया।

मॉडल को कमांड लाइन tlc2 -config cat.cfg cat.tla से लॉन्च किया गया है।

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

निष्कर्ष

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

→ यहाँ कार्य पाया गया

बस मामले में, इंटरैक्टिव समाधान सत्यापन के लिए एक सरल कार्यक्रम। टीएलए + के अध्ययन के लिए सामग्री। एक अन्य मॉडल जाँच प्रणाली, मिश्र धातु, यहाँ वर्णित है ।