Transition System definition

Transition system definition using Java DSL

The different kinds of transitions systems supported by VIBeS may be defined by redefining one of the following abstract classes and by implementing its define() method:

  • LabelledTransitionSystemDefinition: used to define labelled transition systems.
  • FeaturedTransitionDefinition: used to define featured transition systems
  • UsageModelDefinition: used to define usage models (labelled transition systems with probabilities over transitions) 
    import be.unamur.transitionsystem.dsl.*;

public class MyLTS extends LabelledTransitionSystemDefinition{

    public MyLTS(){
        super();
    }

    @Override
    protected void define() {
        initial("initial");
        
        from("initial").action("act1").to("s1");
        
        from("s1").action("doX").to("s2");
        from("s1").action("doXY").to("s3");
        
        from("s2").action("doY").to("s3");
        
        from("s3").action("exit").to("initial");
    }

    public static void main(String[] args){
        MyLTS def = new MyLTS();
        LabelledTransitionSystem lts = def.getTransitionSystem();
    }
}

Feature expression grammar

Feature expressions are boolean expressions defined over features. In VIBeS, feature expressions have to respect the following grammar:

FEXPRESSION: 
        'true'
    |   'false'
    |   FEATURENAME
    |   '!' FEXPRESSION
    |   FEXPRESSION '&&' FEXPRESSION
    |   FEXPRESSION '||' FEXPRESSION
    |   '(' FEXPRESSION ')'

FEATURENAME:
    LETTER (LETTER | DIGIT)*

LETTER:
    'A'..'Z' | 'a'..'z' | '_'

DIGIT:
    '0'..'9'

The operators priority is defined as following : parenthesis ('(' FEXPRESSION ')') > not ('!') > and ('&&'), or ('||')

Transition system XML load and save using Java DSL

Various transition systems may be loaded/saved in XML files.

import static be.unamur.transitionsystem.dsl.TransitionSystemXmlLoaders.*;
import static be.unamur.transitionsystem.dsl.TransitionSystemXmlPrinter.*;

public Main{
    public static void main(String[] args){
        LabelledTransitionSystem lts = loadLabelledTransitionSystem("myLTS.xml");
        // [...]
        print(lts, "otherLTS.xml");
    }
}