Promela
પ્રોમેલા (પ્રક્રિયા અથવા પ્રોટોકોલ મેટા લેંગ્વેજ) એ ગેરાર્ડ જે. હોલ્ઝમેન દ્વારા રજૂ કરાયેલી ચકાસણી મોડેલિંગ ભાષા છે. ભાષા મોડેલ માટે સહવર્તી પ્રક્રિયાઓની ગતિશીલ રચના માટે પરવાનગી આપે છે, ઉદાહરણ તરીકે, વિતરિત પ્રણાલીઓ. PROMELA મોડેલોમાં, સંદેશ ચેનલો દ્વારા સંદેશાવ્યવહારને સુમેળ (એટલે કે, મુલાકાત), અથવા અસિંક્રોનસ (એટલે કે, બફર) તરીકે વ્યાખ્યાયિત કરી શકાય છે. મોડેલ કરેલ સિસ્ટમ ઇચ્છિત વર્તણૂક ઉત્પન્ન કરે છે કે કેમ તે ચકાસવા માટે, પ્રોમેલા મોડેલોનું સ્પિન મોડેલ ચેકર સાથે વિશ્લેષણ કરી શકાય છે. કમ્પ્યુટર એડેડ વેરિફિકેશન ઓફ ઓટોમેટા (સી. એ. વી. એ.) પ્રોજેક્ટના ભાગરૂપે ઇસાબેલ/એચ. ઓ. એલ. સાથે ચકાસાયેલ અમલીકરણ પણ ઉપલબ્ધ છે. પ્રોમેલામાં લખાયેલી ફાઇલોમાં પરંપરાગત રીતે. પી. એમ. એલ. ફાઇલ એક્સ્ટેંશન હોય છે. PROMELA એ એક પ્રક્રિયા-મોડેલિંગ ભાષા છે જેનો હેતુ સમાંતર પ્રણાલીઓના તર્કને ચકાસવાનો છે. PROMELA માં પ્રોગ્રામને જોતાં, સ્પિન મોડેલ્ડ સિસ્ટમના એક્ઝેક્યુશનના રેન્ડમ અથવા ઇટરેટિવ સિમ્યુલેશન કરીને ચોકસાઈ માટે મોડેલને ચકાસી શકે છે, અથવા તે C પ્રોગ્રામ પેદા કરી શકે છે જે સિસ્ટમ સ્ટેટ સ્પેસની ઝડપી સંપૂર્ણ ચકાસણી કરે છે. સિમ્યુલેશન અને ચકાસણી દરમિયાન, સ્પિન ડેડલોકની ગેરહાજરી, અચોક્કસ રિસેપ્શન અને બિનકાર્યક્ષમ કોડની તપાસ કરે છે. ચકાસણીકર્તાનો ઉપયોગ સિસ્ટમ અપરિવર્તનની ચોકસાઈ સાબિત કરવા માટે પણ થઈ શકે છે અને તે બિન-પ્રગતિ અમલ ચક્ર શોધી શકે છે. છેવટે, તે રેખીય સમયની અસ્થાયી મર્યાદાઓની ચકાસણીને ટેકો આપે છે; ક્યાં તો પ્રોમેલા ક્યારેય દાવો કરતું નથી અથવા અસ્થાયી તર્કમાં સીધી રીતે અવરોધો ઘડવામાં આવે છે. દરેક મોડેલને પર્યાવરણ વિશે વિવિધ પ્રકારની ધારણાઓ હેઠળ સ્પિન સાથે ચકાસી શકાય છે. એકવાર મોડેલની ચોકસાઈ સ્પિન સાથે સ્થાપિત થઈ જાય, તે હકીકતનો ઉપયોગ પછીના તમામ મોડેલોના નિર્માણ અને ચકાસણીમાં થઈ શકે છે. PROMELA કાર્યક્રમોમાં પ્રક્રિયાઓ, સંદેશ ચેનલો અને ચલોનો સમાવેશ થાય છે. પ્રક્રિયાઓ વૈશ્વિક પદાર્થો છે જે વિતરિત પ્રણાલીના સહવર્તી ઘટકોનું પ્રતિનિધિત્વ કરે છે. સંદેશ ચેનલો અને ચલને પ્રક્રિયાની અંદર વૈશ્વિક અથવા સ્થાનિક રીતે જાહેર કરી શકાય છે. પ્રક્રિયાઓ વર્તનને સ્પષ્ટ કરે છે, ચેનલો અને વૈશ્વિક ચલો તે વાતાવરણને વ્યાખ્યાયિત કરે છે જેમાં પ્રક્રિયાઓ ચાલે છે. ભાષા સંદર્ભ માહિતીના પ્રકાર PROMELA માં ઉપયોગમાં લેવાતા મૂળભૂત માહિતીના પ્રકારો નીચે કોષ્ટકમાં રજૂ કરવામાં આવ્યા છે. પીસી i386/લિનક્સ મશીન માટે બિટ્સમાં કદ આપવામાં આવ્યા છે. બિટ અને બૂલ નામ એક જ માહિતીના સમાનાર્થી છે. બાઈટ એ હસ્તાક્ષર વગરનો જથ્થો છે જે 0 અને 255 ની વચ્ચે મૂલ્ય સંગ્રહિત કરી શકે છે. શોર્ટ્સ અને ઇન્ટ્સ એ હસ્તાક્ષરિત જથ્થા છે જે ફક્ત તેઓ રાખી શકે તેવા મૂલ્યોની શ્રેણીમાં અલગ પડે છે. ચલને એરે તરીકે પણ જાહેર કરી શકાય છે. ઉદાહરણ તરીકે, ઘોષણાઃ 10 પૂર્ણાંકોની શ્રેણી જાહેર કરે છે જેને એરે સબસ્ક્રિપ્ટ સમીકરણોમાં એક્સેસ કરી શકાય છે જેમ કેઃ x [0] = x [1] + x [2]; પરંતુ એરેની રચના પર ગણતરી કરી શકાતી નથી, તેથી તેમને નીચે પ્રમાણે પ્રારંભ કરવો આવશ્યક છેઃ એરેની અનુક્રમણિકા કોઈપણ અભિવ્યક્તિ હોઈ શકે છે જે અનન્ય પૂર્ણાંક મૂલ્ય નક્કી કરે છે. શ્રેણીની બહારના સૂચકાંકની અસર અવ્યાખ્યાયિત છે. બહુ-પરિમાણીય એરેને ટાઇપડેફ રચનાની મદદથી પરોક્ષ રીતે વ્યાખ્યાયિત કરી શકાય છે (નીચે જુઓ). પ્રક્રિયાઓ ચલ અથવા સંદેશ ચેનલની સ્થિતિ માત્ર પ્રક્રિયાઓ દ્વારા બદલી અથવા તપાસ કરી શકાય છે. પ્રક્રિયાની વર્તણૂક પ્રોક્ટાઇપ ઘોષણા દ્વારા વ્યાખ્યાયિત કરવામાં આવે છે. ઉદાહરણ તરીકે, નીચેના એક ચલ સ્થિતિ સાથે પ્રક્રિયા પ્રકાર A જાહેર કરે છેઃ પ્રોક્ટાઇપ A () {બાઈટ સ્થિતિ; સ્થિતિ = 3;} પ્રોક્ટાઇપ વ્યાખ્યા માત્ર પ્રક્રિયા વર્તન જાહેર કરે છે, તે તેને અમલમાં મૂકતી નથી. શરૂઆતમાં, PROMELA મોડેલમાં, માત્ર એક જ પ્રક્રિયા ચલાવવામાં આવશેઃ init પ્રકારની પ્રક્રિયા, જેને દરેક PROMELA સ્પષ્ટીકરણમાં સ્પષ્ટ રીતે જાહેર કરવી આવશ્યક છે. રન સ્ટેટમેન્ટનો ઉપયોગ કરીને નવી પ્રક્રિયાઓ પેદા કરી શકાય છે, જે પ્રોક્ટાઇપના નામની બનેલી દલીલ લે છે, જેમાંથી પ્રક્રિયા પછી ત્વરિત થાય છે. રન ઓપરેટરનો ઉપયોગ પ્રોક્ટાઇપ વ્યાખ્યાઓના મુખ્ય ભાગમાં થઈ શકે છે, માત્ર પ્રારંભિક પ્રક્રિયામાં જ નહીં. આ PROMELA માં પ્રક્રિયાઓની ગતિશીલ રચના માટે પરવાનગી આપે છે. એક એક્ઝિક્યુટિવ પ્રક્રિયા ત્યારે અદૃશ્ય થઈ જાય છે જ્યારે તે સમાપ્ત થાય છે-એટલે કે, જ્યારે તે પ્રોક્ટાઇપ વ્યાખ્યામાં શરીરના અંત સુધી પહોંચે છે, અને તેણે શરૂ કરેલી તમામ બાળ પ્રક્રિયાઓ સમાપ્ત થઈ જાય છે. પ્રોક્ટાઇપ પણ સક્રિય હોઈ શકે છે (નીચે). અણુ રચના અણુ શબ્દ સાથે કર્લી કૌંસમાં બંધ નિવેદનોના ક્રમને ઉપસર્ગ કરીને, વપરાશકર્તા સૂચવી શકે છે કે ક્રમને એક અવિભાજ્ય એકમ તરીકે ચલાવવામાં આવશે, જે અન્ય કોઈપણ પ્રક્રિયાઓ સાથે જોડાયેલો નથી. અણુ ક્રમ ચકાસણી નમૂનાઓની જટિલતાને ઘટાડવામાં એક મહત્વપૂર્ણ સાધન બની શકે છે. નોંધ લો કે અણુ ક્રમ વહેંચાયેલ પ્રણાલીમાં મંજૂરી આપવામાં આવેલી ઇન્ટરલીવિંગની માત્રાને પ્રતિબંધિત કરે છે. સ્થાનિક ચલોના તમામ હેરફેરને અણુ ક્રમ સાથે લેબલ કરીને જટિલ મોડેલોને ટ્રેક્ટેબલ બનાવી શકાય છે. સંદેશ પસાર કરતી સંદેશ ચેનલોનો ઉપયોગ એક પ્રક્રિયાથી બીજી પ્રક્રિયામાં ડેટાના સ્થાનાંતરણનું મોડેલ બનાવવા માટે થાય છે. તેમને સ્થાનિક રીતે અથવા વૈશ્વિક સ્તરે જાહેર કરવામાં આવે છે, ઉદાહરણ તરીકે નીચે પ્રમાણેઃ {ટૂંકી} ની chan qname = [16] આ એક બફર ચેનલ જાહેર કરે છે જે ટૂંકા પ્રકારના 16 સંદેશાઓ સુધી સંગ્રહિત કરી શકે છે (ક્ષમતા અહીં 16 છે). નિવેદનઃ નામ! એક્સ. પી. આર.; એક્સપ્રેશન એક્સ. પી. આર. નું મૂલ્ય ચેનલને નામ qname સાથે મોકલે છે, એટલે કે, તે ચેનલની પૂંછડીમાં મૂલ્યને જોડે છે. નિવેદનઃ શું નામ? એમ. એસ. જી. સંદેશ મેળવે છે, તેને ચેનલના વડા પાસેથી મેળવે છે, અને તેને ચલ એમ. એસ. જી. માં સંગ્રહિત કરે છે. ચેનલો ફર્સ્ટ-ઇન-ફર્સ્ટ-આઉટ ક્રમમાં સંદેશાઓ પસાર કરે છે. મુલાકાત સ્થળ બંદરને સ્ટોરની લંબાઈ શૂન્ય સાથે સંદેશ ચેનલ તરીકે જાહેર કરી શકાય છે. ઉદાહરણ તરીકે, નીચે મુજબઃ {byte} નું ચાન પોર્ટ = [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)-> બ્રેક od એ PROMELA માં પુનરાવર્તન માળખું વર્ણવે છે. એક સમયે માત્ર એક જ વિકલ્પ પસંદ કરી શકાય છે. વિકલ્પ પૂર્ણ થયા પછી, માળખાના અમલનું પુનરાવર્તન કરવામાં આવે છે. પુનરાવર્તન માળખાને સમાપ્ત કરવાની સામાન્ય રીત વિરામ નિવેદન સાથે છે. તે નિયંત્રણને સૂચનામાં સ્થાનાંતરિત કરે છે જે પુનરાવર્તન માળખાને તરત જ અનુસરે છે. લૂપને તોડવાની બીજી રીત ગોટો સ્ટેટમેન્ટ છે. ઉદાહરણ તરીકે, ઉપરના ઉદાહરણમાં નીચે પ્રમાણે ફેરફાર કરી શકાય છેઃ કરવુંઃઃ ગણતરી = ગણતરી + 1:: a = b + 2:: (ગણતરી = = 0)-> પૂર્ણ થયું od પૂર્ણ થયુંઃ છોડો; આ ઉદાહરણમાં ગોટો પૂર્ણ નામના લેબલ પર કૂદી જાય છે. લેબલ ફક્ત નિવેદન પહેલાં જ દેખાઈ શકે છે. કાર્યક્રમના અંતે કૂદકો મારવા માટે, ઉદાહરણ તરીકે, ડમી સ્ટેટમેન્ટ સ્કિપ ઉપયોગી છેઃ તે એક સ્થાન ધારક છે જે હંમેશા ચલાવવા યોગ્ય હોય છે અને તેની કોઈ અસર થતી નથી. દાવાઓ પ્રોમેલામાં એક મહત્વપૂર્ણ ભાષાની રચના કે જેને થોડી સમજૂતીની જરૂર છે તે ભારપૂર્વકનું નિવેદન છે. ફોર્મના નિવેદનોઃ દાવા (કોઈપણ _ બુલિયન _ શરત) હંમેશા ચલાવવા યોગ્ય હોય છે. જો નિર્દિષ્ટ બુલિયન સ્થિતિ હોય, તો નિવેદનની કોઈ અસર થતી નથી. જો, તેમ છતાં, શરત જરૂરી નથી, તો નિવેદન સ્પિન સાથે ચકાસણી દરમિયાન ભૂલ પેદા કરશે. જટિલ ડેટા સ્ટ્રક્ચર્સ PROMELA વ્યાખ્યાનો ઉપયોગ પૂર્વવ્યાખ્યાયિત અથવા અગાઉ વ્યાખ્યાયિત પ્રકારોના ડેટા ઓબ્જેક્ટ્સની સૂચિ માટે નવું નામ રજૂ કરવા માટે થઈ શકે છે. નવા પ્રકારનાં નામનો ઉપયોગ નવા ડેટા ઓબ્જેક્ટ્સને જાહેર કરવા અને ત્વરિત કરવા માટે થઈ શકે છે, જેનો ઉપયોગ કોઈપણ સંદર્ભમાં સ્પષ્ટ રીતે થઈ શકે છેઃ ટાઈપડેફ બાંધકામમાં જાહેર કરેલા ક્ષેત્રોની પહોંચ સી પ્રોગ્રામિંગ ભાષાની જેમ જ કરવામાં આવે છે. ઉદાહરણ તરીકેઃ માયસ્ટ્રક્ટ x; x.Field1 = 1; એ એક માન્ય PROMELA ક્રમ છે જે ચલ x ના ક્ષેત્ર ક્ષેત્ર 1 ને મૂલ્ય 1 સોંપે છે. સક્રિય પ્રોક્ટાઇપ્સ સક્રિય મુખ્ય શબ્દને કોઈપણ પ્રોક્ટાઇપની વ્યાખ્યા સાથે જોડી શકાય છે. જો મુખ્ય શબ્દ હાજર હોય, તો તે પ્રોક્ટાઈપનું ઉદાહરણ પ્રારંભિક સિસ્ટમ સ્થિતિમાં સક્રિય રહેશે. તે પ્રોક્ટાઇપની બહુવિધ ત્વરિતતાઓને મુખ્ય શબ્દના વૈકલ્પિક એરે પ્રત્યય સાથે સ્પષ્ટ કરી શકાય છે. ઉદાહરણોઃ સક્રિય પ્રોક્ટાઇપ A () {.} સક્રિય [4] પ્રોક્ટાઇપ B () {.} એક્ઝેક્યુટેબિલીટી એક્ઝેક્યુટેબિલીટીના શબ્દાર્થ પ્રોમેલામાં મોડેલિંગ પ્રક્રિયા સુમેળ માટે મૂળભૂત માધ્યમો પૂરા પાડે છે. એમટાઇપ = {M _ UP, M _ DW}; ચાન ચાન ડેટા ડાઉન = [0] ઓફ {mtype}; ચાન ચાન ડેટા અપ = [0] ઓફ {mtype}; પ્રોક્ટાઇપ P1 (ચાન ચાન ડેટા ઇન, ચાન ડેટા આઉટ) {ડુઃ: ચાન ડેટા ઇન? એમ. યુ. પી.-> સ્કિપ કરો;:: ચાન ડેટા આઉટ! M _ DW-> અવગણો; od;}; પ્રોક્ટાઇપ P2 (ચાન ચાન ડેટા _ ઇન, ચાન ડેટા _ આઉટ) {કરવુંઃ: ચાન ડેટા _ ઇન? M _ DW-> સ્કિપ કરો;:: Chan _ Data _ out! M _ UP-> સ્કિપ; od;}; init {atomic {રન P1 (Chan _ ડેટા _ અપ, Chan _ ડેટા _ ડાઉન); રન P2 (Chan _ ડેટા _ ડાઉન, Chan _ ડેટા _ અપ);}} ઉદાહરણમાં, બે પ્રક્રિયાઓ P1 અને P2 પાસે (1) બીજામાંથી ઇનપુટ અથવા (2) બીજામાં આઉટપુટની બિન-નિર્ધારિત પસંદગીઓ છે. બે મુલાકાત હાથ મિલાવવાનું શક્ય છે, અથવા ચલાવવા યોગ્ય છે, અને તેમાંથી એક પસંદ કરવામાં આવે છે. આ કાયમ માટે પુનરાવર્તન થાય છે. તેથી, આ મોડેલ ડેડલોક નહીં કરે. જ્યારે સ્પિન ઉપરોક્ત મોડેલનું વિશ્લેષણ કરે છે, ત્યારે તે બિન-નિર્ધારિત અલ્ગોરિધમ સાથે પસંદગીઓને ચકાસશે, જ્યાં તમામ એક્ઝેક્યુટેબલ પસંદગીઓ શોધવામાં આવશે. જો કે, જ્યારે સ્પિનનું સિમ્યુલેટર સંભવિત બિન-ચકાસાયેલ સંચાર પેટર્નની કલ્પના કરે છે, ત્યારે તે "બિન-નિર્ધારિત" પસંદગીને ઉકેલવા માટે રેન્ડમ જનરેટરનો ઉપયોગ કરી શકે છે. તેથી, સિમ્યુલેટર ખરાબ અમલ દર્શાવવામાં નિષ્ફળ થઈ શકે છે (ઉદાહરણ તરીકે, ત્યાં કોઈ ખરાબ પગેરું નથી). આ ચકાસણી અને અનુકરણ વચ્ચેનો તફાવત દર્શાવે છે. વધુમાં, રિફાઇનમેન્ટનો ઉપયોગ કરીને પ્રોમેલા મોડેલોમાંથી એક્ઝેક્યુટેબલ કોડ જનરેટ કરવું પણ શક્ય છે. કીવર્ડ્સ નીચેના ઓળખકર્તાઓ કીવર્ડ્સ તરીકે ઉપયોગ માટે આરક્ષિત છે. સંદર્ભો બાહ્ય કડીઓ સ્પિન હોમપેજ સ્પિન ટ્યુટોરિયલ્સ અને ઓનલાઇન સંદર્ભો સંક્ષિપ્ત પ્રોમેલા સંદર્ભ કમ્પ્યુટર સહાયિત ઓટોમેટા ચકાસણીઃ "ધ કેવા પ્રોજેક્ટ" (2010-2019) અને "વેરિફાઇડ મોડલ ચેકર્સ" (2016-કર્ર) વેબસાઇટ સ્પષ્ટીકરણ ભાષાઓ મોડલ ચેકર્સ