GRACE

GRACE (GR-ebr reAlizability CheckEr) is a realizability checker for GR-EBR specifications. The tarball contains the Docker container for GRACE, the README file, the test suite and some benchmarks.

Download

Download the tarball from here

structure of the folder

README: this file
/licenses: the licenses of all the tools used by GRACE
/test : contains the test suite. Run make test from top-level directory for running the tests.
/benchmarks: some benchmarks

INPUT format:

The input files of GRACE have the following structure

-- This is a comment
MODULE main
EVAR -- uncontrollable variables
  var1 : boolean;
  ...
  varM : boolean;
VAR  -- controllable variables
  var1 : boolean;
  ...
  varN : boolean;
GREBRSPEC 
  (LTL-EBR-assumption & ((first_GF) & (second_GF) & ...)) 
	-> 
  (LTL-EBR-guarantee & ((first_GF) & (second_GF) & ...)) 

First time running the container

If you run GRACE for the first time, Docker has to download the corresponding image from DockerHub. For performing this download before hand, jsut execute:

docker run lucageatti/grace -h

Executing GRACE

docker run --rm -it -v $(pwd):$(pwd) -w $(pwd) grace:latest \
  -i      input_file.smv  \
  -k      k_bound \
  [-u     upper_bound]

Example

docker run --rm -it -v $(pwd):$(pwd) -w $(pwd) grace:latest -i test/GR-EBR/test6.smv -u 10

Parameters:

[-h] | -i inputfile | [-k] index | [-u] upperbound
-h          : Shows this help
-i          : Input file in .SMV format
-k          : Solves only the safety subproblem with this index
-u          : Solves all the safety subproblems up to this index

Generated with Jekyll

• researcher theme