Compilation

In order to compile the ARE software for a target CPU, first you need NuSMV-2.4.3.2-omcare.tar.gz. The NuSMV-2.4.3.2-omcare.tar.gz can be downloaded from Donwload.

Then, you have to follow the instructions below:

  • Unpack the downloaded source code 
   tar -xzvf NuSMV-2.4.3.2-omcare.tar.gz

This will create the directory ./NuSMV-2.4.3.2 containing the 4 additional sub-directories below: 

   ./NuSMV-2.4.3.2/builders 
   ./NuSMV-2.4.3.2/nusmv
   ./NuSMV-2.4.3.2/ARE_TopLevel
   ./NuSMV-2.4.3.2/cudd-2.4.1.0
  • Move to the ./NuSMV-2.4.3.2/builders directory 
   cd ./NuSMV-2.4.3.2/builders
  • Create the [-config]- file 
   make config
  • edit config file with your favorite editor
    • Modify the variable below to point the place where the rtems-4.8 cross compilers are installed.
      • sparc_rtems_base = /opt/rtems-4.8
    • Modify the variable below to point the place where rtems-4.8 run-time has been installed. In this directory is expected a sub-directory sparc-rtems4.8 containing the target.
    • rtems_os_base = /opt/rtems-4.8
  • Execute the command
    • To build the executable for target SPARC leon3: 
   make build_local_omcare host=rtems rtems_cpu=leon3
  • To build the executable for the target sis: 
   make build_local_omcare host=rtems rtems_cpu=sis
  • To build the executable for a Linux X86 target: 
   make build_local_omcare

This will compile all the needed packages and create a demonstration executable called are in the ARE_TopLevel directory. (Only for the Linux X86 target it will also be created the executable NuSMV in the nusmv directory. This executable allows to interact with the atomic functionalities of the ARE software (initiliazation, plan generaton, plan validatiom, plan loading, assumption loading,...) in an interactive fashion detached from the ARE top level FSM.


Remark: by default RTEMS 4.8 enforce RAM to be 4Mb and ROM to be 2MB. Unfortunately these values cannot be changed because of a bug in the linkcmd script for the sparc target CPU. To solve this problem, by allowing to specify such values at compilation time ovverriding the dafault values, it is necessary to edit the file /opt/rtems-4.8/sparc-rtems4.8/<proc>/lib/linkcmds for <proc> in leon3, leon2, erc32 and sis, and replace the lines: 

    _PROM_SIZE = 2M;
    _RAM_SIZE = 4M;

with the lines: 

   _PROM_SIZE = DEFINED(_PROM_SIZE) ? _PROM_SIZE : 2M;
   _RAM_SIZE = DEFINED(_RAM_SIZE) ? _RAM_SIZE : 4M;


Goto Top

Execution

To execute the demo go inside the Are_TopLevel and execute the top-level "are" binary. For instance if the target cpu is leon3 then execute 

   tsim-leon3 -bopt -ram 32768 -rom 8192 are

If the target cpu is sis/erc32 then type 

   sis64 -ram 32768 -rom 8192 -v -nomexc are.srec

If you downloaded the executable directly from the web page listed above then the same commands can be applied to execute them.
To execute the ARE demo under Linux X86 then go inside the ARE_TopLevel and type the command: 

    ./are

To execute the NuSMV interactive shell go inside the nusmv directory and type the command: 

   ./NuSMV -int

At the NuSMV shell you can then type the different commands (type help to get the list of available commands).


Goto Top

Bug Tracking