SPIN(1) General Commands Manual SPIN(1)

spin - اعتبارسنجی سامانه‌های چندنخی

spin -V
spin [ گزینه‌ها ] file

SPIN ابزاری برای تحلیل سازگاری منطقی سامانه‌های ناهمگام، به‌ویژه نرم‌افزارهای توزیع‌شده، سامانه‌های چندنخی، و پروتکل‌های ارتباطی است. مدلی از سامانه در یک زبان دستورات محافظت‌شده به نام Promela (زبان فرامحیطی فرایند) مشخص می‌شود. این زبان مدل‌سازی از ایجاد پویای فرایندها، انتخاب نامعین حالت‌ها، حلقه‌ها، دستورات goto، و متغیرهای محلی و سراسری پشتیبانی می‌کند. همچنین امکان مشخص‌سازی فشردهٔ نیازمندی‌های درستی منطقی را فراهم می‌آورد، از جمله، ولی نه محدود به، نیازمندی‌هایی که در منطق زمانی خطی (LTL) بیان می‌شوند.

با دریافت یک مدل Promela ذخیره‌شده در file ، SPIN می‌تواند شبیه‌سازی‌های تعاملی، هدایت‌شده یا تصادفی را از اجرای سامانه انجام دهد. همچنین می‌تواند یک برنامهٔ C تولید کند که اعتبارسنجی جامع و کاملی از نیازمندی‌های درستی سامانه را اجرا نماید. گزینه‌های اصلی پشتیبانی‌شده به شرح زیر هستند (همواره می‌توانید با دستور «spin --» فهرست کاملی از گزینه‌های فعلی را دریافت کنید):

