We present ParTraP and its associated toolset, supporting a
light-weight approach to formal methods. In critical systems, such
as medical systems, it is often easy to enhance the code with
tracing information. ParTraP is a language that allows to express
properties over traces of parametric events. It is designed to
ease the understanding and writing of properties by software
engineers without background in formal methods. In the tool
demonstration videos, we present the language and its toolset:
ParTraP-IDE (evaluator, compiler, syntax directed editor) and
ParTraP-EG (generator of trace examples and counter-examples).
We recommend to use Eclipse Oxygen or later with framework
XText installed from : "https://www.eclipse.org/Xtext/"
(Choose "Download" then "Download Eclipse" then under "Download
Packages", and finally " Eclipse IDE for Java and DSL
Developers ". Unzip and click on "eclipse.exe").
You can also choose to install Eclipse DSL from the starting
menu when installing Eclipse
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.
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
Mandatory parameters are "id"
(an identifier representing the event name) and "time" (a
number: an integer or a floating point representing the event
An event can have other
Simple ParTraP properties
Here is some starting properties examples that you can edit and
test on the tool:
first CameraConnected, absence_of Temp t where t.v1<45;
EnterState ee followed_by ExitState xx where
before each EnterState ee where
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
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 is built using "Visual Studio Building tools 2015")
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
Installing Numpy: it is a Python package, mandatory for Jep to
work. You can download the last release from this link "here".
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).
Now that Jep is installed, you should exit and restart your eclipse
environment (simply restarting is not sufficient). Then you should
change the project properties by selecting "Python" in the "Partrap"
option and then checking the button "enable Python support".
Some examples with python
Now you can use python expressions in the properties. Here are
occurrence_of 3 EnterState ee where $'load profile' in
ExitState ee preceded_by EnterState es where
$fabs(es.time-ee.time)<10 and es.state==ee.state$;
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".
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
You can evaluate the satisfiable ParTraP property over the
generated traces using ParTraP-IDE (see above).
This project is partly funded by the ANR MODMED project