File Structure

There are four folders:

SMT_GR(1)_DataSet

• Data1-Data10 are example specifications described based on constraint solving methods. Example is an example of execution.
• Date_Core_1 to Date_Core_59 is the data set for RQ2.

SpectraData
This folder contains the specifications based on Boolean encoding method for Data1-Data10 in SMT_GR(1)_DataSet.

Experiment

The data set for RQ1.

SMGR1
This is a Java project for syntax parsing. The main function is located in parserMain. It takes InputSpec.txt from Data1-Data10 in the SMT_GR(1)_DataSet folder as input, generating the intermediate file AbstractSpec.txt and a file that records various information from the initial specifications.

PythonProject
This is a Python project that includes three parts:

• Calculate unsatisfiable cores: The main function is located in Constraints.py, which takes the intermediate file AbstractSpec.txt generated by the SMGR1 project and the file recording various information from the initial specifications as input. It computes the initial conditions and all the unreachable cores, appending them to the new specifications, with the final specifications located in FinalSpec.txt.
• Example of execution: The main function is located in AutoParse.py, which parses the synthesized automaton using Example as a running example. The input automaton file is automaton.txt, produced from the final specifications generated by Constraints.py. It also reads the file recording various information from the initial specifications, converting to boolean variables based on the environment input set in the function getEnvValue() and the current state set in getCurrentValue(), according to the results parsed from automaton.txt.
• Run RQ2: The main function is located in CoreTimeTest.py, with the input being Date_Core_1 to Date_Core_59 from SMD_GR (1) _SataSet.

Using Spectra Tool for Synthesis

We synthesize the final specifications obtained by our method with the specifications described by Spectra for comparison experiments using the Spectra tool. The configuration scheme for the Spectra environment can be referenced on the website SYNTECH - Spectra (tau.ac.il), and we also list it below:

• Download and install Eclipse for Java and DSL Developers (Windows 64Bit).
• Use "Eclipse/Help/Install new software..." to install Spectra Tools from the site: http://smlab.cs.tau.ac.il/syntech/spectra/tools/update/.

After creating a Spectra project in Eclipse, copy the specifications into the .spectra file, then right-click and run Spectra/Synthesize xx Controller to obtain the strategy automaton.

How to Run

docker build -t smt:latest .
docker run -it --rm smt:latest
bash run.sh