In PLASMA Lab the concepts of Simulator and Model are mixed together. We could say that a model executes itself. For this reason, a Simulator inherits from the AbstractModel 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 AbstractModel class add simulation methods.
In this section, we explain some of the implementation needed for a new simulator plugin. The language executed by our dummy simulator if a succession of "+" and "-". Starting from 0 it will add or remove one to the value. For instance the model "+++--" will produce a trace of "0 1 2 3 2 1". Of course this language has no stochastic property.
We only cover a few important method. The full implemented sources for this tutorial can be retrieved here.
We won't detail the AbstractData class as the source comments should be self sufficients.
The AbstractModel class extends the AbstractData class to add simulation capability. This is mainly done by two methods. newPath initialize a new execution run while simulate progress the execution one step forward.
The content String is inherited from AbstractData and contains the text entered in the edition panel. In our simulator we initialize a stream reader to read content character by character.
@Override
public InterfaceState newPath() {
trace = new ArrayList<InterfaceState>();
trace.add(initialState);
InputStream is = new ByteArrayInputStream(content.getBytes());
br = new BufferedReader(new InputStreamReader(is));
return initialState;
}
We also intialize a trace with the initial state. The initial state starts with time 0 and value 0. This state is created in the checkForErrors function. We will see it in details later.
initialState = new DummyState(0, 0);
In the simulate method we read the next character. In our language, '+' (resp. '-') would add 1 to the value (resp. substract 1 to the value). We build a new state with the new value. Either way, the time value of the new state also increase by one on each simulation step.
@Override
public void simulate() throws PlasmaDeadlockException {
try {
int c = br.read();
if(c==-1)
throw new PlasmaDeadlockException(getCurrentState(), getTraceLength());
else{
InterfaceState current = getCurrentState();
double currentV = current.getValueOf(VALUEID);
double currentT = current.getValueOf(TIMEID);
if(c=='+'){
trace.add(new DummyState(currentV+1, currentT+1));
}
else if(c=='-'){
trace.add(new DummyState(currentV-1, currentT+1));
}
}
} catch (IOException e) {
throw new PlasmaSimulationException(e);
}
}
If there is no more character to read (c == -1), we throw a PlasmaDeadlockException instead of adding a new state to the trace.
The checkForErrors function is called on modification of the edition panel content and before each experimentation/simulation in simulation mode. The purpose of this function is double. Detect any syntax error and build the model before running it.
Our checkForErrors function check if the sequence contains any other characters than '+', '-' or endline (-1). In the eventuality of a syntax error, a PlasmaSyntaxException is added to the list of errors.
Note: the checkForErrors function is part of AbstractData.
@Override
public boolean checkForErrors() {
//Empty from previous erros
errors.clear();
//Verify model content
InputStream is = new ByteArrayInputStream(content.getBytes());
br = new BufferedReader(new InputStreamReader(is));
try {
while(br.ready()){
int c = br.read();
if(!(c=='+'||c=='-'||c==-1)){
errors.add(new PlasmaSyntaxException(
Character.toString((char)c)+" is not a valid command"));
}
}
} catch (IOException e) {
errors.add(new PlasmaException(e));
}
//Configuration step
//We init the initial state which could have been changed by setValueOf function
initialState = new DummyState(0, 0);
return !errors.isEmpty();
}
We also create the initial state which will be used to initialize each trace. The initialization step is done here as a reset. Indeed, we could specify a different initial value for an experiment, for instance using optimization declaration in BLTL. This would call the setValueOf method to modify the initial state.
@Override
public void setValueOf(Map<InterfaceIdentifier, Double> update) {
// This method change the initial state with a set of initial values.
for(InterfaceIdentifier id:update.keySet())
initialState.setValueOf(id, update.get(id));
}
A state object is used to store the values of the model. It inherits from the InterfaceState interface. Our state object is pretty simple as we store only two variables, the time and the value.
public class DummyState implements InterfaceState {
private double value, time;
public DummyState(double value, double time) {
this.value = value;
this.time = time;
}
The InterfaceState declares several ways of accessing and setting values. Get and set methods using String as identifiers were kept for history reasons. InterfaceIdentifier object are the main way to identify object (e.g. variable, constant) through components of PLASMA Lab. Access to a value using a String 'id_str' should have the same effect as accessing with an InterfaceIdentifier 'id' if 'id.getName().equals(id_str)'.
@Override
public Double getValueOf(InterfaceIdentifier id) {
if(id.equals(DummySimulator.VALUEID))
return value;
else if (id.equals(DummySimulator.TIMEID))
return time;
else
throw new PlasmaRunException("Unknown identifier: "+id.getName());
}
@Override
public void setValueOf(InterfaceIdentifier id, double value) {
if(id.equals(DummySimulator.VALUEID))
this.value = value;
else if (id.equals(DummySimulator.TIMEID))
this.time = value;
else
throw new PlasmaRunException("Unknown identifier: "+id.getName());
}
Except getters and setters, the relation between state objects and their associated model is free. As their can be a large number of state for a single model instance, we recommand to keep the memory usage of states as low as possible.
Identifier are a shared objects to identify values (e.g. variable, constant) through different components of PLASMA Lab. As our model has only two variables, time and value, we declared two static identifiers in the simulator.
protected static final DummyId TIMEID = new DummyId("#"); //TIME
protected static final DummyId VALUEID = new DummyId("X"); //VALUE
These identifiers are then stored in a Map, linking a String to the actual identifier. An external component, such as a checker component, would access to the identifier of a variable by getting the map through getIdentifiers.
identifiers = new HashMap<String, InterfaceIdentifier>();
//Identifier for time
identifiers.put("#", TIMEID);
//Identifier for value
identifiers.put("X", VALUEID);
We could then write a BLTL property checking if the value of the model reached a given threshold after 10 simulation steps.
F<=#10 X > 5
Trace length are computed using the getTraceLength function. Since 'TIMEID' is declared as the time identifier of the model:
@Override
public InterfaceIdentifier getTimeId() {
return TIMEID;
}
@Override
public boolean hasTime() {
//Return true if model as a dedicated time value.
//Otherwise only trace length is used.
return true;
}
We could check the property using time instead of simulation steps. This would return the same results as the previous property since time increases at the same pace than steps (we add 1 to time at each step).
F<=10 X > 5