from functools import reduce

from helpers.spec_helper import *
from interfaces.expr import Bool
from interfaces.spec import Spec


n = 2

#
rs_array, r_array = [], []
gs_array, g_array = [], []

for i in range(n):
    rs, r = sig_prop('r_'+str(i))
    gs, g = sig_prop('g_'+str(i))
    rs_array.append(rs)
    r_array.append(r)
    gs_array.append(gs)
    g_array.append(g)

#
mut_excl = Bool(True)
for i in range(n):
    mut_excl &= G(g_array[i] >>
                  ~(reduce(lambda x,y: x|y, g_array[:i], Bool(False)) |
                    reduce(lambda x,y: x|y, g_array[i+1:], Bool(False))))

#
req_is_granted = reduce(lambda x,y: x&y,
                        [G(r_array[i] >> F(g_array[i])) for i in range(n)])

#
resettability = AG(EFG(~reduce(lambda x,y: x|y, g_array)))

#
looping = reduce(lambda x,y: x&y,
                 [EFG(g_array[i]) for i in range(n)])


formula = A(mut_excl & req_is_granted) & resettability & looping
inputs = rs_array
outputs = gs_array
spec = Spec(inputs, outputs, formula)
