توسط نرم افزار

توسط نرم افزار

توسط نرم افزار

به این ترتیب برای بررسی خصوصیت، در ابتدا سعی می کنیم با بررسی ویژگی های ساختاری شبکه مورد نظر، آن را در یکی از این زیر مجموعه ها طبقه بندی کنیم و سپس با استفاده از قضایای آن زیر مجموعه خصوصیات مذکور از جمله Liveness را راحت تر بر روی آن بررسی نمائیم.
با دقت بیشتر خواهیم فهمید که مدل شکل 4.7 یک state machine است زیرا هریک از گزارها در این شبکه تنها یک ورودی و یک خروجی دارند. عضویت این مدل در دیگر زیرمجموعه های شبکه های پتری در شکل 4.8 آمده است. این طبقه بندی توسط نرم افزار PIPE انجام شده است.
شکل 4.8. عضویت شبکه 4.7 در زیرکلاس های شبکه های پتری
پس با تکیه بر قضیه 4 از فصل 2، با توجه به اینکه در وضعیت M0 یک توکن در شبکه وجود دارد، اگر این شبکه متصل قوی باشد بنابراین live نیز هست.
همچنین با مقایسه قضیه 1 و بسط آن در همان فصل می توان نتیجه گرفت که شرط لازم برای متصل قوی بودن یک شبکه، عدم وجود موقعیت source و sink و نیز گزار source و sink در شبکه است. در چنین شرایطی شبکه 4.7 متصل قوی نمی باشد زیرا P11 در آن یک موقعیت sink محسوب می شود.
در نتیجه بر اساس قضیه 4، این شبکه خصوصیت Liveness را ندارد. این امر به این دلیل است که در صورت بروز اختلال در دریافت منابع کافی برای راه اندازی سیستم ثانویه، پروسه HA دچار مشکل خواهد شد. با توجه به این مشکل، مدل متناظر، خاصیت Liveness را از دست می دهد.
4.3.3.2. Safeness
در این مرحله با بررسی قضیه 2 در همان بخش می توانیم خاصیت safeness را در مدل بررسی نمائیم. برای این کار لازم است گراف پوشای مدل را به دست آوریم. با استفاده از نرم افزار PIPE این گراف به صورت شکل 4.9 خواهد بود.
شکل 4.9. گراف پوشای مدل 4.7
با بررسی این گراف در میابیم که برچسب همه گره های آن حاوی مقادیر 0 و 1 برای موقعیت های P0 تا P10 هستند. به این معنی که تعداد توکن های موجود در این موقعیت ها، در هیچ وضعیتی بیش از 1 نبوده است. با این دلیل، مدل همواره 1-bounded یا به عبارت دیگر safe می باشد.
با مقایسه نتیجه حاصل از این دو قضیه می توان فهمید که مدل به دلیل وجود بن بست، دارای خاصیت liveness نیست. به کمک نرم افزار تحلیلگر PIPE می توان مسیری را که مدل طی آن دچار بن بست می شود مشخص کرد. (شکل 4.10)
شکل 4.10. نتیجه تحلیل فضای حالت بر روی مدل
طبق این تحلیل، با طی دنباله گزارهای T0، T11، T12 و T13 سیستم دچار بن بست خواهد شد.
4.3.3.3. Reversibility
برای بررسی این خصوصیت لازم است به تعریف Reversibility توجه کنیم. با یاد آوری تعریف این مفهوم و نیز خاصیت Reachability از فصل 2 داریم: شبکه پتری ()، Reversible خوانده می شود اگر برای هر وضعیت M، در دنباله قابل اجرا از (R())، از طریق M، reachable باشد.
با این تعریف، در شبکه های کوچک می توان با بررسی کلیه وضعیت های محتمل در شبکه، reachable بودن را از طریق آنها بررسی نمود. در صورتی که از طریق تک تک این وضعیت ها ( تا ) قابل دسترسی باشد این شبکه Reversible است. با توجه به اینکه این وضعیت ها تماما در گراف پوشای مدل منعکس می شوند می توان با بررسی یک به یک گره های گراف این حالات را بررسی نمود.
به همین منظور و با بررسی گراف شکل 4.9، در می یابیم که کلیه وضعیت ها غیر از S8 می توانند کنترل سیستم را به S0 () بازگردانند. نحوه توزیع توکن در S8 در شکل 4.11 آمده است.
شکل 4.11. نحوه توزیع توکن در وضعیت S8
لازم به ذکر است که مفهوم S (State) در نرم افزار مدل سازی PIPE، متناظر با مفهوم M (Marking) یا همان “وضعیت” است که قبلا درمورد آن توضیح داده شده است.

 

مدیر

داغ ترین ها

No description. Please update your profile.

~~||~~Comments Are Closed~~||~~