HTTPS SSH

RALib

RALib is a library for active learning algorithms for register automata
(a form of extended finite state machines). RALib is licensed under
the Apache License, Version 2.0.

RALib is developed as an extension to LearnLib. It implements
the SL* algorithm presented in Sofia Cassel, Falk Howar, Bengt Jonsson,
Bernhard Steffen: Learning Extended Finite State Machines. SEFM 2014: 250-264.

Installation

RaLib uses the jConstraints-z3 library as an abstraction layer for
interfacing (some) constraint solvers. While basic functionality of
RaLib can be used without jConstraints-z3, the parent library
jConstraints is required for compilation.
jConstraints and jConstraints-z3 are open source software and are
licensed under the Apache License, Version 2.0.

Using RALib

RALib can be used as a library from Java. The test cases that come with RALib
demonstrate how this can be done. RALib currently also provides two tools
that can be run from the shell. A 'simulator' for inferring RA models from
simulated systems (automata) and a 'class analyzer' for inferring RA models
of Java classes. Running

$ java -ea -jar target/ralib-0.1-SNAPSHOT-jar-with-dependencies.jar

will show some help and available options to the tools. Below we provide two
example configurations.

For learning a model of java.util.LinkedList with the class-analyzer call

$ java -ea -jar target/ralib-0.1-SNAPSHOT-jar-with-dependencies.jar \
  class-analyzer -f config

with the following config file

target=java.util.LinkedList
methods=push(java.lang.Object:int)boolean:boolean+\
  pop()java.lang.Object:int

logging.level=WARNING
max.time.millis=600000
use.ceopt=true
use.suffixopt=true
use.fresh=false
use.rwalk=true
export.model=true
rwalk.prob.fresh=0.8
rwalk.prob.reset=0.1
rwalk.max.depth=6
rwalk.max.runs=10000
rwalk.reset.count=false
rwalk.draw.uniform=false
teachers=int:de.learnlib.ralib.tools.theories.IntegerEqualityTheory

For learning a model of the SIP protocol with the simulator call

$ java -ea -jar target ralib-0.1-SNAPSHOT-jar-with-dependencies.jar \
  iosimulator -f config

with the following config file

target=src/test/resources/de/learnlib/ralib/automata/xml/sip.xml

logging.level=WARNING
max.time.millis=600000
use.eqtest=true
use.ceopt=true
use.suffixopt=true
use.fresh=false
use.rwalk=true
export.model=true
rwalk.prob.fresh=0.8
rwalk.prob.reset=0.1
rwalk.max.depth=100
rwalk.max.runs=10000
rwalk.reset.count=false
rwalk.draw.uniform=false
teachers=int:de.learnlib.ralib.tools.theories.IntegerEqualityTheory

Currently, equality theories can be used with the (default) integrated
constraint solver. Inequality theories only work in combination with
jConstraints. (Configuration option solver=z3