PLASMA Lab Graphical User Interface (GUI) is composed of several elements:
We will have a later look at the experimentation panel so let’s focus on the project panel. In this panel we can edit two types of data. Models that describe our system and properties and contracts that we want to verify. For more information on models and properties see the languages page.
Download this sample project and open it in PLASMA Lab. This can be done using the File menu. You can also find more examples here.
You can now edit your model and properties. You could also create new properties and models or import them using the File menu. Be sure to select the right type when creating a new data or importing one. If you want to rename a file you can do so by right-clicking on the item you want to rename in the project explorer.
At the bottom of the edit panel you can find error messages from the properties and models you are editing as well as an indication showing the type of the selected data. It is not yet possible to change the type of a data object. As we are working with a Bounded Linear Temporal Logical (BLTL), property operators are parameterized with bound. You can now go to the experiment panel to check your model.