matmod/README.md

17 lines
948 B
Markdown
Raw Normal View History

2024-10-15 10:37:44 -04:00
# VSPursuer: Verify Relevance Properties for Matrix Models with Implicative Connectives
2024-05-03 13:06:52 -04:00
2024-06-15 12:02:31 -04:00
Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property?
2024-05-03 13:06:52 -04:00
2024-06-15 12:02:31 -04:00
(1) Generate satisfiable matrix models using `magic`.
- Use the `ugly` data format as the output
- Keep in mind not all logic features in magic are supported, check out the [GitHub issue tracker](https://github.com/Brandon-Rozek/matmod/issues) to see upcoming features or make your own requests
2024-05-29 15:34:39 -04:00
2024-06-15 12:02:31 -04:00
(2) Run our tool! It will first attempt to parse all the matrices in the output file and then check for the variable sharing property one-by-one.
2024-05-29 15:34:39 -04:00
```
python3 parse_magic.py < examples/R6
2024-05-29 15:34:39 -04:00
```
2024-06-15 12:02:31 -04:00
If you face any troubles, feel free to reach out. This tool also has capabilities to generate satisfiable models given a specification (see: R.py), however, it is much slower than magic so you're better off using that.