.ds Z S\s-2PIN\s0
.ds P P\s-2ROMELA\s0
.\"
.\" On CYGWIN move this page to c:/cygwin/usr/man/man1/spin.1
.\"
.TH SPIN 1
.CT 1 comm_mach protocol
.SH "نام (NAME)"
spin \- اعتبارسنجی سامانه‌های چندنخی
.SH "خلاصه دستور (SYNOPSIS)"
.B spin
.BI -V
.br
.B spin
[
گزینه‌ها
]
.I file
.SH "توضیحات (DESCRIPTION)"
\*Z
ابزاری برای تحلیل سازگاری منطقی سامانه‌های ناهمگام،
به‌ویژه نرم‌افزارهای توزیع‌شده، سامانه‌های چندنخی،
و پروتکل‌های ارتباطی است.
مدلی از سامانه در یک زبان دستورات محافظت‌شده به نام Promela (زبان فرامحیطی فرایند)
مشخص می‌شود.
این زبان مدل‌سازی از ایجاد پویای فرایندها،
انتخاب نامعین حالت‌ها، حلقه‌ها، دستورات goto،
و متغیرهای محلی و سراسری پشتیبانی می‌کند.
همچنین امکان مشخص‌سازی فشردهٔ نیازمندی‌های درستی منطقی را فراهم می‌آورد،
از جمله، ولی نه محدود به، نیازمندی‌هایی که در منطق زمانی خطی (LTL)
بیان می‌شوند.
.PP
با دریافت یک مدل Promela ذخیره‌شده در
.I file ،
\*Z می‌تواند شبیه‌سازی‌های تعاملی، هدایت‌شده یا تصادفی را از اجرای سامانه انجام دهد.
همچنین می‌تواند یک برنامهٔ C تولید کند که اعتبارسنجی جامع و کاملی از
نیازمندی‌های درستی سامانه را اجرا نماید.
گزینه‌های اصلی پشتیبانی‌شده به شرح زیر هستند (همواره می‌توانید با دستور
«spin --» فهرست کاملی از گزینه‌های فعلی را دریافت کنید):
.\"----------------------a----------------
.TP
.B -a
یک اعتبارسنج (یک مدل‌چکِر / model checker) برای مشخصات تولید می‌کند.
خروجی در مجموعه‌ای از فایل‌های C با نام
.BR pan. [ cbhmt ]
نوشته می‌شود که می‌توانند کامپایل شوند
.RB ( "cc -o pan pan.c" )
تا یک اعتبارسنج اجرایی تولید شود.
راهنماهای برخط \*Z شامل جزئیات مربوط به کامپایل و استفاده از اعتبارسنج‌ها هستند.
.\"--------------------------b------------
.TP
.B -b
عبارت‌های printf را در طول اجرای شبیه‌سازی اجرا نمی‌کند.
.\"--------------------------c------------
.TP
.B -c
یک تقریب ASCII از نمودار توالی پیام (message sequence chart) را برای یک اجرای
شبیه‌سازی تصادفی یا هدایت‌شده (در هنگام ترکیب با \f3-t\f1) تولید می‌کند.
همچنین گزینهٔ \f3-M\f1 را ببینید.
.\"--------------------------D------------
.TP
.BI -Dxxx
مقدار \f2-Dxxx\f1 را به پیش‌پردازنده ارسال می‌کند (همچنین \f2-E\f1 و \f2-I\f1 را ببینید).
.\"--------------------------d------------
.TP
.BI -d
اطلاعات جدول نمادها (symbol table) را برای مدل مشخص‌شده در
.I file
تولید می‌کند.
برای هر شیء Promela، این اطلاعات شامل نوع، نام، و تعداد عناصر (اگر به‌صورت آرایه اعلان شده باشد)،
مقدار اولیه (اگر شیء داده‌ای باشد) یا اندازه (اگر کانال پیام باشد)،
حوزه (سراسری یا محلی)، و اینکه آیا شیء به عنوان یک متغیر اعلان شده یا به عنوان یک پارامتر، می‌باشد.
برای کانال‌های پیام، نوع داده‌های فیلدهای پیام فهرست می‌شوند.
برای متغیرهای ساختاری، فیلد سوم نام اعلان ساختاری را که حاوی متغیر است تعیین می‌کند.
.\"--------------------------E------------
.TP
.BI -Exxx
مقدار \f2xxx\f1 را به پیش‌پردازنده ارسال می‌کند (همچنین \f2-D\f1 و \f2-I\f1 را ببینید).
.\"--------------------------e------------
.TP
.BI -e
اگر مشخصات شامل چندین ادعای never یا ویژگی ltl باشد، ضرب همگام (synchronous product)
تمام ادعاها را محاسبه کرده و نتیجه را در خروجی استاندارد می‌نویسد.
.\"--------------------------f------------
.TP
.BI "-f \f2LTL\f1"
فرمول LTL به نام \f2LTL\f1 را به یک ادعای never (never claim) ترجمه می‌کند.
.br
این گزینه فرمولی با نحو LTL را از آرگومان دوم می‌خواند
و آن را به نحو Promela (یک ادعای never، که معادل Promela برای اتوماتون B\(u"chi است) ترجمه می‌کند.
عملگرهای LTL بدین صورت نوشته می‌شوند: [] (همیشه / always)، <> (سرانجام / eventually)،
و U (تا زمانِ قوی / strong until). عملگر X (بعدی / next) وجود ندارد، تا سازگاری با
قواعد کاهش مرتبه جزئی (partial order reduction) که در طول فرایند اعتبارسنجی اعمال می‌شوند
حفظ شود.
اگر فرمول حاوی فاصله باشد، باید درون علامت نقل‌قول قرار گیرد تا یک آرگومان واحد
برای دستور \*Z تشکیل دهد.
.br
این گزینه در نسخه ۶.۰ Spin تا حد زیادی با پشتیبانی از مشخص‌سازی درون‌خطی (inline) فرمول‌های ltl
جایگزین شده است.
.\"--------------------------F------------
.TP
.BI "-F \f2file\f1"
فرمول LTL ذخیره‌شده در
.I file
را به یک ادعای never ترجمه می‌کند.
.br
این گزینه رفتاری مشابه با گزینهٔ
.B -f
دارد، اما فرمول را به جای خط فرمان از
.I file
می‌خواند.
فایل باید حاوی فرمول در خط اول خود باشد. هر متنی که پس از این خط اول بیاید
نادیده گرفته می‌شود، بنابراین می‌توان از آن برای ذخیره یادداشت‌ها یا توضیحات درباره فرمول
استفاده کرد.
(در برخی سیستم‌ها، قواعد نقل‌قول پوسته استفاده از گزینهٔ
.B -f
را پیچیده می‌کند. گزینهٔ
.B -F
برای حل این مشکلات در نظر گرفته شده است).
.\"--------------------------g------------
.TP
.BI -g
در ترکیب با گزینهٔ
.BR -p ،
تمام به‌روزرسانی‌های متغیرهای سراسری را در طول اجرای شبیه‌سازی چاپ می‌کند.
.\"--------------------------h------------
.TP
.BI -h
در پایان اجرای شبیه‌سازی، مقدار سید (seed) استفاده‌شده برای مولد اعداد تصادفی را چاپ می‌کند.
با مشخص کردن همان مقدار سید توسط گزینهٔ \f3-n\f1، می‌توان بعداً دقیقاً همان اجرا را تکرار کرد.
.\"--------------------------I------------
.TP
.BI -I
نتیجهٔ درون‌خطی‌سازی (inlining) و پیش‌پردازش را نمایش می‌دهد.
.\"--------------------------i------------
.TP
.BI -i
یک شبیه‌سازی تعاملی انجام می‌دهد، و در هر گام از اجرا که نیاز به یک انتخاب نامعین
(nondeterministic) داشته باشد، از کاربر ورودی می‌خواهد. زمانی که اجرا معین (deterministic)
باشد، شبیه‌سازی بدون مداخلهٔ کاربر ادامه می‌یابد.
.\"--------------------------j------------
.TP
.BI -j\f2N
از چاپ خروجی برای \f2N\f1 گام نخست در یک اجرای شبیه‌سازی صرف‌نظر می‌کند.
.\"--------------------------J------------
.TP
.BI -J
ترتیب ارزیابی را برای دستورات تو در توی unless معکوس می‌کند،
برای مثال جهت تطابق با نحوهٔ مدیریت استثناها در Java.
.\"--------------------------k------------
.TP
.BI "-k \f2file\f1"
از نام فایل \f2file\f1 به عنوان trail-file استفاده می‌کند؛ همچنین \f3-t\f1 را ببینید.
.\"--------------------------l------------
.TP
.BI -l
در ترکیب با گزینهٔ
.BR -p ،
تمام به‌روزرسانی‌های متغیرهای محلی را در خروجی یک اجرای شبیه‌سازی لحاظ می‌کند.
.\"--------------------------M------------
.TP
.BI -M
یک نمودار توالی پیام در قالب tcl/tk برای یک شبیه‌سازی تصادفی یا شبیه‌سازی هدایت‌شده
(در هنگام ترکیب با \f(BI-t\f1)، برای مدل موجود در
.I file
تولید کرده و نتیجه را با wish نمایش می‌دهد.
همچنین گزینهٔ \f3-c\f1 را ببینید.
.\"--------------------------m------------.TP
.BI -m
معناشناسی رویدادهای ارسال را تغییر می‌دهد.
به‌طور معمول، اگر بافر پیام مقصد پر باشد، یک عملیات ارسال مسدود (blocked) خواهد شد.
با این گزینه، پیامی که به یک بافر پر ارسال شود از بین می‌رود.
.\"--------------------------n------------
.TP
.BI "-n\f2N"
مقدار بذر (seed) شبیه‌سازی تصادفی را روی مقدار عدد صحیح
.I N .
تنظیم می‌کند.
هیچ فاصله‌ای بین \f(BI-n\f1 و عدد صحیح \f2N\f1 وجود ندارد.
.\"--------------------------N------------
,TP
.BI "-N \f2file\f1"
از never claim ذخیره‌شده در \f2file\f1 برای تولید وارسی‌گر استفاده می‌کند (\f3-a\f1 را ببینید).
.\"--------------------------O------------
.TP
.BI -O
از قواعد حوزهٔ دید اصلی مربوط به نسخه‌های پیش از نسخهٔ ۶ Spin استفاده می‌کند.
.\"--------------------------o------------
.TP
.BI -o\f2[123]\f1
بهینه‌سازی جریان داده را خاموش می‌کند (\f2-o1\f1).
عدم پنهان‌سازی متغیرهای فقط-نوشتنی (\f2-o2\f1) در طول وارسی.
خاموش کردن ادغام دستورات (\f2-o3\f1) در طول وارسی.
روشن کردن بهینه‌سازی rendezvous (\f2-o4\f1) در طول وارسی.
روشن کردن case caching (\f2-o5\f1) برای کاهش اندازهٔ pan.m،
اما با کاهش دقت در گزارش‌های دسترسی‌پذیری.
.\"--------------------------O------------
.TP
.BI -O
قواعد حوزهٔ دیدِ پیش از نسخهٔ 6.0 را به کار می‌برد. در این حالت تنها دو
سطح حوزهٔ دیدِ ممکن برای تمام اعلان‌های داده وجود دارد: سراسری (global)، یا محلیِ proctype.
در نسخهٔ 6.0 و پس از آن، سطح سومی از حوزهٔ دید وجود دارد: inlines یا بلوک‌ها.
.\"--------------------------P------------
.TP
.BI -P\f2xxx\f1
استفاده از دستور \f2xxx\f1 برای پیش‌پردازش به‌جای پیش‌پردازندهٔ استاندارد C.
.\"--------------------------p------------
.TP
.BI -p
تمام اجراهای دستورات را در خروجی اجراهای شبیه‌سازی می‌گنجاند.
.\"--------------------------q------------
.TP
.BI "-q\f2N\f1"
جلوگیری از خروجی تولیدشده برای کانال \f2N\f1 در طول اجراهای شبیه‌سازی.
.\"--------------------------r------------
.TP
.BI -r
نمایش تمام رویدادهای دریافت پیام، همراه با
نام و شمارهٔ فرایند دریافت‌کننده
و شمارهٔ خط کد مبدأ متناظر.
برای هر پارامتر پیام،
نوع پیام و شماره و نام کانال پیام را نشان می‌دهد.
.TP
.BR -replay
بازپخش یک ردپای خطا (error trace) که در وارسی قبلی یافت شده است (-search را ببینید).
همانند -search، آرگومان‌های مربوط به خود Spin (مانند -p) را می‌توان
\f2پیش از\f1 آرگومان -replay تعیین کرد. اگر بازپخش تنها با فایل اجرایی
./pan امکان‌پذیر باشد، آن‌گاه آرگومان‌های بازپخش با فایل اجرایی
./pan را می‌توان \f2پس از\f1 آرگومان -replay مشخص کرد.
.TP
.BR -search
کامپایل و اجرای مستقیم. پرچم‌های زمان کامپایل و زمان اجرای وارسی
می‌توانند \f2پس از\f1 این پارامتر افزوده شوند. هرگونه پارامتر زمان تجزیهٔ
Spin باید \f2پیش از\f1 پارامتر -search بیاید.
خط فرمان واقعی اجراشده در صورت تعیین -v (پیش از آرگومان -search)
چاپ می‌شود.
.\"--------------------------s------------
.TP
.BI -s
تمام عملیات‌های ارسال را در خروجی اجراهای شبیه‌سازی می‌گنجاند.
.\"--------------------------T------------
.TP
.BI -T
خروجی printf فرایند \f2i\f1 را به‌طور خودکار با \f2i\f1 تب (tab) تورفتگی نمی‌دهد.
.\"--------------------------t------------
.TP
.BI -t[\f2N\f1]
یک شبیه‌سازی هدایت‌شده را با دنبال کردن [\f2N\f1اُمین] ردپای خطایی که
توسط یک اجرای وارسی قبلی تولید شده است، انجام می‌دهد؛ برای جزئیات
وارسی به راهنماهای برخط مراجعه کنید. به‌طور پیش‌فرض، ردپای خطا
در فایلی با همان نام پایهٔ مدل و با پسوند .trail جستجو می‌شود.
همچنین \f3-k\f1 را ببینید.
.\"--------------------------v------------
.TP
.BI -v
حالت پرگو (verbose)، افزودن جزئیات بیشتر، و تولید نکات و
هشدارهای بیشتر دربارهٔ مدل.
.\"--------------------------V------------
.TP
.BI -V
شماره نسخهٔ \*Z را چاپ کرده و خارج می‌شود.
.\"--------------------------x------------
.TP
.BI -x
تولید جدول‌های گذار (transition tables) از روی مدل و خروج
(تولید، کامپایل و اجرای pan.c).
.\"--------------------------.------------
.PP
تنها با یک نام فایل به‌عنوان آرگومان و بدون هیچ پرچم گزینه‌ای،
\*Z یک شبیه‌سازی تصادفی از مدل مشخص‌شده در
فایل را انجام می‌دهد.
این حالت معمولاً خروجی تولید نمی‌کند، مگر مواردی که صراحتاً
توسط کاربر درون مدل با دستورات \f2printf\f1 تولید شده باشند،
و برخی جزئیات دربارهٔ وضعیت نهایی که پس از پایان
شبیه‌سازی حاصل می‌شود.
گروه گزینه‌های
.B -bgilmprstv
برای تنظیم سطح دلخواه اطلاعاتی که کاربر دربارهٔ یک اجرای شبیه‌سازی
تصادفی، هدایت‌شده یا تعاملی می‌خواهد، به کار می‌رود.
هر خط از خروجی معمولاً حاوی ارجاعی به خط کد مبدأ
در مشخصات است که آن را تولید کرده است.
اگر گزینهٔ
.B -i
گنجانده شود، شبیه‌سازی \f2تعاملی\f1 (interactive) است، یا اگر گزینهٔ
.B -t
یا
.B -k \f2file\f1
اضافه شود، شبیه‌سازی \f2هدایت‌شده\f1 (guided) است.
.\"--------------------------bglprsv------------
.TP
.BI -b
جلوگیری از اجرای دستورات \f(CWprintf\f1 در درون مدل.
.TP
.BI -g
نمایش مقدار فعلی متغیرهای سراسری در هر گام زمانی.
.TP
.BI -l
در ترکیب با گزینهٔ
.BR -p ،
مقدار فعلی متغیرهای محلی فرایند را نشان می‌دهد.
.TP
.BI -p
در هر گام شبیه‌سازی نشان می‌دهد کدام فرایند تغییر وضعیت داده،
و کدام دستور کد مبدأ اجرا شده است.
.TP
.BI -r
نمایش تمام رویدادهای دریافت پیام، همراه با
نام و شمارهٔ فرایند دریافت‌کننده
و شمارهٔ خط کد مبدأ متناظر.
برای هر پارامتر پیام،
نوع پیام و شماره و نام کانال پیام را نشان می‌دهد.
.TP
.BI -s
تمام رویدادهای ارسال پیام را نشان می‌دهد.
.TP
.BI -v
حالت پرگو (verbose)، افزودن جزئیات بیشتر، و تولید نکات
و هشدارهای بیشتر دربارهٔ مدل..SH "همچنین ببینید (SEE ALSO)"
راهنماهای برخط در spinroot.com:
.br
.in +4
http://spinroot.com/spin/Man/3_SpinGUI.html
.br
http://spinroot.com/spin/Man/4_SpinVerification.html
.br
http://spinroot.com/spin/Man/1_Exercises.html
.in -4
اطلاعات زمینه‌ای بیشتر دربارهٔ سامانه و فرایند وارسی را می‌توان برای نمونه در مآخذ زیر یافت:
.br
.in +4
.br
G.J. Holzmann, \f2The Spin Model Checker \(um Primer and Reference Manual\f1,
Addison-Wesley, Reading, Mass., 2004.
.br
--, `The model checker \*Z,'
\f2IEEE Trans. on SE\f1, Vol, 23, No. 5, May 1997.
.br
--, `Design and validation of protocols: a tutorial,'
\f2Computer Networks and ISDN Systems\f1,
Vol. 25, No. 9, 1993, pp. 981-1017.
.br
--, \f2Design and Validation of Computer Protocols\f1,
Prentice Hall, Englewood Cliffs, NJ, 1991.
.in -4
.br