Theano

Theano is a tool that checks the completeness and consistency of Requirements Tables.

Repository Folders

Requirements2Z3: contains the Eclipse project that enables converting Requirements Tables (.rt files) in z3
- antlr4: grammar
- java
- resources: four examples of Requirements Tables
Evaluation: contains the script related to the evaluation and the replication package

Install Python libraries, creating a virtual environment

python -m venv .venv
.venv\Scripts\activate
pip install -r requirements.txt

In Arguments Tabs insert the parameters, for example:

-i src/main/resources/Table1_5.rt -o src/main/resources/Table1_5.py -e BeUfVs -t completeness -b 6

All the options are explained here.

Run. At this point Python file is generated. You can run it from terminal:
```
python Table1_5.py
```

Follow instructions from point 5 of this section.

To run Theano, copy the file Theano.jar in this folder. Then run:

java -jar Theano.jar -i Table1_5.rt -o Table1_5.py -e BeUfVs -t completeness -b 6

Then, run

python Table1_5.py

The options for the java -jar Theano.jar are as follows:

i: inputFile (input file path)
o: outputFile (output file path)
t: type (consistency | completeness)
b: bound (the bound)
e: encoding (one among BeArFs | BeArVs | BeUfFs | BeUfVs | UeArFs | UeArVs | UeUfFs | UeUfVs). More details in this section.

You can also generate an .rt file from a Simulink model.

(a) In MATLAB Simulink, generate the .rt files running the following command

RT2Text("SimulinkExamples/Example1.slx")

(b) In a terminal, generate the .py from the .rt file. Run

java -jar Theano.jar -i Table1.rt -o Table1.py -e UeUfVs -t completeness

python3 Table1.py

Encoding	Bound	Trace	Semantics
UeUfFs	Unbounded	Function	Fixed Step
UeUfVs	Unbounded	Function	Variable Step
UeArFs	Unbounded	Array	Fixed Step
UeArVs	Unbounded	Array	Variable Step
BeUfFs	Bounded	Function	Fixed Step
BeUfVs	Bounded	Function	Variable Step
BeArFs	Bounded	Array	Fixed Step
BeArVs	Bounded	Array	Variable Step