{"id":27,"date":"2013-05-16T09:28:48","date_gmt":"2013-05-16T07:28:48","guid":{"rendered":"https:\/\/altarica.labri.fr\/wp\/?page_id=27"},"modified":"2013-08-27T12:12:00","modified_gmt":"2013-08-27T10:12:00","slug":"examples","status":"publish","type":"page","link":"https:\/\/altarica.labri.fr\/wp\/?page_id=27","title":{"rendered":"Examples"},"content":{"rendered":"<p>This page gathers examples illustrating usage of AltaRica language in modelling process and also the use of <a title=\"ARC\" href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=32\">ARC<\/a> tool to analyze these models.<\/p>\n\n<h1>Design of a lift<\/h1>\n<p>In this example the model of a lift system is described. The system must fulfil some safety or liveness properties. The documentation shows how the model is fixed to satisfy requirements.<\/p>\n<p>Download the <a href=\"\/docs\/lift.pdf\">PDF<\/a> file.<\/p>\n<h1>Proof of Peterson&#8217;s algorithm for Mutual Exclusion<\/h1>\n<p>This example studies the well-known algorithm proposed by G. L. Peterson to solve mutual exclusion of concurrent processes.<\/p>\n<p>Download the <a href=\"\/docs\/peterson.pdf\">PDF<\/a> file.<\/p>\n<h1>Controller synthesis: Winning strategy in the Nim game<\/h1>\n<p>Here we model a two-player game and show how one can compute a strategy to ensure the win of the game.<br \/>\nSuch winning strategies are the basics for the synthesis of controllers that guaranteed critical requirements.<\/p>\n<p>Download the <a href=\"\/docs\/nim.pdf\">PDF<\/a> file.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>This page gathers examples illustrating usage of AltaRica language in modelling process and also the use of ARC tool to analyze these models. Design of a lift In this example the model of a lift system is described. The system &hellip; <a href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=27\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":22,"menu_order":3,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-27","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/27","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=27"}],"version-history":[{"count":8,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/27\/revisions"}],"predecessor-version":[{"id":564,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/27\/revisions\/564"}],"up":[{"embeddable":true,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/22"}],"wp:attachment":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=27"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}