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

কার্যক্রম:

NAME এর

lps2lts - একটি LPS থেকে একটি LTS তৈরি করুন

সাইনোপিসিস

lps2lts [অনুযায়ী OPTION]... [ইনফাইল [আউটফাইল]]

বর্ণনাঃ

INFILE-এ LPS থেকে একটি LTS তৈরি করুন এবং ফলাফলটি OUTFILE-এ সংরক্ষণ করুন। যদি INFILE না হয়
সরবরাহ করা হয়, stdin ব্যবহার করা হয়। OUTFILE সরবরাহ করা না হলে, LTS সংরক্ষণ করা হয় না।

যদি 'jittyc' রিরাইটার ব্যবহার করা হয়, তাহলে MCRL2_COMPILEREWRITER পরিবেশ পরিবর্তনশীল
(ডিফল্ট মান: 'mcrl2compilerewriter') স্ক্রিপ্ট নির্ধারণ করে যা পুনঃরায়টার সংকলন করে,
এবং MCRL2_COMPILEDIR (ডিফল্ট মান: '.') অস্থায়ী ফাইলগুলি কোথায় সংরক্ষণ করা হবে তা নির্ধারণ করে।

মনে রাখবেন যে lps2lts যেকোন জোড়ার মধ্যে একই লেবেল সহ একাধিক রূপান্তর প্রদান করতে পারে
রাজ্যগুলি যদি এটি পছন্দসই না হয়, তাহলে একটি শক্তিশালী প্রয়োগ করে এই ধরনের পরিবর্তনগুলি সরানো যেতে পারে
বিসিমুলেশন রিডাক্টন উদাহরণস্বরূপ ltsconvert টুল ব্যবহার করে।

OUTFILE এর বিন্যাস তার এক্সটেনশন দ্বারা নির্ধারিত হয় (যদি না এটি একটি দ্বারা নির্দিষ্ট করা হয়
বিকল্প)। সমর্থিত ফর্ম্যাটগুলি হল:

Aldebaran বিন্যাসের জন্য 'aut' (CADP),
গ্রাফভিজ ফরম্যাটের জন্য 'ডট' (ইনপুট ফরম্যাট হিসেবে আর সমর্থিত নয়),
ফিনিট স্টেট মেশিন ফরম্যাটের জন্য 'fsm', বা
mCRL2 LTS ফরম্যাটের জন্য 'lts' যদি jittyc রিরাইটার ব্যবহার করা হয়, তাহলে
MCRL2_COMPILEREWRITER পরিবেশ পরিবর্তনশীল (ডিফল্ট মান: mcrl2compilereWRITER)
স্ক্রিপ্ট নির্ধারণ করে যেটি রিরাইটারকে কম্পাইল করে এবং MCRL2_COMPILEDIR (ডিফল্ট মান:
'.') অস্থায়ী ফাইলগুলি কোথায় সংরক্ষণ করা হবে তা নির্ধারণ করে। উল্লেখ্য যে lps2lts একাধিক প্রদান করতে পারে
যেকোনো জোড়া রাজ্যের মধ্যে একই লেবেল সহ রূপান্তর। যদি এই কাঙ্ক্ষিত না হয়, যেমন
উদাহরণস্বরূপ ব্যবহার করে একটি শক্তিশালী বিসিমুলেশন রিডাক্টন প্রয়োগ করে রূপান্তরগুলি সরানো যেতে পারে
টুলটি রূপান্তর করে।

বিকল্প

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

-aনামস, --কর্ম=নামস
ট্রানজিশন সিস্টেমে অ্যাকশন সনাক্ত করুন এবং রিপোর্ট করুন যেগুলির থেকে অ্যাকশন নাম রয়েছে
NAMES, একটি কমা দ্বারা পৃথক করা তালিকা৷ এটি উদাহরণস্বরূপ খুঁজে পেতে দরকারী (বা প্রমাণ করুন
অনুপস্থিতি) একটি কর্ম ত্রুটি। প্রতিটি ঘটনার জন্য একটি বার্তা মুদ্রিত হয়
এই কর্ম নাম. এই ক্রিয়াগুলির দিকে -t ফ্ল্যাগ ট্রেস তৈরি করা হয়

-b[NUM টি], --বিট-হ্যাশ[=NUM টি]
রাজ্যগুলি সংরক্ষণ করতে এবং সর্বাধিক NUMটি রাজ্যে সংরক্ষণ করতে বিট হ্যাশিং ব্যবহার করুন৷ এই যে মানে
পরিদর্শন করা হয়েছে এমন সমস্ত রাজ্যের একটি সম্পূর্ণ রেকর্ড রাখার পরিবর্তে, একটি বিট অ্যারে
ব্যবহার করা হয় যা নির্দেশ করে যে একটি রাষ্ট্রের একটি হ্যাশ আগে দেখা গেছে কিনা।
যদিও এর মানে হল যে এই বিকল্পটি অন্যদের জন্য রাজ্যগুলিকে ভুল হতে পারে
(কারণ সেগুলি একই হ্যাশে ম্যাপ করা হয়েছে), এটি খুব বড় অন্বেষণ করতে কার্যকর হতে পারে
LTS যেগুলি অন্যথায় অন্বেষণযোগ্য নয়৷ NUM এর জন্য ডিফল্ট মান প্রায়
2*10^8 (এটি প্রায় 25MB মেমরির সাথে মিলে যায়)

