LearnLib / ralib

Apache License 2.0
4 stars 2 forks source link

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 currently implements the following algorithms for learning register automata:

  1. The SL* algorithm by Sofia Cassel, Falk Howar, Bengt Jonsson, and Bernhard Steffen, presented in the paper Learning Extended Finite State Machines, Software Engineering and Formal Methods (SEFM 2014), pp 250-264.

  2. The SLλ algorithm by Simon Dierl, Paul Fiterau-Brostean, Falk Howar, Bengt Jonsson, Konstantinos Sagonas, and Fredrik Tåquist, presented in the paper Scalable Tree-based Register Automata Learning, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024).

Installation

RaLib uses maven as a build system. You can simply run

mvn package assembly:single

to build RaLib.

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.

  1. 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
  2. For learning a model of the SIP protocol with the iosimulator 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