From 99bb42b47ea264c938de2767c0b42fd6e362ed11 Mon Sep 17 00:00:00 2001
From: Joshua Moerman <joshua.moerman@ou.nl>
Date: Fri, 17 May 2024 22:06:58 +0200
Subject: [PATCH] added some command line options

---
 other/decompose_fsm.py | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/other/decompose_fsm.py b/other/decompose_fsm.py
index f124c3d..7c8c876 100644
--- a/other/decompose_fsm.py
+++ b/other/decompose_fsm.py
@@ -3,9 +3,23 @@ from pysat.card import CardEnc
 from pysat.formula import IDPool
 from pysat.formula import CNF
 
+import argparse
+
 ### Gebruik:
 # Stap 1: pip3 install python-sat
-# Stap 2: python3 decompose_fsm.py
+# Stap 2: python3 decompose_fsm.py -h
+
+parser = argparse.ArgumentParser(description="Decomposes a FSM into smaller components by remapping its outputs. Uses a SAT solver.")
+parser.add_argument('-c', '--components', type=int, default=2, help='number of components')
+parser.add_argument('-n', '--total-size', type=int, help='total number of states of the components')
+args = parser.parse_args()
+
+# als de de total_size te laag is => UNSAT => duurt lang
+c = args.components
+total_size = args.total_size
+
+assert c >= 1           # c = 1 is zinloos, maar zou moeten werken
+assert total_size >= c  # elk component heeft tenminste 1 state
 
 
 ###################################
@@ -41,16 +55,10 @@ def print_table(cell, rs, cs):
 
 ################
 # Voorbeeld data
-N = 8  # fsm heeft 2N states
+N = 8
 machine = rick_koenders_machine(N)
-
 states = [(n, b) for n in range(N) for b in [0, 1]]
 
-# We zoeken 2 componenten met gezamelijke grootte 6 (minder dan 8)
-# als de de total_size te laag is => UNSAT => duurt lang
-c = 2
-total_size = 10
-
 
 ########################
 # Encodering naar logica