A tutorial presenting some background on temporal logic testers and the syntax used in CPSGrader.
We propose currently two methods:
File interface: The simplest method is to have the custom simulator write traces into files and grade them using the program CPSFileGrader.
C++ API interface: CPSGrader main class is STLDriver, which exposes a simple API to run tests defined in a test plan. The easiest way to get started with the C++ API is to modify CPSFileGrader.cpp by replacing the call to the read_data function by a call to the simulator, or a wrapper function which will run a simulation and write the result in a simple vector of vector of double.
Testers to be used with CPSGrader can also be automatically synthesized using labeled examples of student solutions/traces that exhibit certain desired behavior. Details of the technique are in our EMSOFT'14 paper. We also provide a small module to demonstrate how synthesis works. You will need to install the Breach MATLAB toolbox to run this module.
Download Synthesis Module (13 MB zip archive)