یک اعتبارسنج (یک مدل‌چکِر / model checker) برای مشخصات تولید می‌کند. خروجی در مجموعه‌ای از فایل‌های C با نام pan.[cbhmt] نوشته می‌شود که می‌توانند کامپایل شوند (cc -o pan pan.c) تا یک اعتبارسنج اجرایی تولید شود. راهنماهای برخط SPIN شامل جزئیات مربوط به کامپایل و استفاده از اعتبارسنج‌ها هستند.
عبارت‌های printf را در طول اجرای شبیه‌سازی اجرا نمی‌کند.
یک تقریب ASCII از نمودار توالی پیام (message sequence chart) را برای یک اجرای شبیه‌سازی تصادفی یا هدایت‌شده (در هنگام ترکیب با -t) تولید می‌کند. همچنین گزینهٔ -M را ببینید.
مقدار -Dxxx را به پیش‌پردازنده ارسال می‌کند (همچنین -E و -I را ببینید).
اطلاعات جدول نمادها (symbol table) را برای مدل مشخص‌شده در file تولید می‌کند. برای هر شیء Promela، این اطلاعات شامل نوع، نام، و تعداد عناصر (اگر به‌صورت آرایه اعلان شده باشد)، مقدار اولیه (اگر شیء داده‌ای باشد) یا اندازه (اگر کانال پیام باشد)، حوزه (سراسری یا محلی)، و اینکه آیا شیء به عنوان یک متغیر اعلان شده یا به عنوان یک پارامتر، می‌باشد. برای کانال‌های پیام، نوع داده‌های فیلدهای پیام فهرست می‌شوند. برای متغیرهای ساختاری، فیلد سوم نام اعلان ساختاری را که حاوی متغیر است تعیین می‌کند.
مقدار xxx را به پیش‌پردازنده ارسال می‌کند (همچنین -D و -I را ببینید).
اگر مشخصات شامل چندین ادعای never یا ویژگی ltl باشد، ضرب همگام (synchronous product) تمام ادعاها را محاسبه کرده و نتیجه را در خروجی استاندارد می‌نویسد.
فرمول LTL به نام LTL را به یک ادعای never (never claim) ترجمه می‌کند.
این گزینه فرمولی با نحو LTL را از آرگومان دوم می‌خواند و آن را به نحو Promela (یک ادعای never، که معادل Promela برای اتوماتون Bchi است) ترجمه می‌کند. عملگرهای LTL بدین صورت نوشته می‌شوند: [] (همیشه / always)، <> (سرانجام / eventually)، و U (تا زمانِ قوی / strong until). عملگر X (بعدی / next) وجود ندارد، تا سازگاری با قواعد کاهش مرتبه جزئی (partial order reduction) که در طول فرایند اعتبارسنجی اعمال می‌شوند حفظ شود. اگر فرمول حاوی فاصله باشد، باید درون علامت نقل‌قول قرار گیرد تا یک آرگومان واحد برای دستور SPIN تشکیل دهد.
این گزینه در نسخه ۶.۰ Spin تا حد زیادی با پشتیبانی از مشخص‌سازی درون‌خطی (inline) فرمول‌های ltl جایگزین شده است.
فرمول LTL ذخیره‌شده در file را به یک ادعای never ترجمه می‌کند.
این گزینه رفتاری مشابه با گزینهٔ -f دارد، اما فرمول را به جای خط فرمان از file می‌خواند. فایل باید حاوی فرمول در خط اول خود باشد. هر متنی که پس از این خط اول بیاید نادیده گرفته می‌شود، بنابراین می‌توان از آن برای ذخیره یادداشت‌ها یا توضیحات درباره فرمول استفاده کرد. (در برخی سیستم‌ها، قواعد نقل‌قول پوسته استفاده از گزینهٔ -f را پیچیده می‌کند. گزینهٔ -F برای حل این مشکلات در نظر گرفته شده است).
در ترکیب با گزینهٔ -p، تمام به‌روزرسانی‌های متغیرهای سراسری را در طول اجرای شبیه‌سازی چاپ می‌کند.
در پایان اجرای شبیه‌سازی، مقدار سید (seed) استفاده‌شده برای مولد اعداد تصادفی را چاپ می‌کند. با مشخص کردن همان مقدار سید توسط گزینهٔ -n، می‌توان بعداً دقیقاً همان اجرا را تکرار کرد.
نتیجهٔ درون‌خطی‌سازی (inlining) و پیش‌پردازش را نمایش می‌دهد.
یک شبیه‌سازی تعاملی انجام می‌دهد، و در هر گام از اجرا که نیاز به یک انتخاب نامعین (nondeterministic) داشته باشد، از کاربر ورودی می‌خواهد. زمانی که اجرا معین (deterministic) باشد، شبیه‌سازی بدون مداخلهٔ کاربر ادامه می‌یابد.
از چاپ خروجی برای N گام نخست در یک اجرای شبیه‌سازی صرف‌نظر می‌کند.
ترتیب ارزیابی را برای دستورات تو در توی unless معکوس می‌کند، برای مثال جهت تطابق با نحوهٔ مدیریت استثناها در Java.
از نام فایل file به عنوان trail-file استفاده می‌کند؛ همچنین -t را ببینید.
در ترکیب با گزینهٔ -p، تمام به‌روزرسانی‌های متغیرهای محلی را در خروجی یک اجرای شبیه‌سازی لحاظ می‌کند.
یک نمودار توالی پیام در قالب tcl/tk برای یک شبیه‌سازی تصادفی یا شبیه‌سازی هدایت‌شده (در هنگام ترکیب با -t)، برای مدل موجود در file تولید کرده و نتیجه را با wish نمایش می‌دهد. همچنین گزینهٔ -c را ببینید. -m معناشناسی رویدادهای ارسال را تغییر می‌دهد. به‌طور معمول، اگر بافر پیام مقصد پر باشد، یک عملیات ارسال مسدود (blocked) خواهد شد. با این گزینه، پیامی که به یک بافر پر ارسال شود از بین می‌رود.
مقدار بذر (seed) شبیه‌سازی تصادفی را روی مقدار عدد صحیح N . تنظیم می‌کند. هیچ فاصله‌ای بین -n و عدد صحیح N وجود ندارد. ,TP -N file از never claim ذخیره‌شده در file برای تولید وارسی‌گر استفاده می‌کند (-a را ببینید).
از قواعد حوزهٔ دید اصلی مربوط به نسخه‌های پیش از نسخهٔ ۶ Spin استفاده می‌کند.
بهینه‌سازی جریان داده را خاموش می‌کند (-o1). عدم پنهان‌سازی متغیرهای فقط-نوشتنی (-o2) در طول وارسی. خاموش کردن ادغام دستورات (-o3) در طول وارسی. روشن کردن بهینه‌سازی rendezvous (-o4) در طول وارسی. روشن کردن case caching (-o5) برای کاهش اندازهٔ pan.m، اما با کاهش دقت در گزارش‌های دسترسی‌پذیری.
قواعد حوزهٔ دیدِ پیش از نسخهٔ 6.0 را به کار می‌برد. در این حالت تنها دو سطح حوزهٔ دیدِ ممکن برای تمام اعلان‌های داده وجود دارد: سراسری (global)، یا محلیِ proctype. در نسخهٔ 6.0 و پس از آن، سطح سومی از حوزهٔ دید وجود دارد: inlines یا بلوک‌ها.
استفاده از دستور xxx برای پیش‌پردازش به‌جای پیش‌پردازندهٔ استاندارد C.
تمام اجراهای دستورات را در خروجی اجراهای شبیه‌سازی می‌گنجاند.
جلوگیری از خروجی تولیدشده برای کانال N در طول اجراهای شبیه‌سازی.
نمایش تمام رویدادهای دریافت پیام، همراه با نام و شمارهٔ فرایند دریافت‌کننده و شمارهٔ خط کد مبدأ متناظر. برای هر پارامتر پیام، نوع پیام و شماره و نام کانال پیام را نشان می‌دهد.
بازپخش یک ردپای خطا (error trace) که در وارسی قبلی یافت شده است (-search را ببینید). همانند -search، آرگومان‌های مربوط به خود Spin (مانند -p) را می‌توان پیش از آرگومان -replay تعیین کرد. اگر بازپخش تنها با فایل اجرایی
کامپایل و اجرای مستقیم. پرچم‌های زمان کامپایل و زمان اجرای وارسی می‌توانند پس از این پارامتر افزوده شوند. هرگونه پارامتر زمان تجزیهٔ Spin باید پیش از پارامتر -search بیاید. خط فرمان واقعی اجراشده در صورت تعیین -v (پیش از آرگومان -search) چاپ می‌شود.
تمام عملیات‌های ارسال را در خروجی اجراهای شبیه‌سازی می‌گنجاند.
خروجی printf فرایند i را به‌طور خودکار با i تب (tab) تورفتگی نمی‌دهد.
یک شبیه‌سازی هدایت‌شده را با دنبال کردن [Nاُمین] ردپای خطایی که توسط یک اجرای وارسی قبلی تولید شده است، انجام می‌دهد؛ برای جزئیات وارسی به راهنماهای برخط مراجعه کنید. به‌طور پیش‌فرض، ردپای خطا در فایلی با همان نام پایهٔ مدل و با پسوند .trail جستجو می‌شود. همچنین -k را ببینید.
حالت پرگو (verbose)، افزودن جزئیات بیشتر، و تولید نکات و هشدارهای بیشتر دربارهٔ مدل.
شماره نسخهٔ SPIN را چاپ کرده و خارج می‌شود.
تولید جدول‌های گذار (transition tables) از روی مدل و خروج (تولید، کامپایل و اجرای pan.c).

