و با اجرای الگوریتم کزاراجو بر روی گراف خواهیم دید که کل گراف یک حوزه همبند قوی است. با این ترتیب می توان مطمئن بود که شبکه پتری متناظر با آن Reversible است. زیرا همیشه مسیری از هر Mi (Si) به M0 وجود دارد.
شکل ۴٫۳۲٫ جستجوی اول عمق گراف شکل ۴٫۳۱
۴٫۸٫۳٫۲٫ Liveness
همانطور که گفته شد شبکه پتری مربوط به این بخش (شکل ۴٫۳۰) دارای خواص هیچ یک از زیرکلاس های شبکه های پتری نیست. بنابراین برای بررسی liveness در شبکه مربوطه باید به قضایا و لم های کلاسیک در این حوزه رجوع کرد. برای این کار از لم ۱ در فصل ۲ استفاده می کنیم. به کمک این لم می توان بر روی گراف پوشای یک مدل پتری به طور کلی در مورد میزان liveness نظر داد. بر اساس این لم، در صورتی که یک گزار به صورت برچسب یک لبه در گراف پوشا ظاهر نگردد، این گزار dead است. با بررسی گراف پوشای مدل که در شکل ۴٫۳۱ آمده است، می بینیم که همه گزارها به صورت لبه ظاهر شده اند پس می توان نتیجه گرفت که گزار dead در مدل مذکور وجود ندارد.
دانلود پایان نامه - مقاله - پروژه
با این حال باید توجه داشت که این به معنی live بودن کل شبکه نیست چرا که ممکن است دنباله ای از گزارها وجود داشته باشد که با اجرای آن شبکه در وضعیت بن بست قرار گیرد. به عنوان مثال با وجود یک گزار sink، با اینکه خود گزار dead نیست، ولی با مصرف توکن، شبکه را از وجود توکن تهی کرده و دیگر امکان اجرای هیچ گزار وجود نخواهد داشت.
به همین دلیل، لازم است با بررسی تک تک گزارهای شبکه سطح liveness آنها را تشخیص داده و در نهایت با توجه به آن، میزان liveness کلی سیستم را مشخص نمود. در ادامه سطوح liveness گزارها را بررسی می کنیم.
با یادآوری مفهوم L(M0) از فصل ۲، در مدل پتری این بخش، الفبای زبان L تمام وضعیت های ممکن در مدل است که معادل M0 تا M15 در گراف پوشای مدل می باشد. همچنین L شامل تمام دنباله هایی است که Mها با اجرا کردن گزارهای شبکه می توانند ایجاد کنند. یعنی:
L(M0)= {M0 M1 M2 M3 M4 M6, M0 M1 M2 M3 M4 M3 M4 M6, … }
بنابراین می توان دنباله های نامتناهی از اجرای M ها ایجاد کرد که همگی عضو L باشند.
همچنین باید توجه داشت که قرار گرفتن سیستم در هر یک از وضعیت های M0 تا M15 باعث فعال شدن گزارها طبق جدول ۴٫۱ خواهد شد.
جدول ۴٫۱٫ گزارهای فعال در وضعیت های M0 الی M15 از مدل پتری ۴٫۳۰

 

M0 M1 M2 M3 M4 M5 M6 M7 M8 M9 M10 M11 M12 M13 M14 M15
T0 T1 T16 T17,
T18
T19,
T21
T2,
T20
T22 T3 T4 T5,
موضوعات: بدون موضوع  لینک ثابت


فرم در حال بارگذاری ...