--ক্যাশেড
রাষ্ট্রীয় স্থান উৎপাদনের গতি বাড়াতে গণনা ক্যাশিং কৌশল ব্যবহার করুন।

-c[NAME এর], --সঙ্গম[=NAME এর]
অ্যাকশন লেবেল NAME দিয়ে ট্রানজিশনের অগ্রাধিকার প্রয়োগ করুন।(যখন NAME নেই
সরবরাহকৃত (অর্থাৎ, '-c') 'ctau' ক্রিয়াকে অগ্রাধিকার দেওয়া হয়। অগ্রাধিকার দিতে
পতাকা ব্যবহার করতে tau -ctau. উল্লেখ্য যে রৈখিক প্রক্রিয়া যদি টাউ-সঙ্গম না হয়,
উত্পন্ন রাষ্ট্রীয় স্থান অগত্যা রাষ্ট্রীয় স্থানের অনুরূপ শাখায় বিভক্ত
এলপিএস যে প্রজন্মের অ্যালগরিদম ব্যবহার করা হয় তার রৈখিক প্রক্রিয়ার প্রয়োজন হয় না
to be tau convergent

-D, --অচলাবস্থা
অচলাবস্থা সনাক্ত করুন (যেমন প্রতিটি অচলাবস্থার জন্য একটি বার্তা মুদ্রিত হয়)

-F, -- ভিন্নতা
বিচ্যুতি সনাক্ত করুন (অর্থাৎ বিচ্যুতি সহ প্রতিটি রাজ্যের জন্য (=টাউ লুপ) একটি বার্তা
মুদ্রিত)। ভিন্নতা সনাক্ত করার অ্যালগরিদম প্রতিটি রাজ্যের জন্য রৈখিক, তাই
রাষ্ট্রীয় মহাকাশ অন্বেষণ এই বিকল্পের সাথে চতুর্মুখী হয়ে ওঠে, যার ফলে একটি রাষ্ট্র হয়
এই বিকল্পটি সক্ষম হলে মহাকাশ অনুসন্ধান ধীর হয়ে যাবে।

-ybool, --ডামি=bool
BOOL-এর মানের উপর ভিত্তি করে LPS-এ মুক্ত ভেরিয়েবলগুলিকে ডামি মান দিয়ে প্রতিস্থাপন করুন:
'হ্যাঁ' (ডিফল্ট) বা 'না'

--ত্রুটি-ট্রেস
অন্বেষণের সময় যদি একটি ত্রুটি ঘটে, তবে সেই অবস্থায় একটি ট্রেস সংরক্ষণ করুন যা হতে পারে না
অন্বেষণ

--init-tsize=NUM টি
অভ্যন্তরীণভাবে ব্যবহৃত হ্যাশ টেবিলের প্রাথমিক আকার সেট করুন (ডিফল্ট হল 10000)

-lNUM টি, -- সর্বোচ্চ=NUM টি
সর্বাধিক NUMটি রাজ্য অন্বেষণ করুন৷

-mনামস, --গুণ=নামস
NAMES থেকে ট্রানজিশন সিস্টেমে মাল্টিঅ্যাকশন সনাক্ত করুন এবং রিপোর্ট করুন, একটি কমা-
পৃথক তালিকা। -a-এর মত কাজ করে, মাল্টি-অ্যাকশনগুলি হুবহু মিলে যাওয়া ছাড়া,
ডেটা প্যারামিটার সহ।

--কোন তথ্য নেই
OUTFILE-এ রাজ্যের তথ্য যোগ করবেন না এই বিকল্পটি ছাড়া lps2lts রাজ্য যোগ করে
LTS থেকে ভেক্টর। এই বিকল্পটি এই তথ্য বাতিল এবং রাজ্যের কারণ হয়
শুধুমাত্র একটি ক্রম সংখ্যা দ্বারা নির্দেশিত হয়। সুস্পষ্ট রাষ্ট্র তথ্য জন্য দরকারী
উদাহরণস্বরূপ, ভিজ্যুয়ালাইজেশন উদ্দেশ্য, কিন্তু OUTFILE বৃদ্ধির কারণ হতে পারে
অনেক. মনে রাখবেন যে AUT বিন্যাসে লেখার সময় এই বিকল্পটি অন্তর্নিহিত।

-oবিন্যাসে, --আউট=বিন্যাসে
নির্দিষ্ট ফরম্যাটে আউটপুট সংরক্ষণ করুন

-- ছাঁটাই
রাষ্ট্রীয় স্থান উৎপাদনের গতি বাড়ানোর জন্য summand pruning ব্যবহার করুন।

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

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

-sNAME এর, --কৌশল=NAME এর
কৌশল NAME ব্যবহার করে রাষ্ট্রীয় স্থান অন্বেষণ করুন: 'b', 'প্রস্থ' প্রস্থ-প্রথম অনুসন্ধান
(ডিফল্ট) 'd', 'depth' depth-first search 'p', 'prioritized' prioritize single
তার প্রথম যুক্তির উপর ক্রিয়াকলাপ সাজানোর ন্যাট যেখানে শুধুমাত্র সেই ক্রিয়াগুলির সাথে
এই পরামিতি জন্য সর্বনিম্ন মান নির্বাচন করা হয়. যেমন যদি কর্ম থাকে a(3) এবং
b(২০১১), a(3) অবশেষ এবং b(4) এড়িয়ে গেছে। সাজানোর প্রথম প্যারামিটার ছাড়া অ্যাকশন
একাধিক ক্রিয়া সহ Nat এবং multation সর্বদা বেছে নেওয়া হয় (বিকল্প হল
পরীক্ষামূলক) 'q', 'rprioritized' কাজকে অগ্রাধিকার দেয় তার প্রথম যুক্তিতে
Nat বাছাই করুন (বিকল্প -- অগ্রাধিকার দেখুন), এবং এ প্রাপ্ত করার জন্য এলোমেলোভাবে একটি নির্বাচন করুন
অগ্রাধিকারযুক্ত র্যান্ডম সিমুলেশন (বিকল্প পরীক্ষামূলক) 'r', 'র্যান্ডম' র্যান্ডম
সিমুলেশন সমস্ত পরবর্তী রাজ্যগুলির মধ্যে একজনকে এলোমেলোভাবে স্বাধীনভাবে নির্বাচিত করা হয় কিনা
এই অবস্থা ইতিমধ্যে পরিলক্ষিত হয়েছে. ফলস্বরূপ, শুধুমাত্র র্যান্ডম সিমুলেশন
একটি অচলাবস্থার সম্মুখীন হলে সমাপ্ত হয়।

--দমন করা
ভার্বোস মোডে, পরিদর্শনের সংখ্যা নির্দেশ করে অগ্রগতি বার্তা প্রিন্ট করবেন না
রাজ্য এবং রূপান্তর। বড় রাষ্ট্রীয় স্থানগুলির জন্য অগ্রগতির বার্তার সংখ্যা হতে পারে
বেশ ভয়ঙ্কর হতে এই বৈশিষ্ট্য তাদের দমন করতে সাহায্য করে. অন্যান্য শব্দমূলক বার্তা,
যেমন অন্বেষণ করা রাজ্যের মোট সংখ্যা, শুধু দৃশ্যমান থাকে।

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

--todo-max=NUM টি
করণীয় তালিকায় সর্বাধিক NUMটি রাজ্য রাখুন; এই বিকল্পটি শুধুমাত্র প্রস্থের জন্য প্রাসঙ্গিক-
প্রথম অনুসন্ধান, যেখানে NUM হল প্রতি স্তরের সর্বোচ্চ সংখ্যা এবং গভীরতার জন্য
প্রথম অনুসন্ধান, যেখানে NUM হল সর্বোচ্চ গভীরতা

-t[NUM টি], -- ট্রেস[=NUM টি]
প্রতিটি রাজ্যে একটি সংক্ষিপ্ততম ট্রেস লিখুন যা থেকে NAMES-এর একটি অ্যাকশনের সাথে পৌঁছেছে৷
বিকল্প --অ্যাকশন, --deadlock-এর সাথে শনাক্ত করা একটি অচলাবস্থা, অথবা একটি বিচ্যুতি
একটি ফাইলে -- divergence দিয়ে সনাক্ত করা হয়েছে। NUMটির বেশি ট্রেস লেখা হবে না। যদি
NUM সরবরাহ করা হয়নি ট্রেসের সংখ্যা সীমাহীন। প্রতিটি ট্রেসের জন্য যা হতে হবে
লিখিত এক্সটেনশন .trc (ট্রেস) সহ একটি অনন্য ফাইল তৈরি করা হবে যেখানে a
প্রাথমিক অবস্থা থেকে অচল অবস্থা পর্যন্ত সংক্ষিপ্ততম ট্রেস। ট্রেস হতে পারে
বেশ মুদ্রিত এবং tracepp ব্যবহার করে অন্যান্য বিন্যাসে রূপান্তরিত।

-u, --অব্যবহৃত-ডেটা
ডেটা স্পেসিফিকেশনের অব্যবহৃত অংশগুলি সরিয়ে ফেলবেন না

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

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

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

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

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

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

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

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