Skip to content

DeveloperGuide

Jump to bottom
Davide Prandi edited this page Oct 24, 2022 · 10 revisions

Using EvoMBT as a Java library

This page describes the use of EvoMBT as a Java library in your project.

Import EvoMBT

EvoMBT project can be imported using Maven and JitPack.

First add JitPack to your Maven repositories.

	<repositories>
		<repository>
		    <id>jitpack.io</id>
		    <url>https://jitpack.io</url>
		</repository>
	</repositories>

Add last stable version of EvoMBT

	<dependency>
	    <groupId>com.github.iv4xr-project</groupId>
	    <artifactId>iv4xr-mbt</artifactId>
	    <version>1.2.0</version>
	</dependency>

Define an EFSM

In this section will see how to define an EFSM in EvoMBT using traffic light example.

EFSMState

An EFSMState represents a state of an EFSM and it is implemented as a class that takes a String as input. For traffic light we need four states.

public EFSMState red = new EFSMState("Red");
public EFSMState yellow = new EFSMState("Yellow");
public EFSMState green = new EFSMState("Green");
public EFSMState pending = new EFSMState("Pending");

Var and VarSet

Var is a generic class that represents a variable of an EFSM of an arbitrary type. Variable count in traffic light EFSM is implemented as a Var with type Integer.

public Var<Integer> count = new Var<Integer>("count", 0);

The constructor requires to specify the name of the variable and its initial value. Variables in EvoMBT are managed by name, i.e., two variables with the same name are the same. Class Var implements methods update that allows updating the value of a variable. Current EvoMBT supports variables of type Integer, Boolean, Enum, and Double.

For instance, the input pedestrian is represented with a boolean variable.

private Var<Boolean> pedestrian = new Var<Boolean>("pedestrian",true);

A VarSet is a class implementing a set of variables.

EFSMContext

Class EFSMContext implements the context variables of an EFSM. EFSMContext is a wrapper for a VarSet class that provides helper methods to update and create context variables. The traffic light model has only the variable count in its context.

public EFSMContext tlContext = new EFSMContext(count);

Const

Class Const implements constants and it is similar to class Var but, as expected, does not have a method update. The traffic light model requires two constants to model timeout values of 60 and 5.

Const<Integer> sixty = new Const<Integer>(60);
Const<Integer> five = new Const<Integer>(5);

Differently from class Var, a Const does not have a name.

Exp

Exp is a Java interface representing a generic expression of type T used to define EFSM guards.

public interface Exp<T extends Object> extends Cloneable, Serializable {
  // Return the current value of the expression
  Const<T> eval();
  // Return the list of the variables id used in the expression
  VarSet<?> getVariables();
  // update the value of the variables in an expression given a varSet
  void update(VarSet<?>  varSet);
  // ...
}

Implementations of Exp should provide

  • method eval that returns a Const of a generic type T;
  • method getVariables that returns a VarSet comprising all the variables defined in the expression;
  • method update that updates the values of the variables of the expression with the input varSet. Values are updated by value, i.e., the names of the variables are used.

Both classes Var and Const implement interface Exp. EvoMBT provides a set of basic expressions that allows the implementation a wide variety of guards. In the following, we will describe the expressions used in the traffic light example.

Traffic light expressions

The transition from red to the green state requires that the context variable count is greater or equal to 60.

// count greater that 60
IntGreat countGreatThanSixty =  new IntGreat(count, sixty);
// count equal 60
IntEq countEqualSixty =  new IntEq(count, sixty);
// count greater or equal 60
BoolOr countGreatEqThanSixty = new BoolOr(countGreatThanSixty, countEqualSixty);

Self-loop on green check that count is less than 60 is obtained negating countGreatEqThanSixty expression.

BoolNot countLessThanSixty = new BoolNot(countGreatThanSixty);

The guard that checks that count is greater than 5 in transition from yellow to red is implemented similarly.

Finally, the transition from green to yellow checks both the value of count and pedestrian.

BoolAnd countGreatEqThanSixtyAndPedestrian = new BoolAnd(countGreatEqThanSixty,pedestrian);

Note that, being pedestrian a boolean variable, it can be used directly in a boolean expression.

Assign

Class Assign enables the definition of update transformations, as, for instance, reset or increment of count variable in the traffic light examples. Class Assign has a variable of class Var and an expression of class Exp and provides a method to update the value of the variable with the current value of the expression. For the traffic light example, two assignments are required.

// increment count
Assign<Integer> incCount = new Assign(count, new IntSum(count, new Const(1)));
// reset count
Assign<Integer> resetCount = new Assign(count, new Const<Integer>(0));

Class AssignSet implements a set of assignments.

EFSMTransition

Class EFSMTransition implements a transition of the EFSM. An EFSMTransition has the following components:

EFSMState src;
EFSMState tgt;
EFSMGuard guard;
EFSMOperation op;
EFSMParameter inParameter;
EFSMParameter outParameter;

EFSMState src and tgt are the source and the target state, respectively. Transition guard has class EFSMGuard and it is made of a boolean expression. Transition update has class EFSMOperation and it is defined as a set of assignments. Input and output parameters are implemented by the class EFSMParameter, defined as a set of variables.

Traffic light transitions

In the following, we will describe some of the EFSMTransition implementing the transitions of the traffic light example.

Transition t_0 implements self-loop on state red.

// t_0 : red -> red # increment count
EFSMTransition t_0 = new EFSMTransition();
t_0.setGuard(new EFSMGuard(countLessThanSixty));
t_0.setOp(new EFSMOperation(incCount));

