एलपीएसइन्वेलम - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

lpsinvelm - इनवेरिएंट की जाँच करें और LPS के सारांश को सरल बनाने या समाप्त करने के लिए इनका उपयोग करें

SYNOPSIS

lpsinvelm [विकल्प]... --invfile=INVFILE [फाइल मैं [बाहरी]]

वर्णन

जाँचता है कि क्या बूलियन फॉर्मूला (सॉर्ट बूल का mCRL2 डेटा एक्सप्रेशन) प्रदान किया गया है
इनवेरिएंट INFILE में लीनियर प्रोसेस स्पेसिफिकेशन (LPS) का एक इनवेरिएंट है। अगर यह होता है
मामले में, उपकरण एलपीएस के सभी सारांशों को हटा देता है जिनकी स्थिति का उल्लंघन होता है
अपरिवर्तनीय, और परिणाम को OUTFILE पर लिखता है। यदि INFILE मौजूद है, तो stdin का उपयोग किया जाता है। अगर
OUTFILE मौजूद नहीं है, stdout का उपयोग किया जाता है।

टूल का उपयोग दिए गए एलपीएस के सारांश की शर्तों को सरल बनाने के लिए भी किया जा सकता है।

विकल्प

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

-y, --सर्व-उल्लंघन
जैसे ही अपरिवर्तनीय का एक भी उल्लंघन पाया जाता है, उसे समाप्त न करें, लेकिन
इसके बजाय सभी उल्लंघनों की रिपोर्ट करें

-c, --काउंटर-उदाहरण
यह दर्शाते हुए एक मूल्यांकन प्रदर्शित करें कि यदि ऐसा है तो अपरिवर्तनीय का उल्लंघन क्यों किया जा सकता है
यह अनिश्चित है कि क्या कोई सारांश अपरिवर्तनीय का उल्लंघन करता है

-o, --प्रवेश
सूचियों पर प्रेरण लागू करें

-iनिवेश करें, --अपरिवर्तनीय=निवेश करें
INVFILE में बूलियन फॉर्मूला (एक mCRL2 सॉर्ट बूल का डेटा एक्सप्रेशन) का उपयोग करें:
अचल

-n, --नो-चेक
अप्राप्य सारांशों को हटाने से पहले यह जाँच न करें कि अपरिवर्तनीय कायम है या नहीं

-e, --नहीं-उन्मूलन
सारांश को समाप्त या सरल न करें, बल्कि प्रत्येक शर्त में अपरिवर्तनीय जोड़ें

-pउपसर्ग, --प्रिंट-डॉट=उपसर्ग
यदि यह निर्धारित करना असंभव है कि परिणामी BDD की .dot फ़ाइल सहेजें
सारांश अपरिवर्तनीय का उल्लंघन करता है; PREFIX का उपयोग आउटपुट फ़ाइलों के उपसर्ग के रूप में किया जाएगा

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

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

-l, --सरलीकरण-सभी
केवल सारांशों को समाप्त करने के बजाय, सभी सारांशों की शर्तों को सरल बनाएं
जिनकी स्थितियाँ अपरिवर्तनीय के साथ मिलकर विरोधाभास हैं

-zसॉल्वर, --श्रीमती-समाधानकर्ता=सॉल्वर
आंतरिक रूप से उपयोग किए गए बीडीडी से असंगत पथों को हटाने के लिए सॉल्वर का उपयोग करें (डिफ़ॉल्ट रूप से,
कोई पथ उन्मूलन लागू नहीं है): 'सीवीसी' एसएमटी सॉल्वर सीवीसी3

-tसीमा, --समय सीमा=सीमा
किसी एकल सूत्र को सिद्ध करने में अधिकतम LIMIT सेकंड खर्च करें

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

मानक विकल्प:

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

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

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

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

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

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

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