Trustworthy Intelligent Systems

Getting ROLL

ROLL v1.0 is available on GitHub

ROLL v1.0 is now publicly available on GitHub at this repository. ROLL v1.0 is a major rewrite of the previous version used in the TACAS paper. Compared to its previous version, it now supports new features such as:

  • Learning algorithm for limit-deterministic Büchi automata.
  • Jupyter notebook for ROLL (requires websockets to run correctly).
  • Interactive mode for educational purpose.
  • Büchi automata complementation based on learning7.
  • Büchi automata inclusion testing based on word sampling and learning.
  • PAC-learning for Büchi automata based on Monte-Carlo word sampling (our improved version9 of the algorithm by Grosu and Smolka8).
  • Hanoi omega-automata format.

Build ROLL on Ubuntu

You should have installed Java Development Kit on your system. Currently we can successfully build ROLL with JDK 8.0.

Build with Network Connection

Please make sure you have Maven installed on your system or use following command to install it.

sudo apt-get install maven

Then follow the two steps below.

  1. Use following command to clone the repository to your local file system. 
      git clone https://github.com/ISCAS-PMC/roll-library
  2. Under the roll-library directory, type ./build.sh in the command line.

Build without Network Connection

You can use the shell script named build-offline.sh in the roll-library folder to build ROLL offline. However, some prerequisites in the following have to be satisfied before you use that script:

Set up ROLL in Eclipse

This tutorial has been tested on the following distributions:

  • Ubuntu 16.04 LTS, 64-bits

Prerequisites

  • Java Development Kit (only tested with JDK 8.0)
  • Eclipse Oxygen
  • Javacc plugin in Eclipse
  • Maven Integration for Eclipse
  • SPOT (only if you want to run some JUnit tests via autfilt in SPOT and use parallel inclusion checking of Büchi automata)
  • spotj (only if you want to use parallel inclusion checking of Büchi automata, use rollinstall.sh in the directory to install spotj)

Set up ROLL in Eclipse

  1. Use following command to clone the repository to your local file system. 
      git clone https://github.com/ISCAS-PMC/roll-library
  2. Import roll-library as Maven Existing Projects.

You may have life cycle problem with Javacc in pom.xml but this can be fixed by the operations suggested by Eclipse. Then you should be able to run ROLL as a java application by choosing roll.main.ROLL as the main class.

Büchi automata

  • GOAL: a graphical interactive tool for defining and manipulating Büchi automata and temporal logic formulae.
  • SPOT: a library for LTL, ω-automata manipulation and model checking.
  • RABIT: a tool for Büchi automata universality and inclusion testing.

Learning libraries

  • libalf: a comprehensive, open-source library for learning finite-state automata.
  • LearnLib: a free, open-source Java library for active automata learning.

Executables and Logs for the experiments in our TACAS 17 paper

In order to reproduce the experimental results we obtained in the TACAS paper, please use the Büchi automata from Büchi Store. In this version, ROLL does not support the HANOI format yet and thus may get different automaton from the real automaton specified in the HANOI format file of Büchi Store. We thank the authors of Büchi Store for providing us the examples.

Download