Guard of t_0 checks that the value of the context variable is less than 60. Operation of t_0 increments the value of count.

Transition t_1 goes from red to green state. The transition has alsooutput from a defined enumerative:

public enum outSignal{ sigR, sigG, sigY, sigP };
// t_1 : red -> green
EFSMTransition t_1 = new EFSMTransition();
t_1.setGuard(new EFSMGuard(countGreatEqThanSixty));
t_1.setOp(new EFSMOperation(resetCount));
Var<Enum> t1Out = new Var<Enum>("signal", outSignal.sigG);
t_1.setOutParameter(new EFSMParameter(t1Out));

Guard of t_1 checks if the variable count is greater or equal to 60 while the update sets the value of count to 0. When executed, t_1 outputs variable signal with value sigG.

Transition t_2 implements the self-loop on state green and it is similar to transition t_0. Finally, transition t_3 goes from green to yellow and requires input variable pedestrian.

// t_3 : green -> yellow 
EFSMTransition t_3 = new EFSMTransition();
// input
Var<Boolean> t3In = new Var<Boolean>("pedestrian",true);		
t_3.setInParameter(new EFSMParameter(t3In));
// guard
t_3.setGuard(new EFSMGuard(countGreatEqThanSixtyAndPedestrian));
// operation
t_3.setOp(new EFSMOperation(resetCount));
// output
Var<Enum> t3Out = new Var<Enum>("signal", outSignal.sigY);
t_3.setOutParameter(new EFSMParameter(t3Out));

The input of t_3 is defined as a new variable pedestrian with the value true. The name of the variable matches the one in the guard defined by the expression countGreatEqThanSixtyAndPedestrian. Before evaluating the guard, the EFSM update the value of pedestrian in the guard expression with the value in the input variable with the same name.

The other transitions of the traffic light EFSM are similar to t_0, t_1, or t_3.

EFSMBuilder

Class EFSMBuilder builds the EFSM from transitions, initial state, and context.

// The model and the associated builder
EFSM trafficLightEFSM;
EFSMBuilder trafficLightEFSMBuilder = new EFSMBuilder(EFSM.class);
// parameter generator 
TrafficLightParameterGenerator parameterGenerator = new TrafficLightParameterGenerator();
// build EFSM		
trafficLightEFSM = trafficLightEFSMBuilder
	    		.withTransition(red, red, t_0)
	    		.withTransition(red, green, t_1)
	    		.withTransition(green, green, t_2)
	    		.withTransition(green, yellow, t_3)
	    		.withTransition(green, pending, t_4)
	    		.withTransition(yellow, yellow, t_5)
	    		.withTransition(yellow, red, t_6)
	    		.withTransition(pending, pending, t_7)
	    		.withTransition(pending, yellow, t_8)
	    		.build(red,tlContext, parameterGenerator);

Class EFSMBuilder builds an EFSM by adding all transitions. For each transition, the user specifies the source and target state. The build method requires initial state (red), initial EFSM context (tlContext), and parameter generator (parameterGenerator). Class TrafficLightParameterGenerator extends EFSMParameterGenerator and implements the method getRandom, that returns a random parameter for the EFSM. Parameter generator is not currently used by EvoMBT and TrafficLightParameterGenerator simply returns a null value.

For full specification refers to traffic light model.

Run test generation

This section shows how to generate test cases programmatically to integrate EvoMBT in a custom model based testing cycle. An example is implemented in test trafficLightSearchTest.

The interface EFSMProvider is the entry point to add a custom model to EvoMBT

public interface EFSMProvider {
	/**
	 * Every implementation must return a valid EFSM model.
	 */
	public EFSM getModel ();

}

The fully qualified name of the class implementing EFSMProvider is used to access the model. Suppose, for instance, to create a class TrafficLight that implements EFSMProvider and returns the traffic light model described above.

The first step to use EvoMBT to generate test cases for the traffic light model involves defining the parameters of the test case generation from MBTProperties class.

Select the SUT.

MBTProperties.SUT_EFSM = "eu.fbk.iv4xr.mbt.efsm.examples.TrafficLight";

Set the coverage criterion.

MBTProperties.MODELCRITERION = new ModelCriterion[] {
  ModelCriterion.TRANSITION
};

Set the time budget in seconds.

MBTProperties.SEARCH_BUDGET = 120l;

Select a search algorithm, NSGAII for instance.

MBTProperties.ALGORITHM = Algorithm.NSGAII;

Set seed for the random generator to enable repeatability.

MBTProperties.RANDOM_SEED = 4328213l;

Then, a user only needs to call search based strategy and generate test casea.

SearchBasedStrategy sbStrategy = new SearchBasedStrategy<>();
SuiteChromosome generatedTests = sbStrategy.generateTests();
List<MBTChromosome> testChromosomes = generatedTests.getTestChromosomes();

List testChromosomes contains all generated test cases that can be further manipulated. For instance, in the case of Lab Recruits, test cases are transformed into aplib goals that can be executed directly in the game.

Example project

Folder src/test/resources contains an example of projects modelfactory that uses EvoMBT as a Java library. The pom file imports EvoMBT and allows using EvoMBT main to run test generation from command line. The project contains only the class MyModel that implements EFSMProvider. Once compiled with maven, it suffices to execute

java -jar target\modelfactory-0.0.1-SNAPSHOT-jar-with-dependencies.jar -sbt -Dsut_efsm=modelfactory.MyModel

Note that the sut_efsm requires the fully qualified name of the class.

Clone this wiki locally