تنها با یک نام فایل به‌عنوان آرگومان و بدون هیچ پرچم گزینه‌ای، SPIN یک شبیه‌سازی تصادفی از مدل مشخص‌شده در فایل را انجام می‌دهد. این حالت معمولاً خروجی تولید نمی‌کند، مگر مواردی که صراحتاً توسط کاربر درون مدل با دستورات printf تولید شده باشند، و برخی جزئیات دربارهٔ وضعیت نهایی که پس از پایان شبیه‌سازی حاصل می‌شود. گروه گزینه‌های -bgilmprstv برای تنظیم سطح دلخواه اطلاعاتی که کاربر دربارهٔ یک اجرای شبیه‌سازی تصادفی، هدایت‌شده یا تعاملی می‌خواهد، به کار می‌رود. هر خط از خروجی معمولاً حاوی ارجاعی به خط کد مبدأ در مشخصات است که آن را تولید کرده است. اگر گزینهٔ -i گنجانده شود، شبیه‌سازی تعاملی (interactive) است، یا اگر گزینهٔ -t یا -k file اضافه شود، شبیه‌سازی هدایت‌شده (guided) است.

جلوگیری از اجرای دستورات printf در درون مدل.
نمایش مقدار فعلی متغیرهای سراسری در هر گام زمانی.
در ترکیب با گزینهٔ -p، مقدار فعلی متغیرهای محلی فرایند را نشان می‌دهد.
در هر گام شبیه‌سازی نشان می‌دهد کدام فرایند تغییر وضعیت داده، و کدام دستور کد مبدأ اجرا شده است.
نمایش تمام رویدادهای دریافت پیام، همراه با نام و شمارهٔ فرایند دریافت‌کننده و شمارهٔ خط کد مبدأ متناظر. برای هر پارامتر پیام، نوع پیام و شماره و نام کانال پیام را نشان می‌دهد.
تمام رویدادهای ارسال پیام را نشان می‌دهد.
حالت پرگو (verbose)، افزودن جزئیات بیشتر، و تولید نکات و هشدارهای بیشتر دربارهٔ مدل..SH "همچنین ببینید (SEE ALSO)" راهنماهای برخط در spinroot.com:

http://spinroot.com/spin/Man/3_SpinGUI.html
http://spinroot.com/spin/Man/4_SpinVerification.html
http://spinroot.com/spin/Man/1_Exercises.html
اطلاعات زمینه‌ای بیشتر دربارهٔ سامانه و فرایند وارسی را می‌توان برای نمونه در مآخذ زیر یافت:


G.J. Holzmann, The Spin Model Checker Primer and Reference Manual, Addison-Wesley, Reading, Mass., 2004.
--, `The model checker SPIN,' IEEE Trans. on SE, Vol, 23, No. 5, May 1997.
--, `Design and validation of protocols: a tutorial,' Computer Networks and ISDN Systems, Vol. 25, No. 9, 1993, pp. 981-1017.
--, Design and Validation of Computer Protocols, Prentice Hall, Englewood Cliffs, NJ, 1991.