From 646202cb50a1f7a0effc518575a65aaa374624f3 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Thu, 24 Oct 2024 21:18:56 -0400
Subject: [PATCH 1/7] Parse custom connectives from header

---
 parse_magic.py | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index f77295a..25fc6f1 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -28,9 +28,10 @@ class SourceFile:
         return contents
 
 class UglyHeader:
-    def __init__(self, negation: bool, necessitation: bool):
+    def __init__(self, negation: bool, necessitation: bool, custom_model_functions: List[Tuple[int, str]]):
         self.negation = negation
         self.necessitation = necessitation
+        self.custom_model_functions = custom_model_functions
 
 class ModelBuilder:
     def __init__(self):
@@ -199,15 +200,21 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
 def parse_header(infile: SourceFile) -> UglyHeader:
     """
     Parse the header line from the ugly data format.
-    NOTE: Currently Incomplete.
     """
     header_line = next(infile).strip()
     header_tokens = header_line.split(" ")
     assert header_tokens[0] in ["0", "1"]
     assert header_tokens[6] in ["0", "1"]
+    assert len(header_tokens) >= 7
     negation_defined = bool(int(header_tokens[0]))
     necessitation_defined = bool(int(header_tokens[6]))
-    return UglyHeader(negation_defined, necessitation_defined)
+    num_custom_connectives = int(header_tokens[7])
+    custom_model_functions: List[Tuple[int, str]] = []
+    for i in range(num_custom_connectives):
+        arity = int(header_tokens[7 + (2 * i) + 1])
+        symbol = header_tokens[7 + (2 * i) + 2]
+        custom_model_functions.append((arity, symbol))
+    return UglyHeader(negation_defined, necessitation_defined, custom_model_functions)
 
 def carrier_set_from_size(size: int):
     """

From 312e1aeda5951f3f45a951d28c7aff50f1809a8d Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Thu, 24 Oct 2024 21:21:39 -0400
Subject: [PATCH 2/7] Updated hack to adapt for custom connective behavior

---
 parse_magic.py | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index 25fc6f1..4254d5f 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -229,10 +229,13 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]:
     """
     Parse the line representing the matrix size.
     """
+
     size = int(next(infile))
-    # HACK: The first size line may be -1 due to a bug. Skip it
-    if size == -1 and first_run:
-        size = int(next(infile))
+    # HACK: When necessitation and custom connectives are enabled
+    # MaGIC may produce -1s at the beginning of the file
+    if first_run:
+        while size == -1:
+            size = int(next(infile))
 
     if size == -1:
         return None

From 4e4e19e11795ccbda76096674465f4612b29187a Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Fri, 25 Oct 2024 14:52:12 -0400
Subject: [PATCH 3/7] Clarifying the parsing transition system

---
 parse_magic.py | 325 ++++++++++++++++++++++++++++---------------------
 1 file changed, 186 insertions(+), 139 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index 4254d5f..8e0bb76 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -21,12 +21,19 @@ class SourceFile:
     def __init__(self, fileobj: TextIO):
         self.fileobj = fileobj
         self.current_line = 0
+        self.reststr = ""
 
     def __next__(self):
+        if self.reststr != "":
+            return self.reststr
+
         contents = next(self.fileobj)
         self.current_line += 1
         return contents
 
+    def set_reststr(self, reststr: str):
+        self.reststr = reststr
+
 class UglyHeader:
     def __init__(self, negation: bool, necessitation: bool, custom_model_functions: List[Tuple[int, str]]):
         self.negation = negation
@@ -48,135 +55,212 @@ class ModelBuilder:
         self.mimplication: Optional[ModelFunction] = None
         self.num_necessitation: int = 0
         self.mnecessitation: Optional[ModelFunction] = None
+        self.custom_model_functions: List[Tuple[int, ModelFunction]]
+
+class Stage:
+    def __init__(self, name: str):
+        self.name = name
+        self.next: Optional['Stage'] = None
+        self.previous: Optional['Stage'] = None
+    def __str__(self):
+        return self.name
+
+class Stages:
+    def __init__(self):
+        self.stages: Dict[str, Stage] = {}
+        self.last_stage: Optional[Stage] = None
+    def add(self, name: str):
+        stage = Stage(name)
+        stage.next = stage
+        if self.last_stage is not None:
+            stage.previous = self.last_stage
+            self.last_stage.next = stage
+        else:
+            stage.previous = Stage("end")
+
+        self.stages[name] = stage
+        self.last_stage = stage
+    def next_stage(self, name):
+        return self.stages[name].next
+    def previous_stage(self, name):
+        return self.stages[name].previous
+    def get(self, name):
+        return self.stages[name]
+
+def derive_stages(header: UglyHeader) -> Stages:
+    stages = Stages()
+    stages.add("size")
+    if header.negation:
+        stages.add("negation")
+    stages.add("order")
+    stages.add("designated")
+    stages.add("implication")
+    if header.necessitation:
+        stages.add("necessitation")
+    # TODO: Can't use -- as that can be a custom symbol
+    # for (acidity, symbol) in header.custom_model_functions:
+        # stages.add(f"custom--{acidity}--{symbol}")
+    stages.add("process_model")
+
+    # After processing the model, go to the previous stage
+    stages.get("process_model").next = stages.get("process_model").previous
+
+    return stages
+
 
 def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
     solutions = [] # Reset
     header = parse_header(infile)
+    stages = derive_stages(header)
+    first_run = True
     current_model_parts = ModelBuilder()
-    process_sizes(infile, header, current_model_parts, solutions)
+    stage = stages.get("size")
+    while True:
+        print("Current stage:", stage)
+        match stage.name:
+            case "end":
+                break
+            case "process_model":
+                process_model(current_model_parts, solutions)
+                stage = stage.next
+            case "size":
+                processed = process_sizes(infile, current_model_parts, first_run)
+                first_run = False
+                stage = stage.next if processed else stage.previous
+            case "negation":
+                processed = process_negations(infile, current_model_parts)
+                stage = stage.next if processed else stage.previous
+            case "order":
+                processed = process_orders(infile, current_model_parts)
+                stage = stage.next if processed else stage.previous
+            case "designated":
+                processed = process_designateds(infile, current_model_parts)
+                stage = stage.next if processed else stage.previous
+            case "implication":
+                processed = process_implications(infile, current_model_parts)
+                stage = stage.next if processed else stage.previous
+            case "necessitation":
+                processed = process_necessitations(infile, current_model_parts)
+                stage = stage.next if processed else stage.previous
+            case _:
+                raise NotImplementedError("Custom Connectives are not yet supported")
+
     return solutions
 
-def process_sizes(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
-    """Stage 1"""
+def process_sizes(infile: SourceFile, current_model_parts: ModelBuilder, first_run: bool) -> bool:
+    try:
+        size = parse_size(infile, first_run)
+    except StopIteration:
+        return False
+    if size is None:
+        return False
 
-    first_run = True
+    carrier_set = carrier_set_from_size(size)
+    current_model_parts.size = size
+    current_model_parts.carrier_set = carrier_set
 
-    while True:
-        print("Processing next size")
-        try:
-            size = parse_size(infile, first_run)
-            first_run = False
-        except StopIteration:
-            # For some reason, when necessitation is enabled this doesn't
-            # have a -1 on the last line
-            break
-        if size is None:
-            break
+    # Reset counts
+    current_model_parts.num_negation = 0
+    current_model_parts.num_order = 0
+    current_model_parts.num_designated = 0
+    current_model_parts.num_implication = 0
+    current_model_parts.num_necessitation = 0
 
-        carrier_set = carrier_set_from_size(size)
-        current_model_parts.size = size
-        current_model_parts.carrier_set = carrier_set
-        process_negations(infile, header, current_model_parts, solutions)
+    return True
 
-def process_negations(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+def process_negations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
     """Stage 2 (Optional)"""
-    num_negation = 0
-    while True:
-        print("Processing next negation")
-        mnegation = None
-        if header.negation:
-            mnegation = parse_single_negation(infile, current_model_parts.size)
-            if mnegation is None:
-                break
-            num_negation += 1
+    mnegation = parse_single_negation(infile, current_model_parts.size)
+    if mnegation is None:
+        return False
 
-        current_model_parts.num_negation = num_negation
-        current_model_parts.mnegation = mnegation
+    current_model_parts.num_negation += 1
+    current_model_parts.mnegation = mnegation
 
-        process_orders(infile, header, current_model_parts, solutions)
+    # Reset counts
+    current_model_parts.num_order = 0
+    current_model_parts.num_designated = 0
+    current_model_parts.num_implication = 0
+    current_model_parts.num_necessitation = 0
 
-        if not header.negation:
-            break
+    return True
 
-def process_orders(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
     """Stage 3"""
-    num_order = 0
-    while True:
-        print("Processing next order")
-        result = parse_single_order(infile, current_model_parts.size)
-        if result is None:
-            break
-        num_order += 1
-        mconjunction, mdisjunction = result
-        current_model_parts.num_order = num_order
-        current_model_parts.mconjunction = mconjunction
-        current_model_parts.mdisjunction = mdisjunction
-        process_designateds(infile, header, current_model_parts, solutions)
+    result = parse_single_order(infile, current_model_parts.size)
+    if result is None:
+        return False
 
-def process_designateds(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+    mconjunction, mdisjunction = result
+    current_model_parts.num_order += 1
+    current_model_parts.mconjunction = mconjunction
+    current_model_parts.mdisjunction = mdisjunction
+
+    # Reset counts
+    current_model_parts.num_designated = 0
+    current_model_parts.num_implication = 0
+    current_model_parts.num_necessitation = 0
+
+    return True
+
+def process_designateds(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
     """Stage 4"""
-    num_designated = 0
-    while True:
-        print("Processing next designated")
-        designated_values = parse_single_designated(infile, current_model_parts.size)
-        if designated_values is None:
-            break
-        num_designated += 1
-        current_model_parts.num_designated = num_designated
-        current_model_parts.designated_values = designated_values
-        process_implications(infile, header, current_model_parts, solutions)
+    designated_values = parse_single_designated(infile, current_model_parts.size)
+    if designated_values is None:
+        return False
 
-def process_implications(
-    infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+    current_model_parts.num_designated += 1
+    current_model_parts.designated_values = designated_values
+
+    # Reset counts
+    current_model_parts.num_implication = 0
+    current_model_parts.num_necessitation = 0
+
+    return True
+
+def process_implications(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
     """Stage 5"""
-    if header.necessitation:
-        num_implication = 0
-        while True:
-            print("Processing next implication")
-            instr = next(infile).strip()
-            mimplication, reststr = parse_single_implication(instr, infile.current_line, current_model_parts.size)
-            if mimplication is None:
-                break
-            num_implication += 1
-            current_model_parts.num_implication = num_implication
-            current_model_parts.mimplication = mimplication
-            process_necessitations(infile, reststr, header, current_model_parts, solutions)
-    else:
-        results = parse_implications(infile, current_model_parts.size)
-        for num_implication, mimplication in enumerate(results, 1):
-            current_model_parts.num_implication = num_implication
-            current_model_parts.mimplication = mimplication
-            process_model(current_model_parts, solutions)
+    if infile.reststr == "":
+        infile.reststr = next(infile).strip()
 
-def process_necessitations(infile: SourceFile, instr: str, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+    mimplication, reststr = parse_single_implication(infile.reststr, infile.current_line, current_model_parts.size)
+    infile.reststr = reststr
+    if mimplication is None:
+        return False
 
-    # NOTE: For some reason, one necessitation table will be on the same line as the implication table
-    mnecessitation = parse_single_necessitation_from_str(instr, infile.current_line, current_model_parts.size)
-    assert mnecessitation is not None, f"Expected Necessitation Table at line {infile.current_line}"
-    num_necessitation = 1
+    current_model_parts.num_implication += 1
+    current_model_parts.mimplication = mimplication
 
-    current_model_parts.num_necessitation = num_necessitation
+     # Reset counts
+    current_model_parts.num_necessitation = 0
+
+    return True
+
+def process_necessitations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
+    # TODO: In progress
+    if infile.reststr != "":
+        infile.reststr = next(infile).strip()
+
+    # TODO: This should match the implication way of doing things when
+    # custom conenctives are involved (returning reststr)
+    mnecessitation, reststr = parse_single_necessitation_from_str(infile.reststr, infile.current_line, current_model_parts.size)
+    infile.reststr = reststr
+    if mnecessitation is None:
+        return False
+
+    current_model_parts.num_necessitation += 1
     current_model_parts.mnecessitation = mnecessitation
-    process_model(current_model_parts, solutions)
 
-    while True:
-        print("Processing next necessitation")
-        mnecessitation = parse_single_necessitation(infile, current_model_parts.size)
-        if mnecessitation is None:
-            break
-        num_necessitation += 1
-
-        current_model_parts.num_necessitation = num_necessitation
-        current_model_parts.mnecessitation = mnecessitation
-        process_model(current_model_parts, solutions)
+    return True
 
 def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
     """Create Model"""
     assert mp.mimplication is not None
     assert len(mp.carrier_set) > 0
+    assert mp.size + 1 == len(mp.carrier_set)
 
     logical_operations = { mp.mimplication }
-    model_name = f"{mp.size}{'.' + str(mp.num_negation) if mp.num_negation != 0 else ''}.{mp.num_order}.{mp.num_designated}.{mp.num_implication}{'.' + str(mp.num_necessitation) if mp.num_necessitation != 0 else ''}"
+    model_name = f"{mp.size + 1}{'.' + str(mp.num_negation) if mp.num_negation != 0 else ''}.{mp.num_order}.{mp.num_designated}.{mp.num_implication}{'.' + str(mp.num_necessitation) if mp.num_necessitation != 0 else ''}"
     model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name)
     interpretation = {
         Implication: mp.mimplication
@@ -216,7 +300,7 @@ def parse_header(infile: SourceFile) -> UglyHeader:
         custom_model_functions.append((arity, symbol))
     return UglyHeader(negation_defined, necessitation_defined, custom_model_functions)
 
-def carrier_set_from_size(size: int):
+def carrier_set_from_size(size: int) -> Set[ModelValue]:
     """
     Construct a carrier set of model values
     based on the desired size.
