lps2lts - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

lps2lts - LPS से LTS उत्पन्न करें

SYNOPSIS

lps2lts [विकल्प]...[फाइल मैं [बाहरी]]

वर्णन

INFILE में LPS से एक LTS जेनरेट करें और परिणाम को OUTFILE में सेव करें। यदि INFILE नहीं है
आपूर्ति की गई, stdin का उपयोग किया जाता है। यदि आउटफ़ाइल की आपूर्ति नहीं की जाती है, तो एलटीएस संग्रहीत नहीं किया जाता है।

यदि 'जिटिक' रीराइटर का उपयोग किया जाता है, तो MCRL2_COMPILEREWRITER पर्यावरण चर
(डिफ़ॉल्ट मान: 'mcrl2compilerewriter') उस स्क्रिप्ट को निर्धारित करता है जो पुनर्लेखक को संकलित करती है,
और MCRL2_COMPILEDIR (डिफ़ॉल्ट मान: '.') निर्धारित करता है कि अस्थायी फ़ाइलें कहाँ संग्रहीत हैं।

ध्यान दें कि lps2lts किसी भी जोड़ी के बीच एक ही लेबल के साथ कई ट्रांज़िशन प्रदान कर सकता है
राज्य. यदि यह वांछित नहीं है, तो किसी मजबूत पदार्थ का प्रयोग करके ऐसे संक्रमणों को हटाया जा सकता है
उदाहरण के लिए उपकरण ltsconvert का उपयोग करके बिसिमुलेशन रिडक्टन।

OUTFILE का प्रारूप उसके एक्सटेंशन द्वारा निर्धारित किया जाता है (जब तक कि इसे किसी द्वारा निर्दिष्ट न किया गया हो)।
विकल्प)। समर्थित प्रारूप हैं:

एल्डेबरन प्रारूप (सीएडीपी) के लिए 'ऑट',
ग्राफ़विज़ प्रारूप के लिए 'डॉट' (अब इनपुट प्रारूप के रूप में समर्थित नहीं है),
परिमित राज्य मशीन प्रारूप के लिए 'एफएसएम', या
एमसीआरएल2 एलटीएस प्रारूप के लिए 'एलटीएस' यदि जिट्टीसी रीराइटर का उपयोग किया जाता है, तो
MCRL2_COMPILEREWRITER पर्यावरण चर (डिफ़ॉल्ट मान: mcrl2compilerewriter)
उस स्क्रिप्ट को निर्धारित करता है जो पुनर्लेखक को संकलित करता है, और MCRL2_COMPILEDIR (डिफ़ॉल्ट मान:
'.') यह निर्धारित करता है कि अस्थायी फ़ाइलें कहाँ संग्रहीत हैं। ध्यान दें कि lps2lts एकाधिक वितरित कर सकता है
राज्यों के किसी भी जोड़े के बीच समान लेबल वाले संक्रमण। यदि यह वांछित नहीं है, तो ऐसा
उदाहरण के लिए एक मजबूत द्विसिमुलेशन रिडक्टन का उपयोग करके संक्रमण को हटाया जा सकता है
उपकरण ltsconvert.

विकल्प

विकल्प निम्नलिखित में से कोई भी हो सकता है:

-aनाम, --कार्य=नाम
ट्रांज़िशन सिस्टम में उन क्रियाओं का पता लगाएं और रिपोर्ट करें जिनमें क्रिया नाम हैं
नाम, अल्पविराम से अलग की गई सूची। उदाहरण के लिए, इसे खोजना (या सिद्ध करना) उपयोगी है
एक क्रिया त्रुटि की अनुपस्थिति)। इनमें से प्रत्येक घटना के लिए एक संदेश मुद्रित होता है
ये क्रिया नाम. -t ध्वज के साथ इन क्रियाओं के निशान उत्पन्न होते हैं

-b[NUM], --बिट-हैश[=NUM]
राज्यों को संग्रहीत करने और अधिकतम NUM राज्यों में संग्रहीत करने के लिए बिट हैशिंग का उपयोग करें। इस का मतलब है कि
जिन राज्यों का दौरा किया गया है, उनका पूरा रिकॉर्ड रखने के बजाय, एक छोटी सी सारणी
इसका उपयोग यह बताने के लिए किया जाता है कि किसी राज्य का हैश पहले देखा गया है या नहीं।
हालाँकि इसका मतलब यह है कि इस विकल्प के कारण राज्यों को दूसरों के लिए ग़लत समझा जा सकता है
(क्योंकि वे एक ही हैश पर मैप किए गए हैं), यह बहुत बड़े पैमाने पर अन्वेषण करने के लिए उपयोगी हो सकता है
एलटीएस जो अन्यथा अन्वेषण योग्य नहीं हैं। NUM का डिफ़ॉल्ट मान लगभग है
2*10^8 (यह लगभग 25एमबी मेमोरी के अनुरूप है)

