lpsinvelm - ক্লাউডে অনলাইন

কার্যক্রম:

NAME এর

lpsinvelm - invariants চেক করুন এবং একটি LPS এর সামন্ড সরলীকরণ বা নির্মূল করতে এগুলি ব্যবহার করুন

সাইনোপিসিস

lpsinvelm [অনুযায়ী OPTION]... --invfile=INVFILE [ইনফাইল [আউটফাইল]]

বর্ণনাঃ

বুলিয়ান সূত্র (সর্ট বুল-এর একটি mCRL2 ডেটা এক্সপ্রেশন) হিসাবে দেওয়া হয়েছে কিনা তা পরীক্ষা করে
invariant হল INFILE-এ লিনিয়ার প্রসেস স্পেসিফিকেশন (LPS) এর একটি অপরিবর্তনীয়। এই যদি হয়
ক্ষেত্রে, টুলটি এলপিএস-এর সমস্ত সারমন্ড মুছে দেয় যার শর্ত লঙ্ঘন করে
invariant, এবং ফলাফলটি OUTFILE এ লেখে। INFILE উপস্থিত থাকলে, stdin ব্যবহার করা হয়। যদি
OUTFILE উপস্থিত নেই, stdout ব্যবহার করা হয়।

প্রদত্ত এলপিএসের সমমানের শর্তগুলিকে সরল করতেও টুলটি ব্যবহার করা যেতে পারে।

বিকল্প

অনুযায়ী OPTION নিম্নলিখিত যে কোনো হতে পারে:

-y, --সব-লঙ্ঘন
invariant একটি একক লঙ্ঘন পাওয়া গেলেই বন্ধ করবেন না, কিন্তু
পরিবর্তে সমস্ত লঙ্ঘনের রিপোর্ট করুন

-c, --পাল্টা উদাহরণ
কেন invariant সম্ভবত লঙ্ঘন হতে পারে তা নির্দেশ করে একটি মূল্যায়ন প্রদর্শন করুন
একটি সমন্ড invariant লঙ্ঘন কিনা অনিশ্চিত

-o, --আবেশ
তালিকায় আনয়ন প্রয়োগ করুন

-iINVFILE, -- অপরিবর্তনীয়=INVFILE
INVFILE-এ বুলিয়ান সূত্র (সর্ট বুলের একটি mCRL2 ডেটা এক্সপ্রেশন) ব্যবহার করুন
অপরিবর্তনীয়

-n, --না-চেক
নাগালযোগ্য সমণ্ডগুলিকে নির্মূল করার আগে invariant ধরে রেখেছে কিনা তা পরীক্ষা করবেন না

-e, --না-বর্জন
সারমন্ড বাদ বা সরলীকরণ করবেন না, তবে প্রতিটি শর্তে অপরিবর্তনীয় যোগ করুন

-pপ্রিফিক্স, --প্রিন্ট-ডট=প্রিফিক্স
ফলাফল বিডিডির একটি .dot ফাইল সংরক্ষণ করুন যদি এটি নির্ধারণ করা অসম্ভব হয় কিনা a
summand invariant লঙ্ঘন করে; আউটপুট ফাইলের উপসর্গ হিসাবে PREFIX ব্যবহার করা হবে

-QNUM টি, --ক্লিমিট=NUM টি
কোয়ান্টিফায়ারের গণনাকে NUM ভেরিয়েবলে সীমাবদ্ধ করুন। (ডিফল্ট NUM=1000, NUM=0 এর জন্য
সীমাহীন)।

-rNAME এর, --পুনঃ লেখক=NAME এর
পুনর্লিখন কৌশল ব্যবহার করুন NAME: 'jitty' jitty রিরাইটিং (ডিফল্ট) 'jittyc' সংকলিত
jitty rewriting 'jittyp' jitty rewriting with prover

-l, --সরলীকরণ-সমস্ত
সমস্ত সমমানের শর্তগুলিকে সরলীকরণ করুন, শুধুমাত্র সমমানগুলিকে বাদ দেওয়ার পরিবর্তে
যার শর্তগুলি invariant-এর সাথে মিলিত হয় দ্বন্দ্ব

-zসমাধান, --smt-সলভার=সমাধান
অভ্যন্তরীণভাবে ব্যবহৃত BDDs থেকে অসামঞ্জস্যপূর্ণ পথগুলি সরাতে SOLVER ব্যবহার করুন (ডিফল্টরূপে,
কোন পথ নির্মূল প্রয়োগ করা হয় না): 'cvc' SMT সমাধানকারী CVC3

-tLIMIT টি, --সময় সীমা=LIMIT টি
একটি একক সূত্র প্রমাণ করতে সর্বাধিক LIMIT সেকেন্ড ব্যয় করুন

--সময়[=ফাইল]
সময় পরিমাপ FILE এ যোগ করুন। পরিমাপ স্ট্যান্ডার্ড ত্রুটি লিখিত হয় যদি
কোন FILE প্রদান করা হয় না

স্ট্যান্ডার্ড বিকল্প:

-q, -- শান্ত
সতর্কতা বার্তা প্রদর্শন করবেন না

-v, -- ভারবোস
সংক্ষিপ্ত মধ্যবর্তী বার্তা প্রদর্শন করুন

-d, --ডিবাগ
বিস্তারিত মধ্যবর্তী বার্তা প্রদর্শন করুন

--লগ-স্তর=লেভেল
স্তর পর্যন্ত এবং সহ মধ্যবর্তী বার্তা প্রদর্শন করুন

-h, --help
সাহায্য তথ্য প্রদর্শন

--সংস্করণ
প্রদর্শন সংস্করণ তথ্য

onworks.net পরিষেবা ব্যবহার করে lpsinvelm অনলাইন ব্যবহার করুন