This repo contains an example of usage of the extension of MultiVeStA Statistical Model Checker ( to support the DESMO-J Discrete Event Simulator framework ( This is draft version. Here, the MultiVeStA extension is used to validate the outcomes of the simulations of the popular Sardinian game known as "Sa Murra" (The Morra Game). It evaluates and validates the probability with which the first player wins. Players could have different abilities, thus influencing their probability of winning a game.

The libs folder contains the multivesta.jar, already extended with the vesta.desmoj.DesmojState.class. Also, a folder is present containing the file.


Fetch the project, reference the libs, set up two "run configurations":

  • Server Conf.
    Main Class: entrypointmultivesta.UniqueEntryPoint
    Program Arguments:
    -s 50751

  • Client Conf.
    Main Class: entrypointmultivesta.UniqueEntryPoint
    Program Arguments:
    -m src/mv/conf.xml
    -l src/mv/server.txt
    -f src/mv/query.quatex
    -bs 10
    -a 0.05
    -d1 100
    -ms 100
    -sots 12345
    -se game.SaMurraEvaluator
    -sd vesta.desmoj.DesmojState

Run them :)


DesmojState.class makes use of the conf.xml file to set up the Experiment and the Model of our DESMO-J Simulations. The conf.xml shown in this example should be used as a general model file to set up simulations. Through conf.xml it is possible to specify the Experiment parameters.

Desmoj requires a Model class (in this example SaMurraModel) that must have an empty constructor in order to let the DesmojState.class instantiate it with java.lang.reflect.

Furthermore, DesmojState best works with a "stopCondition", in our example the MatchIsOver class.