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

कार्यक्रम:

नाम

mcrl22lps - mCRL2 विनिर्देशन को LPS में अनुवादित करें

SYNOPSIS

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

वर्णन

INFILE में mCRL2 विनिर्देश को रैखिक बनाता है और परिणामी LPS को OUTFILE में लिखता है। अगर
OUTFILE मौजूद नहीं है, stdout का उपयोग किया गया है। यदि INFILE मौजूद नहीं है, तो stdin का उपयोग किया जाता है।

विकल्प

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

-b, --बाइनरी
क्लस्टरिंग करते समय n-ary के बजाय बाइनरी केस फ़ंक्शंस का उपयोग करें; की उपस्थिति में
-w/--newstate, राज्य चर बूलियन चर के एक वेक्टर द्वारा एन्कोड किए गए हैं

-e, --चेक-ओनली
वाक्यविन्यास और स्थैतिक शब्दार्थ की जाँच करें; रैखिकरण मत करो

-c, --समूह
अंतिम एलपीएस में सभी क्रियाएं क्लस्टर की गई हैं। क्लस्टरिंग का मतलब है कि के साथ सारांश
समान क्रिया लेबल एक साथ समूहीकृत किए गए हैं। उदाहरण के लिए, a(f1) . P(g1) + a(f2) .
P(g2) को योग b: बूल द्वारा प्रतिस्थापित किया जाता है। a(if(b, f1, f2)) . P(if(b, f2, g2)).
लाभ यह है कि इस तरह से सारांशों की संख्या को काफी हद तक कम किया जा सकता है।
नुकसान यह है कि सम ऑपरेटरों को पेश किया जाता है और नए डेटा को सॉर्ट किया जाता है
सहायक कार्य उत्पन्न होते हैं। नये प्रकार की उत्पत्ति से बचने के लिए,
विकल्प -b/--बाइनरी का उपयोग किया जा सकता है।

-D, --डेल्टा
प्रत्येक प्रक्रिया में प्रत्येक स्थिति में एक ट्रू->डेल्टा सारांश जोड़ें; ये डेल्टा सभी को समाहित करते हैं
अन्य सशर्त समयबद्ध डेल्टा, डेल्टा सारांश की संख्या को प्रभावी ढंग से कम करते हैं
परिणामी रैखिक प्रक्रिया में अत्यधिक; रैखिककरण को गति देता है। यह है
डिफ़ॉल्ट, लेकिन यह समय के साथ सही ढंग से व्यवहार नहीं करता है।

-lनाम, --lin-विधि=नाम
नियमित रूप में एलपीएस उत्पन्न करने के लिए रैखिककरण विधि नाम: 'नियमित' का उपयोग करें
(विनिर्देश नियमित होना चाहिए) (डिफ़ॉल्ट) 'नियमित' के एक प्रकार के लिए 'नियमित2'
जो अधिक डेटा वेरिएबल्स का उपयोग करता है (उपयोगी जब 'नियमित' काम नहीं करता है) 'स्टैक' के लिए
स्टैक डेटा प्रकारों का उपयोग करना (उपयोगी जब 'नियमित' और 'नियमित2' काम नहीं करते हैं)

-w, --न्यूस्टेट
राज्य चर को सकारात्मक प्राकृतिक के बजाय प्रगणित प्रकारों का उपयोग करके एन्कोड किया गया है
संख्याएँ (स्थिति)। इस विकल्प का उपयोग करके Enumk नामक नए परिमित प्रकार उत्पन्न किए जाते हैं
जहाँ k डोमेन का आकार है। इसके अलावा, सहायक केस फ़ंक्शंस और समानताएँ
परिभाषित किया गया हैं। विकल्प --बाइनरी के संयोजन में परिमित प्रकार एन्कोड किए गए हैं
बूलियन्स द्वारा. (रैखिकीकरण विधि 'नियमित' या 'नियमित2' की आवश्यकता है)।

