masterThesisProject-Piquet

This repository contains the material and tools used and implemented during my thesis project.

The tool implemented for converting log files into traces and then create samples is the traceGenerator script for which there is a dedicated repository with related documentation here.

A version of the same tool that allows, however, to obtain uncompressed traces to allow comparison between files was implemented and provided traceGeneratorNotComp.

The three folders RAL-simulation, tour-guide-robot_simulation and R1-experiments contain within them three other folders containing:

  • log_files: the log files obtained from the experiments with the different approaches (here you can see videos of the different experiments: RAL-simulation-experiments, tour-guide-robot_simulation-experiments and R1-experiments)
  • trace_folders: the folders of traces (obtained from the log files through the use of the implemented tool)
  • samples: the samples composed of the traces (obtained through the use of the implemented tool)

For the results obtained in the section of the thesis on comparing compressed and uncompressed files, the files used are:

  • test.txt to compare the difference between a compressed and an uncompressed trace
  • RAL1 and RAL_sample_notComp for comparison between a sample obtained from compressed traces and one obtained from uncompressed traces

To obtain the solutions seen in the thesis using the IIT solver, you can use the samples contained in the sample folders (or you can generate the samples from the log files using the traceGenerator tool) and use the tool that you find, with its documentation, here: learn_LTL.