Promela
প্রোমেলা (প্রসেস বা প্রোটোকল মেটা ল্যাঙ্গুয়েজ) হল জেরার্ড জে. হোলজম্যান দ্বারা প্রবর্তিত একটি যাচাইকরণ মডেলিং ভাষা। ভাষাটি মডেলের সমবর্তী প্রক্রিয়াগুলির গতিশীল সৃষ্টির অনুমতি দেয়, উদাহরণস্বরূপ, বিতরণ ব্যবস্থা। প্রোমেলা মডেলগুলিতে, বার্তা চ্যানেলের মাধ্যমে যোগাযোগকে সিঙ্ক্রোনাস (অর্থাৎ, মিলনস্থল), বা অ্যাসিঙ্ক্রোনাস (অর্থাৎ, বাফার) হিসাবে সংজ্ঞায়িত করা যেতে পারে। মডেল করা সিস্টেমটি কাঙ্ক্ষিত আচরণ তৈরি করে কিনা তা যাচাই করার জন্য প্রোমেলা মডেলগুলি স্পিন মডেল চেকারের সাহায্যে বিশ্লেষণ করা যেতে পারে। কম্পিউটার এডেড ভেরিফিকেশন অফ অটোমাটা (সিএভিএ) প্রকল্পের অংশ হিসাবে ইসাবেল/এইচওএল-এর সাথে যাচাই করা একটি বাস্তবায়নও পাওয়া যায়। প্রোমেলায় লেখা ফাইলগুলিতে ঐতিহ্যগতভাবে একটি. পি. এম. এল ফাইল এক্সটেনশন থাকে। ভূমিকা প্রোমেলা একটি প্রক্রিয়া-মডেলিং ভাষা যার উদ্দেশ্য হল সমান্তরাল ব্যবস্থার যুক্তি যাচাই করা। প্রোমেলায় একটি প্রোগ্রাম দেওয়া হলে, স্পিন মডেল করা সিস্টেমের কার্যকরকরণের এলোমেলো বা পুনরাবৃত্তিমূলক সিমুলেশন সম্পাদন করে সঠিকতার জন্য মডেলটি যাচাই করতে পারে, অথবা এটি একটি সি প্রোগ্রাম তৈরি করতে পারে যা সিস্টেম স্টেট স্পেসের দ্রুত সম্পূর্ণ যাচাইকরণ সম্পাদন করে। সিমুলেশন এবং যাচাইকরণের সময়, স্পিন ডেডলক, অনির্দিষ্ট অভ্যর্থনা এবং অব্যবহৃত কোডের অনুপস্থিতি পরীক্ষা করে। ভেরিফায়ারটি সিস্টেমের অপরিবর্তনীয়গুলির সঠিকতা প্রমাণ করতেও ব্যবহার করা যেতে পারে এবং এটি অ-অগ্রগতি সম্পাদন চক্র খুঁজে পেতে পারে। পরিশেষে, এটি রৈখিক সময় সাময়িক সীমাবদ্ধতার যাচাইকরণকে সমর্থন করে; হয় প্রোমেলা কখনই দাবি করে না বা সরাসরি সাময়িক যুক্তিতে সীমাবদ্ধতাগুলি তৈরি করে। প্রতিটি মডেলকে পরিবেশ সম্পর্কে বিভিন্ন ধরনের অনুমানের অধীনে স্পিন দিয়ে যাচাই করা যেতে পারে। একবার স্পিন দিয়ে একটি মডেলের সঠিকতা প্রতিষ্ঠিত হয়ে গেলে, সেই তথ্যটি পরবর্তী সমস্ত মডেলের নির্মাণ এবং যাচাইকরণে ব্যবহার করা যেতে পারে। প্রোমেলা প্রোগ্রামগুলি প্রক্রিয়া, বার্তা চ্যানেল এবং পরিবর্তনশীল নিয়ে গঠিত। প্রক্রিয়াগুলি হল বৈশ্বিক বস্তু যা বণ্টিত ব্যবস্থার সমবর্তী সত্তার প্রতিনিধিত্ব করে। বার্তা চ্যানেল এবং পরিবর্তনশীল একটি প্রক্রিয়ার মধ্যে বিশ্বব্যাপী বা স্থানীয়ভাবে ঘোষণা করা যেতে পারে। প্রক্রিয়াগুলি আচরণ নির্দিষ্ট করে, চ্যানেল এবং গ্লোবাল ভেরিয়েবলগুলি সেই পরিবেশকে সংজ্ঞায়িত করে যেখানে প্রক্রিয়াগুলি চলে। ভাষা রেফারেন্স ডেটা প্রকার PROMELA-তে ব্যবহৃত মৌলিক ডেটা প্রকারগুলি নীচের সারণিতে উপস্থাপন করা হয়েছে। একটি পিসি আই386/লিনাক্স মেশিনের জন্য বিটের আকার দেওয়া হয়েছে। বিট এবং বুল নামগুলি একটি একক বিট তথ্যের সমার্থক। একটি বাইট হল একটি স্বাক্ষরহীন পরিমাণ যা 0 এবং 255 এর মধ্যে একটি মান সংরক্ষণ করতে পারে। শর্টস এবং ইন্টগুলি স্বাক্ষরিত পরিমাণ যা কেবল তাদের ধরে রাখতে পারে এমন মানের পরিসরে পৃথক হয়। ভেরিয়েবলগুলিকে অ্যারে হিসাবেও ঘোষণা করা যেতে পারে। উদাহরণস্বরূপ, ঘোষণাঃ 10 টি পূর্ণসংখ্যার একটি অ্যারে ঘোষণা করে যা অ্যারে সাবস্ক্রিপ্ট এক্সপ্রেশনগুলিতে অ্যাক্সেস করা যেতে পারে যেমনঃ x [0] = x [1] + x [2]; তবে অ্যারেগুলি সৃষ্টির সময় গণনা করা যায় না, তাই সেগুলি অবশ্যই নিম্নরূপ শুরু করা উচিতঃ একটি অ্যারের সূচক এমন কোনও এক্সপ্রেশন হতে পারে যা একটি অনন্য পূর্ণসংখ্যা মান নির্ধারণ করে। সীমার বাইরে একটি সূচকের প্রভাব অনির্ধারিত। বহুমাত্রিক অ্যারেগুলি পরোক্ষভাবে টাইপেডেফ গঠনের সাহায্যে সংজ্ঞায়িত করা যেতে পারে (নীচে দেখুন)। প্রক্রিয়া একটি পরিবর্তনশীল বা একটি বার্তা চ্যানেলের অবস্থা শুধুমাত্র প্রক্রিয়া দ্বারা পরিবর্তন বা পরিদর্শন করা যেতে পারে। একটি প্রক্রিয়ার আচরণ একটি প্রক্টাইপ ঘোষণা দ্বারা সংজ্ঞায়িত করা হয়। উদাহরণস্বরূপ, নিম্নলিখিতটি একটি পরিবর্তনশীল অবস্থা সহ একটি প্রক্রিয়া প্রকার এ ঘোষণা করেঃ প্রক্টাইপ এ () {বাইট অবস্থা; অবস্থা = 3;} প্রক্টাইপ সংজ্ঞাটি শুধুমাত্র প্রক্রিয়া আচরণ ঘোষণা করে, এটি কার্যকর করে না। প্রাথমিকভাবে, PROMELA মডেলে, শুধুমাত্র একটি প্রক্রিয়া কার্যকর করা হবেঃ init টাইপের একটি প্রক্রিয়া, যা প্রতিটি PROMELA স্পেসিফিকেশনে স্পষ্টভাবে ঘোষণা করতে হবে। রান স্টেটমেন্ট ব্যবহার করে নতুন প্রক্রিয়াগুলি তৈরি করা যেতে পারে, যা একটি প্রক্টাইপের নাম নিয়ে গঠিত একটি যুক্তি গ্রহণ করে, যেখান থেকে একটি প্রক্রিয়া তাত্ক্ষণিকভাবে তৈরি করা হয়। রান অপারেটর শুধুমাত্র প্রাথমিক প্রক্রিয়ায় নয়, প্রক্টাইপ সংজ্ঞার মূল অংশেও ব্যবহার করা যেতে পারে। এটি প্রোমেলায় প্রক্রিয়াগুলির গতিশীল সৃষ্টির অনুমতি দেয়। একটি সম্পাদন প্রক্রিয়া শেষ হয়ে গেলে অদৃশ্য হয়ে যায়-অর্থাৎ, যখন এটি প্রক্টাইপ সংজ্ঞায় শরীরের শেষে পৌঁছায় এবং এটি শুরু করা সমস্ত শিশু প্রক্রিয়া শেষ হয়ে যায়। একটি প্রক্টাইপ সক্রিয়ও থাকতে পারে (নীচে)। পারমাণবিক গঠন পারমাণবিক শব্দের সাথে কোঁকড়ানো বন্ধনীতে আবদ্ধ বিবৃতিগুলির একটি ক্রমের উপসর্গ স্থাপন করে, ব্যবহারকারী নির্দেশ করতে পারেন যে ক্রমটি একটি অবিভাজ্য একক হিসাবে কার্যকর করা হবে, অন্য কোনও প্রক্রিয়ার সাথে অ-সংযুক্ত। পারমাণবিক ক্রম যাচাইকরণ মডেলের জটিলতা হ্রাসে একটি গুরুত্বপূর্ণ হাতিয়ার হতে পারে। লক্ষ্য করুন যে পারমাণবিক ক্রমগুলি একটি বিতরণ ব্যবস্থায় অনুমোদিত ইন্টারলিভিংয়ের পরিমাণকে সীমাবদ্ধ করে। জটিল মডেলগুলিকে পারমাণবিক ক্রমের সাথে স্থানীয় চলকগুলির সমস্ত ম্যানিপুলেশন লেবেল করে ট্র্যাক্টেবল করা যেতে পারে। বার্তা প্রেরণকারী বার্তা চ্যানেলগুলি এক প্রক্রিয়া থেকে অন্য প্রক্রিয়ায় তথ্য স্থানান্তরের মডেল তৈরি করতে ব্যবহৃত হয়। এগুলি স্থানীয়ভাবে বা বিশ্বব্যাপী ঘোষণা করা হয়, উদাহরণস্বরূপঃ চ্যান ক্যুনম = [16] অফ {শর্ট} এটি একটি বাফার চ্যানেল ঘোষণা করে যা সংক্ষিপ্ত ধরনের 16টি বার্তা সংরক্ষণ করতে পারে (এখানে ক্ষমতা 16টি)। উক্তিঃ নাম! এক্সপ্রে; এক্সপ্রেশন এক্সপ্রেশনের মানটি চ্যানেলে qname নামে পাঠায়, অর্থাৎ এটি চ্যানেলের লেজের সাথে মানটি যুক্ত করে। উক্তিঃ কি নাম? এম. এস. জি; বার্তাটি গ্রহণ করে, চ্যানেলের প্রধান থেকে এটি পুনরুদ্ধার করে এবং এটি পরিবর্তনশীল এম. এস. জি-তে সংরক্ষণ করে। চ্যানেলগুলি ফার্স্ট-ইন-ফার্স্ট-আউট ক্রমে বার্তা পাঠায়। একটি মিলন বন্দরকে দোকানের দৈর্ঘ্য শূন্য সহ একটি বার্তা চ্যানেল হিসাবে ঘোষণা করা যেতে পারে। উদাহরণস্বরূপ, নিম্নলিখিতঃ {byte}-এর চ্যান পোর্ট = [0] একটি মিলন বন্দরকে সংজ্ঞায়িত করে যা টাইপ বাইটের বার্তা প্রেরণ করতে পারে। এই ধরনের মিলিত বন্দরগুলির মাধ্যমে বার্তার মিথস্ক্রিয়া সংজ্ঞায়িতভাবে সিঙ্ক্রোনাস, অর্থাৎ। প্রেরক বা রিসিভার (যিনি প্রথমে চ্যানেলে আসবেন) দ্বিতীয় স্থানে আসা প্রতিযোগীকে (রিসিভার বা প্রেরক) ব্লক করবেন। যখন একটি বাফার করা চ্যানেল তার ক্ষমতার সাথে পূরণ করা হয় (ইনপুট গ্রহণের আগে আউটপুটগুলির "ক্ষমতা" সংখ্যা পাঠানো হয়), তখন চ্যানেলের ডিফল্ট আচরণটি সিঙ্ক্রোনাস হয়ে যায় এবং প্রেরক পরবর্তী পাঠানোর সময় ব্লক করে দেয়। লক্ষ্য করুন যে চ্যানেলগুলির মধ্যে কোনও সাধারণ বার্তা বাফার ভাগ করা নেই। ক্রমবর্ধমান জটিলতা, একটি চ্যানেলকে একমুখী এবং পয়েন্ট টু পয়েন্ট হিসাবে ব্যবহার করার তুলনায়, একাধিক রিসিভার বা একাধিক প্রেরকের মধ্যে চ্যানেল ভাগ করে নেওয়া এবং একক ভাগ করা চ্যানেলে স্বাধীন ডেটা-স্ট্রিমগুলিকে একত্রিত করা সম্ভব। এর থেকে দ্বিমুখী যোগাযোগের জন্য একটি একক মাধ্যমও ব্যবহার করা যেতে পারে। নিয়ন্ত্রণ প্রবাহ গঠন প্রোমেলায় তিনটি নিয়ন্ত্রণ প্রবাহ গঠন রয়েছে। সেগুলি হল কেস নির্বাচন, পুনরাবৃত্তি এবং নিঃশর্ত লাফ। কেস নির্বাচন সবচেয়ে সহজ গঠন হল সিলেকশন স্ট্রাকচার। উদাহরণস্বরূপ, a এবং b দুটি চলকের আপেক্ষিক মান ব্যবহার করে কেউ লিখতে পারেনঃ যদিঃঃ (a! = b)-> বিকল্প 1:: (a = = b)-> বিকল্প 2 ফাই নির্বাচন কাঠামোতে দুটি সম্পাদন ক্রম থাকে, যার প্রত্যেকটির আগে একটি ডাবল কোলন থাকে। তালিকা থেকে একটি ক্রম কার্যকর করা হবে। একটি ক্রম শুধুমাত্র তখনই নির্বাচন করা যেতে পারে যখন তার প্রথম বিবৃতিটি সম্পাদনযোগ্য হয়। একটি নিয়ন্ত্রণ অনুক্রমের প্রথম বিবৃতিটিকে গার্ড বলা হয়। উপরের উদাহরণে, রক্ষীরা পারস্পরিক একচেটিয়া, তবে তাদের হওয়ার দরকার নেই। যদি একাধিক গার্ড এক্সিকিউটেবল হয়, তাহলে সংশ্লিষ্ট ক্রমগুলির মধ্যে একটি অনির্ধারিতভাবে নির্বাচন করা হয়। যদি সমস্ত রক্ষী নিষ্ক্রিয় হয়, তবে তাদের মধ্যে একজন নির্বাচিত না হওয়া পর্যন্ত প্রক্রিয়াটি অবরুদ্ধ থাকবে। (বিপরীতে, ওক্যাম প্রোগ্রামিং ভাষা বন্ধ হয়ে যাবে বা কোনও এক্সিকিউটেবল গার্ড ছাড়াই এগিয়ে যেতে সক্ষম হবে না।) যদিঃ (A = = সত্য)-> বিকল্প 1;: (B = = সত্য)-> বিকল্প 2;/* এখানেও আসতে পারে যদি A = = সত্য */:: অন্য-> ফলথ্রু বিকল্প; ফাই অ-নির্ধারক পছন্দের পরিণতি হল, উপরের উদাহরণে, যদি A সত্য হয়, তবে উভয় পছন্দই নেওয়া যেতে পারে। "ঐতিহ্যবাহী" প্রোগ্রামিং-এ, একজন ক্রমানুসারে একটি "যদি-যদি-অন্য" কাঠামো বুঝতে পারবেন। এখানে, যদি-ডাবল কোলন-ডাবল কোলনকে অবশ্যই "যে কেউ প্রস্তুত" হিসাবে বুঝতে হবে এবং যদি কেউ প্রস্তুত না থাকে তবেই বাকিটি নেওয়া হবে। যদিঃ: মান = 3;:: মান = 4; ফাই উপরের উদাহরণে, মানটি অনির্ধারিতভাবে 3 বা 4 দেওয়া হয়। দুটি ছদ্ম-বিবৃতি রয়েছে যা রক্ষী হিসাবে ব্যবহার করা যেতে পারেঃ সময়সীমা বিবৃতি এবং অন্য বিবৃতি। টাইমআউট বিবৃতি একটি বিশেষ শর্তের মডেল তৈরি করে যা একটি প্রক্রিয়াটিকে এমন একটি শর্তের জন্য অপেক্ষা বাতিল করার অনুমতি দেয় যা কখনও সত্য হতে পারে না। অন্য বিবৃতিটি একটি নির্বাচন বা পুনরাবৃত্তির বিবৃতিতে শেষ বিকল্প ক্রমের প্রাথমিক বিবৃতি হিসাবে ব্যবহার করা যেতে পারে। যদি একই সিলেকশনের অন্যান্য সমস্ত অপশন এক্সিকিউটেবল না হয় তবেই এ্যালস এক্সিকিউটেবল। এছাড়াও, অন্যগুলি চ্যানেলের সাথে একসাথে ব্যবহার করা নাও হতে পারে। পুনরাবৃত্তি (লুপ) নির্বাচন কাঠামোর একটি যৌক্তিক সম্প্রসারণ হল পুনরাবৃত্তি কাঠামো। উদাহরণস্বরূপঃ ডুঃঃ কাউন্ট = কাউন্ট + 1:: a = b + 2:: (কাউন্ট = = 0)-> ব্রেক ওড প্রোমেলায় একটি পুনরাবৃত্তি কাঠামো বর্ণনা করে। একটি সময়ে শুধুমাত্র একটি বিকল্প নির্বাচন করা যেতে পারে। বিকল্পটি সম্পূর্ণ হওয়ার পরে, কাঠামোর সম্পাদন পুনরাবৃত্তি করা হয়। পুনরাবৃত্তি কাঠামোটি শেষ করার স্বাভাবিক উপায় হল একটি বিরতি বিবৃতি। এটি নিয়ন্ত্রণকে নির্দেশে স্থানান্তরিত করে যা অবিলম্বে পুনরাবৃত্তি কাঠামো অনুসরণ করে। শর্তহীন লাফ একটি লুপ ভাঙার আরেকটি উপায় হল গোটো বিবৃতি। উদাহরণস্বরূপ, উপরের উদাহরণটি নিম্নরূপ পরিবর্তন করা যেতে পারেঃ করুনঃঃ গণনা = গণনা + 1:: a = b + 2:: (গণনা = = 0)-> সম্পন্ন হয়েছে od সম্পন্ন হয়েছেঃ এড়িয়ে চলুন; এই উদাহরণে গোটো সম্পন্ন নামে একটি লেবেলে ঝাঁপিয়ে পড়ে। একটি লেবেল শুধুমাত্র একটি বিবৃতির আগে উপস্থিত হতে পারে। উদাহরণস্বরূপ, প্রোগ্রামের শেষে ঝাঁপ দেওয়ার জন্য, একটি ডামি স্টেটমেন্ট স্কিপ দরকারীঃ এটি এমন একটি স্থান-ধারক যা সর্বদা কার্যকরযোগ্য এবং এর কোনও প্রভাব নেই। দাবিগুলি প্রোমেলার একটি গুরুত্বপূর্ণ ভাষা গঠন যার সামান্য ব্যাখ্যার প্রয়োজন তা হল দাবি বিবৃতি। ফর্মের বিবৃতিঃ দাবি (যে কোনও _ বুলিয়ান _ শর্ত) সর্বদা কার্যকরযোগ্য। যদি একটি নির্দিষ্ট বুলিয়ান শর্ত থাকে, তবে বিবৃতিটির কোনও প্রভাব নেই। যাইহোক, যদি শর্তটি অগত্যা ধরে না থাকে, তবে বিবৃতিটি স্পিন দিয়ে যাচাইয়ের সময় একটি ত্রুটি তৈরি করবে। জটিল তথ্য কাঠামো পূর্বনির্ধারিত বা পূর্ববর্তী সংজ্ঞায়িত প্রকারের তথ্য বস্তুর তালিকার জন্য একটি নতুন নাম প্রবর্তন করতে একটি প্রোমেলা সংজ্ঞা ব্যবহার করা যেতে পারে। নতুন ধরনের নামটি নতুন ডেটা অবজেক্টগুলি ঘোষণা এবং তাত্ক্ষণিক করার জন্য ব্যবহার করা যেতে পারে, যা যে কোনও প্রসঙ্গে সুস্পষ্ট উপায়ে ব্যবহার করা যেতে পারেঃ টাইপডেফ নির্মাণে ঘোষিত ক্ষেত্রগুলিতে অ্যাক্সেস সি প্রোগ্রামিং ভাষার মতো একই পদ্ধতিতে করা হয়। উদাহরণস্বরূপঃ মাইস্ট্রাকট x; x.Field1 = 1; একটি বৈধ PROMELA ক্রম যা পরিবর্তনশীল x এর ফিল্ড 1 ক্ষেত্রকে মান 1 প্রদান করে। সক্রিয় প্রক্টাইপ সক্রিয় কীওয়ার্ডটি যে কোনও প্রক্টাইপ সংজ্ঞার সাথে যুক্ত করা যেতে পারে। যদি মূলশব্দটি উপস্থিত থাকে, তবে সেই প্রক্টাইপের একটি উদাহরণ প্রাথমিক সিস্টেম অবস্থায় সক্রিয় থাকবে। সেই প্রক্টাইপের একাধিক তাৎক্ষণিকতা কীওয়ার্ডের একটি ঐচ্ছিক অ্যারে প্রত্যয় দিয়ে নির্দিষ্ট করা যেতে পারে। উদাহরণস্বরূপঃ অ্যাক্টিভ প্রক্টাইপ এ () {.} অ্যাক্টিভ [4] প্রক্টাইপ বি () {.} এক্সিকিউটেবিলিটি এক্সিকিউটেবিলিটির শব্দার্থ প্রোমেলায় মডেলিং প্রক্রিয়া সিঙ্ক্রোনাইজেশনের জন্য মৌলিক উপায় সরবরাহ করে। mtype = {M _ UP, M _ DW}; চ্যান চ্যান ডেটা ডাউন = [0] এর {mtype}; চ্যান চ্যান ডেটা আপ = [0] এর {mtype}; প্রক্টাইপ পি1 (চ্যান চ্যান ডেটা ইন, চ্যান ডেটা আউট) {করবেনঃ: চ্যান ডেটা ইন? M _ UP-> এড়িয়ে চলুন;:: চ্যান _ ডেটা _ আউট! M _ DW-> এড়িয়ে চলুন; od;}; প্রক্টাইপ P2 (চ্যান চ্যান ডেটা _ ইন, চ্যান ডেটা _ আউট) {করবেনঃ: চ্যান ডেটা _ ইন? এম _ ডিডাব্লু-> এড়িয়ে যান;:: চ্যান _ ডেটা _ আউট! M _ UP-> স্কিপ; od;}; init {atomic {অমলু P1 (চ্যান _ ডেটা _ আপ, চ্যান _ ডেটা _ ডাউন); চালান P2 (চ্যান _ ডেটা _ ডাউন, চ্যান _ ডেটা _ আপ);}} উদাহরণস্বরূপ, দুটি প্রক্রিয়া P1 এবং P2-এর (1) অন্য থেকে ইনপুট বা (2) অন্যটিতে আউটপুটের অ-নির্ধারিত পছন্দ রয়েছে। দুটি মিলিত হাত মেলানো সম্ভব, বা সম্পাদনযোগ্য, এবং তাদের মধ্যে একটি বেছে নেওয়া হয়। চিরকালের জন্য এর পুনরাবৃত্তি ঘটবে। অতএব, এই মডেলটি অচল হবে না। স্পিন যখন উপরের মত একটি মডেল বিশ্লেষণ করে, তখন এটি একটি অনির্ধারিত অ্যালগরিদম দিয়ে পছন্দগুলি যাচাই করবে, যেখানে সমস্ত এক্সিকিউটেবল পছন্দগুলি অন্বেষণ করা হবে। যাইহোক, যখন স্পিনের সিমুলেটর সম্ভাব্য অ-যাচাইকৃত যোগাযোগের নিদর্শনগুলি কল্পনা করে, তখন এটি "অ-নির্ধারক" পছন্দটি সমাধান করতে একটি এলোমেলো জেনারেটর ব্যবহার করতে পারে। অতএব, সিমুলেটর একটি খারাপ এক্সিকিউশন দেখাতে ব্যর্থ হতে পারে (উদাহরণস্বরূপ, কোনও খারাপ ট্রেইল নেই)। এটি যাচাইকরণ এবং অনুকরণের মধ্যে একটি পার্থক্য চিত্রিত করে। উপরন্তু, রিফাইনমেন্ট ব্যবহার করে প্রোমেলা মডেল থেকে এক্সিকিউটেবল কোড তৈরি করাও সম্ভব। কীওয়ার্ড নিম্নলিখিত শনাক্তকারীগুলি কীওয়ার্ড হিসাবে ব্যবহারের জন্য সংরক্ষিত। রেফারেন্স বাহ্যিক লিঙ্ক স্পিন হোমপেজ স্পিন টিউটোরিয়াল এবং অনলাইন রেফারেন্স সংক্ষিপ্ত প্রোমেলা রেফারেন্স কম্পিউটার এডেড ভেরিফিকেশন অফ অটোম্যাটাঃ "দ্য সিএভিএ প্রজেক্ট" (2010-2019) এবং "ভেরিফাইড মডেল চেকার্স" (2016-সিআরআর) ওয়েবসাইট নির্দিষ্টকরণ ভাষা মডেল চেকার