-z, --नो-अल्फ़ा
वर्णमाला में कटौती लागू नहीं की जाती है। डिफ़ॉल्ट रूप से mcrl22lps वितरित करने का प्रयास करता है
संचार, छिपाना और ऑपरेटरों को समानांतर रचना ऑपरेटर के रूप में अनुमति देना
इससे मध्यवर्ती रैखिक प्रक्रियाओं का आकार कम हो जाता है। इस विकल्प का प्रयोग करके यह
कदम से बचा जा सकता है. नाम प्रक्रिया बीजगणित में वर्णमाला स्वयंसिद्धों से उत्पन्न होता है।

-n, --नो-क्लस्टर
मध्यवर्ती एलपीएस में क्रियाओं को समानांतर में रखे जाने से पहले क्लस्टर नहीं किया जाता है।
डिफ़ॉल्ट रूप से इन प्रक्रियाओं को संख्या में विस्फोट से बचने के लिए क्लस्टर किया जाता है
दो समानांतर रैखिक प्रक्रियाओं को एक रैखिक में परिवर्तित करते समय सारांश
प्रक्रिया। यदि एम सारांश के साथ एक रैखिक प्रक्रिया को एक रैखिक के समानांतर रखा जाता है
एन सारांश के साथ प्रक्रिया परिणामी प्रक्रिया में एम × एन + एम + एन सारांश है। एम और दोनों
नई किस्मों को पेश करने की कीमत पर क्लस्टरिंग द्वारा एन को काफी हद तक कम किया जा सकता है
और कार्य. देखें -c/--क्लस्टर, esp। क्लस्टरिंग की संक्षिप्त व्याख्या के लिए
प्रक्रिया.

--नहीं-constelm
एक रेखीय प्रक्रिया उत्पन्न करते समय निरंतर उन्मूलन लागू करने का प्रयास न करें।

-g, --नो-डेल्टेल्म
नकली डेल्टा समन को हटाने से बचें। समय के अस्तित्व के कारण डेल्टा
सारांश को छोड़ा नहीं जा सकता. बहुक्रियाओं की उपस्थिति के कारण इनकी संख्या
सारांश बहुत बड़ा हो सकता है. डेल्टा समन को हटाने के लिए एल्गोरिदम बस काम करता है
यह देखने के लिए कि क्या स्थिति है, प्रत्येक डेल्टा सारांश की एक दूसरे सारांश से तुलना करें
एक का तात्पर्य दूसरे की स्थिति से है। स्पष्टतः, यह द्विघात है
जटिलता, और इसमें लंबा समय लग सकता है।

-f, --नो-ग्लोबवर्स
इंस्टेंटियेट मनमाने स्थिरांक वाले मूल्यों की परवाह नहीं करता, बजाय उन्हें मॉडलिंग करने के
वैश्विक चर द्वारा. इसमें घोषित वैश्विक चरों पर इसका कोई प्रभाव नहीं पड़ता है
विनिर्देश।

-o, --नहीं-पुनर्लिखित
रैखिककरण करते समय डेटा शब्दों को दोबारा न लिखें; जब पुनर्लेखन प्रणाली उपयोगी होती है
समाप्त नहीं. यह विकल्प स्थिरांक के अनुप्रयोग को भी बंद कर देता है
निकाल देना।

-m, --नो-सुमेल्म
समांतर संरचना में योग विलोपन लागू करने से बचें

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

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

-a, --राज्यनाम
उत्पन्न डेटा मापदंडों के नाम प्रक्रिया के नाम के साथ बढ़ाए जाते हैं
जो वे घटित होते हैं. इससे यह निर्धारित करना आसान हो जाता है कि पैरामीटर कहां से आता है।

-T, --समयबद्ध
सभी समयबद्ध जानकारी को संरक्षित करते हुए प्रक्रिया को रैखिक रूप में अनुवादित करें। समानांतर में
प्रक्रियाओं में संभावित समय की कमी की संख्या बड़ी हो सकती है, जो धीमी हो सकती है
रैखिककरण। --डेल्टा विकल्प प्रदान करें जो बहुत तेज़ अनुवाद प्रदान करता है
समय को सही ढंग से सुरक्षित नहीं रखता

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

मानक विकल्प:

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

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

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

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

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

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

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