Skip to content

Instantly share code, notes, and snippets.

@tchaumeny
Last active January 6, 2024 09:34
Show Gist options
  • Save tchaumeny/93c512e0f5cfa0c36da7ea749d04ac88 to your computer and use it in GitHub Desktop.
Save tchaumeny/93c512e0f5cfa0c36da7ea749d04ac88 to your computer and use it in GitHub Desktop.
from automathon import DFA
from collections import defaultdict
from itertools import zip_longest
from math import floor
from random import randint
# See https://www21.in.tum.de/teaching/sar/SS20/9.pdf
def ineq_to_dfa(A: list[int], b: int) -> DFA:
n = len(A)
Q = set()
sigma = {bin(i)[2:].zfill(n) for i in range(2**n)}
delta = defaultdict(dict)
F = set()
W = {b}
while W:
k = W.pop()
Q.add(k)
if k >= 0:
F.add(str(k))
for s in sigma:
j = floor((k - sum(a * int(d) for a, d in zip(A, s))) / 2)
if j not in Q:
W.add(j)
delta[str(k)][s] = str(j)
# authomaton.DFA requires states to be strings
return DFA({str(q) for q in Q}, sigma, delta, str(b), F)
### Build a DFA for 2x + 3y <= 100
A = [2, 3]
b = 100
automata = ineq_to_dfa(A, b)
def encode(*args):
return ["".join(digits) for digits in zip_longest(*(bin(x)[-1:1:-1] for x in args), fillvalue="0")]
for _ in range(10):
X = tuple(randint(0, 2 * b / sum(A)) for _ in range(len(A)))
print((X, sum(a * x for a, x in zip(A, X)), automata.accept(encode(*X))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment