Promela
PROMELA (پروسیس یا پروٹوکول میٹا لینگویج) ایک تصدیقی ماڈلنگ زبان ہے جسے جیرارڈ جے ہولزمین نے متعارف کرایا ہے۔ زبان ماڈل کے لیے ہم آہنگی کے عمل کی متحرک تخلیق کی اجازت دیتی ہے، مثال کے طور پر، تقسیم شدہ نظام۔ PROMELA ماڈلز میں، میسج چینلز کے ذریعے مواصلات کو ہم وقت (یعنی ملاقات)، یا غیر ہم وقت (یعنی بفرڈ) کے طور پر بیان کیا جا سکتا ہے۔ پرومیلا ماڈلز کا تجزیہ اسپن ماڈل چیکر کے ساتھ کیا جا سکتا ہے، تاکہ اس بات کی تصدیق کی جا سکے کہ ماڈل شدہ نظام مطلوبہ طرز عمل پیدا کرتا ہے۔ کمپیوٹر ایڈیڈ ویریفکیشن آف آٹومیٹا (سی اے وی اے) پروجیکٹ کے حصے کے طور پر اسابیل/ایچ او ایل کے ساتھ تصدیق شدہ عمل درآمد بھی دستیاب ہے۔ پرومیلا میں لکھی گئی فائلوں میں روایتی طور پر. پی ایم ایل فائل کی توسیع ہوتی ہے۔ تعارف PROMELA ایک عمل ماڈلنگ زبان ہے جس کا مطلوبہ استعمال متوازی نظاموں کی منطق کی تصدیق کرنا ہے۔ PROMELA میں ایک پروگرام کو دیکھتے ہوئے، اسپن ماڈل شدہ سسٹم کے نفاذ کے بے ترتیب یا تکراری تخروپن انجام دے کر درست ہونے کے لیے ماڈل کی تصدیق کر سکتا ہے، یا یہ ایک C پروگرام تیار کر سکتا ہے جو سسٹم اسٹیٹ اسپیس کی تیز رفتار مکمل تصدیق انجام دیتا ہے۔ تخروپن اور تصدیق کے دوران، اسپن ڈیڈ لاک، غیر متعین استقبالیہ، اور ناقابل عمل کوڈ کی عدم موجودگی کی جانچ کرتا ہے۔ تصدیق کنندہ کو نظام کے غیر متغیرات کی درستگی کو ثابت کرنے کے لیے بھی استعمال کیا جا سکتا ہے اور یہ غیر پیش رفت پر عمل درآمد کے چکروں کو تلاش کر سکتا ہے۔ آخر میں، یہ لکیری وقت کی عارضی رکاوٹوں کی تصدیق کی حمایت کرتا ہے۔ یا تو پرومیلا کبھی دعوی نہیں کرتا ہے یا براہ راست عارضی منطق میں رکاوٹوں کو تشکیل دیتا ہے۔ ماحول کے بارے میں مختلف قسم کے مفروضوں کے تحت ہر ماڈل کی تصدیق اسپن سے کی جا سکتی ہے۔ ایک بار جب سپن کے ساتھ کسی ماڈل کی درستگی قائم ہو جاتی ہے، تو اس حقیقت کو بعد کے تمام ماڈلز کی تعمیر اور تصدیق میں استعمال کیا جا سکتا ہے۔ PROMELA پروگرام عمل، پیغام چینلز اور متغیرات پر مشتمل ہوتے ہیں۔ عمل عالمی اشیاء ہیں جو تقسیم شدہ نظام کے ہم آہنگی والے اداروں کی نمائندگی کرتے ہیں۔ میسج چینلز اور متغیرات کو ایک عمل کے اندر عالمی سطح پر یا مقامی طور پر اعلان کیا جا سکتا ہے۔ عمل رویے کی وضاحت کرتے ہیں، چینل اور عالمی متغیرات اس ماحول کی وضاحت کرتے ہیں جس میں عمل چلتے ہیں۔ زبان حوالہ ڈیٹا کی اقسام PROMELA میں استعمال ہونے والی بنیادی ڈیٹا کی اقسام کو نیچے دیے گئے جدول میں پیش کیا گیا ہے۔ بٹس میں سائز پی سی i386/لینکس مشین کے لیے دیے گئے ہیں۔ نام بٹ اور بول ایک چھوٹی سی معلومات کے مترادف ہیں۔ بائٹ ایک غیر دستخط شدہ مقدار ہے جو 0 اور 255 کے درمیان قدر کو ذخیرہ کر سکتی ہے۔ شارٹس اور انٹس دستخط شدہ مقدار ہیں جو صرف ان اقدار کی حد میں مختلف ہوتی ہیں جو وہ رکھ سکتے ہیں۔ متغیرات کو صفوں کے طور پر بھی قرار دیا جا سکتا ہے۔ مثال کے طور پر، اعلامیہ: 10 عددوں کی ایک صف کا اعلان کرتا ہے جس تک صف کے سبسکرپٹ تاثرات میں رسائی حاصل کی جا سکتی ہے جیسے: x [0] = x [1] + x [2] ؛ لیکن صفوں کو تخلیق پر شمار نہیں کیا جا سکتا، اس لیے انہیں مندرجہ ذیل طور پر شروع کیا جانا چاہیے: صف کا اشاریہ کوئی بھی اظہار ہو سکتا ہے جو ایک منفرد عدد قدر کا تعین کرتا ہے۔ رینج سے باہر انڈیکس کا اثر غیر متعین ہے۔ کثیر جہتی صفوں کو بالواسطہ طور پر ٹائپ ڈیف کنسٹرکٹ کی مدد سے بیان کیا جا سکتا ہے (نیچے دیکھیں)۔ عمل متغیر یا پیغام چینل کی حالت کو صرف عمل کے ذریعے تبدیل یا معائنہ کیا جا سکتا ہے۔ کسی عمل کے رویے کی وضاحت پروکٹائپ اعلامیے سے کی جاتی ہے۔ مثال کے طور پر، مندرجہ ذیل ایک متغیر حالت کے ساتھ ایک عمل کی قسم A کا اعلان کرتا ہے: پروکٹائپ A () {بائٹ اسٹیٹ ؛ اسٹیٹ = 3 ؛} پروکٹائپ کی تعریف صرف عمل کے رویے کا اعلان کرتی ہے، یہ اسے انجام نہیں دیتی ہے۔ ابتدائی طور پر، PROMELA ماڈل میں، صرف ایک عمل انجام دیا جائے گا: قسم init کا ایک عمل، جس کا ہر PROMELA تفصیلات میں واضح طور پر اعلان کیا جانا چاہیے۔ رن سٹیٹمنٹ کا استعمال کرتے ہوئے نئے عمل کو جنم دیا جا سکتا ہے، جو ایک پروکٹائپ کے نام پر مشتمل دلیل لیتا ہے، جس سے ایک عمل کو فوری کیا جاتا ہے۔ رن آپریٹر کو نہ صرف ابتدائی عمل میں بلکہ پروکٹائپ تعریفوں کے بنیادی حصے میں بھی استعمال کیا جا سکتا ہے۔ یہ PROMELA میں عمل کی متحرک تخلیق کی اجازت دیتا ہے۔ ایک عمل انجام دینے کا عمل اس وقت غائب ہو جاتا ہے جب یہ ختم ہو جاتا ہے-یعنی جب یہ پروکٹائپ کی تعریف میں جسم کے آخر تک پہنچ جاتا ہے، اور بچے کے تمام عمل جو اس نے شروع کیے تھے وہ ختم ہو جاتے ہیں۔ ایک پروکٹائپ بھی فعال ہو سکتا ہے (نیچے)۔ ایٹمک کنسٹرکٹ کلیدی لفظ ایٹمک کے ساتھ گھوبگھرالی قوسین میں منسلک بیانات کی ترتیب کو پہلے سے جوڑ کر، صارف اس بات کی نشاندہی کر سکتا ہے کہ اس ترتیب کو ایک ناقابل تقسیم اکائی کے طور پر انجام دیا جانا ہے، جو کسی دوسرے عمل کے ساتھ غیر مربوط ہے۔ جوہری ترتیبات تصدیق کے نمونوں کی پیچیدگی کو کم کرنے میں ایک اہم ذریعہ ہو سکتے ہیں۔ نوٹ کریں کہ جوہری ترتیبات انٹرلیونگ کی مقدار کو محدود کرتے ہیں جس کی تقسیم شدہ نظام میں اجازت ہے۔ مقامی متغیرات کے تمام ہیرا پھیری کو جوہری ترتیب کے ساتھ لیبل لگا کر پیچیدہ ماڈلز کو ٹریک ایبل بنایا جا سکتا ہے۔ میسج پاسنگ میسج چینلز کا استعمال ایک عمل سے دوسرے عمل میں ڈیٹا کی منتقلی کے ماڈل کے لیے کیا جاتا ہے۔ انہیں مقامی طور پر یا عالمی سطح پر اعلان کیا جاتا ہے، مثال کے طور پر: چن ق نام = [16] آف {شارٹ} یہ ایک بفرڈ چینل کا اعلان کرتا ہے جو ٹائپ شارٹ کے 16 پیغامات کو اسٹور کر سکتا ہے (یہاں گنجائش 16 ہے)۔ بیان: نام! ایکسپرا ؛ ایکسپریشن ایکسپرا کی ویلیو کو چینل کو نام qname کے ساتھ بھیجتا ہے، یعنی یہ ویلیو کو چینل کی دم سے جوڑتا ہے۔ بیان: نام؟ ایم ایس جی ؛ پیغام وصول کرتا ہے، اسے چینل کے سر سے بازیافت کرتا ہے، اور اسے متغیر ایم ایس جی میں محفوظ کرتا ہے۔ چینل فرسٹ ان فرسٹ آؤٹ ترتیب میں پیغامات منتقل کرتے ہیں۔ ایک ملاقات کی بندرگاہ کو اسٹور کی لمبائی صفر کے ساتھ ایک پیغام چینل کے طور پر اعلان کیا جا سکتا ہے۔ مثال کے طور پر، مندرجہ ذیل: {بائٹ} کا چن پورٹ = [0] ایک ملاقات بندرگاہ کی وضاحت کرتا ہے جو بائٹ قسم کے پیغامات منتقل کر سکتا ہے۔ اس طرح کی ملاقات کی بندرگاہوں کے ذریعے پیغامات کی بات چیت تعریف کے مطابق مطابقت پذیر ہوتی ہے، یعنی۔ بھیجنے والا یا وصول کنندہ (جو چینل پر پہلے پہنچے گا) دوسرے نمبر پر آنے والے مدمقابل (وصول کنندہ یا بھیجنے والے) کو بلاک کر دے گا۔ جب کسی بفرڈ چینل کو اس کی صلاحیت کے مطابق بھرا جاتا ہے (ان پٹ وصول کرنے سے پہلے آؤٹ پٹ کی "صلاحیت" کی تعداد بھیجنا ہوتا ہے)، تو چینل کا ڈیفالٹ طرز عمل مطابقت پذیر ہونا ہوتا ہے، اور بھیجنے والا اگلے بھیجنے پر بلاک کر دے گا۔ مشاہدہ کریں کہ چینلز کے درمیان کوئی مشترکہ میسج بفر شیئر نہیں ہے۔ بڑھتی ہوئی پیچیدگی، کسی چینل کو یک طرفہ اور پوائنٹ ٹو پوائنٹ کے طور پر استعمال کرنے کے مقابلے میں، متعدد وصول کنندگان یا متعدد بھیجنے والوں کے درمیان چینلز کا اشتراک کرنا، اور آزاد ڈیٹا اسٹریمز کو ایک مشترکہ چینل میں ضم کرنا ممکن ہے۔ اس سے پتہ چلتا ہے کہ ایک واحد چینل کو دو طرفہ مواصلات کے لیے بھی استعمال کیا جا سکتا ہے۔ کنٹرول فلو تعمیرات PROMELA میں تین کنٹرول فلو تعمیرات ہیں۔ وہ کیس کا انتخاب، تکرار اور غیر مشروط چھلانگ ہیں۔ کیس کا انتخاب سب سے آسان تعمیر سلیکشن ڈھانچہ ہے۔ مثال کے طور پر، دو متغیرات a اور b کی متعلقہ اقدار کا استعمال کرتے ہوئے، کوئی بھی لکھ سکتا ہے: اگر:: (a! = b)-> آپشن 1:: (a = = b)-> آپشن 2 فائی سلیکشن اسٹرکچر میں دو پھانسی کے سلسلے ہوتے ہیں، جن میں سے ہر ایک سے پہلے ڈبل کالون ہوتا ہے۔ فہرست میں سے ایک ترتیب پر عمل کیا جائے گا۔ ایک ترتیب صرف اس صورت میں منتخب کی جا سکتی ہے جب اس کا پہلا بیان قابل عمل ہو۔ کنٹرول سیکوینس کے پہلے بیان کو گارڈ کہا جاتا ہے۔ مندرجہ بالا مثال میں، محافظ باہمی طور پر خصوصی ہیں، لیکن ان کی ضرورت نہیں ہے۔ اگر ایک سے زیادہ گارڈ قابل عمل ہیں، تو متعلقہ ترتیبات میں سے ایک کو غیر تعیناتی طور پر منتخب کیا جاتا ہے۔ اگر تمام گارڈز ناقابل عمل ہیں، تو یہ عمل اس وقت تک روک دے گا جب تک کہ ان میں سے کسی ایک کا انتخاب نہ ہو جائے۔ (اس کے برعکس، اوکیم پروگرامنگ زبان رک جائے گی یا بغیر کسی قابل عمل محافظ کے آگے بڑھنے کے قابل نہیں ہوگی۔) اگر:: (A = = سچ ہے)-> آپشن 1 ؛:: (B = = سچ ہے)-> آپشن 2 ؛/* یہاں بھی پہنچ سکتا ہے اگر A = = سچ ہے */:: ورنہ-> فالتھرو آپشن ؛ فائی غیر متعین انتخاب کا نتیجہ یہ ہے کہ، اوپر کی مثال میں، اگر A سچ ہے، تو دونوں انتخاب کیے جا سکتے ہیں۔ "روایتی" پروگرامنگ میں، ایک اگر-اگر-دوسری ساخت کو ترتیب وار سمجھا جائے گا۔ یہاں، اگر-ڈبل کولن-ڈبل کولن کو "کوئی بھی تیار ہے" کے طور پر سمجھنا چاہیے اور اگر کوئی تیار نہیں ہے، تب ہی باقی لیا جائے گا۔ اگر:: ویلیو = 3 ؛:: ویلیو = 4 ؛ فائی مندرجہ بالا مثال میں، ویلیو کو غیر متعین طور پر ویلیو 3 یا 4 دی گئی ہے۔ دو فرضی بیانات ہیں جنہیں محافظ کے طور پر استعمال کیا جا سکتا ہے: ٹائم آؤٹ بیان اور دیگر بیان۔ ٹائم آؤٹ بیان ایک خاص شرط کا نمونہ بناتا ہے جو کسی عمل کو کسی ایسی شرط کے انتظار کو ترک کرنے کی اجازت دیتا ہے جو شاید کبھی درست نہ ہو۔ دیگر بیان کو سلیکشن یا تکرار بیان میں آخری آپشن کی ترتیب کے ابتدائی بیان کے طور پر استعمال کیا جا سکتا ہے۔ باقی صرف اس صورت میں قابل عمل ہے جب ایک ہی انتخاب میں موجود دیگر تمام آپشن قابل عمل نہ ہوں۔ اس کے علاوہ، ایلیس کو چینلز کے ساتھ مل کر استعمال نہیں کیا جا سکتا ہے۔ تکرار (لوپ) سلیکشن ڈھانچے کی منطقی توسیع تکرار کا ڈھانچہ ہے۔ مثال کے طور پر: ڈو:: کاؤنٹ = کاؤنٹ + 1:: a = b + 2:: (کاؤنٹ = = 0)-> بریک اوڈ PROMELA میں تکرار کی ساخت کو بیان کرتا ہے۔ ایک وقت میں صرف ایک آپشن منتخب کیا جا سکتا ہے۔ آپشن مکمل ہونے کے بعد، ڈھانچے پر عمل درآمد کو دہرایا جاتا ہے۔ تکرار کے ڈھانچے کو ختم کرنے کا عام طریقہ بریک سٹیٹمنٹ کے ساتھ ہے۔ یہ کنٹرول کو ہدایت میں منتقل کرتا ہے جو فوری طور پر تکرار کے ڈھانچے کی پیروی کرتا ہے۔ غیر مشروط چھلانگ لوپ کو توڑنے کا ایک اور طریقہ گوٹو بیان ہے۔ مثال کے طور پر، اوپر کی مثال میں مندرجہ ذیل ترمیم کی جا سکتی ہے:: شمار کریں:: شمار = شمار + 1:: a = b + 2:: (شمار = = 0)-> کیا کیا گیا od کیا گیا: چھوڑ دیں ؛ اس مثال میں گوٹو کیا گیا نامی لیبل پر چھلانگ لگاتا ہے۔ لیبل صرف بیان سے پہلے ظاہر ہو سکتا ہے۔ پروگرام کے اختتام پر چھلانگ لگانے کے لیے، مثال کے طور پر، ایک ڈمی سٹیٹمنٹ سکپ مفید ہے: یہ ایک پلیس ہولڈر ہے جو ہمیشہ قابل عمل ہوتا ہے اور اس کا کوئی اثر نہیں ہوتا ہے۔ دعوی PROMELA میں ایک اہم زبان کی تعمیر جس کی تھوڑی سی وضاحت کی ضرورت ہوتی ہے وہ دعوی بیان ہے۔ فارم کے بیانات: دعوی (کوئی بھی _ بولین _ شرط) ہمیشہ قابل عمل ہوتے ہیں۔ اگر کوئی مخصوص بولین حالت برقرار رہتی ہے، تو بیان کا کوئی اثر نہیں ہوتا ہے۔ اگر، تاہم، شرط لازمی طور پر برقرار نہیں رہتی ہے، تو بیان اسپن کے ساتھ تصدیق کے دوران ایک غلطی پیدا کرے گا۔ پیچیدہ ڈیٹا ڈھانچے ایک PROMELA تعریف کو پہلے سے طے شدہ یا پہلے سے متعین اقسام کے ڈیٹا آبجیکٹ کی فہرست کے لیے ایک نیا نام متعارف کرانے کے لیے استعمال کیا جا سکتا ہے۔ نئی قسم کا نام نئے ڈیٹا آبجیکٹ کو ظاہر کرنے اور فوری کرنے کے لیے استعمال کیا جا سکتا ہے، جسے کسی بھی سیاق و سباق میں واضح طریقے سے استعمال کیا جا سکتا ہے: ٹائپ ڈیف کنسٹرکشن میں اعلان کردہ فیلڈز تک رسائی اسی انداز میں کی جاتی ہے جیسے سی پروگرامنگ زبان میں ہوتی ہے۔ مثال کے طور پر: مائی اسٹرک x ؛ x.Field1 = 1 ؛ ایک درست PROMELA ترتیب ہے جو متغیر x کے فیلڈ 1 کو ویلیو 1 تفویض کرتی ہے۔ فعال پروکٹائپ فعال کلیدی لفظ کو کسی بھی پروکٹائپ تعریف سے پہلے لگایا جا سکتا ہے۔ اگر کلیدی لفظ موجود ہے، تو اس پروکٹائپ کی ایک مثال ابتدائی نظام کی حالت میں فعال ہوگی۔ اس پروکٹائپ کے متعدد لمحات کو مطلوبہ الفاظ کے اختیاری صف لاحقہ کے ساتھ متعین کیا جا سکتا ہے۔ مثال: فعال پروکٹائپ A () {.} فعال [4] پروکٹائپ B () {.} قابل نفاذ عمل کی ہم آہنگی کے ماڈلنگ کے لیے پرومیلا میں بنیادی ذرائع فراہم کرتا ہے۔ mtype = {M _ UP, M _ DW} ؛ چن چن ڈیٹا ڈاؤن = [0] آف {mtype} ؛ چن چن ڈیٹا اپ = [0] آف {mtype} ؛ پروکٹائپ P1 (چن چن ڈیٹا ان، چن ڈیٹا آؤٹ) {کرو:: چن ڈیٹا ان؟ M _ UP-> چھوڑ دیں ؛:: چان _ ڈیٹا _ آؤٹ! M _ DW-> سکیپ ؛ od ؛} ؛ پروکٹائپ P2 (چن چن ڈیٹا _ ان، چن ڈیٹا _ آؤٹ) {کرو:: چن ڈیٹا _ ان؟ M _ DW-> چھوڑ دیں ؛:: چان _ ڈیٹا _ آؤٹ! مثال کے طور پر، دونوں عمل P1 اور P2 میں (1) دوسرے سے ان پٹ یا (2) دوسرے سے آؤٹ پٹ کے غیر متعین انتخاب ہوتے ہیں۔ دو ملاقاتوں میں ہاتھ ملانا ممکن ہے، یا قابل عمل ہے، اور ان میں سے ایک کا انتخاب کیا جاتا ہے۔ یہ ہمیشہ کے لیے دہرایا جاتا ہے۔ لہذا، یہ ماڈل تعطل کا شکار نہیں ہوگا۔ جب اسپن مندرجہ بالا جیسے ماڈل کا تجزیہ کرتا ہے، تو یہ غیر متعین الگورتھم کے ساتھ انتخاب کی تصدیق کرے گا، جہاں تمام قابل عمل انتخاب تلاش کیے جائیں گے۔ تاہم، جب اسپن کا سمیلیٹر ممکنہ غیر تصدیق شدہ مواصلاتی نمونوں کا تصور کرتا ہے، تو یہ "غیر متعین" انتخاب کو حل کرنے کے لیے بے ترتیب جنریٹر کا استعمال کر سکتا ہے۔ لہذا، سمیلیٹر خراب کارکردگی دکھانے میں ناکام ہو سکتا ہے (مثال کے طور پر، کوئی برا راستہ نہیں ہے)۔ یہ تصدیق اور تخروپن کے درمیان فرق کی وضاحت کرتا ہے۔ اس کے علاوہ ریفائنمنٹ کا استعمال کرتے ہوئے پرومیلا ماڈلز سے قابل عمل کوڈ تیار کرنا بھی ممکن ہے۔ مطلوبہ الفاظ درج ذیل شناخت کنندگان مطلوبہ الفاظ کے طور پر استعمال کے لیے مخصوص ہیں۔ حوالہ جات بیرونی لنکس اسپن ہوم پیج اسپن ٹیوٹوریلز اور آن لائن حوالہ جات جامع پرومیلا حوالہ کمپیوٹر کی مدد سے آٹومیٹا کی تصدیق: "دی سی اے وی اے پروجیکٹ" (2010-2019) اور "تصدیق شدہ ماڈل چیکرز" (2016-کر) ویب سائٹ وضاحتی زبانیں ماڈل چیکرز