tag:blogger.com,1999:blog-33088885322269617922024-02-08T04:40:11.147-08:00MTECH TEXT BOOKS, QUESTION PAPERS, LAB PROGRAMS,IEEE PAPERSHere you can find latest IEEE papers and M.Tech (CSE) Materials for download.Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.comBlogger16125tag:blogger.com,1999:blog-3308888532226961792.post-37341865898609534072012-07-10T09:41:00.005-07:002012-07-10T09:49:02.984-07:00<div dir="ltr" style="text-align: left;" trbidi="on">
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!172&parid=ECF891E08C3692F5!101&authkey=!APmkrGGwGhXcZDU"><b>COMPUTER GRAPHICS PROJECTS</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!260&authkey=!AJPw-NSEgZTjUNE"><b>Mobile communication 7th sem CSE Text Books</b></a>
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com0tag:blogger.com,1999:blog-3308888532226961792.post-19950868580518175152012-04-08T11:07:00.000-07:002012-06-09T09:24:39.787-07:00<div dir="ltr" style="text-align: left;" trbidi="on">
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!249&authkey=!AEpMnhyY3MFR_z4"> <b>TUGZIP35.exe(Zip and Unzip Software)</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!246&authkey=!ADZ-vci3t4v32CY"> <b>IDM CRACK</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!250&authkey=!AAQR97pp4D89lh0"> <b>INS CHAPTER WISE SLIDES</b></a>
<br />
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!175&parid=ECF891E08C3692F5!101&authkey=!AEAelnASvfUzNZU"><b>FMCS NEW LAB PROGRAMS AND CHAPTER WISE SLIDES</b></a>
<br />
<b><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!170&parid=ECF891E08C3692F5!101&authkey=!AGmf8l8bHEx0Ecs">MTech 2nd SEM ADA LAB PROGRAMS</a>(</b><b><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!170&parid=ECF891E08C3692F5!101&authkey=!AGmf8l8bHEx0Ecs"> c#.NET</a>)</b><br />
<b><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!171&parid=ECF891E08C3692F5!101&authkey=!AAEz7cQVrod6yxQ">MTech 2nd SEM ADA LAB PROGRAMS</a>(</b><b><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!171&parid=ECF891E08C3692F5!101&authkey=!AAEz7cQVrod6yxQ">C</a> PROGRAMS)</b>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!186&authkey=!AGiFQVmrtllgu6k"><b>FMCS NOTES MTECH(CS)</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!190&authkey=!ANldtHQrrjlDziM"><b>FMCS CHAPTER WISE SLIDES MTECH(CS)</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!206&authkey=!AHEZgCiwbaRPSy8"><b>DIP NOTES MTECH(CS)</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!219&authkey=!ADvfpB30x-JrTAA"> <b>MTECH(CS)ALL COLLEGE QUESTION INTERNAL QUESTION PAPERS</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!223&authkey=!AASbFLWo9ETwkvo"> <b>COMPUTER GRAPHICS NOTES MTECH(CS)</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!206&authkey=!ALvO4p2Cw29sUIc"> <b>VLSI MATERIALS,NOTES MTECH</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!244&authkey=!AChAUg6NapOP528"> <b>MTECH CSE ALL SEM SYLLABUS COPY</b></a>
<br />
<a href="https://skydrive.live.com/redir?resid=ECF891E08C3692F5!245&authkey=!AG2e04XOCl6ET1k"> <b>OS LAB PROGRAMS</b></a>
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com4tag:blogger.com,1999:blog-3308888532226961792.post-90455588129343272542012-04-05T07:19:00.001-07:002012-04-05T07:19:45.188-07:00<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!172&parid=ECF891E08C3692F5!101&authkey=!APmkrGGwGhXcZDU"><b>CG 6th SEM ENGG PROJECTS</b></a>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com3tag:blogger.com,1999:blog-3308888532226961792.post-46282296004375783932012-03-20T05:38:00.000-07:002012-07-10T09:39:26.484-07:00M.Tech CSE TEXT BOOKS<div dir="ltr" style="text-align: left;" trbidi="on">
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!163&parid=ECF891E08C3692F5!101&authkey=!AG6v2ZH6rrohiR8"></a><br />
<br />
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!164&parid=ECF891E08C3692F5!101&authkey=!AFwyPmkmBIFowg4"></a><br />
<br />
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!165&parid=ECF891E08C3692F5!101&authkey=!AM36lbhn2k0qybA"></a><br />
<h3>
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!163&parid=ECF891E08C3692F5!101&authkey=!AG6v2ZH6rrohiR8"><b>M.Tech First sem CSE Text Books</b></a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!164&parid=ECF891E08C3692F5!101&authkey=!AFwyPmkmBIFowg4"><b>M.Tech Second sem CSE Text Books</b></a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!165&parid=ECF891E08C3692F5!101&authkey=!AM36lbhn2k0qybA"><b>M.Tech Third sem CSE Text Books</b></a></li>
</ul>
</h3>
<input name="google" type="hidden" value="facebook" />
<input name="google" type="hidden" value="google news" />
<input name="Language" type="hidden" value="IPL" />
<input name="Language" type="hidden" value="signin" />
<input name="Language" type="hidden" value="sports" />
<input name="Language" type="hidden" value="gmail" />
<input name="Language" type="hidden" value="yahoo"" />
<input name="Language" type="hidden" value="cricket" />
<input name="Language" type="hidden" value="mtech" />
<input name="Language" type="hidden" value="football" />
<input name="Language" type="hidden" value="games" />
<input name="Language" type="hidden" value="picture" />
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com105tag:blogger.com,1999:blog-3308888532226961792.post-3027110311508153722012-03-18T10:30:00.003-07:002012-03-20T05:57:19.003-07:00POST GRADUATION DETAILS<div dir="ltr" style="text-align: left;" trbidi="on">
<a href="http://kea.kar.nic.in/pgcet.htm"><b></b></a><br />
<h3>
<ul>
<li><b><a href="http://kea.kar.nic.in/pgcet.htm">PG DETAILS CLICK ME!!</a></b></li>
<li><a href="http://vtu.ac.in/"><b>VTU Website</b></a></li>
</ul>
</h3>
<a href="http://vtu.ac.in/"><b></b></a></div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com1tag:blogger.com,1999:blog-3308888532226961792.post-9895796498338649742012-03-18T10:10:00.000-07:002012-03-20T05:41:35.557-07:00<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!151&parid=ECF891E08C3692F5!101&authkey=!ALuQsFfHpwmkl4A"><b><H3>PG CET 2010 PAPER</H3></b></a>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com2tag:blogger.com,1999:blog-3308888532226961792.post-67188570692091693692012-03-18T04:57:00.000-07:002012-03-20T05:54:59.750-07:00VLSI TEXT BOOX<div dir="ltr" style="text-align: left;" trbidi="on">
<br />
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!125&parid=ECF891E08C3692F5!101&authkey=!AAL-HEjUyc05QSY">VLSI</a></li>
</ul>
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com4tag:blogger.com,1999:blog-3308888532226961792.post-17856628107385248792012-03-18T04:55:00.001-07:002012-03-20T05:55:31.369-07:00APTITUDE MATERIALS<div dir="ltr" style="text-align: left;" trbidi="on">
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!127&parid=ECF891E08C3692F5!101&authkey=!AGm6DTk6kcmvQb8"><b></b></a><br />
<h3>
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!127&parid=ECF891E08C3692F5!101&authkey=!AGm6DTk6kcmvQb8"><b>APTITUDE MATERIALS</b></a></li>
</ul>
</h3>
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!127&parid=ECF891E08C3692F5!101&authkey=!AGm6DTk6kcmvQb8"><b>
</b></a></div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com0tag:blogger.com,1999:blog-3308888532226961792.post-84443572591600024242012-03-17T22:30:00.002-07:002012-03-20T05:48:03.543-07:00IEEE PAPERS<div dir="ltr" style="text-align: left;" trbidi="on">
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!121&parid=ECF891E08C3692F5!104&authkey=!AOZHXWFk_raoslI"></a><br />
<h3>
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!121&parid=ECF891E08C3692F5!104&authkey=!AOZHXWFk_raoslI">CLOUD COMPUTING</a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!120&parid=ECF891E08C3692F5!104&authkey=!AA21Htr3YZgieUc">DATA MINING</a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!123&parid=ECF891E08C3692F5!104&authkey=!ANV7uzeHbpeJwgg">IMAGE PROCESSING</a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!124&parid=ECF891E08C3692F5!104&authkey=!AFKJZo_qSHRLuB8">NETWORKS</a></li>
</ul>
</h3>
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!120&parid=ECF891E08C3692F5!104&authkey=!AA21Htr3YZgieUc"></a><br />
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!123&parid=ECF891E08C3692F5!104&authkey=!ANV7uzeHbpeJwgg"></a><br />
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!124&parid=ECF891E08C3692F5!104&authkey=!AFKJZo_qSHRLuB8"></a></div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com4tag:blogger.com,1999:blog-3308888532226961792.post-62929346927674951012012-03-17T21:35:00.001-07:002012-03-20T05:57:58.955-07:00ACA and OTHER MATERIALS<div dir="ltr" style="text-align: left;" trbidi="on">
<br />
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!115&parid=ECF891E08C3692F5!104&authkey=!ABv2M5DKjn9S3mw">ACA</a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!117&parid=ECF891E08C3692F5!104&authkey=!AF23cr4l2Oxgo8c">Second Sem Question Paper</a></li>
</ul>
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com1tag:blogger.com,1999:blog-3308888532226961792.post-31174636809930472062012-03-17T21:34:00.001-07:002012-03-20T05:46:21.081-07:00MULTIMEDIA<div dir="ltr" style="text-align: left;" trbidi="on">
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!111&parid=ECF891E08C3692F5!104&authkey=!AKme_7H8HO1i5Kc"></a><br />
<h3>
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!111&parid=ECF891E08C3692F5!104&authkey=!AKme_7H8HO1i5Kc">MULTIMEDIA</a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!113&parid=ECF891E08C3692F5!104&authkey=!AI3Xg11GbhbiU7U">MULTIMEDIA QUESTION PAPER</a></li>
</ul>
</h3>
<br />
<a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!113&parid=ECF891E08C3692F5!104&authkey=!AI3Xg11GbhbiU7U"></a><br />
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com0tag:blogger.com,1999:blog-3308888532226961792.post-31563799702143414942012-03-17T21:33:00.000-07:002012-03-20T05:50:23.377-07:00INS and SAN<div dir="ltr" style="text-align: left;" trbidi="on">
<br />
<br />
<br />
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!167&parid=ECF891E08C3692F5!101&authkey=!AHl0Y3jGD2uMkEE"><b>INS</b></a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!166&parid=ECF891E08C3692F5!101&authkey=!ALRQaqBJZhRYCng"><b>SAN</b></a></li>
</ul>
<br />
<br /></div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com3tag:blogger.com,1999:blog-3308888532226961792.post-83693286614111748572012-03-17T21:30:00.001-07:002012-03-20T06:13:22.628-07:00Formal Model Computer Science<div dir="ltr" style="text-align: left;" trbidi="on">
<br />
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!106&parid=ECF891E08C3692F5!104&authkey=!AKV0HxK-KLwWZ0Q"><b>FMCS</b></a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!114&parid=ECF891E08C3692F5!104&authkey=!AEn9Ci07Tt4Xo4E"><b>FMCS</b></a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!109&parid=ECF891E08C3692F5!104&authkey=!APhtKy7MrMQEE1c"><b>FMCS</b></a></li>
</ul>
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com1tag:blogger.com,1999:blog-3308888532226961792.post-30791359547868160272012-03-17T21:28:00.000-07:002012-03-20T05:54:19.704-07:00Advance Algorithm Question paper(MTech 2nd sem)<div dir="ltr" style="text-align: left;" trbidi="on">
<br />
<ul style="text-align: left;">
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!105&parid=ECF891E08C3692F5!104&authkey=!AChKg8JDQrC7Rlc">ADA</a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!107&parid=ECF891E08C3692F5!104&authkey=!APXwwFXQYaP1R9E">ADA PPT</a></li>
<li><a href="https://skydrive.live.com/redir.aspx?cid=ecf891e08c3692f5&resid=ECF891E08C3692F5!108&parid=ECF891E08C3692F5!104&authkey=!ANyQteB9W5qOnHA">ALGORITHM SOLUTION MANUAL</a></li>
</ul>
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com3tag:blogger.com,1999:blog-3308888532226961792.post-2400145330212393932012-03-17T04:14:00.000-07:002012-03-17T04:14:25.957-07:00MTech Computer Science and Engg Formal Model in computer science programs<div dir="ltr" style="text-align: left;" trbidi="on">
Hi,<br />
<br />
<div align="center" class="MsoNormal" style="text-align: center;">
<b><u><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 14pt;">Software Requirements:<o:p></o:p></span></u></b></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 14pt;">1 .NuSMV<o:p></o:p></span></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 14pt;">2. Alloy<o:p></o:p></span></div>
<div class="MsoNormal">
<br /></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<b><u><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Installing and using NuSMV (under
Windows)<o:p></o:p></span></u></b></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">1. Go to the
address below and chose an installation file according to your system version:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN"><a href="http://nusmv.fbk.eu/bin/bin_download2-v2.cgi"><span style="font-family: 'Times New Roman', serif; font-size: 12pt;">http://nusmv.fbk.eu/bin/bin_download2-v2.cgi</span></a></span><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"><o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">For instance,
for a system running windows vista on a 32 machine you can paste this in your
web browser:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN"><a href="http://nusmv.fbk.eu/distrib/NuSMV-2.5.2-i586-pc-mingw32msvc.exe"><span style="font-family: 'Times New Roman', serif; font-size: 12pt;">http://nusmv.fbk.eu/distrib/NuSMV-2.5.2-i586-pc-mingw32msvc.exe</span></a></span><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"><o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">2. Open the
download directory and run the executable (by double-clicking on the file, for
instance). Do the following during the installation wizard:<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">a. click
'Proceed',<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">b.
click 'Next'<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">c. choose
a location, for instance: Browse ! Desktop, (the default installation directory is 'C/Program Files/NuSMV') and
click 'Install'<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">3. Open a
command prompt (for instance by: Start ! All Programs !Accessories ! Command
Prompt)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">4. Go to your
installation place (by writing at command prompt:) <o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">cd
\Desktop\nusmv\2.5.2\bin<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">5. Open your
favorite text editor (by writing, for instance): notepad tictactoe.smv<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">6. Write and
save your program (below you have a basic program template):<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">MODULE
main<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
: boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">init(variable)
:= TRUE;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">next(variable)
:= !variable;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">LTLSPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">G
(variable & X !variable)<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">CTLSPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">EF
(!variable & AX variable)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">7. Run your
program to check the assertions from the specifications section,<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">by writing the
following at the command prompt:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">NuSMV.exe
tictactoe.smv<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">8. This will
produce the following output:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">--
specification EF (!variable & AX variable) is true<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">--
specification G (variable & X !variable) is false<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">-- as
demonstrated by the following execution sequence<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Trace
Description: LTL Counterexample<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Trace
Type: Counterexample<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">--
Loop starts here<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">->
State: 1.1 <-<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
= TRUE<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">->
State: 1.2 <-<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
= FALSE<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">->
State: 1.3 <-<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
= TRUE<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">9. Include the
program code in your (.tex) assignment file and you are done.<o:p></o:p></span></div>
<div class="MsoNormal">
<br /></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<b><u><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Installing and using ALLOY (under
Windows)<o:p></o:p></span></u></b></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">1. Download and
Install Java Developer Kit 6 (JDK 6).<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">2. Now download the
alloy4.jar file (available at alloy.mit.edu) then double-click on the jar file,
or type: <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: 0.0001pt;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"> java -jar
alloy4.jar in the console. <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: 0.0001pt;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">------------------------------------------------------------------------------------------------------------</span><b style="line-height: 150%; text-align: justify;"><span lang="EN-IN">1. Design,
develop and run a program in ALLOY (or in any equivalent system) to model a
Software Package Dependency System. Make suitable assumptions regarding the
system. The model should allow checking to see if prerequisites in the form of
libraries or other packages are present for all components in the system.</span></b></div>
<div class="MsoNormal" style="text-align: justify;">
<br /></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">module
PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">open
std/ord -- opens specification template for linear order<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">sig
Component <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">name: Name,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">main: option
Service,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">export: set
Service,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">import: set
Service,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">version: Number<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{ <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">no import &
export <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">sig
PDS <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">components: set
Component,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">schedule:
components -> Service ->? components,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">requires:
components -> components<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{ <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">components.import
in components.export<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">fact
SoundPDSs <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">all P : PDS | with
P<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">all c :
components, s : Service | let c’ = c.schedule[s] <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">(some c’ iff s
in c.import) && (some c’ => s in c’.export) <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">all c :
components | c.requires = c.schedule[Service] <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">sig
Name, Number, Service {}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">fun AddComponent(P, P’: PDS, c:
Component) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">not c in
P.components<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">P’.components =
P.components + c<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">} <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">run AddComponent for 3 but 2 PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">fun RemoveComponent(P, P’: PDS, c :
Component) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">c in
P.components<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">P’.components =
P.components - c<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">run RemoveComponent for 3 but 2 PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">fun HighestVersionPolicy(P: PDS) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">with P <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">all s : Service, c : components, c’ :
c.schedule[s],<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">c’’ : components - c’ <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">s in c’’.export
&& c’’.name = c’.name =><o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">c’’.version in
c’.version.^(Ord[Number].prev)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">} <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"> run HighestVersionPolicy for 3 but 1 PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">fun AGuidedSimulation(P,P’,P’’ : PDS,
c1, c2 : Component) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">AddComponent(P,P’,c1)
RemoveComponent(P,P’’,c2)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">HighestVersionPolicy(P)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">HighestVersionPolicy(P’)
<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">HighestVersionPolicy(P’’)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"> run AGuidedSimulation for 3<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">assert AddingIsFunctionalForPDSs <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">all P, P’, P’’:
PDS, c: Component <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">AddComponent(P,P’,c)
&&<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">AddComponent(P,P’’,c)
=> P’ = P’’<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">} <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">check
AddingIsFunctionalForPDSs for 3<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: 0.0001pt;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"><br /></span></div>
<div class="MsoNormal" style="margin-bottom: 0.0001pt;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">------------------------------------------------------------------------------------------------------------</span></div>
<div class="MsoNormal" style="margin-bottom: 0.0001pt;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"></span></div>
<div class="Default" style="line-height: 150%; text-align: justify; text-justify: inter-ideograph;">
<b><span lang="EN-IN">2. Design,
develop and run a program in NuSMV (or in any equivalent system) to model and
solve the Mutual Exclusion problem. <o:p></o:p></span></b></div>
<div class="Default" style="line-height: 150%; text-align: justify; text-justify: inter-ideograph;">
<br /></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE main<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">pr1: process prc(pr2.st, turn, 0);<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">pr2: process prc(pr1.st, turn, 1);<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">turn:
boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(turn)
:= 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- safety<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G!((pr1.st = c) &
(pr2.st = c))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- liveness<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G((pr1.st = t) -> F
(pr1.st = c))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G((pr2.st = t) -> F
(pr2.st = c))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- ‘negation’ of strict sequencing
(desired to be false)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G(pr1.st=c -> ( G
pr1.st=c | (pr1.st=c U<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(!pr1.st=c
& G !pr1.st=c | ((!pr1.st=c) U pr2.st=c)))))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<br /></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE prc(other-st, turn, myturn)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st: <i>{</i>n, t, c<i>}</i>;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(st) := n;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(st) :=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.0in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = n) : <i>{</i>t,n<i>}</i>;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = t) & (other-st = n) : c;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = t) & (other-st = t) &
(turn = myturn) : c;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = c) : <i>{</i>c,n<i>}</i>;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : st;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.0in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(turn) :=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.0in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">turn = myturn & st = c : !turn;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : turn;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">FAIRNESS running<o:p></o:p></span></div>
<div class="Default" style="line-height: 115%; text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN">FAIRNESS !(st = c)<b><o:p></o:p></b></span></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt;"><o:p> -----------------------------------------------------------------------------------------------------------</o:p></span></div>
<br />
<div class="MsoNormal" style="margin-bottom: 0.0001pt;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"></span></div>
<div class="MsoNormal" style="line-height: 150%; text-align: justify; text-justify: inter-ideograph;">
<b><span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">3.
Design, develop and run a program in NuSMV (or in any equivalent system) to
model and simulate the Alterate Bit Protocol.<o:p></o:p></span></b></div>
<div class="MsoNormal" style="line-height: 150%; text-align: justify; text-justify: inter-ideograph;">
<u><span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">The ABP sender in SMV:<o:p></o:p></span></u></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE
sender (ack)<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st : {sending,sent};<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">message1 : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">message2 : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(st) :=
sending;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(st) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ack = message2 &
!(st=sent) : sent;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :
sending;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(message1)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = sent : {0,1};<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : message1;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(message2)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = sent : !message2;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : message2;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">FAIRNESS
running<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC
G F st=sent<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; text-align: justify; text-justify: inter-ideograph;">
<br /></div>
<div class="MsoNormal" style="line-height: 150%; text-align: justify; text-justify: inter-ideograph;">
<u><span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">The ABP receiver in SMV:<o:p></o:p></span></u></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE
receiver (message1,message2)<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st : {receiving,received};<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ack : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">expected :
boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(st) := receiving;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(st) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">message2=expected &
!(st=received) : received;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : receiving;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(ack)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = received : message2;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : ack;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(expected)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = received : !expected;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.0in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : expected;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-align: justify; text-indent: .5in; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">FAIRNESS
running<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC
G F st=received<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">------------------------------------------------------------------------------------------------------------</span></div>
<div class="MsoNormal" style="text-align: justify; text-justify: inter-ideograph;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;"></span></div>
<div class="Default" style="line-height: 150%; margin-bottom: 0.95pt;">
<b><span lang="EN-IN">4. Design, develop and run a program in NuSMV (or in any equivalent
system) to model and solve the planning problem of Ferry Man. <o:p></o:p></span></b></div>
<div class="MsoNormal" style="line-height: normal;">
<br /></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE main<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Ferryman : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Goat : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Cabbage : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Wolf : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Carry : {g,c,w,0};<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(ferryman)
:= 0; init(goat) := 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(cabbage)
:= 0; init(wolf) := 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(carry)
:= 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<br /></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(ferryman)
:= 0,1;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<br /></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(carry)
:= case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=goat
: g;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac
union<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=cabbage : c;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac
union<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=wolf
: w;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac
union 0;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(goat) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=goat
& next(carry)=g :
next(ferryman);<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1
:goat;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(cabbage) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=cabbage
& next(carry)=c : next(ferryman);<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1
:cabbage;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(wolf) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=wolf
& next(carry)=w : next(ferryman);<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1
:wolf;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<b><span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Output:</span></b><span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">
<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC !(( (goat=cabbage | goat=wolf) ->
goat=ferryman)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">U
(cabbage & goat & wolf & ferryman))<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">acws-0116% nusmv ferryman.smv<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** This is NuSMV 2.1.2 (compiled
2002-11-22 12:00:00)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** For more information of NuSMV see
<http://nusmv.irst.itc.it><o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** or email to
<nusmv-users@irst.itc.it>.<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** Please report bugs to
<nusmv-users@irst.itc.it>.<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- specification !(((goat = cabbage |
goat = wolf) -> goat = ferryman)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">U (((cabbage & goat) & wolf)
& ferryman)) is false<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- as demonstrated by the following
execution sequence<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- loop starts here --<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.1 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0 -> State 1.8
<-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">goat = 0 ferryman = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">cabbage = 0 goat = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">wolf = 0 carry = g<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = 0 -> State 1.9 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.2 <- ->
State 1.10 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 1 ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">goat = 1 cabbage = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = g carry = c<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.3 <- ->
State 1.11 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0 ferryman = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = 0 carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.4 <- ->
State 1.12 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 1 ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">cabbage = 1 wolf = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = c carry = w<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.5 <- -> State
1.13 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0 ferryman = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">goat = 0 carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = g ->State 1.14 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.6 <- ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 1 goat = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">wolf = 1 carry
= g<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = w -> State 1.15 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.7 <- carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">------------------------------------------------------------------------------------------------------------</span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;"></span></div>
<div class="Default" style="line-height: 150%;">
<b><span lang="EN-IN">5.
Design, develop and run a program in NuSMV (or in any equivalent system) to
model and solve the Dining Philosophers Problem. <o:p></o:p></span></b></div>
<div class="MsoNormal" style="line-height: normal;">
<br /></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">MODULE main<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> forks
: array 0..4 of {nobody,0,1,2,3,4}; <o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p0
: process philosopher(0,forks[0],forks[1]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p1
: process philosopher(1,forks[1],forks[2]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p2
: process philosopher(2,forks[2],forks[3]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p3
: process philosopher(3,forks[3],forks[4]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p4
: process philosopher(4,forks[4],forks[0]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[0])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[1])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[2])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[3])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[4])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<br /></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">MODULE philosopher(i,left,right)<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> state
: {thinking, hungry, eating, done};<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> --
done state is used to drop the forks properly<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">DEFINE<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> gotleft
:= (left=i);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> gotright
:= (right=i);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> leftfree
:= (left=nobody);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> rightfree
:= (right=nobody);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(state)
:= thinking;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> next(left)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> case<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state
= done) : nobody; -- drop fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> !leftfree
: left; -- can't grab if not free<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> leftfree
& (state=hungry) : i; -- grab fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> 1
: left;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> next(right)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> case<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state
= done) : nobody; -- drop fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> !gotleft
: right; -- grab left one first<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> !rightfree
: right; -- can't grab if not free<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> rightfree
& (state=hungry) : i; -- grab fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> 1
: right;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> next(state)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> case<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=thinking)
: {thinking, hungry};<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=hungry)
& gotleft & gotright : eating;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=hungry)
: hungry; -- don't have forks<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=eating)
: {eating, done};<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=done)
: thinking;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> 1
: state;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">FAIRNESS<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> running<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">SPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> --
must have both forks to eat<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> AG
((state = eating) -> (gotleft)&(gotright))<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">SPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> --
if hungry, must eventually get to eat<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> AG
((state = hungry) -> AF (state = eating))<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: normal;">
<br /></div>
<div class="MsoNormal" style="line-height: normal;">
<span lang="EN-IN"><o:p> -----------------------------------------------------------------------------------------------------------</o:p></span></div>
<div class="MsoNormal" style="line-height: normal;">
<span lang="EN-IN"><o:p><br /></o:p></span></div>
<br />
<br />
<br />
<div class="MsoNormal">
<br /></div>
</div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com3tag:blogger.com,1999:blog-3308888532226961792.post-70620889921688203552012-03-17T04:11:00.005-07:002012-03-17T04:19:37.913-07:00<div dir="ltr" style="text-align: left;" trbidi="on">
Hi,<br />
<br />
<div align="center" class="MsoNormal" style="text-align: center;">
<b><u><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 14pt;">Software Requirements:<o:p></o:p></span></u></b></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 14pt;">1 .NuSMV<o:p></o:p></span></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 14pt;">2. Alloy<o:p></o:p></span></div>
<div class="MsoNormal">
<br /></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<b><u><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Installing and using NuSMV (under
Windows)<o:p></o:p></span></u></b></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">1. Go to the
address below and chose an installation file according to your system version:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN"><a href="http://nusmv.fbk.eu/bin/bin_download2-v2.cgi"><span style="font-family: 'Times New Roman', serif; font-size: 12pt;">http://nusmv.fbk.eu/bin/bin_download2-v2.cgi</span></a></span><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"><o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">For instance,
for a system running windows vista on a 32 machine you can paste this in your
web browser:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN"><a href="http://nusmv.fbk.eu/distrib/NuSMV-2.5.2-i586-pc-mingw32msvc.exe"><span style="font-family: 'Times New Roman', serif; font-size: 12pt;">http://nusmv.fbk.eu/distrib/NuSMV-2.5.2-i586-pc-mingw32msvc.exe</span></a></span><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"><o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">2. Open the
download directory and run the executable (by double-clicking on the file, for
instance). Do the following during the installation wizard:<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">a. click
'Proceed',<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">b.
click 'Next'<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">c. choose
a location, for instance: Browse ! Desktop, (the default installation directory is 'C/Program Files/NuSMV') and
click 'Install'<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">3. Open a
command prompt (for instance by: Start ! All Programs !Accessories ! Command
Prompt)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">4. Go to your
installation place (by writing at command prompt:) <o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">cd
\Desktop\nusmv\2.5.2\bin<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">5. Open your
favorite text editor (by writing, for instance): notepad tictactoe.smv<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">6. Write and
save your program (below you have a basic program template):<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">MODULE
main<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
: boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">init(variable)
:= TRUE;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">next(variable)
:= !variable;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">LTLSPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">G
(variable & X !variable)<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">CTLSPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">EF
(!variable & AX variable)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">7. Run your
program to check the assertions from the specifications section,<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">by writing the
following at the command prompt:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">NuSMV.exe
tictactoe.smv<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">8. This will
produce the following output:<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">--
specification EF (!variable & AX variable) is true<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">--
specification G (variable & X !variable) is false<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">-- as
demonstrated by the following execution sequence<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Trace
Description: LTL Counterexample<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Trace
Type: Counterexample<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">--
Loop starts here<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">->
State: 1.1 <-<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
= TRUE<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">->
State: 1.2 <-<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
= FALSE<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">->
State: 1.3 <-<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">variable
= TRUE<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">9. Include the
program code in your (.tex) assignment file and you are done.<o:p></o:p></span></div>
<div class="MsoNormal">
<br /></div>
<div align="center" class="MsoNormal" style="text-align: center;">
<b><u><span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">Installing and using ALLOY (under
Windows)<o:p></o:p></span></u></b></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">1. Download and
Install Java Developer Kit 6 (JDK 6).<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;">2. Now download the
alloy4.jar file (available at alloy.mit.edu) then double-click on the jar file,
or type: <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: 0.0001pt;">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"> java -jar
alloy4.jar in the console. <o:p></o:p></span></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"><o:p> -----------------------------------------------------------------------------------------------------------</o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-family: 'Times New Roman', serif; font-size: 12pt;"><o:p></o:p></span></div>
<div class="Default" style="line-height: 150%; text-align: justify; text-justify: inter-ideograph;">
<b><span lang="EN-IN">1. Design,
develop and run a program in ALLOY (or in any equivalent system) to model a
Software Package Dependency System. Make suitable assumptions regarding the
system. The model should allow checking to see if prerequisites in the form of
libraries or other packages are present for all components in the system.<o:p></o:p></span></b></div>
<div class="MsoNormal" style="text-align: justify;">
<br /></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-size: 12pt;">module
PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-size: 12pt;">open
std/ord -- opens specification template for linear order<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-size: 12pt;">sig
Component <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">name: Name,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">main: option
Service,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">export: set
Service,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">import: set
Service,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">version: Number<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{ <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">no import &
export <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-size: 12pt;">sig
PDS <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">components: set
Component,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">schedule:
components -> Service ->? components,<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">requires:
components -> components<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{ <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">components.import
in components.export<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-size: 12pt;">fact
SoundPDSs <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">all P : PDS | with
P<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">all c :
components, s : Service | let c’ = c.schedule[s] <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">(some c’ iff s
in c.import) && (some c’ => s in c’.export) <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">all c :
components | c.requires = c.schedule[Service] <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify;">
<span lang="EN-IN" style="font-size: 12pt;">sig
Name, Number, Service {}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">fun AddComponent(P, P’: PDS, c:
Component) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">not c in
P.components<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">P’.components =
P.components + c<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">} <o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">run AddComponent for 3 but 2 PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">fun RemoveComponent(P, P’: PDS, c :
Component) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">c in
P.components<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">P’.components =
P.components - c<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">run RemoveComponent for 3 but 2 PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">fun HighestVersionPolicy(P: PDS) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">with P <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">all s : Service, c : components, c’ :
c.schedule[s],<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">c’’ : components - c’ <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">s in c’’.export
&& c’’.name = c’.name =><o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">c’’.version in
c’.version.^(Ord[Number].prev)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">} <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;"> run HighestVersionPolicy for 3 but 1 PDS<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">fun AGuidedSimulation(P,P’,P’’ : PDS,
c1, c2 : Component) <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">AddComponent(P,P’,c1)
RemoveComponent(P,P’’,c2)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">HighestVersionPolicy(P)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">HighestVersionPolicy(P’)
<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">HighestVersionPolicy(P’’)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;"> run AGuidedSimulation for 3<o:p></o:p></span></div>
<div class="MsoNormal" style="text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">assert AddingIsFunctionalForPDSs <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">all P, P’, P’’:
PDS, c: Component <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">{<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">AddComponent(P,P’,c)
&&<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">AddComponent(P,P’’,c)
=> P’ = P’’<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">}<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">} <o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">check
AddingIsFunctionalForPDSs for 3</span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;">------------------------------------------------------------------------------------</span></div>
<div class="MsoNormal" style="margin-left: 1in; text-align: justify; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt;"></span></div>
<div class="Default" style="line-height: 150%;">
<b><span lang="EN-IN">2. Design,
develop and run a program in NuSMV (or in any equivalent system) to model and
solve the Mutual Exclusion problem. <o:p></o:p></span></b></div>
<div class="Default" style="line-height: 150%;">
<br /></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE main<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">pr1: process prc(pr2.st, turn, 0);<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">pr2: process prc(pr1.st, turn, 1);<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">turn:
boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(turn)
:= 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- safety<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G!((pr1.st = c) &
(pr2.st = c))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- liveness<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G((pr1.st = t) -> F
(pr1.st = c))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G((pr2.st = t) -> F
(pr2.st = c))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- ‘negation’ of strict sequencing
(desired to be false)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC G(pr1.st=c -> ( G
pr1.st=c | (pr1.st=c U<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(!pr1.st=c
& G !pr1.st=c | ((!pr1.st=c) U pr2.st=c)))))<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<br /></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE prc(other-st, turn, myturn)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st: <i>{</i>n, t, c<i>}</i>;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(st) := n;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(st) :=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.0in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = n) : <i>{</i>t,n<i>}</i>;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = t) & (other-st = n) : c;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = t) & (other-st = t) &
(turn = myturn) : c;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">(st = c) : <i>{</i>c,n<i>}</i>;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : st;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.0in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: .5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(turn) :=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.0in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">turn = myturn & st = c : !turn;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; margin-left: 1.5in; margin-right: 0in; margin-top: 0in; mso-layout-grid-align: none; text-autospace: none; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : turn;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-bottom: .0001pt; margin-bottom: 0in; mso-layout-grid-align: none; text-autospace: none;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">FAIRNESS running<o:p></o:p></span></div>
<div class="Default" style="line-height: 115%;">
<span lang="EN-IN">FAIRNESS !(st = c)<b><o:p></o:p></b></span></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
<br /></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt;"><o:p> -----------------------------------------------------------------------------------</o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt;"><o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%;">
<b><span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">3.
Design, develop and run a program in NuSMV (or in any equivalent system) to
model and simulate the Alterate Bit Protocol.<o:p></o:p></span></b></div>
<div class="MsoNormal" style="line-height: 150%;">
<u><span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">The ABP sender in SMV:<o:p></o:p></span></u></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE
sender (ack)<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st : {sending,sent};<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">message1 : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">message2 : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(st) :=
sending;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(st) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ack = message2 &
!(st=sent) : sent;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :
sending;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(message1)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = sent : {0,1};<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : message1;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(message2)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = sent : !message2;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : message2;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">FAIRNESS
running<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC
G F st=sent<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%;">
<br /></div>
<div class="MsoNormal" style="line-height: 150%;">
<u><span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">The ABP receiver in SMV:<o:p></o:p></span></u></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE
receiver (message1,message2)<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st : {receiving,received};<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ack : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">expected :
boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(st) := receiving;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(st) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">message2=expected &
!(st=received) : received;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : receiving;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(ack)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = received : message2;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : ack;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(expected)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">st = received : !expected;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 : expected;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 0.5in; text-indent: 0.5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">FAIRNESS
running<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC
G F st=received<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">------------------------------------------------------------------------------------</span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;"></span></div>
<div class="Default" style="line-height: 150%; margin-bottom: 0.95pt;">
<b><span lang="EN-IN">4. Design, develop and run a program in NuSMV (or in any equivalent
system) to model and solve the planning problem of Ferry Man. <o:p></o:p></span></b></div>
<div class="MsoNormal" style="line-height: normal;">
<br /></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">MODULE main<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Ferryman : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Goat : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Cabbage : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Wolf : boolean;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Carry : {g,c,w,0};<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(ferryman)
:= 0; init(goat) := 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(cabbage)
:= 0; init(wolf) := 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">init(carry)
:= 0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<br /></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(ferryman)
:= 0,1;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<br /></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(carry)
:= case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=goat
: g;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac
union<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=cabbage : c;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac
union<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">case<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=wolf
: w;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 2.0in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1 :0;<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: 1.5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac
union 0;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(goat) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=goat
& next(carry)=g :
next(ferryman);<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1
:goat;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(cabbage) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=cabbage
& next(carry)=c : next(ferryman);<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1
:cabbage;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">next(wolf) := case<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman=wolf
& next(carry)=w : next(ferryman);<o:p></o:p></span></div>
<div class="MsoNormal" style="text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">1
:wolf;<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">esac;<o:p></o:p></span></div>
<div class="MsoNormal">
<b><span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">Output:</span></b><span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">
<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">LTLSPEC !(( (goat=cabbage | goat=wolf) ->
goat=ferryman)<o:p></o:p></span></div>
<div class="MsoNormal" style="margin-left: .5in; text-indent: .5in;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">U
(cabbage & goat & wolf & ferryman))<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">acws-0116% nusmv ferryman.smv<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** This is NuSMV 2.1.2 (compiled
2002-11-22 12:00:00)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** For more information of NuSMV see
<http://nusmv.irst.itc.it><o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** or email to
<nusmv-users@irst.itc.it>.<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">*** Please report bugs to
<nusmv-users@irst.itc.it>.<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- specification !(((goat = cabbage |
goat = wolf) -> goat = ferryman)<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">U (((cabbage & goat) & wolf)
& ferryman)) is false<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- as demonstrated by the following
execution sequence<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-- loop starts here --<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.1 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0 -> State 1.8
<-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">goat = 0 ferryman = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">cabbage = 0 goat = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">wolf = 0 carry = g<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = 0 -> State 1.9 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.2 <- ->
State 1.10 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 1 ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">goat = 1 cabbage = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = g carry = c<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.3 <- ->
State 1.11 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0 ferryman = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = 0 carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.4 <- ->
State 1.12 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 1 ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">cabbage = 1 wolf = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = c carry = w<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.5 <- -> State
1.13 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0 ferryman = 1<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">goat = 0 carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = g ->State 1.14 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.6 <- ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 1 goat = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">wolf = 1 carry
= g<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = w -> State 1.15 <-<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">-> State 1.7 <- carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">ferryman = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">carry = 0<o:p></o:p></span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;">------------------------------------------------------------------------------------</span></div>
<div class="MsoNormal">
<span lang="EN-IN" style="font-size: 12pt; line-height: 115%;"></span></div>
<div class="Default" style="line-height: 150%;">
<b><span lang="EN-IN">5.
Design, develop and run a program in NuSMV (or in any equivalent system) to
model and solve the Dining Philosophers Problem. <o:p></o:p></span></b></div>
<div class="MsoNormal" style="line-height: normal;">
<br /></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">MODULE main<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> forks
: array 0..4 of {nobody,0,1,2,3,4}; <o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p0
: process philosopher(0,forks[0],forks[1]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p1
: process philosopher(1,forks[1],forks[2]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p2
: process philosopher(2,forks[2],forks[3]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p3
: process philosopher(3,forks[3],forks[4]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> p4
: process philosopher(4,forks[4],forks[0]);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[0])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[1])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[2])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[3])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(forks[4])
:= nobody;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<br /></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">MODULE philosopher(i,left,right)<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">VAR<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> state
: {thinking, hungry, eating, done};<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> --
done state is used to drop the forks properly<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">DEFINE<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> gotleft
:= (left=i);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> gotright
:= (right=i);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> leftfree
:= (left=nobody);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> rightfree
:= (right=nobody);<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">ASSIGN<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> init(state)
:= thinking;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> next(left)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> case<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state
= done) : nobody; -- drop fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> !leftfree
: left; -- can't grab if not free<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> leftfree
& (state=hungry) : i; -- grab fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> 1
: left;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> next(right)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> case<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state
= done) : nobody; -- drop fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> !gotleft
: right; -- grab left one first<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> !rightfree
: right; -- can't grab if not free<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> rightfree
& (state=hungry) : i; -- grab fork<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> 1
: right;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> next(state)
:=<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> case<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=thinking)
: {thinking, hungry};<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=hungry)
& gotleft & gotright : eating;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=hungry)
: hungry; -- don't have forks<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=eating)
: {eating, done};<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> (state=done)
: thinking;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> 1
: state;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> esac;<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">FAIRNESS<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> running<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">SPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> --
must have both forks to eat<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> AG
((state = eating) -> (gotleft)&(gotright))<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;">SPEC<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> --
if hungry, must eventually get to eat<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: 150%; margin-bottom: .0001pt; margin-bottom: 0in; tab-stops: 45.8pt 91.6pt 137.4pt 183.2pt 229.0pt 274.8pt 320.6pt 366.4pt 412.2pt 458.0pt 503.8pt 549.6pt 595.4pt 641.2pt 687.0pt 732.8pt;">
<span lang="EN-IN" style="font-size: 12pt; line-height: 150%;"> AG
((state = hungry) -> AF (state = eating))<o:p></o:p></span></div>
<div class="MsoNormal" style="line-height: normal;">
<br /></div>
<div class="MsoNormal" style="line-height: normal;">
<span lang="EN-IN"><o:p> -----------------------------------------------------------------------------------</o:p></span></div>
<div class="MsoNormal" style="line-height: normal;">
<span lang="EN-IN"><o:p> Thanks</o:p></span></div>
<br />
<br />
<br />
<br />
<br />
<br /></div>Anonymoushttp://www.blogger.com/profile/09707545036644546390noreply@blogger.com0