README.md

@@ -1,16 +1,12 @@
-# Matmod: Verify Relevance Properties for Matrix Models with Implicative Connectives
+# Matmod: Matrix Model Generator for Implicative Connectives
 
-Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property?
+This repository is mostly an experiment to help
+me better understand matrix models.
 
-(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
+You're likely better off using [arranstewart/magic](https://github.com/arranstewart/magic).
 
-(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.
+We support output from magic using the ugly data format.
 
 ```
 python3 parse_magic.py < UGLY_FILE_FROM_MAGIC
 ```
-
-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.
-

parse_magic.py

@@ -80,8 +80,9 @@ def carrier_set_from_size(size: int):
 def parse_size(infile: TextIO) -> Optional[int]:
     """
     Parse the line representing the matrix size.
+    NOTE: Elements are represented in hexidecimal.
     """
-    size = int(next(infile))
+    size = int(next(infile), 16)
     if size == -1:
         return None
     assert size > 0, "Unexpected size"
@@ -109,16 +110,16 @@ def parse_negation(infile: TextIO, size: int) -> Optional[ModelFunction]:
 
 def mvalue_from_index(i: int):
     """
-    Given an index, return the
+    Given an index, return the hexidecimal
     representation of the model value.
     """
-    return ModelValue(f"a{i}")
+    return ModelValue(f"a{hex(i)[-1]}")
 
 def parse_mvalue(x: str) -> ModelValue:
     """
     Parse an element and return the model value.
     """
-    return mvalue_from_index(int(x))
+    return mvalue_from_index(int(x, 16))
 
 def determine_cresult(size: int, ordering: Dict[ModelValue, ModelValue], a: ModelValue, b: ModelValue) -> ModelValue:
     """