P2C: instrument model
Runtime checker monitors the execution by checking the events emitted during simulation or execution. To facilitate this, a model must be instrumented to emit events. In MIST, this is done by P2C. P2C takes a variant of PEDL (Primitive Event Description Language), mPEDL which defines events as the changes of predicates. The predicates, referred as conditions in mPEDL are defined on the variables in models. A sample mPEDL script is given as below,
MonScr Dog
export event isVisible, isInvisible, lost, track;
monobj int dog.vision;
monobj int dog.ball_pan_delta;
condition visibility =dogvision>10;
event isVisible= start (visibility);
event isInvisible= end (visibility);
event lost = start (dog.ball_pan_delta>10);
event track = end (dog.ball_pan_delta>10);
End
Figure 1. dog.pedl: a sample mPEDL script.
In this example, the variables being monitored are vision and ball_pan_delta in the agent dog. The detail of model, including the names of monitored variables, are hidden from runtime checker. Instead, four type of events isVisible, isInvisible, lost, and track are used to communicate the status changes of these variables to the runtime checker. For instance, event isVisible occurs when the predicate visibility changes from false to true.
Internally, mPEDL generates observers for each predicates. Events are emitted when transitions in the observers are taken. P2C has two options. If only mPEDL script is provided,
localhost> p2c dog.pedl
Then it will produce the synthesized observer for the manual instrumentation.
localhost> PEDL script parsed successfully.
localhost>The synthesized observer is output to dogObs.cn
If a model file is provided,
localhost> p2c -i examples/cleanroom/dog.cn dog.pedl
Then it will produce the synthesized observer and instrument the model file as well,
localhost> PEDL script parsed successfully.
localhost>The synthesized observer is output to dogObs.cn
localhost>The model file is given at /home/tanli/examples/dog.cn
localhost>The instrumented model file is output to /home/tanli/examples/cleanroom/dogInst.cn
In either case, P2C will assign each event with an unique id number and this information is given in the generated files.
//* isVisible 0
//* isInvisible 1
//* lost 2
//* track 3
Important: Do not edit these lines in the generated file, as M2C and its generated runtime checker refers events by their ids, not by their names. Such information is necessary to perserve the correct semantics of events when the model files are being instrumented.