Code for constructing rLTL monitors.
Make sure you satisfy the following requirements:
- Java 11
- Apache Ant
To compile the sources, change into the root directory of this project and execute the command
ant
After compilation is has finished, execute
ant jar
to generate a jar file.
To construct an rLTL monitor, execute the following command in the root directory of the project:
java -cp 'rltlmonitor.jar:lib/*' de.mpi_sws.rltlmonitor.CommandLineInterface logic formula
The tools requires two arguments:
-
The argument
logicand be eitherrltlorltl. It specifies whether to construct an rLTL monitor or an LTL monitor. -
The argument
rLTL-formulaspecifies the (r)LTL formula for which the monitor is constructed. Note that the formula must be a single argument. Thus, you most likely need to enclose this argument with quotes (e.g.,'a U b').
The experiments consist of building an rLTL and an LTL monitor for LTL formulas on github.
You can start the experiments by running run_experiments.py without any arguments.
If necessary, grant execution permission using chmod +x ./run_experiments.py.
The script will download and format the LTL formulas. When running the experiments more than once, you can skip this step by providing a path to the spec file:
./run_experiments.py <path_to_specs>
The resulting statistics file will contain information about each LTL formula as well as the size of the resulting (r)LTL monitor.