User Tools

Site Tools


release

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
release [2018/11/13 19:41] liyongrelease [2020/12/16 14:32] (current) – [ROLL v1.0 is available on GitHub] liyong
Line 9: Line 9:
 ===== ROLL v1.0 is available on GitHub =====  ===== ROLL v1.0 is available on GitHub ===== 
  
-ROLL v1.0 is now publicly available on GitHub at [[https://github.com/ISCAS-PMC/roll-library| this repository]]. ROLL v1.0 is a large rewrite of the previous version used in the TACAS paper.+ROLL v1.0 is now publicly available on GitHub at [[https://github.com/ISCAS-PMC/roll-library| 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: Compared to its previous version, it now supports new features such as:
   * Learning algorithm for limit-deterministic Büchi automata.   * Learning algorithm for limit-deterministic Büchi automata.
-  *  Interactive mode for education purpose.+  * [[https://iscasmc.ios.ac.cn/roll/jupyter|Jupyter notebook for ROLL]] (requires **websockets** to run correctly). 
 +  *  Interactive mode for educational purpose.
   *  Büchi automata complementation based on learning [7].   *  Büchi automata complementation based on learning [7].
   *  Büchi automata inclusion testing based on word sampling and learning.   *  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 version of [8]).+  *  PAC-learning for Büchi automata based on Monte-Carlo word sampling (our improved version [9] of [8]).
   *  [[http://adl.github.io/hoaf/|Hanoi omega-automata format]].    *  [[http://adl.github.io/hoaf/|Hanoi omega-automata format]]. 
  
 ===== Build ROLL on Ubuntu ===== ===== 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 ====+==== Build with Network Connection ====
  
 Please make sure you have Maven installed on your system or use following command to install it. Please make sure you have Maven installed on your system or use following command to install it.
Line 34: Line 37:
 2. Under the roll-library directory, type ./build.sh in the command line. 2. Under the roll-library directory, type ./build.sh in the command line.
  
-==== Build Without Network Connection ====+==== Build without Network Connection ====
  
 You can use the shell script named build-offline.sh in the roll-library folder to build roll offline. 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: However, some prerequisites in the following have to be satisfied before you use that script:
  
-  *  The javacc.jar file in the roll-library directory for generating Javacc parsers.  +  *  The [[https://mvnrepository.com/artifact/net.java.dev.javacc/javacc|javacc.jar]] file in the roll-library directory for generating Javacc parsers.  
-  *  The [[https://mvnrepository.com/artifact/net.sf.trove4j/trove4j/3.0.3|GNU trove]] jar file and Jupyter jvm-expr-0.3.1.jar file in the roll-library/lib directory. +  *  The [[https://mvnrepository.com/artifact/net.sf.trove4j/trove4j/3.0.3|GNU trove]] jar file and Jupyter [[https://mvnrepository.com/artifact/com.github.jupyter/jvm-repr/0.3.1|jvm-repr-0.3.1.jar]] file in the roll-library/lib directory. 
  
 ===== Set up ROLL in Eclipse ===== ===== Set up ROLL in Eclipse =====
Line 52: Line 55:
   *  Javacc plugin in Eclipse   *  Javacc plugin in Eclipse
   *  Maven Integration for Eclipse   *  Maven Integration for Eclipse
-  *  [[https://spot.lrde.epita.fr|SPOT]] (only if you want to run some JUnit tests via autfilt in SPOT)+  *  [[https://spot.lrde.epita.fr|SPOT]] (only if you want to run some JUnit tests via autfilt in SPOT and use parallel inclusion checking of Büchi automata) 
 +  * [[https://github.com/ISCAS-PMC/spotj/tree/master/src/main/c/spot|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 ==== ==== Set up ROLL in Eclipse ====
Line 65: Line 69:
 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. 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.
  
-===== Executables and Logs for TACAS experiments ===== 
- 
-In order to reproduce the experimental results we obtained in the TACAS paper, please use the Büchi automata from [[http://buchi.im.ntu.edu.tw/|Büchi Store]]. In this version, ROLL does not support HANOI format yet and thus may get different automaton from the real automaton specified in the HANOI format file of [[http://buchi.im.ntu.edu.tw/|Büchi Store]]. We thank the authors of Büchi Store for providing us the examples. 
- 
-=== Download === 
-  * {{ :jar.zip | Download ROLL executable}} {{ :cases.zip | Download simple cases}} {{ :learning-logs.zip | Learning logs}} 
-  * {{ :roll-lib.zip |ROLL library}} {{ :roll-release.zip | ROLL source code}} 
-  * {{ :rabit-teacher.zip |RABIT teacher}}. We add some code in RABIT to resolve the membership queries, which is in "oracle" directory. 
  
 ===== Related tools ===== ===== Related tools =====
Line 81: Line 77:
   * [[http://www.languageinclusion.org/|RABIT]]: a tool for Büchi automata universality and inclusion testing.   * [[http://www.languageinclusion.org/|RABIT]]: a tool for Büchi automata universality and inclusion testing.
  
-=== Learning library === +=== Learning libraries === 
-  * [[http://libalf.informatik.rwth-aachen.de/|LibAlf]]:  a comprehensive, open-source library for learning finite-state automata.+  * [[http://libalf.informatik.rwth-aachen.de/|libalf]]:  a comprehensive, open-source library for learning finite-state automata.
   * [[https://learnlib.de/|LearnLib]]: a free, open-source Java library for active automata learning.   * [[https://learnlib.de/|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 [[http://buchi.im.ntu.edu.tw/|Büchi Store]]. In this version, ROLL does not support HANOI format yet and thus may get different automaton from the real automaton specified in the HANOI format file of [[http://buchi.im.ntu.edu.tw/|Büchi Store]]. We thank the authors of Büchi Store for providing us the examples.
 +
 +=== Download ===
 +  * {{ :jar.zip | Download ROLL executable}} {{ :cases.zip | Download simple cases}} {{ :learning-logs.zip | Learning logs}}
 +  * {{ :roll-lib.zip |ROLL library}} {{ :roll-release.zip | ROLL source code}}
 +  * {{ :rabit-teacher.zip |RABIT teacher}}. We add some code in RABIT to resolve the membership queries, which is in "oracle" directory.
  
release.1542109316.txt.gz · Last modified: 2018/11/13 19:41 by liyong