Untitled

from z3 import *


#State vector function per state
S_f = {0: lambda S: And(S[0],Not(S[1])),
       1: lambda S: And(S[0],Not(S[1])),
       2: lambda S: And(S[0],Not(S[1])),
       3: lambda S: And(Not(S[0]),S[1])}


edges = {
    0: [1,2],
    1: [2,3],
    2: [0],
    3: [3]
}

solver = Solver()
K = 2

#Make the state vectors
S = []

for i in range(0,K+1):
    si = []
    for attribute in ["a","b"]: #Change the attributes
        si += [Bool(f"{attribute}_{i}")]
    S += [si]


#First we make the transition system
I0 = S_f[0](S[0])
solver.add(I0)

#We add all possible transitions

#Set the initial state
Q = [0]
visited = dict()

def transition_si_sj(si,sj,k):
    return [And(S_f[si](S[k]),S_f[sj](S[k + 1]))]

for k in range(K):
    bigV = []
    Q_new = []
    while len(Q)>0:
        si = Q.pop()
        for sj in edges[si]:
            if(sj == 6):
                pass
            bigV += transition_si_sj(si,sj,k)

            #Add to the queue
            Q_new += [sj]
            visited[sj] = True

    solver.add(Or(*bigV))
    Q = Q_new

#The last states in Q are the states K depth away from the initial state
"""
Lk = []
for sk in Q:
    for si in range(7):
        for i in range(K):
            if(si != sk):
                Lk += [And(S_f[sk](S[K]),S_f[si](S[k]))]

print(Or(*Lk))

"""


#solver.add(Or(*Lk))
"""
def phi1(S,i,k):
    if(i>k):
        return False
    else:
        return Or(Not(S[i][2]),And(S[i][1],phi1(S,i+1,k)))

solver.add(phi1(S,0,K))
"""

"""def X(S,i,k):
    if(i>=k):
        return False
    else:
        return Not(S[i+1][3])
def phi2(S,i,k):
    if(i>k):
        return False
    else:
        return Or(And(S[i][3],X(S,i,k)),phi2(S,i+1,k))
        
solver.add(phi2(S,0,K))
"""

def get_solutions(s: z3.z3.Solver):
    result = s.check()
    # While we still get solutions
    while (result == z3.sat):
      m = s.model()
      yield m
      # Add new solution as a constraint
      block = []
      for var in m:
          block.append(var() != m[var])
      s.add(z3.Or(block))
      # Look for new solution
      result = s.check()


def pretty_print_all_solutions(solver):
    # Continue to find solutions as long as the solver can satisfy the constraints
    solution_count = 0
    while solver.check() == sat:
        solution_count += 1
        model = solver.model()

        # Print the current solution in a readable way
        print(f"Solution {solution_count}:")
        for d in model.decls():
            if is_true(model[d]):  # Only print variables that are True
                print(f"{d.name()} = True")
        print()

        # Add a new constraint to block the current model (to find other solutions)
        # This constraint ensures that the next solution must differ from the current one
        blocking_clause = []
        for d in model.decls():
            blocking_clause.append(d() != model[d])
        solver.add(Or(blocking_clause))

    if solution_count == 0:
        print("No solutions found.")



if __name__ == "__main__":
    if solver.check() == sat:
        print("sat")
        pretty_print_all_solutions(solver)
        """
        solutions = get_solutions(solver)
        upper_bound = 100
        r = set()
        for m, _ in zip(solutions, range(upper_bound)):
            for x in m:
                if(is_true(m[x])):
                    r.add(x)
            #print(r)
        """