Asynchronous Composition of LTL Properties over Infinite and Finite Traces - Experimental evaluation

The attached tar files contains the data of the experiments of the paper "Asynchronous Composition of LTL Properties over Infinite and Finite Traces". Experimental Outputs The directories `out`, `outEVA`, and `outEVAFinite` contain the experimental results, includingrunlim log files and the outputs produced by the executed commands. Each experiment can be re-run by executing the corresponding *non_internal.sh script.Before running the scripts, make sure to set the correct OCRA path (located in tools/ocra)inside the script. The directory models contains the various types of model used in this experimentalevaluation. The models inside models/pattern are parametrized and OCRA instantiatethem with the command 'ocra_instantiate_parametric_arch -i file.oss -p "par_name=par_val,..."'.The script `models/pattern/instantiate.sh` generates the instantiated models by providing 3 parameters:i) The path to the OCRA executableii) maximum size of the instantiated models (it generates from 1 to size) iii) The JSON files are configuration files for the experimental evaluation and forthe generation of plots/csv data. The tools directory contains:- runlim- OCRA (Othello Constraint Requirement Analysis) NOTE: For the official version of OCRA (which does not include the features describedin this paper), please refer to the following website: ocra.fbk.eu