From 3b535fdfa52a88732e97a65bb355f03246deec79 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Thu, 3 Oct 2024 21:38:15 -0400
Subject: [PATCH 01/11] Optimization: Discard subalgebras with bottom/top

Currently this doesn't work since it discards the subalgebras {a3} and {a2} which show VSP for R using Model 5.2.1.1.3
---
 vsp.py | 41 ++++++++++++++++++++++++++++++++++++++---
 1 file changed, 38 insertions(+), 3 deletions(-)

diff --git a/vsp.py b/vsp.py
index 23d6beb..52d9f43 100644
--- a/vsp.py
+++ b/vsp.py
@@ -8,7 +8,7 @@ from common import set_to_str
 from model import (
     Model, model_closure, ModelFunction, ModelValue
 )
-from logic import Implication, Operation
+from logic import Conjunction, Disjunction, Implication, Operation
 
 def preseed(
         initial_set: Set[ModelValue],
@@ -38,6 +38,33 @@ def preseed(
     same_set = candidate_preseed[1] == 0
     return candidate_preseed[0], same_set
 
+def has_top_bottom(subalgebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]):
+    """
+    Checks the subalgebra to see whether it
+    contains a top or bottom element.
+
+    Note: This does not compute the closure.
+
+    By definition,
+    The top element is any element x where x || x = x
+    The bottom element is any element x where x && x = x
+    """
+    if mconjunction is None or mdisjunction is None:
+        return False
+
+    for x in subalgebra:
+        if mconjunction(x, x) == x:
+            # print("Bottom Element Found")
+            return True
+
+        if mdisjunction(x, x) == x:
+            # print("Top Element Found")
+            return True
+
+    return False
+
+
+
 class VSP_Result:
     def __init__(
             self, has_vsp: bool, model_name: Optional[str] = None,
@@ -62,6 +89,8 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
     sharing property.
     """
     impfunction = interpretation[Implication]
+    mconjunction = interpretation.get(Conjunction)
+    mdisjunction = interpretation.get(Disjunction)
 
     # Compute I the set of tuples (x, y) where
     # x -> y does not take a designiated value
@@ -96,11 +125,17 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
 
 
         # NOTE: Optimziation before model_closure
-        # If the carrier set intersects, then move on to the next
-        # subalgebra
+        # If the two subalgebras intersect, move
+        # onto the next pair
         if len(xs & ys) > 0:
             continue
 
+        # NOTE: Optimization
+        # if either subalgebra contains top or bottom, move
+        # onto the next pair
+        if has_top_bottom(xs, mconjunction, mdisjunction) or has_top_bottom(ys, mconjunction, mdisjunction):
+            continue
+
         # Compute the closure of all operations
         # with just the xs
         carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations)

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 02/11] 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 03/11] 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 bed3d09f4abcb9c4c98784af3df757dfeed9912c Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Thu, 24 Oct 2024 21:38:36 -0400
Subject: [PATCH 04/11] Check for top and bottom within subalgebra

---
 vsp.py | 49 ++++++++++++++++++++++++++++++-------------------
 1 file changed, 30 insertions(+), 19 deletions(-)

diff --git a/vsp.py b/vsp.py
index 52d9f43..27994c0 100644
--- a/vsp.py
+++ b/vsp.py
@@ -38,31 +38,38 @@ def preseed(
     same_set = candidate_preseed[1] == 0
     return candidate_preseed[0], same_set
 
-def has_top_bottom(subalgebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]):
+
+def find_top(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]:
     """
-    Checks the subalgebra to see whether it
-    contains a top or bottom element.
-
-    Note: This does not compute the closure.
-
-    By definition,
-    The top element is any element x where x || x = x
-    The bottom element is any element x where x && x = x
+    Find the top of the order lattice.
+    T || a = T, T && a = a for all a in the carrier set
     """
     if mconjunction is None or mdisjunction is None:
-        return False
+        return None
 
-    for x in subalgebra:
-        if mconjunction(x, x) == x:
-            # print("Bottom Element Found")
-            return True
+    for x in algebra:
+        for y in algebra:
+            if mdisjunction(x, y) == x and mconjunction(x, y) == y:
+                return x
 
-        if mdisjunction(x, x) == x:
-            # print("Top Element Found")
-            return True
+    print("[Warning] Failed to find the top of the lattice")
+    return None
 
-    return False
+def find_bottom(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]:
+    """
+    Find the bottom of the order lattice
+    F || a = a, F && a = F for all a in the carrier set
+    """
+    if mconjunction is None or mdisjunction is None:
+        return None
 
+    for x in algebra:
+        for y in algebra:
+            if mdisjunction(x, y) == y and mconjunction(x, y) == x:
+                return x
+
+    print("[Warning] Failed to find the bottom of the lattice")
+    return None
 
 
 class VSP_Result:
@@ -91,6 +98,8 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
     impfunction = interpretation[Implication]
     mconjunction = interpretation.get(Conjunction)
     mdisjunction = interpretation.get(Disjunction)
+    top = find_top(model.carrier_set, mconjunction, mdisjunction)
+    bottom = find_bottom(model.carrier_set, mconjunction, mdisjunction)
 
     # Compute I the set of tuples (x, y) where
     # x -> y does not take a designiated value
@@ -133,7 +142,9 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
         # NOTE: Optimization
         # if either subalgebra contains top or bottom, move
         # onto the next pair
-        if has_top_bottom(xs, mconjunction, mdisjunction) or has_top_bottom(ys, mconjunction, mdisjunction):
+        if top is not None and (top in xs or top in ys):
+            continue
+        if bottom is not None and (bottom in xs or bottom in ys):
             continue
 
         # Compute the closure of all operations

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 05/11] 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 06/11] 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 07/11] 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 08/11] 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 af81342a7421f006f7da73af3c0ded50aa55c9e2 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Wed, 30 Oct 2024 16:11:03 -0400
Subject: [PATCH 09/11] Break out of saturation computation early when
 top/bottom are found

---
 model.py | 36 +++++++++++++++++++++++++++++++++++-
 vsp.py   | 13 +++++++++++--
 2 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/model.py b/model.py
index 46406b5..d15d094 100644
--- a/model.py
+++ b/model.py
@@ -219,15 +219,18 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode
 
 
 
-def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]):
+def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], top: Optional[ModelValue], bottom: Optional[ModelValue]) -> Set[ModelValue]:
     """
     Given an initial set of model values and a set of model functions,
     compute the complete set of model values that are closed
     under the operations.
+
+    If top or bottom is encountered, then we end the saturation procedure early.
     """
     closure_set: Set[ModelValue] = initial_set
     last_new: Set[ModelValue] = initial_set
     changed: bool = True
+    topbottom_found = False
 
     while changed:
         changed = False
@@ -251,6 +254,18 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]):
                     if element not in closure_set:
                         new_elements.add(element)
 
+                    # Optimization: Break out of computation
+                    # early when top or bottom element is foun
+                    if top is not None and element == top:
+                        topbottom_found = True
+                    if bottom is not None and element == bottom:
+                        topbottom_found = True
+                    if topbottom_found:
+                        break
+
+                if topbottom_found:
+                    break
+
                 # We don't need to compute the arguments
                 # thanks to the cache, so move onto the
                 # next function.
@@ -274,8 +289,27 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]):
                         if element not in closure_set:
                             new_elements.add(element)
 
+                        # Optimization: Break out of computation
+                        # early when top or bottom element is foun
+                        if top is not None and element == top:
+                            topbottom_found = True
+                        if bottom is not None and element == bottom:
+                            topbottom_found = True
+                        if topbottom_found:
+                            break
+
+                    if topbottom_found:
+                        break
+
+                if topbottom_found:
+                    break
+
+
         closure_set.update(new_elements)
         changed = len(new_elements) > 0
         last_new = new_elements
 
+        if topbottom_found:
+            break
+
     return closure_set
diff --git a/vsp.py b/vsp.py
index 27994c0..6982c16 100644
--- a/vsp.py
+++ b/vsp.py
@@ -149,21 +149,30 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
 
         # Compute the closure of all operations
         # with just the xs
-        carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations)
+        carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, top, bottom)
 
         # Save to cache
         if cached_xs[0] is not None and not cached_ys[1]:
             closure_cache.append((orig_xs, carrier_set_left))
 
+        if top is not None and top in carrier_set_left:
+            continue
+        if bottom is not None and bottom in carrier_set_left:
+            continue
+
 
         # Compute the closure of all operations
         # with just the ys
-        carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations)
+        carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations, top, bottom)
 
         # Save to cache
         if cached_ys[0] is not None and not cached_ys[1]:
             closure_cache.append((orig_ys, carrier_set_right))
 
+        if top is not None and top in carrier_set_right:
+            continue
+        if bottom is not None and bottom in carrier_set_right:
+            continue
 
         # If the carrier set intersects, then move on to the next
         # subalgebra

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 10/11] 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 = []

From f057ba64fccd7fb4fc1a79a42452da3e755622e0 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 5 Nov 2024 13:19:44 -0500
Subject: [PATCH 11/11] Updated interface

---
 README.md      |  8 ++++----
 parse_magic.py | 22 ----------------------
 vspursuer.py   | 35 +++++++++++++++++++++++++++++++++++
 3 files changed, 39 insertions(+), 26 deletions(-)
 create mode 100755 vspursuer.py

diff --git a/README.md b/README.md
index a96daf3..4904685 100644
--- a/README.md
+++ b/README.md
@@ -2,15 +2,15 @@
 
 Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property?
 
-(1) Generate satisfiable matrix models using `magic`.
+(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
 
 (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.
 
 ```
-python3 parse_magic.py < examples/R6
+./vspursuer.py -i examples/R6
 ```
 
-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.
+If you face any troubles, feel free to reach out. This tool also is able to generate satisfiable models given a specification (see: R.py). This is, however, much slower than MaGIC so you're better off using that.
 
+Check out the [GitHub issue tracker](https://github.com/Brandon-Rozek/matmod/issues) to see upcoming features or make your own requests.
diff --git a/parse_magic.py b/parse_magic.py
index ca9e83e..ca5d671 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -3,9 +3,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
 
 from model import Model, ModelValue, ModelFunction
@@ -17,7 +15,6 @@ from logic import (
     Disjunction,
     Operation
 )
-from vsp import has_vsp
 
 class SourceFile:
     def __init__(self, fileobj: TextIO):
@@ -594,22 +591,3 @@ def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int) -
             mapping[(x, y)] = r
 
     return ModelFunction(2, mapping, symbol)
-
-
-if __name__ == "__main__":
-    parser = argparse.ArgumentParser(description="VSP Checker")
-    parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices")
-    args = vars(parser.parse_args())
-    solutions = parse_matrices(SourceFile(sys.stdin))
-    print(f"Parsed {len(solutions)} matrices")
-    num_has_vsp = 0
-    for i, (model, interpretation) in enumerate(solutions):
-        vsp_result = has_vsp(model, interpretation)
-        print(vsp_result)
-
-        if args['verbose'] or vsp_result.has_vsp:
-            print(model)
-
-        if vsp_result.has_vsp:
-            num_has_vsp += 1
-    print(f"Tested {len(solutions)} models, {num_has_vsp} of which satisfy VSP")
diff --git a/vspursuer.py b/vspursuer.py
new file mode 100755
index 0000000..f56e2fe
--- /dev/null
+++ b/vspursuer.py
@@ -0,0 +1,35 @@
+#!/usr/bin/env python3
+import argparse
+from parse_magic import (
+    SourceFile,
+    parse_matrices
+)
+from vsp import has_vsp
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(description="VSP Checker")
+    parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices")
+    parser.add_argument("-i", type=str, help="Path to MaGIC ugly data file")
+    args = vars(parser.parse_args())
+
+    data_file_path = args.get("i")
+    if data_file_path is None:
+        data_file_path = input("Path to MaGIC Ugly Data File: ")
+
+    solutions = []
+    with open(data_file_path, "r") as data_file:
+        solutions = parse_matrices(SourceFile(data_file))
+    print(f"Parsed {len(solutions)} matrices")
+
+    num_has_vsp = 0
+    for i, (model, interpretation) in enumerate(solutions):
+        vsp_result = has_vsp(model, interpretation)
+        print(vsp_result)
+
+        if args['verbose'] or vsp_result.has_vsp:
+            print(model)
+
+        if vsp_result.has_vsp:
+            num_has_vsp += 1
+
+    print(f"Tested {len(solutions)} models, {num_has_vsp} of which satisfy VSP")