PLASMA Lab book

Algorithms

In this section we introduce a generic view on algorithm class in PLASMA Lab. For this purpose we consider the case of a local (non distributed) algorithm.

Two sub-sections, Scheduler and Worker, will then explain in details how the distributed algorithms are implemented. A distributed algorithm being a specific case of the local algorithm.

InterfaceAlgorithmScheduler

Every algorithm must implement InterfaceAlgorithmScheduler (package fr.inria.plasmalab.algorithm). This interface extends the Runnable interface. Thus an algorithm will have a run method. This is the main method of an SMC algorithm.

    public interface InterfaceAlgorithmScheduler extends Runnable

The InterfaceAlgorithmScheduler also defines a setExpListener method. Object implementing the ExperimentationListener interface will be kept up to date on the experiment progress. Mainly with call to function such as notifyAlgorithmStarted, notifyAlgorithmCompleted and publishResults.

    public void setExpListener(ExperimentationListener listener);

The abortScheduling method is called when the user want to stop a running experiment before it finishes.

    public void abortScheduling();

Run method of an SMC Algorithm

The run method of an SMC Algorithm is where the work is done. A run method could be based on the following pseudo-code:

    initialize(model, property)
    listeners.notifyAlgorithmStarted

    while(continue)
        state = model.newPath
        positive += property.check(state)
        total ++
        if(total > required)
            continue = false

    listeners.publishResults(getResults(positive))
    listeners.notifyAlgorithmCompleted

For each run needed, the model initialize a new trace. The property is checked starting from the initial state. If the property has been checked on enough traces, the algorithm terminates and the results are published.

SMCResult interface

The data structure used to return results of an experimentation is the SMCResult interface (package fr.inria.plasmalab.algorithm.data). This interface also inherits from the ResultInterface (package fr.inria.plasmalab.workflow.shared).

In PLASMA Lab, a class implementing the ResultInterface represents the output of a task such as a simulation or an experiment. It provides access to a header array of type String with each header being associated to a value.

The SMCResult interface add specific methods to represent the output of a SMC experimentation. Thus, headers are separated in two categories. SMC headers common to all SMC algorithm such as probability and total number of simulation, and other headers, depending on the particular algorithm. SMC headers have one accesser method for each.

An SMCResult also contains the property that was used to produce the output. The property is present in two form, the origin (AbstractRequirement type) and the instance (String type). The origin requirement parameter may be used to group results together and compare the influence off some parameters in instance requirement.