TAPAAL Model Checker
ট্যাপাল হল ডেনমার্কের আলবার্গ বিশ্ববিদ্যালয়ের কম্পিউটার বিজ্ঞান বিভাগে তৈরি টাইমড-আর্ক পেট্রি নেটের মডেলিং, সিমুলেশন এবং যাচাইকরণের একটি সরঞ্জাম এবং এটি লিনাক্স, উইন্ডোজ এবং ম্যাক ওএস এক্স প্ল্যাটফর্মের জন্য উপলব্ধ। টাইমড-আর্ক পেট্রি নেট (টিএপিএন) হল ধ্রুপদী পেট্রি নেট মডেলের একটি সময় সম্প্রসারণ (1962 সালে কার্ল অ্যাডাম পেট্রি তাঁর গবেষণাপত্রে প্রবর্তিত বিতরণকৃত গণনার একটি সাধারণভাবে ব্যবহৃত গ্রাফিকাল মডেল)। টিএপিএন-এ বিবেচিত সময় সম্প্রসারণ রিয়েল-টাইমের স্পষ্ট চিকিত্সার অনুমতি দেয়, যা নেটের টোকেনের সাথে যুক্ত (প্রতিটি টোকেনের নিজস্ব বয়স রয়েছে) এবং স্থান থেকে ট্রানজিশনে চাপগুলি সময়ের ব্যবধান দ্বারা লেবেল করা হয় যা টোকেনের বয়সকে সীমাবদ্ধ করে যা সংশ্লিষ্ট ট্রানজিশন চালানোর জন্য ব্যবহার করা যেতে পারে। টি. এ. পি. এ. এ. এল সরঞ্জামটিতে পরিবহন চাপের সাথে বয়সের অপরিবর্তনীয় (যা পূর্বে রিড-আর্ক হিসাবে বিবেচিত হওয়ার তুলনায় বেশি অভিব্যক্তিপূর্ণ) এবং প্রতিরোধক চাপের সাথে এই মডেলটির আরও সম্প্রসারণ প্রয়োগ করা হয়। টি. এ. পি. এ. এল টুলটি টি. এ. পি. এন মডেল আঁকার জন্য একটি গ্রাফিক্যাল এডিটর, নকশাকৃত জাল নিয়ে পরীক্ষা-নিরীক্ষার জন্য সিমুলেটর এবং একটি যাচাইকরণ পরিবেশ প্রদান করে যা স্বয়ংক্রিয়ভাবে সি. টি. এল লজিকের একটি উপসেটে তৈরি যৌক্তিক প্রশ্নের উত্তর দেয় (মূলত ই. এফ, ই. জি, এ. এফ, এ. জি সূত্র নেস্টিং ছাড়াই)। এটি ব্যবহারকারীকে একটি প্রদত্ত নেট একটি প্রদত্ত সংখ্যা k-এর জন্য কে-বাউন্ডেড কিনা তা পরীক্ষা করার অনুমতি দেয়। তপাল তার নিজস্ব যাচাইকরণ ইঞ্জিনগুলির সাথে সজ্জিত যা তপালের সাথে একসাথে বিতরণ করা হয় (একটি অবিচ্ছিন্ন সময়ের জন্য এবং একটি পৃথক সময়ের জন্য)। ঐচ্ছিকভাবে, ব্যবহারকারী স্বয়ংক্রিয়ভাবে ট্যাপাল মডেলগুলিকে ইউ. পি. পি. এ. এ. এল-এ অনুবাদ করতে পারেন এবং ইউ. পি. পি. এ. এ. এল যাচাইকরণ ইঞ্জিনের উপর নির্ভর করতে পারেন। বাহ্যিক লিঙ্ক ট্যাপাল ওয়েবসাইট, ডিইএস ইউনিট ডাউনলোড করুন, কম্পিউটার বিজ্ঞান বিভাগ, আলবার্গ বিশ্ববিদ্যালয়, ডেনমার্ক ট্যাপালঃ সম্পাদক, সিমুলেটর এবং টাইমড-আর্ক পেট্রি নেটের যাচাইকারী জে. বাইগ, কে. ওয়াই। জর্জেনসেন এবং জে. সারবা, এটিভিএ '09, স্প্রিংগার অ্যান এফিশিয়েন্ট ট্রান্সলেশন অফ টাইমড-আর্ক পেট্রি নেটস টু নেটওয়ার্কস অফ টাইমড অটোমাটা জে. বাইগ, কে. ওয়াই। জর্জেনসেন এবং জে. সারবা, আই. সি. এফ. ই. এম '09, স্প্রিংগার এ ফ্রেমওয়ার্ক ফর রিলেটিং টাইমড ট্রানজিশন সিস্টেমস অ্যান্ড প্রিজারভিং টি. সি. টি. এল মডেল চেকিং এল জ্যাকবসেন, এম জ্যাকবসেন, এম. এইচ। মোলার এবং জে. সারবা, ইপিইডব্লিউ '10, স্প্রিংগার ভেরিফিকেশন অফ টাইমড-আর্ক পেট্রি নেটস এল জ্যাকবসেন, এম জ্যাকবসেন, এম. এইচ। মোলার এবং জে. সারবা, সোফসেম '11, স্প্রিঙ্গার রেফারেন্স মডেল চেকার্স