Checker

In PLASMA Lab the concepts of Checker and Requirements are mixed together. We could say that a requirement checks itself. For this reason, a Checker inherits from the AbstractRequirement class which in turns inherits from the AbstractData class. The AbstractData class describes an object, model or requirement, editable in the PLASMA Lab edition view. The AbstractRequirement class add verification methods.

In this section, we explain some of the implementation needed for a new checker plugin. The language verified by our plugin contain two values. The first is a time stamp TIME and the second a value VAL. For a given trace, at time TIME, if the value of the model variable "X" is stricly superior to VAL, the property is evaluated to true. Otherwise the evaluation returns false.

AbstractData

We won't detail the AbstractData class except for the configuration part. Others functions and methods simple enough to understand with the comment.

Configuration

The checkForErrors function is called on modification of the edition panel content and before each experimentation or simulation in simulation mode. The purpose of this function is double. Detect any syntax error and build the property before checking it.

Our checkForErrors function check if the sequence contains at least two integer values. One for the time bound, the other for the threshold. A PlasmaSyntaxException is added to the list of errors if an error is found.

    @Override
    public boolean checkForErrors() {
        errors.clear();

        String[] splitted = content.split(" ");

        try{
            if(splitted.length < 2)
                errors.add(new PlasmaSyntaxException("Dummy checker need a time and a threshold value"));
            until = Integer.valueOf(splitted[0]);
            threshold = Integer.valueOf(splitted[1]);
        }catch(Exception e){
            errors.add(new PlasmaException("Exception occured while parsing", e));
        }

        return !errors.isEmpty();
    }

AbstractRequirement

The AbstractRequirement class extends the AbstractData class to add checking capability. This task is done by two check functions.

Check

Our properties check if the value "X" is superior to a threshold after TIME timestamp was reached. To evaluate this property, we advance the simulation as needed by calling the simulate method. Once enough states were generated, we check the variable against the threshold and return the result. 1 meaning true, 0 false.

    @Override
    public Double check(InterfaceState path) throws PlasmaDeadlockException,
        PlasmaParameterException {
        while(model.getCurrentState().getValueOf(TIME)<until){
            model.simulate();
        }
        return (model.getCurrentState().getValueOf("X") > threshold ? 1.:0.);
    }

The other check function is used in simulation mode. In this mode the user as direct control over the simulation. So the checker is not allowed to control the simulation. The check with untilStep parameter check the model current path. If more step are needed, the checker returns a NaN value meaning "undecided".

    @Override
    public Double check(int untilStep, InterfaceState path)
            throws PlasmaDeadlockException {

        for(int step=0; step < untilStep || step >= model.getTraceLength(); step++){
            InterfaceState state = model.getStateAtPos(step);
            if(state.getValueOf(TIME) == until)
                //Time bound reached
                return (model.getCurrentState().getValueOf("X") > threshold ? 1.:0.);
        }
        //Untilstep reached or not enough state to reach time bound
        return Double.NaN;
    }