The variables used in these requirements must be variables logged by Simulink. We therefore advice to include C code functions using the S-Function builder block.ī-LTL requirement can be written using the standard syntax used by PLASMA Lab. This is not possible using on the shelf Simulink blocks, as random sequences generated in these blocks are always the same at each simulation. However to provide significant results the models should present true random behaviors.
Alternatively you can download a PLASMA Lab project file already set here. As the model compile for the first time, MATLAB/Simulink should launch itself and load the ‘F14’ model.
You can also see this by checking the information in the Help>About PLASMA Lab menu. If you are running PLASMA Lab from a terminal you should see a line indicating that the MATLAB/Simulink model has been loaded. Or download the latest PLASMA Lab bundle already including MATLAB/Simulink plugin.
How to install and use this plugin? (this was only tested on Linux) PLASMA Lab and MATLAB/Simuling running together