-- कैश्ड
राज्य अंतरिक्ष निर्माण में तेजी लाने के लिए गणना कैशिंग तकनीकों का उपयोग करें।

-c[नाम], --संगम हे[=नाम]
एक्शन लेबल NAME के ​​साथ ट्रांज़िशन की प्राथमिकता लागू करें। (जब कोई NAME न हो
आपूर्ति की गई (अर्थात, '-सी') कार्रवाई 'ctau' को प्राथमिकता दी जाती है। को प्राथमिकता देना
ध्वज का उपयोग करने के लिए -ctau. ध्यान दें कि यदि रैखिक प्रक्रिया ताऊ-संगम नहीं है,
उत्पन्न राज्य स्थान आवश्यक रूप से राज्य स्थान के समान शाखाबद्ध है
एलपीएस. जिस पीढ़ी एल्गोरिथ्म का उपयोग किया जाता है उसे रैखिक प्रक्रिया की आवश्यकता नहीं होती है
ताऊ अभिसरण होना।

-D, --गतिरोध
गतिरोधों का पता लगाएं (अर्थात् प्रत्येक गतिरोध के लिए एक संदेश मुद्रित होता है)

-F, --विचलन
विचलन का पता लगाएं (अर्थात् विचलन (=ताऊ लूप) वाले प्रत्येक राज्य के लिए एक संदेश है
मुद्रित)। विचलन का पता लगाने के लिए एल्गोरिदम प्रत्येक राज्य के लिए रैखिक है
इस विकल्प के चालू होने पर राज्य अंतरिक्ष अन्वेषण द्विघात हो जाता है, जिससे एक राज्य उत्पन्न होता है
इस विकल्प के सक्षम होने पर अंतरिक्ष अन्वेषण धीमा हो जाएगा।

-yBOOL, -- डमी=BOOL
LPS में मुफ़्त वेरिएबल को BOOL के मान के आधार पर डमी मानों से बदलें:
'हाँ' (डिफ़ॉल्ट) या 'नहीं'

--त्रुटि-निशान
यदि अन्वेषण के दौरान कोई त्रुटि होती है, तो उस स्थिति में ट्रेस सहेजें जो नहीं हो सका
पता लगाया

--init-tsize=NUM
आंतरिक रूप से उपयोग की जाने वाली हैश तालिकाओं का प्रारंभिक आकार सेट करें (डिफ़ॉल्ट 10000 है)

-lNUM, --मैक्स=NUM
अधिकतम NUM राज्यों का अन्वेषण करें

-mनाम, --बहुक्रिया=नाम
NAMES से संक्रमण प्रणाली में बहुक्रियाओं का पता लगाएं और रिपोर्ट करें, एक अल्पविराम-
अलग सूची. -ए की तरह काम करता है, सिवाय इसके कि बहु-क्रियाएँ बिल्कुल मेल खाती हैं,
डेटा पैरामीटर सहित।

--कोई सूचना नहीं
OUTFILE में राज्य की जानकारी न जोड़ें, इस विकल्प के बिना lps2lts राज्य जोड़ता है
एलटीएस के लिए वेक्टर। यह विकल्प इस जानकारी को खारिज कर देता है और बताता है
केवल अनुक्रम संख्या द्वारा दर्शाया जाता है। स्पष्ट राज्य की जानकारी के लिए उपयोगी है
उदाहरण के लिए, विज़ुअलाइज़ेशन उद्देश्य, लेकिन आउटफ़ाइल के बढ़ने का कारण बन सकता है
काफ़ी. ध्यान दें कि AUT प्रारूप में लिखते समय यह विकल्प अंतर्निहित होता है।

-oFORMAT, --बाहर=FORMAT
आउटपुट को निर्दिष्ट प्रारूप में सहेजें

--छटना
राज्य अंतरिक्ष निर्माण में तेजी लाने के लिए समैंड प्रूनिंग का उपयोग करें।

-QNUM, --qlimit=NUM
परिमाणकों की गणना को NUM चरों तक सीमित करें। (डिफ़ॉल्ट NUM=1000, NUM=0 for
असीमित)।

-rनाम, --रीराइटर=नाम
पुनर्लेखन रणनीति का उपयोग करें NAME: 'जिट्टी' जिट्टी रीराइटिंग (डिफ़ॉल्ट) 'जिटिक' संकलित
जिट्टी पुनर्लेखन 'जिट्टीप' कहावत के साथ जिट्टी पुनर्लेखन

-sनाम, --रणनीति=नाम
रणनीति नाम का उपयोग करके राज्य स्थान का पता लगाएं: 'बी', 'चौड़ाई' चौड़ाई-पहली खोज
(डिफ़ॉल्ट) 'डी', 'गहराई' गहराई-पहली खोज 'पी', 'प्राथमिकताकृत' एकल को प्राथमिकता दें
इसके पहले तर्क पर क्रियाएँ नेट की तरह होती हैं जहाँ केवल वे क्रियाएँ होती हैं
इस पैरामीटर के लिए न्यूनतम मान का चयन किया जाता है। जैसे यदि क्रियाएं हैं a(3) और
b(4) a(3) रहता है और b(4) छोड़ दिया गया है. सॉर्ट के पहले पैरामीटर के बिना क्रियाएँ
एक से अधिक क्रियाओं वाले नेट और मल्टीएक्शन हमेशा चुने जाते हैं (विकल्प है)।
प्रयोगात्मक) 'q', 'rprioritized' अपने पहले तर्क पर कार्यों को प्राथमिकता देते हैं
नेट को सॉर्ट करें (विकल्प देखें - प्राथमिकता दें), और प्राप्त करने के लिए यादृच्छिक रूप से इनमें से एक का चयन करें
प्राथमिकता वाले यादृच्छिक सिमुलेशन (विकल्प प्रयोगात्मक है) 'आर', 'यादृच्छिक' यादृच्छिक
अनुकरण. अगले सभी राज्यों में से एक को यादृच्छिक रूप से स्वतंत्र रूप से चुना जाता है
यह अवस्था पहले ही देखी जा चुकी है। परिणामस्वरूप, केवल यादृच्छिक अनुकरण
गतिरोध की स्थिति आने पर समाप्त हो जाता है।

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

