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 MEC 5.
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:
- Support of the AltaRica language with extension proposed during ACI Persee
- support for compound types (arrays, structures)
- definition of abstract types and signatures of functions
- Acheck specifications are supported using explicit or symbolic representation (however not all the set of commands are supported in both encoding)
- MEC 5 specifications with Decision Diagrams encoding. ARC extends the set of predefined sets with, for instance,
N!reachthat specifies the set of reachable configurations of the node N. - ARC integrates an small graphical tool called AltaRica Studio.
- Large relations can be serialized in binary files for future use.
- Preprocessors can be specified using the configuration file of ARC
- CTL* logic is supported in Acheck specs or can be checked separately.
Downloading ARC
You will find instruction to get ARC tool on Download page.
Documentation
The ARC handbook distributed within source package but you can download a pre-compiled version here.
Support
Do not hesitate to report bugs or to send us request for new features using forms in Support pages.