pablogventura / OpenDef

GNU General Public License v2.0
3 stars 0 forks source link

OpenDef

To run a definability check, you have to run:

python3 main.py < your_model.model

Where "your_model.model" is a file containing your relational model, all relations which names started with "T" are checked by Open Definability.

The output will be the answer to definability and if it's not definable, the counterexample.

Format of model files

The first line should contain each element of universe separated by a space and then a empty line. Example:

0 1 2

A relation should start with a declaration line with the name, number of tuples and arity separated by one space. Next lines sould be one for each tuple in the relation containing the relation tuple separated by a space. Finally must be a empty line. Example:

E 3 2
0 1 2
2 1 0

Interactive running on Google Colab

https://colab.research.google.com/github/pablogventura/OpenDef/blob/master/OpenDef_Running_Example.ipynb