Here you can download our plugins and find information about them. We will update this list as we add new features. All currently available algorithms are already included in PLASMA Lab’s main libraries. We only list the available simulator and checker plugins. Some of them are already distributed with PLASMA Lab’s distribution bundles.
| Model languages / Simulator – Latest release : 1.4.4 | |||
|---|---|---|---|
| Name | Id | Description | Download links |
| RML | rml | This plugin provides a simulator for the Reactive Module Language of the model-checker PRISM. This plugin is included in the B-LTL plugin. |
|
| RML Adaptive | rmladaptive | Extension of RML for adaptive systems. This plugin is included in the B-LTL plugin. |
|
| Bio | bio | This plugin provides our biological systems simulator. This plugin is already included in PLASMA Lab’s distribution bundle. |
Release |
| MATLAB/ Simulink |
matlab | This plugin integrates MATLAB simulation engine into PLASMA Lab allowing to perform SMC experimentation over Simulink models. |
Release |
| SystemC | systemc | This plugin works with the MAG tool to perform statistical model checking on SystemC models. | Release |
| LLVM | llvm | This plugin allows to simulate LLVM program using the LODIN simulator. | Release |
| Requirement languages / Property checker – Latest release : 1.4.4 | |||
|---|---|---|---|
| Name | Id | Description | Download links |
| B-LTL | bltl | This plugin provides a checker for the B-LTL logic. This plugin is already included in PLASMA Lab’s distribution bundle. |
Release |
| A-BLTL | altl | This plugin provides a checker for the A-BLTL logic, an extension of B-LTL for adaptive systems. This plugin is included in the B-LTL plugin. |
|
| GCSL | gcsl | This plugin provides a checker for the Goal Contracts Specification Language, a high level specification language. This plugin is included in the B-LTL plugin. |
|
| Observer | observer | This plugin provides a way to write properties as observers in the RML language. This plugin is included in the B-LTL plugin. |
|
| Nested BLTL | nested | This plugin provides a B-LTL checker enhanced with the nested probability operator. This plugin is already included in PLASMA Lab’s distribution bundle. |
Release |
We recommend you to download the plugin corresponding to your PLASMA Lab version (see the build-id in the about PLASMA Lab menu).
Until PLASMA Lab version 1.2.0, plugins were integrated in the PLASMA Lab main jar and didn’t have to be downloaded on their own.
PLASMA Lab can also load custom simulator and checker plugins, as described in this tutorial.
Algorithms
Up to now all algorithms plugins are included in the core of PLASMA Lab. Most of them can be used in distributed mode. It is also possible to write custom algorithms and load them dynamically in PLASMA Lab, as described in this tutorial.
| Algorithms | |||
|---|---|---|---|
| Name | Id | Description | Distributed |
| Monte-Carlo | montecarlo | Monte-Carlo methods for probability estimation. | Yes |
| Sequential | sequential | Sequential hypothesis testing. | Yes |
| Comparison | comparison | Compare the probabilities of two different properties. | No |
| Smart sampling | smartsampling | Smart sampling Monte Carlo estimation algorithm for non-deterministic models. | Yes |
| Sequential smart sampling | seqsmartsampling | Smart sampling sequential hypothesis testing for non-deterministic models. | No |
| Importance splitting | splitting | Importance splitting algorithm for rare event estimation. | Yes |
| Cross entropy | crossentropy | Cross entropy algorithm for rare event estimation with importance sampling. | Yes |
| CUSUM | cusum | CUSUM algorithm for change detection. | No |
| Sequential nested | nestedalgo | Nested hypothesis testing algorithm (only works with the nested BLTL plugin. | No |
Additional plugins
These plugins are not part of the main release of Plasma Lab. Therefore they can be limited to specific version of Plasma Lab.
- PTASmartSampling This plugin provides a simulator, a checker and algorithms for Probabilistic Timed Automata. It uses a specific language for modelling PTA and writing property. Currently, it can only be used with the algorithms provided by the plugins.
Latest Release : 1.2, compatible with Plasma Lab 1.4.2.
Previous Release : 1.0, compatible with Plasma Lab 1.4.0. - Pi-ADL This plugin provides a simulator for Pi-ADL architecture description language.
Documentation and Download
