We have uploaded a new experimental version (1.4.5) of Plasma Lab. It includes new plugins for analyzing incomplete models (with unknowns): The plugins work with normal RML models that have atomic propositions that may take three values (1 for True, 0 for False, and -1 for Unknown). A new BLTLU…
A new version of PLASMA Lab (v1.4.4) has been released. This version adds the following updates: Correction of the distribution mechanism to limit the number of threads created. New option for controlling the frequency of the heartbeat mechanism. Update of the nested BLTL plugin: it now works with a dedicated…
We have released a new simulator plugin to run LLVM code in PLASMA Lab. The plugin is a wrapper for the external simulator LODIN developed by the Dependable System Group at the University of Kiel. It allows to run LLVM code with a stochastic semantics, notably to detect race conditions.…
A new version of PLASMA Lab (v1.4.2) has been released. This version provides several modifications and new functionalities to PLASMA LAb’s user: Reorganisation and renaming of some SMC algorithms: Merging Monte-Carlo and Chernoff algorithms: the new algorithm interface has 3 parameters, but not all are mandatory. Either “Total sample” is…
We gave a tutorial on Plasma Lab at the last SOFSEM conference in Limerick. The slides are available here. We presented the architecture of Plasma Lab, its usage and how the tool can be extended with new plugins. A post-proceedings paper on this tutorial should follow soon.
A new plugin for Plasma Lab is available. It provides a language and simulator for modeling Probabilistic Timed Automata, a property language and checker, and specific algorithms for PTA. The plugin is available on the plugin page.
A new version of PLASMA Lab (v1.4.0) has been released. This version makes some important changes on the structure of PLASMA Lab. Old versions of the plugins may not be compatible. It provides a new command line interface with more capabilities. It provides a new cross-entropy minimization algorithm for rare…
A new version of PLASMA Lab (v1.3.8) has been released. This version improves the importance splitting algorithm: Better performances. Improvement of the results display. A bug with the observers has been fixed.
A new version of PLASMA Lab (v1.3.6) has been released. This version introduces several corrections: The CUSUM algorithm has been corrected. The CUSUM interface now provides three different checks: one for the classical CUSUM algorithm, one for simulating the algorithm in order to estimate the stopping rule, and one that…
A new version of PLASMA Lab (v1.3.4) has been released. It provides a new simulator for the RML language to perform importance sampling simulations. The simulator uses special annotations of RML models to specify sampling parameters.
