Syntax and Semantics

A short introduction to the ParTraP language is also available here.

Getting started with ParTraP-IDE

Create a ParTraP project

Once you have installed the ParTraP-IDE plugin, you can create your first ParTraP project.

You should choose "New" from file menu then "Other" then "Partrap project". Enter a project name and click finish. A window asking to convert the project to an XText is opened you should validate by "OK". A project is created with all necessary materials for execution : jars and packages. An editor for ParTraP properties is opened. Now you can edit properties.

Use case examples

Sample trace files

Before executing any property, you should have a json trace file.

You can download two examples of traces anywhere on your machine from http://vasco.imag.fr/tools/partrap/traces where you have one short trace "test_trace.json" and one long trace "long_trace.json".

Traces should conform to the following constraints in order to be exploited with the ParTraP language:

• The top level element should be an array of json objects representing events.
• Each event has a set of parameters.
• Mandatory parameters are "id" (an identifier representing the event name) and "time" (a number: an integer or a floating point representing the event time-stamp).
• An event can have other parameters.

Simple ParTraP properties

Here is some starting properties examples that you can edit and test on the tool:

• VAlidTemp1: after first CameraConnected, absence_of Temp t where t.v1<45;
• ValidExit: EnterState ee followed_by ExitState xx where ee.state==xx.state;
• TrackerDetected: before each EnterState ee where ee.state=='mainCasp.TrackingConnection.TrackersVisibCheck', given last SearchTrackers st, forall type in st.types, occurrence_of TrackerDetected td where td.ty ==type;

When saving, properties are compiled and you can execute them from "src-gen" package. You can also use the ParTraP Evaluator by right click on the editor window and choosing "Interprete Properties".

Selecting a trace file

To change the trace file, you can right click on the ParTraP file from the project explorer window and choose "Update Trace File".

ParTraP Toolset with Python

To use Python expressions in the ParTraP toolset editor you should have a configured and working Jep with python. The eclipse ParTraP plugins is configured to work

• under windows 10
• with python 3.6
• using jep 3.7.1 (you can build it with "pip install jep==3.7.1")
• (jep is built using "Visual Studio Building tools 2015")

Jep Installation Guide (under windows)

To install a working Jep Version with Eclipse you should follow the steps below:

• Installing Python: from "this link".We recommend version 3.6 since it corresponds to the jep in the plugin. The Python configuration (32bits or 64 bits) should be the same as Java. It might be useful to declare the environment variable "python" with the path to the executable command.
• Installing pip: pip is already installed in Python 2 >=2.7.9 or Python 3 >=3.4. Otherwise, you can install it from "here".
• Installing Numpy: it is a Python package, mandatory for Jep to work. You can download the last release from this link "here".
• Installing Visual C++: not all versions are compatible with python. we recommend the use of the version provided by this "link" which corresponds to Visual Studio Building tools 2015.
• Installing Jep: now that all modules are installed, Jep package should be downloaded from this "link". Open a command prompt as admin with visual C++ environment variables (in the windows menu, choose Visual C++2015, locate a command prompt corresponding to your machine (32 or 64 bits), click right on this menu entry, and choose "More > Run as administrator"). In the command prompt you execute either "pip install jep" or "python setup.py install".
• Jep is installed but you have to configure it to be accessible by Eclipse. You should either add to the Windows PATH the directory "C:\Program Files\Python36\Lib\site-packages\jep", or to declare the environment variable "LD_LIBRARY_PATH" with the path to the "jep.dll" situated under python "\Lib\site-packages\jep" (setting the LD_LIBRARY_PATH is mandatory if you work on the source code of the ParTraP plugin).

Some examples with python

Now you can use python expressions in the properties. Here are some examples:

• import math
• test_py1: occurrence_of 3 EnterState ee where $'load profile' in ee.state$;
• test_py2: ExitState ee preceded_by EnterState es where $fabs(es.time-ee.time)<10 and es.state==ee.state$;
• test_py3: given last SearchTrackers st, forall type in $['P','F','T','R']$, occurrence_of TrackerDetected td where td.ty==type;

Generation of trace examples with ParTraP-EG

• Once you have installed the ParTraP-IDE and ParTraP-EG plugins, you can first create ParTraP project and ParTraP properties using ParTraP-IDE (see above).
• To generate a trace example, you can right click on the ParTraP property from the project explorer window and choose "ParTraP-EG/ Generate Trace Example".
• After generating:
  • An SMT2 file that specifies the property in SMT-LIB language is created in the folder "src-gen".
  • A JSON trace file that satisfies the property is created in the folder "trace-examples". ParTraP-EG may return UNSAT if the property is unsatisfiable, or UNKNOWN when it cannot determine whether a property is satisfiable or not.
• You can generate a trace counter-example from the negation of the property.
• You can evaluate the satisfiable ParTraP property over the generated traces using ParTraP-IDE (see above).