--समय[=फ़ाइल]
FILE में समय मापन जोड़ें। माप मानक त्रुटि के लिए लिखे जाते हैं यदि
कोई फ़ाइल प्रदान नहीं की गई है

--टूडो-मैक्स=NUM
कार्य सूची में अधिकतम NUM राज्यों को रखें; यह विकल्प केवल चौड़ाई के लिए प्रासंगिक है-
पहली खोज, जहां NUM प्रति स्तर और गहराई के लिए राज्यों की अधिकतम संख्या है
पहली खोज, जहां NUM अधिकतम गहराई है

-t[NUM], --ट्रेस[=NUM]
प्रत्येक राज्य का सबसे छोटा ट्रेस लिखें जिस पर NAMES की कार्रवाई से पहुंचा जा सके
विकल्प --कार्रवाई, --गतिरोध के साथ पाया गया एक गतिरोध है, या एक विचलन है
फ़ाइल में --विचलन के साथ पता चला। NUM से अधिक अंश नहीं लिखे जायेंगे। अगर
NUM की आपूर्ति नहीं की गई है, निशानों की संख्या असीमित है। प्रत्येक निशान के लिए जो होना है
एक्सटेंशन .trc (ट्रेस) के साथ एक अनूठी फ़ाइल लिखी जाएगी जिसमें a शामिल होगा
प्रारंभिक अवस्था से गतिरोध अवस्था तक का सबसे छोटा ट्रेस। निशान हो सकते हैं
ट्रेसप का उपयोग करके सुंदर रूप से मुद्रित और अन्य प्रारूपों में परिवर्तित किया गया।

-u, --अप्रयुक्त-डेटा
डेटा विनिर्देश के अप्रयुक्त भागों को न हटाएं

मानक विकल्प:

-q, --शांत
चेतावनी संदेश प्रदर्शित न करें

-v, --शब्दशः
लघु मध्यवर्ती संदेश प्रदर्शित करें

-d, - दाढ़
विस्तृत मध्यवर्ती संदेश प्रदर्शित करें

--छांटने का स्तर=LEVEL
स्तर तक और सहित मध्यवर्ती संदेश प्रदर्शित करें

-h, --मदद
सहायता जानकारी प्रदर्शित करें

--संस्करण
संस्करण जानकारी प्रदर्शित करें

onworks.net सेवाओं का उपयोग करके ऑनलाइन lps2lts का उपयोग करें