TAPAAL Model Checker
تاپال ڈنمارک میں آلبورگ یونیورسٹی کے شعبہ کمپیوٹر سائنس میں تیار کردہ ٹائمڈ آرک پیٹری نیٹ کی ماڈلنگ، تخروپن اور تصدیق کے لیے ایک ٹول ہے اور یہ لینکس، ونڈوز اور میک او ایس ایکس پلیٹ فارمز کے لیے دستیاب ہے۔ ٹائمڈ آرک پیٹری نیٹ (ٹی اے پی این) کلاسیکی پیٹری نیٹ ماڈل کی وقت کی توسیع ہے (تقسیم شدہ حسابات کا عام طور پر استعمال ہونے والا گرافیکل ماڈل جسے کارل ایڈم پیٹری نے 1962 میں اپنے مقالے میں متعارف کرایا تھا)۔ ٹی اے پی این میں زیر غور وقت کی توسیع حقیقی وقت کے واضح علاج کی اجازت دیتی ہے، جو نیٹ میں ٹوکن سے وابستہ ہے (ہر ٹوکن کی اپنی عمر ہوتی ہے) اور جگہوں سے منتقلی تک کے آرکس کو وقت کے وقفوں سے لیبل کیا جاتا ہے جو ٹوکن کی عمر کو محدود کرتا ہے جو متعلقہ منتقلی کو چلانے کے لیے استعمال کیا جا سکتا ہے۔ ٹی اے پی اے اے ایل ٹول میں ٹرانسپورٹ آرکس کے ساتھ عمر کے غیر متغیرات کے ساتھ اس ماڈل کی مزید توسیع (جو مثال کے طور پر پہلے ریڈ آرکس سمجھے جانے والے سے زیادہ اظہار خیال کرتے ہیں) اور انفیکٹر آرکس کے ساتھ لاگو کیا جاتا ہے۔ ٹی اے پی اے اے ایل ٹول ٹی اے پی این ماڈل کھینچنے کے لیے ایک گرافیکل ایڈیٹر، ڈیزائن کردہ جالوں کے ساتھ تجربہ کرنے کے لیے سمیلیٹر اور ایک تصدیق کا ماحول پیش کرتا ہے جو خود بخود سی ٹی ایل منطق کے ذیلی سیٹ میں وضع کردہ منطقی سوالات کا جواب دیتا ہے (بنیادی طور پر ای ایف، ای جی، اے ایف، اے جی فارمولے بغیر گھونسلے کے)۔ یہ صارف کو یہ چیک کرنے کی بھی اجازت دیتا ہے کہ آیا دیا ہوا نیٹ کسی دیئے گئے نمبر k کے لیے k-باؤنڈ ہے۔ تپال اپنے تصدیق کے انجنوں سے لیس ہے جو تپال کے ساتھ تقسیم کیے گئے ہیں (ایک مسلسل وقت کے لیے اور ایک مجرد وقت کے لیے)۔ اختیاری طور پر، صارف خود بخود تاپال ماڈلز کو یو پی پی اے اے ایل میں ترجمہ کر سکتا ہے اور یو پی پی اے اے ایل تصدیقی انجن پر انحصار کر سکتا ہے۔ بیرونی روابط تاپال ویب سائٹ، ڈاؤن لوڈ ڈی ای ایس یونٹ، ڈیپارٹمنٹ آف کمپیوٹر سائنس، آلبورگ یونیورسٹی، ڈنمارک تاپال: ایڈیٹر، سمیلیٹر اینڈ ویریفائر آف ٹائمڈ آرک پیٹری نیٹ بائی جے بیگ، کے وائی۔ جارجینسن اور جے سربا، اے ٹی وی اے '09، سپرنگر این ایفیشنٹ ٹرانسلیشن آف ٹائمڈ آرک پیٹری نیٹ ٹو نیٹ ورکس آف ٹائمڈ آٹومیٹا بذریعہ جے بیگ، کے وائی۔ جارجینسن اور جے سربا، آئی سی ایف ای ایم '09، سپرنگر اے فریم ورک فار ریلیٹنگ ٹائمڈ ٹرانزیشن سسٹمز اینڈ پریزرویشن ٹی سی ٹی ایل ماڈل چیکنگ بذریعہ ایل جیکبسن، ایم جیکبسن، ایم ایچ۔ مولر اور جے سربا، ای پی ای ڈبلیو '10، ایل جیکبسن، ایم جیکبسن، ایم ایچ کے ذریعہ ٹائمڈ آرک پیٹری نیٹ کی سپرنگر تصدیق۔ مولر اور جے سربا، SOFSEM '11، سپرنگر حوالہ جات ماڈل چیکرز