TAPAAL Model Checker
தபால் என்பது டென்மார்க்கில் உள்ள ஆல்போர்க் பல்கலைக்கழகத்தில் கணினி அறிவியல் துறையில் உருவாக்கப்பட்ட டைம்ட்-ஆர்க் பெட்ரி வலைகளின் மாடலிங், உருவகப்படுத்துதல் மற்றும் சரிபார்ப்புக்கான ஒரு கருவியாகும், மேலும் இது லினக்ஸ், விண்டோஸ் மற்றும் மேக் ஓஎஸ் எக்ஸ் இயங்குதளங்களில் கிடைக்கிறது. டைம்ட்-ஆர்க் பெட்ரி நெட் (டிஏபிஎன்) என்பது கிளாசிக்கல் பெட்ரி நெட் மாடலின் நேர நீட்டிப்பாகும் (1962 ஆம் ஆண்டில் கார்ல் ஆடம் பெட்ரி தனது ஆய்வுக் கட்டுரையில் அறிமுகப்படுத்திய விநியோகிக்கப்பட்ட கணக்கீடுகளின் பொதுவாகப் பயன்படுத்தப்படும் வரைகலை மாதிரி). டிஏபிஎனில் கருதப்படும் நேர நீட்டிப்பு நிகழ்நேரத்தின் வெளிப்படையான சிகிச்சையை அனுமதிக்கிறது, இது வலையில் உள்ள டோக்கன்களுடன் தொடர்புடையது (ஒவ்வொரு டோக்கன்களுக்கும் அதன் சொந்த வயது உள்ளது) மற்றும் இடங்களிலிருந்து மாற்றங்களுக்கு வளைவுகள் நேர இடைவெளிகளால் பெயரிடப்படுகின்றன, இது அந்தந்த மாற்றத்தை சுட பயன்படுத்தக்கூடிய டோக்கன்களின் வயதைக் கட்டுப்படுத்துகிறது. தபால் கருவியில் போக்குவரத்து வளைவுகளுடன் வயது மாறுபாடுகளுடன் இந்த மாதிரியின் மேலும் விரிவாக்கம் (எடுத்துக்காட்டாக முன்பு ரீட்-ஆர்க்குகள் என்று கருதப்பட்டதை விட அதிக வெளிப்பாட்டைக் கொண்டவை) மற்றும் இன்ஹிபிட்டர் வளைவுகளுடன் செயல்படுத்தப்படுகின்றன. டிஏபிஎன் மாதிரிகளை வரைவதற்கு ஒரு வரைகலை எடிட்டர், வடிவமைக்கப்பட்ட வலைகளை பரிசோதிப்பதற்கான சிமுலேட்டர் மற்றும் சி. டி. எல் தர்க்கத்தின் துணைக்குழுவில் வடிவமைக்கப்பட்ட தர்க்கரீதியான கேள்விகளுக்கு தானாகவே பதிலளிக்கும் சரிபார்ப்பு சூழலை டிஏபிஏஎல் கருவி வழங்குகிறது (அடிப்படையில் ஈஎஃப், ஈஜி, ஏஎஃப், ஏஜி சூத்திரங்கள் கூடு கட்டாமல்). கொடுக்கப்பட்ட எண் k க்கு கொடுக்கப்பட்ட வலை k-எல்லைக்குட்பட்டதா என்பதைச் சரிபார்க்கவும் இது பயனரை அனுமதிக்கிறது. தபால் அதன் சொந்த சரிபார்ப்பு இயந்திரங்களைக் கொண்டுள்ளது, இது தபாலுடன் (தொடர்ச்சியான நேரத்திற்கு ஒன்று மற்றும் தனித்துவமான நேரத்திற்கு ஒன்று) விநியோகிக்கப்படுகிறது. விருப்பப்படி, பயனர் தானாகவே தபால் மாதிரிகளை யுபிபிஏஏஎல் ஆக மொழிபெயர்க்கலாம் மற்றும் யுபிபிஏஏஎல் சரிபார்ப்பு இயந்திரத்தை நம்பலாம். வெளி இணைப்புகள் தபால் வலைத்தளம், பதிவிறக்கம் DES அலகு, கணினி அறிவியல் துறை, ஆல்போர்க் பல்கலைக்கழகம், டென்மார்க் தபால்ஃ ஆசிரியர், சிமுலேட்டர் மற்றும் டைம் ஆர்க் பெட்ரி நெட்ஸின் சரிபார்ப்பவர் ஜே. பைக், கே. ஒய். ஜோர்ஜென்சன் மற்றும் ஜே. ஸ்ர்பா, ஏடிவிஏ '09, ஸ்ப்ரிங்கர் டைம்ட்-ஆர்க் பெட்ரி நெட்டுகளின் திறமையான மொழிபெயர்ப்பு டைம்ட் ஆட்டோமேட்டாவின் நெட்வொர்க்குகளுக்கு ஜே. பைக், கே. ஒய். ஜோர்ஜென்சன் மற்றும் ஜே. ஸ்ர்பா, ஐசிஎஃப்இஎம் '09, ஸ்ப்ரிங்கர் ஏ ஃபிரேம்வொர்க் ஃபார் ரிலேட்டிங் டைம் டிரான்சிஷன் சிஸ்டம்ஸ் அண்ட் பிரஷர்விங் டிசிடிஎல் மாடல் செக்கிங் எல். ஜேக்கப்ஸென், எம். ஜேக்கப்ஸென், எம்எச். மோலர் மற்றும் ஜே. ஸ்ர்பா, EPEW '10, ஸ்ப்ரிங்கர் சரிபார்ப்பு டைம்ட்-ஆர்க் பெட்ரி நெட்ஸ் எல். ஜேக்கப்ஸென், எம். ஜேக்கப்ஸென், எம். எச். மோலர் மற்றும் ஜே. ஸ்ர்பா, சோஃப்ஸெம் '11, ஸ்ப்ரிங்கர் குறிப்புகள் மாதிரி சரிபார்ப்பவர்கள்