ARC - AltaRica Checker¶
The ARC model-checker syndicates developments on the two AltaRica based model-checkers Altatools and Mec 5.
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 simulator that replaces the old one implemented in Altatools
- 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.
How and where to get ARC ?¶
ARC source code is freely available and can be used, distribute and modify under the terms of the AltaRica Public License (see source:COPYING).
You can download ARC from the download area.
The last release is ARC 1.4. A nightly built version is also available: arc-current.tar.gz.
Source code is also available via our version control system (GIT):
- Using the HTTP protocol, sources are freely available for read only access:
git clone http://altarica.labri.fr/git/arc.git - Using a SSH authorized access, the repository is accessible for read and write synchronizations:
git clone git@altarica.labri.fr:arc.git
For now on, ARC tarballs come with CCL library that is automatically installed and ARsyntax is integrated into ARC sources and replaced by the libaltarica library.
Compilation and Installation¶
Installation by hands¶
In order to compile ARC you will need to install our CCL and ARsyntax libraries (either stable or nightly built version).
Installation procedure is described in the INSTALL file that comes with the ARC archive:- Current installation notes are source:INSTALL.
- Last stable installation notes are source:INSTALL@5f395e51.
Automatic installation (Experimental)¶
We provide an experimental installation script. Follow this link to download the last version of the script: export:install-arc.sh. The script takes one or two arguments and assumes that neither CCL nor ARsyntax are installed. If you want to install ARC in the directory DIR (DIR must be an absolute path) then:
./install-arc.sh DIR
will install the current version of CCL, ARsyntax and ARC in the
DIR directory. You can specify explicitly if you want to install the current (i.e. nightly built) version or the last stable version of ARC using, respectively, the options --current and --stable. The following command should install the last stable version:./install-arc.sh --stable DIR
Use
--help to get all options accepted by the ./install-arc.sh script.
ARC under Microsoft systems¶
There is no actual port of AltaRica tools under MS Windows. Currently, users interested by running ARC on these systems should install Cygwin or MinGW environment.
In the sequel we describe the installation procedure for a Windows Vista system starting from scratch i.e. without Cygwin installed.
Cygwin Required Packages¶
To install Cygwin environment download the installation program (setup.exe) on the Cygwin website. Then follow the instructions of the Cygwin installation process. When the Select Packages window appears choose the following packages (of course you can add your own selection e.g. emacs, ...):- Devel/
- binutils
- bison
- flex
- gcc4
- gtk2-X11-devel
- make
- minres-devel
- pango-devel
- pkg-config
- readline
- Doc/
- texinfo
- Gnome/
- atk-devel
- Utils/
- diffutils
- Web/
- wget
- X11/
- xinit
Downloading and installation of ARC packages¶
Now that Cygwin is installed, open an Xterm (look for the XWin Server entry in the Start menu of Windows) andexecute the following commands:
- We install ARC in the directory
$HOME/dev. For this purpose we define and export an environment variableINSTthat
store the installation root.
export INST=$HOME/dev mkdir $INST cd $INST mkdir src cd src
- In the
srcdirectory, download and extract ARC packages:
wget http://altarica.labri.fr/pub/tools/packages/current/arc-current.tar.gz tar zxf arc-current.tar.gz wget http://altarica.labri.fr/pub/tools/packages/current/arsyntax-current.tar.gz tar zxf arsyntax-current.tar.gz wget http://altarica.labri.fr/pub/tools/packages/current/ccl-current.tar.gz tar zxf ccl-current.tar.gz
- Build and install packages
cd ccl-current ./configure --prefix=$INST && make && make install cd ../arsyntax-current ./configure --prefix=$INST && make && make install cd ../arc-current ./configure --prefix=$INST && make && make install
- Now add the
bindirectory to your PATH variable:
export PATH=$INST/bin:$PATH
- For future use you should open your configuration file
~/.bashrcwith your favourite editor and update yourPATHvariable e.g add the following lines at the end of.bashrc:
export INST=$HOME/dev export PATH=$INST/bin:$PATH
Installation procedure for MinGW¶
For MinGW the installation process is quiet similar to the one for Cygwin. We refer the reader to http://sourceforge.net/projects/mingw/ for the installation details
of MinGW. Once the installation of MinGW/MSYS is done, open a MSYS terminal and start the installation of ARC packages.
Bug report and New feature requests¶
Report any bug and do not hesitate to request us for improvement using New issue tab.