Murφ
મુર્ફી એ સ્ટેનફોર્ડ યુનિવર્સિટી ખાતે વિકસાવવામાં આવેલું એક સ્પષ્ટ-રાજ્ય મોડેલ ચેકર છે, અને કેશ-સુસંગતતા પ્રોટોકોલની ઔપચારિક ચકાસણી માટે તેનો વ્યાપકપણે ઉપયોગ થાય છે. ડેવિડ ડિલ દ્વારા એક પેપરમાં ઇતિહાસ મુર્ફીના પ્રારંભિક ઇતિહાસનું વર્ણન કરવામાં આવ્યું છે. મુર્ફીનું પ્રથમ સંસ્કરણ 1990 અને 1991માં સ્ટેનફોર્ડ યુનિવર્સિટીમાં પ્રોફેસર ડેવિડ ડિલ અને તેમના સ્નાતક વિદ્યાર્થીઓ એન્ડ્રેસ ડ્રેક્સલર, એલન હુ અને હાન યાંગ દ્વારા તૈયાર કરવામાં આવ્યું હતું અને મુખ્યત્વે એન્ડ્રેસ ડ્રેક્સલર દ્વારા અમલમાં મૂકવામાં આવ્યું હતું. ડેવિડ ડિલ, એલન હુ, સી. નોરિસ ઇપ, રાલ્ફ મેલ્ટન, સેઉંગજૂન પાર્ક અને હાન યાંગ દ્વારા સ્પષ્ટીકરણ ભાષામાં વ્યાપકપણે ફેરફાર અને વિસ્તરણ કરવામાં આવ્યું હતું. રાલ્ફ મેલ્ટને 1992ના ઉનાળા અને પાનખર દરમિયાન નવા સંસ્કરણનો અમલ કર્યો હતો. સેઉંગજૂન પાર્કે જીવંતતા ચકાસણી અને નિષ્પક્ષતા અવરોધો ઉમેર્યા, પરંતુ જીવંતતા ચકાસણી માટેનું અલ્ગોરિધમ મહત્વપૂર્ણ ઓપ્ટિમાઇઝેશન, ખાસ કરીને સમપ્રમાણતા ઘટાડા સાથે વિરોધાભાસી હોવાથી, જીવંતતા ચકાસણી પછીના પ્રકાશનોમાં અવગણવામાં આવી હતી. સી. નોરિસ આઈપીએ રિવર્સિબલ નિયમો અને પુનરાવર્તન કન્સ્ટ્રક્ટર્સ (જે પ્રકાશન 3.1 માં શામેલ નથી) અમલમાં મૂક્યા, અને સમપ્રમાણતા અને મલ્ટીસેટ ઘટાડા (જે છે) ઉમેર્યા. ઉલરિચ સ્ટર્ને હેશ કોમ્પેક્શન અમલમાં મૂક્યું, ડિસ્કના ઉપયોગમાં સુધારો કર્યો અને પેરેલલ મુર્ફી અમલમાં મૂક્યું. સ્ટેનફોર્ડનું છેલ્લું પ્રકાશન 1993ના નવેમ્બરમાં 3.1 રિલીઝ થયું હતું. ત્યારથી અન્ય જૂથો દ્વારા મુર્ફીની ઘણી વ્યુત્પન્ન આવૃત્તિઓ બનાવવામાં આવી છે. લક્ષણો મર્ફ કમ્પાઇલર મર્ફ સ્પષ્ટીકરણ ભાષામાં લખાયેલ મોડેલને સ્વીકારે છે અને C + + કોડને આઉટપુટ કરે છે જે તે મોડેલ માટે ચકાસણીકર્તા બનાવે છે. (એટલે કે, સી + + કોડ, જ્યારે ચલાવવામાં આવે છે, ત્યારે સ્પષ્ટીકરણ દ્વારા વર્ણવેલ ડિઝાઇન પર સ્પષ્ટ-સ્થિતિ મોડેલની તપાસ કરે છે.) મુર્ફી સ્પષ્ટીકરણ ભાષા વૈશ્વિક ચલ દ્વારા કરવામાં આવતા તમામ સુમેળ અને સંદેશાવ્યવહાર સાથે સંરક્ષિત આદેશો અને અસિંક્રોનસ, ઇન્ટરલીવિંગ મોડેલનો ઉપયોગ કરે છે. વેરિફાયર મોડેલમાં નિર્દિષ્ટ કરેલા અપરિવર્તનશીલ અને આંતરિક દાવાઓના સ્વરૂપમાં સલામતીના ગુણધર્મોની તપાસ કરે છે અને ડેડલોકની તપાસ કરે છે. તે જીવંત ગુણધર્મોની તપાસ કરતું નથી, જોકે મુર્ફી પ્રકાશન 2.7 એલ સામાન્ય એલ. ટી. એલ જીવંત ગુણધર્મોના સમૂહની ચકાસણીને સમર્થન આપે છે. ભાષા અને ચકાસણીકર્તા અમુક પ્રકારના સમપ્રમાણતા ઘટાડાને ટેકો આપે છે. મુર્ફી મૂળરૂપે કેશ-સુસંગતતા પ્રોટોકોલની ચકાસણી માટે લાગુ કરવામાં આવ્યું હતું, પરંતુ સુરક્ષા પ્રોટોકોલની ચકાસણી સહિત અન્ય સમસ્યાઓ પર પણ લાગુ કરવામાં આવ્યું છે. મરફી લાઇસન્સ એમ. આઈ. ટી. લાઇસન્સ જેવું જ છે. મર્ફનો ઉપયોગ, નકલ, ફેરફાર, વેચાણ અને કોઈપણ હેતુ માટે પુનઃવિતરણ કરી શકાય છે, જો કે કૉપિરાઇટ નોટિસ અને લાઇસન્સ શામેલ હોય, તો સ્ટેનફોર્ડ યુનિવર્સિટીનું નામ પરવાનગી વિના જાહેરાત અથવા પ્રચાર માટે ઉપયોગમાં લેવાતું નથી, અને સંશોધિત આવૃત્તિઓને પરવાનગી વિના મર્ફિ કહેવામાં આવતી નથી. મર્ફની ઘણી વ્યુત્પન્ન આવૃત્તિઓ સ્ટેનફોર્ડ અને અન્યત્ર બનાવવામાં આવી છે, જેમાં નીચેનાનો સમાવેશ થાય છેઃ સમાંતર મર્ફ એડી-સમાંતર અને વિતરિત મર્ફ. PReach (સમાંતર પહોંચ)-એર્લાંગમાં લાગુ કરાયેલ સમાંતર મોડેલ ચકાસણી. વિતરિત મર્ફિ પેરેલલ રેન્ડમ-વોક મર્ફિ પીએએમ-પ્રેડિકેટ એબ્સ્ટ્રેક્શન મર્ફિ કવિતા-આંશિક-ઓર્ડર સક્ષમ મર્ફિ સીએમર્ફિ-કેચિંગ મર્ફિ. એફ. એચ. પી.-મર્ફી-ફાઈનાઇટ હોરાઇઝન પ્રોબેબિલિસ્ટિક મર્ફી. એડી મર્ફી-સમાંતર અને વિતરિત, CMurphy પર આધારિત, સંદેશ પસાર કરવા માટે MPI નો ઉપયોગ કરે છે. યુનિવર્સલ પ્લાનર મર્ફિ-પ્રક્રિયાઓ અને ઘટનાઓ સાથે રેખીય અને બિનરેખીય સતત PDDL + મોડેલો માટે આયોજન અને સાર્વત્રિક આયોજન; પ્રારંભિક શાબ્દિક અને સમયબદ્ધ પ્રારંભિક પ્રવાહી પણ. અફવા પણ જુઓ મોડેલ ચેકિંગ ટૂલ્સની મોડેલ ચેકિંગ સૂચિ સંદર્ભો બાહ્ય કડીઓ મર્ફિ એનોટેટેડ સંદર્ભ માર્ગદર્શિકા, પ્રકાશન 3.1 સ્ટેનફોર્ડ સુરક્ષા પ્રયોગશાળા, સુરક્ષા પ્રોટોકોલ માટે મોડેલ ચેકિંગ પદ્ધતિઓ યુનિવર્સિટી ઓફ ઉટાહ, સ્કૂલ ઓફ કમ્પ્યુટિંગ-મર્ફની આવૃત્તિઓનો સંગ્રહ. મોડેલ ચકાસણી C + + માં પ્રોગ્રામ કરેલ મફત સોફ્ટવેર