TAPAAL Model Checker
ટી. એ. પી. એ. એ. એલ. એ ડેનમાર્કમાં આલબોર્ગ યુનિવર્સિટી ખાતે કોમ્પ્યુટર સાયન્સ વિભાગમાં વિકસિત ટાઇમ-આર્ક પેટ્રી નેટના મોડેલિંગ, સિમ્યુલેશન અને ચકાસણી માટેનું એક સાધન છે અને તે લિનક્સ, વિન્ડોઝ અને મેક ઓએસ એક્સ પ્લેટફોર્મ માટે ઉપલબ્ધ છે. ટાઈમ્ડ-આર્ક પેટ્રી નેટ (ટી. એ. પી. એન.) એ શાસ્ત્રીય પેટ્રી નેટ મોડેલનું સમય વિસ્તરણ છે (વિતરિત ગણતરીઓનું સામાન્ય રીતે વપરાતું ગ્રાફિકલ મોડેલ જે કાર્લ એડમ પેટ્રી દ્વારા 1962માં તેમના શોધ નિબંધમાં રજૂ કરવામાં આવ્યું હતું). ટી. એ. પી. એન. માં ધ્યાનમાં લેવાયેલ સમય વિસ્તરણ વાસ્તવિક સમયની સ્પષ્ટ સારવાર માટે પરવાનગી આપે છે, જે નેટમાં ટોકન્સ સાથે સંકળાયેલ છે (દરેક ટોકન્સની પોતાની ઉંમર હોય છે) અને સ્થાનોથી સંક્રમણો તરફના ચાપને સમય અંતરાલો દ્વારા લેબલ કરવામાં આવે છે જે ટોકન્સની ઉંમરને પ્રતિબંધિત કરે છે જેનો ઉપયોગ સંબંધિત સંક્રમણને ચલાવવા માટે કરી શકાય છે. ટી. એ. પી. એ. એ. એલ. સાધનમાં પરિવહન ચાપ સાથે વય અપરિવર્તન સાથે આ મોડેલનું વધુ વિસ્તરણ (જે ઉદાહરણ તરીકે અગાઉ રીડ-આર્ક્સ તરીકે ગણવામાં આવતા કરતાં વધુ અભિવ્યક્ત છે) અને અવરોધક ચાપ સાથે અમલમાં મૂકવામાં આવે છે. ટી. એ. પી. એ. એ. એલ. ટૂલ ટી. એ. પી. એન. મોડેલો દોરવા માટે ગ્રાફિકલ એડિટર, ડિઝાઇન કરેલી જાળીઓ સાથે પ્રયોગ કરવા માટે સિમ્યુલેટર અને ચકાસણી વાતાવરણ પ્રદાન કરે છે જે સી. ટી. એલ. તર્કના સબસેટમાં ઘડવામાં આવેલા તાર્કિક પ્રશ્નોના આપમેળે જવાબ આપે છે (આવશ્યકપણે ઇ. એફ., ઇ. જી., એ. એફ., એ. જી. સૂત્રોને નેસ્ટિંગ વિના). તે વપરાશકર્તાને એ તપાસવાની પણ મંજૂરી આપે છે કે આપેલ જાળી આપેલ સંખ્યા k માટે k-બાઉન્ડેડ છે કે કેમ. તપાલ તેના પોતાના ચકાસણી એન્જિનથી સજ્જ છે જે તપાલ (એક સતત સમય માટે અને એક અલગ સમય માટે) સાથે વહેંચાયેલું છે. વૈકલ્પિક રીતે, વપરાશકર્તા આપમેળે ટી. એ. પી. એ. એ. એલ. મોડેલોને યુ. પી. પી. એ. એ. એલ. માં અનુવાદિત કરી શકે છે અને યુ. પી. પી. એ. એ. એલ. ચકાસણી એન્જિન પર આધાર રાખી શકે છે. બાહ્ય લિંક્સ તપાલ વેબસાઇટ, DES એકમ ડાઉનલોડ કરો, કમ્પ્યુટર વિજ્ઞાન વિભાગ, આલબોર્ગ યુનિવર્સિટી, ડેનમાર્ક તપાલઃ સંપાદક, સિમ્યુલેટર અને જે. બાયગ, કે. વાય. દ્વારા ટાઇમ-આર્ક પેટ્રી નેટ્સની ચકાસણી. જોર્ગેન્સન અને જે. સર્બા, એટીવીએ '09, સ્પ્રિંગર એન એફિશિયન્ટ ટ્રાન્સલેશન ઓફ ટાઈમ્ડ-આર્ક પેટ્રી નેટ્સ ટુ નેટવર્ક્સ ઓફ ટાઈમ્ડ ઓટોમેટા જે. બાયગ, કે. વાય. જોર્ગેન્સન અને જે. સર્બા, આઇસીએફઇએમ '09, સ્પ્રિંગર એ ફ્રેમવર્ક ફોર રિલેટિંગ ટાઈમ્ડ ટ્રાન્ઝિશન સિસ્ટમ્સ એન્ડ પ્રિઝર્વેશન ટીસીટીએલ મોડલ ચેકિંગ એલ. જેકોબ્સન, એમ. જેકોબ્સન, એમ. એચ. મોલર અને જે. સર્બા, EPEW '10, સ્પ્રિંગર વેરિફિકેશન ઓફ ટાઈમ્ડ-આર્ક પેટ્રી નેટ્સ એલ. જેકોબ્સન, એમ. જેકોબ્સન, એમ. એચ. મોલર અને જે. સર્બા, SOFSEM '11, સ્પ્રિંગર રેફરન્સ મોડલ ચેકર્સ