{"id":32,"date":"2013-05-16T09:30:53","date_gmt":"2013-05-16T07:30:53","guid":{"rendered":"https:\/\/altarica.labri.fr\/wp\/?page_id=32"},"modified":"2013-08-21T10:22:28","modified_gmt":"2013-08-21T08:22:28","slug":"arc","status":"publish","type":"page","link":"https:\/\/altarica.labri.fr\/wp\/?page_id=32","title":{"rendered":"ARC"},"content":{"rendered":"<p>ARC is the AltaRica Checker. Its main purpose is to offer model-checking algorithms to verify if an AltaRica model satisfies critical properties. Requirements are described as fixpoint equations or CTL* formulas. For the model-checking part, this tool is essentially an integration of functionalities of two older tools Acheck and <a title=\"PhD Thesis on MEC 5.\" href=\"http:\/\/tel.archives-ouvertes.fr\/tel-00007067\/fr\/\">MEC 5<\/a>.<\/p>\n<p>ARC is a command-line oriented tool that offers, beside model-cheking, many other kind of commands to analyse or translate AltaRica models. Main features implemented in ARC are listed below:<\/p>\n<ul>\n<li>Support of the AltaRica language with extension proposed during <a href=\"http:\/\/www.labri.fr\/perso\/herbrete\/persee\">ACI Persee<\/a>\n<ul>\n<li>support for compound types (arrays, structures)<\/li>\n<li>definition of abstract types and signatures of functions<\/li>\n<\/ul>\n<\/li>\n<li>Acheck specifications are supported using explicit or symbolic representation (however not all the set of commands are supported in both encoding)<\/li>\n<li>MEC 5\u00a0specifications with Decision Diagrams encoding. ARC extends the set of predefined sets with, for instance, <code>N!reach<\/code> that specifies the set of reachable configurations of the node N.<\/li>\n<li>ARC integrates an small graphical tool called <a title=\"AltaRica Studio\" href=\"http:\/\/altarica.labri.fr\/wp\/?page_id=286\">AltaRica Studio<\/a>.<\/li>\n<li>Large relations can be serialized in binary files for future use.<\/li>\n<li>Preprocessors can be specified using the configuration file of ARC<\/li>\n<li>CTL* logic is supported in Acheck specs or can be checked separately.<\/li>\n<\/ul>\n<h1>Downloading ARC<\/h1>\n<p>You will find instruction to get ARC tool on <a title=\"Downloads\" href=\"http:\/\/altarica.labri.fr\/wp\/?page_id=44\">Download<\/a> page.<\/p>\n<h1>Documentation<\/h1>\n<p>The ARC handbook distributed within source package but you can download a pre-compiled version <a title=\"FAQ\" href=\"http:\/\/altarica.labri.fr\/docs\/arc-handbook.pdf\">here<\/a>.<\/p>\n<h1>Support<\/h1>\n<p>Do not hesitate to <a title=\"Bug report\" href=\"http:\/\/altarica.labri.fr\/wp\/?page_id=37\">report bugs<\/a> or to send us <a title=\"New feature request\" href=\"http:\/\/altarica.labri.fr\/wp\/?page_id=40\">request for new features<\/a> using forms in Support pages.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>ARC is the AltaRica Checker. Its main purpose is to offer model-checking algorithms to verify if an AltaRica model satisfies critical properties. Requirements are described as fixpoint equations or CTL* formulas. For the model-checking part, this tool is essentially an &hellip; <a href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=32\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"footnotes":""},"class_list":["post-32","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/32","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=32"}],"version-history":[{"count":31,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/32\/revisions"}],"predecessor-version":[{"id":535,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/32\/revisions\/535"}],"wp:attachment":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=32"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}