jSSTL Eclipse plug-in

After you have installed the jSSTL Plug-In you can create a new jSSTL Project by selecting File>>New>>Other

Screen Shot 2016-04-15 at 15.09.48

and then select jSSTL Project under jSSTL Plug-In category.

Screen Shot 2016-04-15 at 15.10.00

The jSSTL Eclipse plugin uses the jSSTL API and provides an editor based on Xtext for supporting the definition of SSTL scripts and a view to visualise the results of the analyses.

plug_in_view

In the jSSTL editor it is possible to define a script that contains the list of properties that we want to analyse using jSSTL. Besides the list of formulae, each script contains the list of the variables considered in the model, a set of constants, and a list of parameters that may occur in the formula. The parameters can be declared belonging to an interval. When the monitoring procedure is performed, the user can select a specific value for each parameter in the corresponding interval. Standard expression can be used to define both constant and parameter intervals. In the script, each formula is associated with a name, that is used to select the specific property during the monitoring procedure.

script_code

The jSSTL view provides three different panels to visualise the spatial models, the relevant data declared in a script and to plot the system’s trajectories and the boolean and quantitative satisfaction signals.

signal_view

To open the jSSTL View press Window>>Show View>>Other

Screen Shot 2016-04-15 at 15.09.17

 

In the Show View dialog selects jSSTL View under jSSTL plug-in category

Screen Shot 2016-04-15 at 15.09.34