Skip to content

pablogventura/OpenDef

Repository files navigation

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

About

No description, website, or topics provided.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published