We provide two different ways of using this feature:<\/p>\n
- \n
- Use PLASMA Lab SMC algorithms from within MATLAB<\/li>\n
- Launch a MATLAB session from the PLASMA Lab user interface<\/li>\n<\/ul>\n
\nFrom MATLAB\/Simulink<\/h3>\n
This MatLab App allows you to choose a Simulink model and test a B-LTL property on it using on of our three SMC algorithms (Monte Carlo, Chernoff and Sequential).<\/p>\n
![\"plasma2simulink_screenshot\"](\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/11\/plasma2simulink_screenshot-256x300.png\" "\\"PLASMA2Simulink")
<\/a>PLASMA2Simulink MatLab App<\/p><\/div>\n
How to install and use this App?<\/p>\n
- \n
- Requirements: This App was tested with MATLAB R2013a and R2013b, under Windows7 and Fedora 19.<\/li>\n
- Installation: Download PLASMA2Simulink App (latest version is 1.2.20 accessible here<\/strong><\/a>) and install it in MATLAB (Click on “Install App” in the tab “APPS”) <\/strong><\/strong>. The installer should add a PLASMA2Simulink icon in the category “My APPS”.
\n![\"PLASMA2Simulink_24\"](\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/11\/PLASMA2Simulink_24.png\")
<\/a><\/li>\n- Launch the App.<\/li>\n
- Choose a Simulink model, write your B-LTL<\/strong><\/a> requirement and choose your algorithm.
\nAlgorithm parameters are separated by spaces and are given following the order as in the PLASMA Lab tutorial<\/strong><\/a>.<\/li>\n- You are now set up, click on the “Go !” button to launch the experiment.<\/li>\n<\/ol>\n
See How does it work ?<\/strong> below for further details.<\/p>\n
\nFrom PLASMA Lab<\/h3>\n
Since PLASMA Lab v1.2.6, you can download the MATLAB\/Simulink PLASMA Lab plugin and run it from PLASMA Lab. This plugin will allow you to:<\/p>\n
- \n
- Run a Simulink model from within PLASMA Lab<\/li>\n
- Check a property on this model<\/li>\n<\/ul>\n
![\"tutoPlasmaMatlab\"](\"https:\/\/project.inria.fr\/plasma-lab\/files\/2013\/11\/tutoPlasmaMatlab-300x187.png\")
<\/a>PLASMA Lab and MATLAB\/Simuling running together<\/p><\/div>\n
How to install and use this plugin? (this was only tested on Linux)<\/p>\n
- \n
- Requirements: PLASMA Lab v1.2.6 or superior, a MATLAB\/Simulink installation accessible from the command line.<\/li>\n
- Install the MATLAB\/Simulink plugin (accessible here<\/strong><\/a>) following the instruction plugin installation<\/strong><\/a>. Or download the latest PLASMA Lab bundle already including MATLAB\/Simulink plugin — [tar.gz]<\/a> — [zip]<\/a><\/strong><\/strong>.<\/li>\n
- Run PLASMA Lab. If you are running PLASMA Lab from a terminal you should see a line indicating that the MATLAB\/Simulink model has been loaded. You can also see this by checking the information in the Help>About PLASMA Lab menu.<\/li>\n
- Create a new model for your project, and choose the MATLAB\/Simulink plugin as the type of the model. As the model compile for the first time, MATLAB\/Simulink should launch itself and load the ‘F14’ model. It may take some time. Alternatively you can download a PLASMA Lab project file already set here<\/strong><\/a>.<\/li>\n
- You are now set up and can use PLASMA Lab simulator<\/strong><\/a> or experiment<\/strong><\/a> mode.<\/li>\n<\/ol>\n
\nConfiguration of Simulink models and examples<\/h3>\n
Any Simulink model can be used by PLASMA Lab. However to provide significant results the models should present true random behaviors. This is not possible using on the shelf Simulink blocks, as random sequences generated in these blocks are always the same at each simulation. We therefore advice to include C code functions using the S-Function builder block.<\/p>\n
B-LTL requirement can be written using the standard syntax used by PLASMA Lab. The variables used in these requirements must be variables logged by Simulink. To log a signal apply the following steps:<\/p>\n
- \n
- Select a link in the Simulink model and right click on properties.<\/li>\n
- Give a name to the signal.<\/li>\n
- Check the box “Log signal data” under the tab “Logging and accessibility”<\/li>\n<\/ol>\n
We provide two examples that can be used with PLASMA Lab:<\/p>\n
- \n
- Fault-Tolerant Fuel Control System<\/strong><\/a><\/li>\n
- Temperature controller of a pig shed<\/strong><\/a><\/li>\n<\/ul>\n
\nHow does it work?<\/h3>\n
- Temperature controller of a pig shed<\/strong><\/a><\/li>\n<\/ul>\n
- Fault-Tolerant Fuel Control System<\/strong><\/a><\/li>\n