@@ -261,8 +345,7 @@ def parse_single_negation(infile: SourceFile, size: int) -> Optional[ModelFuncti
 
     return ModelFunction(1, mapping, "¬")
 
-
-def mvalue_from_index(i: int):
+def mvalue_from_index(i: int) -> ModelValue:
     """
     Given an index, return the
     representation of the model value.
@@ -394,7 +477,6 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model
 
     return designated_values
 
-
 def parse_single_implication(instr: str, line: int, size: int) -> Tuple[ModelFunction, str]:
     """
     Take the current string, parse an implication table from it,
@@ -423,40 +505,6 @@ def parse_single_implication(instr: str, line: int, size: int) -> Tuple[ModelFun
     reststr = " ".join(table[(size + 1)**2:])
     return mimplication, reststr
 
-
-def parse_implications(infile: SourceFile, size: int) -> List[ModelFunction]:
-    """
-    Parse the line representing the list of implication
-    tables.
-    """
-    line = next(infile).strip()
-
-    # Split and remove the last '-1' character
-    table = line.split(" ")[:-1]
-
-    assert len(table) % (size + 1)**2 == 0, f"Implication table does not match expected size at line {infile.current_line}"
-
-    table_i = 0
-    mimplications: List[ModelFunction] = []
-
-    for _ in range(len(table) // (size + 1)**2):
-        mapping = {}
-
-        for i in range(size + 1):
-            x = mvalue_from_index(i)
-            for j in range(size + 1):
-                y = mvalue_from_index(j)
-
-                r = parse_mvalue(table[table_i])
-                table_i += 1
-
-                mapping[(x, y)] = r
-
-        mimplication = ModelFunction(2, mapping, "→")
-        mimplications.append(mimplication)
-
-    return mimplications
-
 def parse_single_necessitation_from_str(instr: str, line: int, size: int) -> Optional[ModelFunction]:
     """
     Parse the line representing the necessitation table.
@@ -465,7 +513,7 @@ def parse_single_necessitation_from_str(instr: str, line: int, size: int) -> Opt
         return None
 
     row = instr.split(" ")
-    assert len(row) == size + 1, f"Necessitation table doesn't match size at line {line}"
+    assert len(row) >= size + 1, f"Necessitation table doesn't match size at line {line}"
     mapping = {}
 
     for i, j in zip(range(size + 1), row):
@@ -473,11 +521,10 @@ def parse_single_necessitation_from_str(instr: str, line: int, size: int) -> Opt
         y = parse_mvalue(j)
         mapping[(x, )] = y
 
-    return ModelFunction(1, mapping, "!")
+    mnecessitation = ModelFunction(1, mapping, "!")
+    reststr = " ".join(row[(size + 1):])
 
-def parse_single_necessitation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
-    line = next(infile).strip()
-    return parse_single_necessitation_from_str(line, infile.current_line, size)
+    return mnecessitation, reststr
 
 
 if __name__ == "__main__":

From e293e5ac3e70ab4d893bb196993cfa92131a0878 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Mon, 28 Oct 2024 11:14:33 -0400
Subject: [PATCH 4/7] Finished parse refactor

---
 parse_magic.py | 92 +++++++++++++++++++++++++++++++-------------------
 1 file changed, 57 insertions(+), 35 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index 8e0bb76..0e1166c 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -23,14 +23,31 @@ class SourceFile:
         self.current_line = 0
         self.reststr = ""
 
-    def __next__(self):
+    def next_line(self):
         if self.reststr != "":
-            return self.reststr
+            reststr = self.reststr
+            self.reststr = ""
+            return reststr
 
-        contents = next(self.fileobj)
+        contents = next(self.fileobj).strip()
         self.current_line += 1
         return contents
 
+    def __next__(self):
+        """
+        Grabs the next word token from the stream
+        """
+        if self.reststr == "":
+            self.reststr = next(self.fileobj).strip()
+            self.current_line += 1
+
+        tokens = self.reststr.split(" ")
+        next_token = tokens[0]
+        self.reststr = " ".join(tokens[1:])
+
+        return next_token
+
+
     def set_reststr(self, reststr: str):
         self.reststr = reststr
 
@@ -220,11 +237,7 @@ def process_designateds(infile: SourceFile, current_model_parts: ModelBuilder) -
 
 def process_implications(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
     """Stage 5"""
-    if infile.reststr == "":
-        infile.reststr = next(infile).strip()
-
-    mimplication, reststr = parse_single_implication(infile.reststr, infile.current_line, current_model_parts.size)
-    infile.reststr = reststr
+    mimplication = parse_single_implication(infile, current_model_parts.size)
     if mimplication is None:
         return False
 
@@ -237,14 +250,7 @@ def process_implications(infile: SourceFile, current_model_parts: ModelBuilder)
     return True
 
 def process_necessitations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
-    # TODO: In progress
-    if infile.reststr != "":
-        infile.reststr = next(infile).strip()
-
-    # TODO: This should match the implication way of doing things when
-    # custom conenctives are involved (returning reststr)
-    mnecessitation, reststr = parse_single_necessitation_from_str(infile.reststr, infile.current_line, current_model_parts.size)
-    infile.reststr = reststr
+    mnecessitation = parse_single_necessitation(infile, current_model_parts.size)
     if mnecessitation is None:
         return False
 
@@ -285,7 +291,7 @@ def parse_header(infile: SourceFile) -> UglyHeader:
     """
     Parse the header line from the ugly data format.
     """
-    header_line = next(infile).strip()
+    header_line = infile.next_line()
     header_tokens = header_line.split(" ")
     assert header_tokens[0] in ["0", "1"]
     assert header_tokens[6] in ["0", "1"]
@@ -314,12 +320,12 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]:
     Parse the line representing the matrix size.
     """
 
-    size = int(next(infile))
+    size = int(infile.next_line())
     # HACK: When necessitation and custom connectives are enabled
     # MaGIC may produce -1s at the beginning of the file
     if first_run:
         while size == -1:
-            size = int(next(infile))
+            size = int(infile.next_line())
 
     if size == -1:
         return None
@@ -330,7 +336,7 @@ def parse_single_negation(infile: SourceFile, size: int) -> Optional[ModelFuncti
     """
     Parse the line representing the negation table.
     """
-    line = next(infile).strip()
+    line = infile.next_line()
     if line == '-1':
         return None
 
@@ -410,7 +416,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
     """
     Parse the line representing the ordering table
     """
-    line = next(infile).strip()
+    line = infile.next_line()
     if line == '-1':
         return None
 
@@ -461,7 +467,7 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model
     """
     Parse the line representing which model values are designated.
     """
-    line = next(infile).strip()
+    line = infile.next_line()
     if line == '-1':
         return None
 
@@ -477,17 +483,26 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model
 
     return designated_values
 
-def parse_single_implication(instr: str, line: int, size: int) -> Tuple[ModelFunction, str]:
+def parse_single_implication(infile: SourceFile, size: int) -> Tuple[ModelFunction]:
     """
     Take the current string, parse an implication table from it,
     and return along with it the remainder of the string
     """
-    if instr == "-1":
-        return None, ""
 
-    table = instr.split(" ")
+    try:
+        first_token = next(infile)
+        if first_token == "-1":
+            return None
+    except StopIteration:
+        return None
 
-    assert len(table) >= (size + 1)**2, f"Implication table does not match expected size at line {line}"
+    table = []
+    try:
+        table = [first_token] + [next(infile) for _ in range((size + 1)**2 - 1)]
+    except StopIteration:
+        pass
+
+    assert len(table) == (size + 1)**2, f"Implication table does not match expected size at line {infile.current_line}"
 
     mapping = {}
     table_i = 0
@@ -502,18 +517,26 @@ def parse_single_implication(instr: str, line: int, size: int) -> Tuple[ModelFun
             mapping[(x, y)] = r
 
     mimplication = ModelFunction(2, mapping, "→")
-    reststr = " ".join(table[(size + 1)**2:])
-    return mimplication, reststr
+    return mimplication
 
-def parse_single_necessitation_from_str(instr: str, line: int, size: int) -> Optional[ModelFunction]:
+def parse_single_necessitation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
     """
     Parse the line representing the necessitation table.
     """
-    if instr == "-1":
+    try:
+        first_token = next(infile)
+        if first_token == "-1":
+            return None
+    except StopIteration:
         return None
 
-    row = instr.split(" ")
-    assert len(row) >= size + 1, f"Necessitation table doesn't match size at line {line}"
+    row = []
+    try:
+        row = [first_token] + [next(infile) for _ in range(size)]
+    except StopIteration:
+        pass
+
+    assert len(row) == size + 1, f"Necessitation table doesn't match size at line {infile.current_line}"
     mapping = {}
 
     for i, j in zip(range(size + 1), row):
@@ -522,9 +545,8 @@ def parse_single_necessitation_from_str(instr: str, line: int, size: int) -> Opt
         mapping[(x, )] = y
 
     mnecessitation = ModelFunction(1, mapping, "!")
-    reststr = " ".join(row[(size + 1):])
 
-    return mnecessitation, reststr
+    return mnecessitation
 
 
 if __name__ == "__main__":

From 17fb542bd048157f83699eb2dee04cc86e97ffef Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Mon, 28 Oct 2024 12:54:13 -0400
Subject: [PATCH 5/7] Progress on handling custom connectives TODO: Fix matrix
 numbering

---
 parse_magic.py | 129 ++++++++++++++++++++++++++++---------------------
 1 file changed, 74 insertions(+), 55 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index 0e1166c..1b19576 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -4,6 +4,7 @@ Parses the Magic Ugly Data File Format
 Assumes the base logic is R with no extra connectives
 """
 import argparse
+import re
 import sys
 from typing import TextIO, List, Optional, Tuple, Set, Dict
 
@@ -72,7 +73,7 @@ class ModelBuilder:
         self.mimplication: Optional[ModelFunction] = None
         self.num_necessitation: int = 0
         self.mnecessitation: Optional[ModelFunction] = None
-        self.custom_model_functions: List[Tuple[int, ModelFunction]]
+        self.custom_model_functions: Dict[str,  ModelFunction] = {}
 
 class Stage:
     def __init__(self, name: str):
@@ -89,10 +90,13 @@ class Stages:
     def add(self, name: str):
         stage = Stage(name)
         stage.next = stage
+
         if self.last_stage is not None:
             stage.previous = self.last_stage
             self.last_stage.next = stage
         else:
+            # The previous of the first stage
+            # is the end
             stage.previous = Stage("end")
 
         self.stages[name] = stage
@@ -114,9 +118,8 @@ def derive_stages(header: UglyHeader) -> Stages:
     stages.add("implication")
     if header.necessitation:
         stages.add("necessitation")
-    # TODO: Can't use -- as that can be a custom symbol
-    # for (acidity, symbol) in header.custom_model_functions:
-        # stages.add(f"custom--{acidity}--{symbol}")
+    for (adicity, symbol) in header.custom_model_functions:
+        stages.add(f"custom--{adicity}--{symbol}")
     stages.add("process_model")
 
     # After processing the model, go to the previous stage
@@ -124,7 +127,6 @@ def derive_stages(header: UglyHeader) -> Stages:
 
     return stages
 
-
 def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
     solutions = [] # Reset
     header = parse_header(infile)
@@ -160,7 +162,23 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
                 processed = process_necessitations(infile, current_model_parts)
                 stage = stage.next if processed else stage.previous
             case _:
-                raise NotImplementedError("Custom Connectives are not yet supported")
+                custom_stage = re.search(r"custom--(\d+)--(\S+)", stage.name)
+                if custom_stage is None or len(custom_stage.groups()) != 2:
+                    raise NotImplementedError(f"Unrecognized Stage: {stage.name}")
+                adicity, symbol = custom_stage.groups()
+                adicity = int(adicity)
+                if adicity == 0:
+                    # We don't need to do anything here
+                    stage = stage.next
+                elif adicity == 1:
+                    processed = process_monadic_connective(infile, symbol, current_model_parts)
+                    stage = stage.next if processed else stage.previous
+                elif adicity == 2:
+                    processed = process_dyadic_connective(infile, symbol, current_model_parts)
+                    stage = stage.next if processed else stage.previous
+                else:
+                    raise NotImplementedError("Unable to process connectives of adicity greater than 2")
+
 
     return solutions
 
@@ -259,10 +277,25 @@ def process_necessitations(infile: SourceFile, current_model_parts: ModelBuilder
 
     return True
 
+def process_monadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
+    mfunction = parse_single_monadic_connective(infile, symbol, current_model_parts.size)
+    if mfunction is None:
+        return False
+
+    current_model_parts.custom_model_functions[symbol] = mfunction
+    return True
+
+def process_dyadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
+    mfunction = parse_single_dyadic_connective(infile, symbol, current_model_parts.size)
+    if mfunction is None:
+        return False
+
+    current_model_parts.custom_model_functions[symbol] = mfunction
+    return True
+
 def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
     """Create Model"""
     assert mp.mimplication is not None
-    assert len(mp.carrier_set) > 0
     assert mp.size + 1 == len(mp.carrier_set)
 
     logical_operations = { mp.mimplication }
@@ -284,6 +317,12 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
         logical_operations.add(mp.mnecessitation)
         interpretation[Necessitation] = mp.mnecessitation
 
+    for custom_mf in mp.custom_model_functions.values():
+        if custom_mf is None:
+            logical_operations.add(custom_mf)
+        # NOTE: No need to assign interpretation
+        # for VSP check
+
     solutions.append((model, interpretation))
     print(f"Parsed Matrix {model.name}")
 
@@ -336,20 +375,7 @@ def parse_single_negation(infile: SourceFile, size: int) -> Optional[ModelFuncti
     """
     Parse the line representing the negation table.
     """
-    line = infile.next_line()
-    if line == '-1':
-        return None
-
-    row = line.split(" ")
-    assert len(row) == size + 1, f"Negation table doesn't match size at line {infile.current_line}"
-    mapping = {}
-
-    for i, j in zip(range(size + 1), row):
-        x = mvalue_from_index(i)
-        y = parse_mvalue(j)
-        mapping[(x, )] = y
-
-    return ModelFunction(1, mapping, "¬")
+    return parse_single_monadic_connective(infile, "¬", size)
 
 def mvalue_from_index(i: int) -> ModelValue:
     """
@@ -485,10 +511,33 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model
 
 def parse_single_implication(infile: SourceFile, size: int) -> Tuple[ModelFunction]:
     """
-    Take the current string, parse an implication table from it,
-    and return along with it the remainder of the string
+    Take the current string, parse an implication table from it.
     """
+    return parse_single_dyadic_connective(infile, "→", size)
 
+def parse_single_necessitation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
+    """
+    Parse the line representing the necessitation table.
+    """
+    return parse_single_monadic_connective(infile, "!", size)
+
+def parse_single_monadic_connective(infile: SourceFile, symbol: str, size: int) -> Optional[ModelFunction]:
+    line = infile.next_line()
+    if line == '-1':
+        return None
+
+    row = line.split(" ")
+    assert len(row) == size + 1, f"{symbol} table doesn't match size at line {infile.current_line}"
+    mapping = {}
+
+    for i, j in zip(range(size + 1), row):
+        x = mvalue_from_index(i)
+        y = parse_mvalue(j)
+        mapping[(x, )] = y
+
+    return ModelFunction(1, mapping, symbol)
+
+def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int) -> Optional[ModelFunction]:
     try:
         first_token = next(infile)
         if first_token == "-1":
@@ -502,7 +551,7 @@ def parse_single_implication(infile: SourceFile, size: int) -> Tuple[ModelFuncti
     except StopIteration:
         pass
 
-    assert len(table) == (size + 1)**2, f"Implication table does not match expected size at line {infile.current_line}"
+    assert len(table) == (size + 1)**2, f"{symbol} table does not match expected size at line {infile.current_line}"
 
     mapping = {}
     table_i = 0
@@ -516,37 +565,7 @@ def parse_single_implication(infile: SourceFile, size: int) -> Tuple[ModelFuncti
 
             mapping[(x, y)] = r
 
-    mimplication = ModelFunction(2, mapping, "→")
-    return mimplication
-
-def parse_single_necessitation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
-    """
-    Parse the line representing the necessitation table.
-    """
-    try:
-        first_token = next(infile)
-        if first_token == "-1":
-            return None
-    except StopIteration:
-        return None
-
-    row = []
-    try:
-        row = [first_token] + [next(infile) for _ in range(size)]
-    except StopIteration:
-        pass
-
-    assert len(row) == size + 1, f"Necessitation table doesn't match size at line {infile.current_line}"
-    mapping = {}
-
-    for i, j in zip(range(size + 1), row):
-        x = mvalue_from_index(i)
-        y = parse_mvalue(j)
-        mapping[(x, )] = y
-
-    mnecessitation = ModelFunction(1, mapping, "!")
-
-    return mnecessitation
+    return ModelFunction(2, mapping, symbol)
 
 
 if __name__ == "__main__":

From 9744f976dd466ae921c413d3d853d9eadc98afa2 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Mon, 28 Oct 2024 13:48:36 -0400
Subject: [PATCH 6/7] Fixed numbering scheme

---
 parse_magic.py | 173 ++++++++++++++++++++++++++++++-------------------
 1 file changed, 108 insertions(+), 65 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index 1b19576..840739a 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -62,16 +62,11 @@ class ModelBuilder:
     def __init__(self):
         self.size : int = 0
         self.carrier_set : Set[ModelValue] = set()
-        self.num_negation: int = 0
         self.mnegation: Optional[ModelFunction] = None
-        self.num_order: int = 0
         self.mconjunction: Optional[ModelFunction] = None
         self.mdisjunction: Optional[ModelFunction] = None
-        self.num_designated: int = 0
         self.designated_values: Set[ModelValue] = set()
-        self.num_implication: int = 0
         self.mimplication: Optional[ModelFunction] = None
-        self.num_necessitation: int = 0
         self.mnecessitation: Optional[ModelFunction] = None
         self.custom_model_functions: Dict[str,  ModelFunction] = {}
 
@@ -80,34 +75,82 @@ class Stage:
         self.name = name
         self.next: Optional['Stage'] = None
         self.previous: Optional['Stage'] = None
+        self.num = 0
+
+    def increment(self):
+        self.num += 1
+
+    def reset(self):
+        self.num = 0
+
     def __str__(self):
         return self.name
 
 class Stages:
     def __init__(self):
         self.stages: Dict[str, Stage] = {}
-        self.last_stage: Optional[Stage] = None
+        self.last_added_stage: Optional[Stage] = None
+        self.first_stage: Optional[Stage] = None
+
     def add(self, name: str):
         stage = Stage(name)
         stage.next = stage
 
-        if self.last_stage is not None:
-            stage.previous = self.last_stage
-            self.last_stage.next = stage
+        if self.last_added_stage is not None:
+            stage.previous = self.last_added_stage
+            self.last_added_stage.next = stage
         else:
             # The previous of the first stage
             # is the end
+            self.first_stage = stage
             stage.previous = Stage("end")
 
         self.stages[name] = stage
-        self.last_stage = stage
+        self.last_added_stage = stage
+
     def next_stage(self, name):
         return self.stages[name].next
+
     def previous_stage(self, name):
         return self.stages[name].previous
+
+    def reset_after(self, name):
+        stage = self.stages[name]
+        stage.reset()
+        if stage.next.name == "process_model":
+            return
+        next_stage = stage.next
+        while next_stage is not None:
+            next_stage.reset()
+            if next_stage.next.name == "process_model":
+                next_stage = None
+            else:
+                next_stage = next_stage.next
+
     def get(self, name):
         return self.stages[name]
 
+    def name(self):
+        result = ""
+        stage = self.first_stage
+        if stage is None:
+            return ""
+
+        result = f"{stage.num}"
+        if stage.next == "process_model":
+            return result
+
+        stage = stage.next
+        while stage is not None:
+            result += f".{stage.num}"
+            if stage.next.name != "process_model":
+                stage = stage.next
+            else:
+                stage = None
+
+        return result
+
+
 def derive_stages(header: UglyHeader) -> Stages:
     stages = Stages()
     stages.add("size")
@@ -135,49 +178,84 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
     current_model_parts = ModelBuilder()
     stage = stages.get("size")
     while True:
-        print("Current stage:", stage)
         match stage.name:
             case "end":
                 break
             case "process_model":
-                process_model(current_model_parts, solutions)
+                process_model(stages.name(), current_model_parts, solutions)
                 stage = stage.next
             case "size":
                 processed = process_sizes(infile, current_model_parts, first_run)
                 first_run = False
-                stage = stage.next if processed else stage.previous
+                if processed:
+                    stage.num = current_model_parts.size + 1
+                    stage = stage.next
+                else:
+                    stages.reset_after(stage.name)
+                    stage = stage.previous
             case "negation":
                 processed = process_negations(infile, current_model_parts)
-                stage = stage.next if processed else stage.previous
+                if processed:
+                    stage.increment()
+                    stage = stage.next
+                else:
+                    stages.reset_after(stage.name)
+                    stage = stage.previous
             case "order":
                 processed = process_orders(infile, current_model_parts)
-                stage = stage.next if processed else stage.previous
+                if processed:
+                    stage.increment()
+                    stage = stage.next
+                else:
+                    stages.reset_after(stage.name)
+                    stage = stage.previous
             case "designated":
                 processed = process_designateds(infile, current_model_parts)
-                stage = stage.next if processed else stage.previous
+                if processed:
+                    stage.increment()
+                    stage = stage.next
+                else:
+                    stages.reset_after(stage.name)
+                    stage = stage.previous
             case "implication":
                 processed = process_implications(infile, current_model_parts)
-                stage = stage.next if processed else stage.previous
+                if processed:
+                    stage.increment()
+                    stage = stage.next
+                else:
+                    stages.reset_after(stage.name)
+                    stage = stage.previous
             case "necessitation":
                 processed = process_necessitations(infile, current_model_parts)
-                stage = stage.next if processed else stage.previous
+                if processed:
+                    stage.increment()
+                    stage = stage.next
+                else:
+                    stages.reset_after(stage.name)
+                    stage = stage.previous
             case _:
                 custom_stage = re.search(r"custom--(\d+)--(\S+)", stage.name)
                 if custom_stage is None or len(custom_stage.groups()) != 2:
                     raise NotImplementedError(f"Unrecognized Stage: {stage.name}")
                 adicity, symbol = custom_stage.groups()
                 adicity = int(adicity)
+                processed = True
                 if adicity == 0:
                     # We don't need to do anything here
                     stage = stage.next
                 elif adicity == 1:
-                    processed = process_monadic_connective(infile, symbol, current_model_parts)
-                    stage = stage.next if processed else stage.previous
+                    processed = process_custom_monadic_connective(infile, symbol, current_model_parts)
                 elif adicity == 2:
-                    processed = process_dyadic_connective(infile, symbol, current_model_parts)
-                    stage = stage.next if processed else stage.previous
+                    processed = process_custom_dyadic_connective(infile, symbol, current_model_parts)
                 else:
-                    raise NotImplementedError("Unable to process connectives of adicity greater than 2")
+                    raise NotImplementedError("Unable to process connectives of adicity greater than c2")
+
+                if processed:
+                    stage.increment()
+                    stage = stage.next
+                else:
+                    stages.reset_after(stage.name)
+                    stage = stage.previous
 
 
     return solutions
@@ -191,15 +269,8 @@ def process_sizes(infile: SourceFile, current_model_parts: ModelBuilder, first_r
         return False
 
     carrier_set = carrier_set_from_size(size)
-    current_model_parts.size = size
     current_model_parts.carrier_set = carrier_set
-
-    # Reset counts
-    current_model_parts.num_negation = 0
-    current_model_parts.num_order = 0
-    current_model_parts.num_designated = 0
-    current_model_parts.num_implication = 0
-    current_model_parts.num_necessitation = 0
+    current_model_parts.size = size
 
     return True
 
@@ -209,15 +280,7 @@ def process_negations(infile: SourceFile, current_model_parts: ModelBuilder) ->
     if mnegation is None:
         return False
 
-    current_model_parts.num_negation += 1
     current_model_parts.mnegation = mnegation
-
-    # Reset counts
-    current_model_parts.num_order = 0
-    current_model_parts.num_designated = 0
-    current_model_parts.num_implication = 0
-    current_model_parts.num_necessitation = 0
-
     return True
 
 def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
@@ -227,15 +290,9 @@ def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> boo
         return False
 
     mconjunction, mdisjunction = result
-    current_model_parts.num_order += 1
     current_model_parts.mconjunction = mconjunction
     current_model_parts.mdisjunction = mdisjunction
 
-    # Reset counts
-    current_model_parts.num_designated = 0
-    current_model_parts.num_implication = 0
-    current_model_parts.num_necessitation = 0
-
     return True
 
 def process_designateds(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
@@ -244,13 +301,7 @@ def process_designateds(infile: SourceFile, current_model_parts: ModelBuilder) -
     if designated_values is None:
         return False
 
-    current_model_parts.num_designated += 1
     current_model_parts.designated_values = designated_values
-
-    # Reset counts
-    current_model_parts.num_implication = 0
-    current_model_parts.num_necessitation = 0
-
     return True
 
 def process_implications(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
@@ -259,12 +310,7 @@ def process_implications(infile: SourceFile, current_model_parts: ModelBuilder)
     if mimplication is None:
         return False
 
-    current_model_parts.num_implication += 1
     current_model_parts.mimplication = mimplication
-
-     # Reset counts
-    current_model_parts.num_necessitation = 0
-
     return True
 
 def process_necessitations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
@@ -272,12 +318,10 @@ def process_necessitations(infile: SourceFile, current_model_parts: ModelBuilder
     if mnecessitation is None:
         return False
 
-    current_model_parts.num_necessitation += 1
     current_model_parts.mnecessitation = mnecessitation
-
     return True
 
-def process_monadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
+def process_custom_monadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
     mfunction = parse_single_monadic_connective(infile, symbol, current_model_parts.size)
     if mfunction is None:
         return False
@@ -285,7 +329,7 @@ def process_monadic_connective(infile: SourceFile, symbol: str, current_model_pa
     current_model_parts.custom_model_functions[symbol] = mfunction
     return True
 
-def process_dyadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
+def process_custom_dyadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
     mfunction = parse_single_dyadic_connective(infile, symbol, current_model_parts.size)
     if mfunction is None:
         return False
@@ -293,13 +337,12 @@ def process_dyadic_connective(infile: SourceFile, symbol: str, current_model_par
     current_model_parts.custom_model_functions[symbol] = mfunction
     return True
 
-def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+def process_model(model_name: str, mp: ModelBuilder,  solutions: List[Tuple[Model, Dict]]):
     """Create Model"""
     assert mp.mimplication is not None
     assert mp.size + 1 == len(mp.carrier_set)
 
     logical_operations = { mp.mimplication }
-    model_name = f"{mp.size + 1}{'.' + str(mp.num_negation) if mp.num_negation != 0 else ''}.{mp.num_order}.{mp.num_designated}.{mp.num_implication}{'.' + str(mp.num_necessitation) if mp.num_necessitation != 0 else ''}"
     model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name)
     interpretation = {
         Implication: mp.mimplication
@@ -318,10 +361,10 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
         interpretation[Necessitation] = mp.mnecessitation
 
     for custom_mf in mp.custom_model_functions.values():
-        if custom_mf is None:
+        if custom_mf is not None:
             logical_operations.add(custom_mf)
-        # NOTE: No need to assign interpretation
-        # for VSP check
+            # NOTE: No need to assign interpretation
+            # for VSP check
 
     solutions.append((model, interpretation))
     print(f"Parsed Matrix {model.name}")

From 76eeee701e9dc8420d551ff7bd3cadd684a40a4c Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 5 Nov 2024 12:45:47 -0500
Subject: [PATCH 7/7] Process nullary connectives

---
 parse_magic.py | 143 ++++++++++++++++++++++---------------------------
 1 file changed, 64 insertions(+), 79 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index 840739a..ca9e83e 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -14,7 +14,8 @@ from logic import (
     Conjunction,
     Negation,
     Necessitation,
-    Disjunction
+    Disjunction,
+    Operation
 )
 from vsp import has_vsp
 
@@ -25,6 +26,11 @@ class SourceFile:
         self.reststr = ""
 
     def next_line(self):
+        """
+        Grabs the next line.
+        If reststr is populated return that, otherwise
+        consume generator
+        """
         if self.reststr != "":
             reststr = self.reststr
             self.reststr = ""
@@ -48,14 +54,13 @@ class SourceFile:
 
         return next_token
 
-
-    def set_reststr(self, reststr: str):
-        self.reststr = reststr
-
 class UglyHeader:
     def __init__(self, negation: bool, necessitation: bool, custom_model_functions: List[Tuple[int, str]]):
+        # Booleans describing the logical fragment
         self.negation = negation
         self.necessitation = necessitation
+        # List of custom model functions described as
+        # a sequence of (adicity, symbol) pairs
         self.custom_model_functions = custom_model_functions
 
 class ModelBuilder:
@@ -68,6 +73,7 @@ class ModelBuilder:
         self.designated_values: Set[ModelValue] = set()
         self.mimplication: Optional[ModelFunction] = None
         self.mnecessitation: Optional[ModelFunction] = None
+        # Map symbol to model function
         self.custom_model_functions: Dict[str,  ModelFunction] = {}
 
 class Stage:
@@ -75,6 +81,7 @@ class Stage:
         self.name = name
         self.next: Optional['Stage'] = None
         self.previous: Optional['Stage'] = None
+        # This corresponds to a portion of the model name in MaGIC
         self.num = 0
 
     def increment(self):
@@ -88,44 +95,39 @@ class Stage:
 
 class Stages:
     def __init__(self):
-        self.stages: Dict[str, Stage] = {}
-        self.last_added_stage: Optional[Stage] = None
+        end_stage = Stage("end")
+        self.stages: Dict[str, Stage] = {"end": end_stage}
+        self.last_added_stage: Stage = end_stage
         self.first_stage: Optional[Stage] = None
 
     def add(self, name: str):
         stage = Stage(name)
         stage.next = stage
 
-        if self.last_added_stage is not None:
-            stage.previous = self.last_added_stage
+        stage.previous = self.last_added_stage
+
+        # End stage is a sink so don't
+        # mark any stages as next
+        if self.last_added_stage.name != "end":
             self.last_added_stage.next = stage
         else:
-            # The previous of the first stage
-            # is the end
+            # If this is triggered, than this is the first
+            # stage added
             self.first_stage = stage
-            stage.previous = Stage("end")
 
         self.stages[name] = stage
         self.last_added_stage = stage
 
-    def next_stage(self, name):
-        return self.stages[name].next
-
-    def previous_stage(self, name):
-        return self.stages[name].previous
-
     def reset_after(self, name):
+        """
+        Resets the stage counters after a given stage.
+        This is to accurately reflect the name of the
+        model within MaGIC.
+        """
         stage = self.stages[name]
-        stage.reset()
-        if stage.next.name == "process_model":
-            return
-        next_stage = stage.next
-        while next_stage is not None:
-            next_stage.reset()
-            if next_stage.next.name == "process_model":
-                next_stage = None
-            else:
-                next_stage = next_stage.next
+        while stage.name != "process_model":
+            stage.reset()
+            stage = stage.next
 
     def get(self, name):
         return self.stages[name]
@@ -171,12 +173,12 @@ def derive_stages(header: UglyHeader) -> Stages:
     return stages
 
 def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
-    solutions = [] # Reset
+    solutions = []
     header = parse_header(infile)
     stages = derive_stages(header)
     first_run = True
     current_model_parts = ModelBuilder()
-    stage = stages.get("size")
+    stage = stages.first_stage
     while True:
         match stage.name:
             case "end":
@@ -239,16 +241,7 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
                     raise NotImplementedError(f"Unrecognized Stage: {stage.name}")
                 adicity, symbol = custom_stage.groups()
                 adicity = int(adicity)
-                processed = True
-                if adicity == 0:
-                    # We don't need to do anything here
-                    stage = stage.next
-                elif adicity == 1:
-                    processed = process_custom_monadic_connective(infile, symbol, current_model_parts)
-                elif adicity == 2:
-                    processed = process_custom_dyadic_connective(infile, symbol, current_model_parts)
-                else:
-                    raise NotImplementedError("Unable to process connectives of adicity greater than c2")
+                processed = process_custom_connective(infile, symbol, adicity, current_model_parts)
 
                 if processed:
                     stage.increment()
@@ -257,7 +250,6 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
                     stages.reset_after(stage.name)
                     stage = stage.previous
 
-
     return solutions
 
 def process_sizes(infile: SourceFile, current_model_parts: ModelBuilder, first_run: bool) -> bool:
@@ -276,7 +268,7 @@ def process_sizes(infile: SourceFile, current_model_parts: ModelBuilder, first_r
 
 def process_negations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
     """Stage 2 (Optional)"""
-    mnegation = parse_single_negation(infile, current_model_parts.size)
+    mnegation = parse_single_monadic_connective(infile, "¬", current_model_parts.size)
     if mnegation is None:
         return False
 
@@ -306,7 +298,7 @@ def process_designateds(infile: SourceFile, current_model_parts: ModelBuilder) -
 
 def process_implications(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
     """Stage 5"""
-    mimplication = parse_single_implication(infile, current_model_parts.size)
+    mimplication = parse_single_dyadic_connective(infile, "→", current_model_parts.size)
     if mimplication is None:
         return False
 
@@ -314,23 +306,23 @@ def process_implications(infile: SourceFile, current_model_parts: ModelBuilder)
     return True
 
 def process_necessitations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool:
-    mnecessitation = parse_single_necessitation(infile, current_model_parts.size)
+    mnecessitation = parse_single_monadic_connective(infile, "!", current_model_parts.size)
     if mnecessitation is None:
         return False
 
     current_model_parts.mnecessitation = mnecessitation
     return True
 
-def process_custom_monadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
-    mfunction = parse_single_monadic_connective(infile, symbol, current_model_parts.size)
-    if mfunction is None:
-        return False
+def process_custom_connective(infile: SourceFile, symbol: str, adicity: int, current_model_parts: ModelBuilder) -> bool:
+    if adicity == 0:
+        mfunction = parse_single_nullary_connective(infile, symbol)
+    elif adicity == 1:
+        mfunction = parse_single_monadic_connective(infile, symbol, current_model_parts.size)
+    elif adicity == 2:
+        mfunction = parse_single_dyadic_connective(infile, symbol, current_model_parts.size)
+    else:
+        raise NotImplementedError("Unable to process connectives of adicity greater than 2")
 
-    current_model_parts.custom_model_functions[symbol] = mfunction
-    return True
-
-def process_custom_dyadic_connective(infile: SourceFile, symbol: str, current_model_parts: ModelBuilder) -> bool:
-    mfunction = parse_single_dyadic_connective(infile, symbol, current_model_parts.size)
     if mfunction is None:
         return False
 
@@ -339,8 +331,10 @@ def process_custom_dyadic_connective(infile: SourceFile, symbol: str, current_mo
 
 def process_model(model_name: str, mp: ModelBuilder,  solutions: List[Tuple[Model, Dict]]):
     """Create Model"""
-    assert mp.mimplication is not None
+    assert mp.size > 0
     assert mp.size + 1 == len(mp.carrier_set)
+    assert len(mp.designated_values) <= len(mp.carrier_set)
+    assert mp.mimplication is not None
 
     logical_operations = { mp.mimplication }
     model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name)
@@ -363,11 +357,10 @@ def process_model(model_name: str, mp: ModelBuilder,  solutions: List[Tuple[Mode
     for custom_mf in mp.custom_model_functions.values():
         if custom_mf is not None:
             logical_operations.add(custom_mf)
-            # NOTE: No need to assign interpretation
-            # for VSP check
+            op = Operation(custom_mf.operation_name, custom_mf.arity)
+            interpretation[op] = custom_mf
 
     solutions.append((model, interpretation))
-    print(f"Parsed Matrix {model.name}")
 
 def parse_header(infile: SourceFile) -> UglyHeader:
     """
@@ -403,6 +396,7 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]:
     """
 
     size = int(infile.next_line())
+
     # HACK: When necessitation and custom connectives are enabled
     # MaGIC may produce -1s at the beginning of the file
     if first_run:
@@ -414,12 +408,6 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]:
     assert size > 0, f"Unexpected size at line {infile.current_line}"
     return size
 
-def parse_single_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
-    """
-    Parse the line representing the negation table.
-    """
-    return parse_single_monadic_connective(infile, "¬", size)
-
 def mvalue_from_index(i: int) -> ModelValue:
     """
     Given an index, return the
@@ -506,7 +494,6 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
     cmapping = {}
     dmapping = {}
 
-
     for i in range(size + 1):
         x = mvalue_from_index(i)
         for j in range(size + 1):
@@ -552,17 +539,18 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model
 
     return designated_values
 
-def parse_single_implication(infile: SourceFile, size: int) -> Tuple[ModelFunction]:
-    """
-    Take the current string, parse an implication table from it.
-    """
-    return parse_single_dyadic_connective(infile, "→", size)
 
-def parse_single_necessitation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
-    """
-    Parse the line representing the necessitation table.
-    """
-    return parse_single_monadic_connective(infile, "!", size)
+def parse_single_nullary_connective(infile: SourceFile, symbol: str) -> Optional[ModelFunction]:
+    line = infile.next_line()
+    if line == "-1":
+        return None
+
+    row = line.split(" ")
+    assert len(row) == 1, f"More than one assignment for a nullary connective was provided at line {infile.current_line}"
+
+    mapping = {}
+    mapping[()] = parse_mvalue(row[0])
+    return ModelFunction(0, mapping, symbol)
 
 def parse_single_monadic_connective(infile: SourceFile, symbol: str, size: int) -> Optional[ModelFunction]:
     line = infile.next_line()
@@ -581,11 +569,8 @@ def parse_single_monadic_connective(infile: SourceFile, symbol: str, size: int)
     return ModelFunction(1, mapping, symbol)
 
 def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int) -> Optional[ModelFunction]:
-    try:
-        first_token = next(infile)
-        if first_token == "-1":
-            return None
-    except StopIteration:
+    first_token = next(infile)
+    if first_token == "-1":
         return None
 
     table = []