def caw(fsm, agents, phi, psi):
    """
    Return the set of states of fsm satisfying [agents][phi W psi].
    
    fsm -- a MAS representing the system
    agents -- a list of agents names
    phi -- a BDD representing the set of states of fsm satisfying phi
    psi -- a BDD representing the set of states of fsm satisfying psi
    """
    if len(fsm.fairness_constraints) == 0:
        return fp(lambda Z: psi | (phi & fsm.pre_nstrat(Z, agents)), BDD.true(fsm.bddEnc.DDmanager))
    else:

        def inner(Z):
            res = phi
            for f in fsm.fairness_constraints:
                res = res & fsm.pre_nstrat(
                    fp(
                        lambda Y: (psi & fair_gamma_states(fsm, agents)) | (Z & f) | (phi & fsm.pre_nstrat(Y, agents)),
                        BDD.false(fsm.bddEnc.DDmanager),
                    ),
                    agents,
                )
            return (psi & fair_gamma_states(fsm, agents)) | res

        return fp(inner, BDD.true(fsm.bddEnc.DDmanager))

def ceu(fsm, agents, phi, psi, strat=None):
    """
    Return the set of states of strat satisfying <agents>[phi U psi]
    under full observability in strat.
    If strat is None, strat is considered true.
    
    fsm -- a MAS representing the system
    agents -- a list of agents names
    phi -- a BDD representing the set of states of fsm satisfying phi
    psi -- a BDD representing the set of states of fsm satisfying psi
    strat -- a BDD representing allowed state/inputs pairs, or None
    
    """
    
    if len(fsm.fairness_constraints) == 0:
        return fp(lambda Z : psi | (phi & fsm.pre_strat(Z, agents, strat)),
                  BDD.false(fsm.bddEnc.DDmanager))
    else:
        nfair = nfair_gamma(fsm, agents, strat)
        def inner(Z):
            res = psi
            for f in fsm.fairness_constraints:
                nf = ~f
                res = res | fsm.pre_strat(fp(lambda Y :
                                             (phi | psi | nfair) &
                                             (Z | nf) &
                                             (psi |
                                              fsm.pre_strat(Y, agents, strat)),
                                             BDD.true(fsm.bddEnc.DDmanager)),
                                              agents, strat)
            return (psi | phi | nfair) & res
        return fp(inner, BDD.false(fsm.bddEnc.DDmanager))

 def check_free_choice(self):
     """
     Check whether this MAS satisfies the free-choice property, that is,
     in every state, the choices of actions for each agent is not
     constrained by the choices of other agents.
     
     Return the set of moves that are not present in the MAS and should,
     or that are present but should not.
     """
     
     if len(self.agents) <= 0:
         return BDD.false(self.bddEnc.DDmanager)
     
     true = BDD.true(self.bddEnc.DDmanager)
     protocols = {agent: self.protocol({agent}) for agent in self.agents}
     enabled = (self.weak_pre(self.reachable_states) &
                self.reachable_states & self.bddEnc.statesInputsMask)
     
     for s in self.pick_all_states(self.reachable_states):
         product = self.bddEnc.statesInputsMask
         for agent in self.agents:
             product &= protocols[agent] & s
         if (enabled & s) != product:
             return product.xor(enabled & s)
     return BDD.false(self.bddEnc.DDmanager)

def nfair_gamma_si(fsm, agents, strat=None):
    """
    Return the set of state/inputs pairs of strat
    in which agents can avoid a fair path in strat.
    If strat is None, it is considered true.
    
    fsm -- the model
    agents -- a list of agents names
    strat -- a BDD representing allowed state/inputs pairs, or None
    
    """
    if not strat:
        strat = BDD.true(fsm.bddEnc.DDmanager)
    
    if len(fsm.fairness_constraints) == 0:
        return BDD.false(fsm.bddEnc.DDmanager)
    else:
        def inner(Z):
            res = BDD.false(fsm.bddEnc.DDmanager)
            for f in fsm.fairness_constraints:
                nf = ~f & fsm.bddEnc.statesMask & strat
                res = res | fsm.pre_strat_si(fp(lambda Y :
                                                 (Z | nf) &
                                                 fsm.pre_strat_si(Y, agents,
                                                                  strat),
                                             BDD.true(fsm.bddEnc.DDmanager)),
                                             agents, strat)
            return res
        return fp(inner, BDD.false(fsm.bddEnc.DDmanager))

 def check_cex(self, fsm, explanation, agents, phi):
     """Check that the explanation is correct."""
     # Get the cubes
     gamma_cube = fsm.inputs_cube_for_agents(agents)
     ngamma_cube = fsm.bddEnc.inputsCube - gamma_cube
     
     # The first state satisfies the spec
     self.assertTrue(explanation.state <= cex(fsm, agents, phi))
     acts = BDD.false(fsm.bddEnc.DDmanager)
     states = BDD.false(fsm.bddEnc.DDmanager)
     for (act, succ) in explanation.successors:
         ag_action = act.forsome(ngamma_cube)
         # The successor satisfies phi
         self.assertTrue(succ.state <= phi)
         # The action is effectively possible
         self.assertTrue(act <= fsm.get_inputs_between_states(
                                              explanation.state, succ.state))
         # Accumulate states and actions
         acts = acts | act
         states = states | succ.state
     
     # The reached states are effectively the reachable states
     # through the action
     self.assertTrue(states <= fsm.post(explanation.state, ag_action))
     self.assertTrue(states >= fsm.post(explanation.state, ag_action)
                                                     & fsm.bddEnc.statesMask)
                                                     
     # The actions are effectively all the possible actions completing ag_act
     self.assertTrue(acts <= ag_action)
     self.assertTrue(acts >= ag_action & 
                   fsm.get_inputs_between_states(explanation.state, states) &
                   fsm.bddEnc.inputsMask)

def nfair_gamma_states(fsm, agents):
    """
    Return the set of states in which agents cann avoid fair paths.
    
    fsm -- the model
    agents -- a list of agents names
    """
    # NFair_Gamma = not([Gamma] G True) = <Gamma> F False
    agents = frozenset(agents)
    if agents not in __nfair_gamma_states:
        if len(fsm.fairness_constraints) == 0:
            __nfair_gamma_states[agents] = BDD.false(fsm.bddEnc.DDmanager)
        else:

            def inner(Z):
                res = BDD.false(fsm.bddEnc.DDmanager)
                for f in fsm.fairness_constraints:
                    nf = ~f  # & fsm.bddEnc.statesMask
                    res = res | fsm.pre_strat(
                        fp(lambda Y: (Z | nf) & fsm.pre_strat(Y, agents), BDD.true(fsm.bddEnc.DDmanager)), agents
                    )
                return res

            __nfair_gamma_states[agents] = fp(inner, BDD.false(fsm.bddEnc.DDmanager))
    return __nfair_gamma_states[agents]

 def check_cax(self, fsm, explanation, agents, phi):
     """Check that the explanation is correct."""
     # Get the cubes
     gamma_cube = fsm.inputs_cube_for_agents(agents)
     ngamma_cube = fsm.bddEnc.inputsCube - gamma_cube
     
     # The first state satisfies the spec
     self.assertTrue(explanation.state <= ~cex(fsm, agents, ~phi))
     acts = BDD.false(fsm.bddEnc.DDmanager)
     states = BDD.false(fsm.bddEnc.DDmanager)
     for (act, succ) in explanation.successors:
         # The successor satisfies phi
         self.assertTrue(succ.state <= phi)
         # The action is effectively possible
         self.assertTrue(act <= fsm.get_inputs_between_states(
                                              explanation.state, succ.state))
         # Accumulate states and actions
         acts = acts | act
         states = states | succ.state
     
     # The actions are effectively all the possible ones
     self.assertEqual((fsm.protocol(agents) &
                       explanation.state).forsome(fsm.bddEnc.statesCube).
                       forsome(ngamma_cube) &
                      fsm.bddEnc.statesMask,
                      acts.forsome(ngamma_cube) & fsm.bddEnc.statesMask)

def ceu(fsm, agents, phi, psi):
    """
    Return the set of states of fsm satisfying <agents>[phi U psi].
    
    fsm -- a MAS representing the system
    agents -- a list of agents names
    phi -- a BDD representing the set of states of fsm satisfying phi
    psi -- a BDD representing the set of states of fsm satisfying psi
    """
    # phi = phi & fsm.bddEnc.statesInputsMask
    # psi = psi & fsm.bddEnc.statesInputsMask

    if len(fsm.fairness_constraints) == 0:
        return fp(lambda Z: psi | (phi & fsm.pre_strat(Z, agents)), BDD.false(fsm.bddEnc.DDmanager))
    else:
        nfair = nfair_gamma_states(fsm, agents)

        def inner(Z):
            res = psi
            for f in fsm.fairness_constraints:
                nf = ~f  # & fsm.bddEnc.statesMask
                res = res | fsm.pre_strat(
                    fp(
                        lambda Y: (phi | psi | nfair) & (Z | nf) & (psi | fsm.pre_strat(Y, agents)),
                        BDD.true(fsm.bddEnc.DDmanager),
                    ),
                    agents,
                )
            return (psi | phi | nfair) & res

        return fp(inner, BDD.false(fsm.bddEnc.DDmanager))

 def test_get_false(self):
     (fsm, enc, manager) = self.init_model()
     
     false = BDD.false(manager)
     self.assertIsNotNone(false)
     self.assertTrue(false.is_false())
     self.assertFalse(false.is_true())
     self.assertTrue(false.isnot_true())
     self.assertFalse(false.isnot_false())
     self.assertTrue(false.isnot_true())
     
     false = BDD.false()
     self.assertIsNotNone(false)
     self.assertTrue(false.is_false())
     self.assertFalse(false.is_true())
     self.assertTrue(false.isnot_true())
     self.assertFalse(false.isnot_false())
     self.assertTrue(false.isnot_true())
     
     false = BDD.false()
     self.assertIsNotNone(false)
     self.assertTrue(false.is_false())
     self.assertFalse(false.is_true())
     self.assertTrue(false.isnot_true())
     self.assertFalse(false.isnot_false())
     self.assertTrue(false.isnot_true())

def eg(fsm, phi):
    """
    Return the set of states of fsm satisfying EG phi.
    
    fsm -- a MAS representing the system
    phi -- a BDD representing the set of states of fsm satisfying phi
    """
    # def inner(Z):
    #    res = Z
    #    for f in fsm.fairness_constraints:
    #        res = res & fp(lambda Y : (Z & f) | (phi & fsm.weak_pre(Y)),
    #                             BDD.false(fsm.bddEnc.DDmanager))
    #    return phi & fsm.weak_pre(res)
    #
    # r = fp(inner, BDD.true(fsm.bddEnc.DDmanager))
    # return r.forsome(fsm.bddEnc.inputsCube)

    phi = phi.forsome(fsm.bddEnc.inputsCube) & fsm.bddEnc.statesMask

    if len(fsm.fairness_constraints) == 0:
        return fp(lambda Z: phi & fsm.pre(Z), BDD.true(fsm.bddEnc.DDmanager)).forsome(fsm.bddEnc.inputsCube)
    else:

        def inner(Z):
            res = phi
            for f in fsm.fairness_constraints:
                res = res & fsm.pre(fp(lambda Y: (Z & f) | (phi & fsm.pre(Y)), BDD.false(fsm.bddEnc.DDmanager)))
            return res

        return fp(inner, BDD.true(fsm.bddEnc.DDmanager)).forsome(fsm.bddEnc.inputsCube)

def eg(fsm, phi):
    res = BDD.true(fsm.bddEnc.DDmanager)
    old = BDD.false(fsm.bddEnc.DDmanager)
    while res != old:
        old = res
        new = ex(fsm, res)
        res = res & new & phi & fsm.reachable_states
    return res

 def inner(Z):
     res = BDD.false(fsm.bddEnc.DDmanager)
     for f in fsm.fairness_constraints:
         nf = ~f  # & fsm.bddEnc.statesMask
         res = res | fsm.pre_strat(
             fp(lambda Y: (Z | nf) & fsm.pre_strat(Y, agents), BDD.true(fsm.bddEnc.DDmanager)), agents
         )
     return res

 def test_init(self):
     fsm = self.init_model()
     manager = fsm.bddEnc.DDmanager
     init = fsm.init
     
     initState = fsm.pick_one_state(init)
     
     self.assertTrue(BDD.false(manager) <= init <= BDD.true(manager))
     self.assertTrue(BDD.false(manager) < initState <= init)

 def test_true_false_equalities(self):
     (fsm, enc, manager) = self.init_model()
     
     true = BDD.true(manager)
     false = BDD.false(manager)
     
     self.assertTrue(false != true)        
     self.assertFalse(false == true)
     self.assertTrue(false == false)
     self.assertTrue(true == true)
     self.assertTrue((false != true) == (not false == true))

def eval_strat_FSF(fsm, spec):
    """
    Return the BDD representing the set of states of fsm satisfying spec.
    spec is a strategic operator <G> pi.
    
    Implement a variant of the algorithm that
    filters, splits and then filters.
    
    fsm -- a MAS representing the system;
    spec -- an AST-based ATLK specification with a top strategic operator.
    
    """
    
    if type(spec) is CAX:
        # [g] X p = ~<g> X ~p
        newspec = CEX(spec.group, Not(spec.child))
        return ~eval_strat_FSF(fsm, newspec)
        
    elif type(spec) is CAG:
        # [g] G p = ~<g> F ~p
        newspec = CEF(spec.group, Not(spec.child))
        return ~eval_strat_FSF(fsm, newspec)
        
    elif type(spec) is CAU:
        # [g][p U q] = ~<g>[ ~q W ~p & ~q ]
        newspec = CEW(spec.group,
                      Not(spec.right),
                      And(Not(spec.left), Not(spec.right)))
        return ~eval_strat_FSF(fsm, newspec)
        
    elif type(spec) is CAF:
        # [g] F p = ~<g> G ~p
        newspec = CEG(spec.group, Not(spec.child))
        return ~eval_strat_FSF(fsm, newspec)
        
    elif type(spec) is CAW:
        # [g][p W q] = ~<g>[~q U ~p & ~q]
        newspec = CEU(spec.group,
                      Not(spec.right),
                      And(Not(spec.left), Not(spec.right)))
        return ~eval_strat_FSF(fsm, newspec)
        
        
    sat = BDD.false(fsm.bddEnc.DDmanager)
    agents = {atom.value for atom in spec.group}
    
    # First filtering
    winning = filter_strat(fsm, spec, variant="FSF")
    
    if winning.is_false(): # no state/inputs pairs are winning => return false
        return winning
    
    return split_eval(fsm, spec, BDD.false(fsm.bddEnc.DDmanager),
                      winning)

 def test_true_false_xor(self):
     (fsm, enc, manager) = self.init_model()
     
     true = BDD.true(manager)
     false = BDD.false(manager)
     init = fsm.init
     
     self.assertTrue(true ^ false == true)
     self.assertTrue(true ^ true == false)
     self.assertTrue(false ^ false == false)
     self.assertTrue(init ^ true == ~init)
     self.assertTrue(init ^ false == init)

 def test_true_false_not(self):
     (fsm, enc, manager) = self.init_model()
     
     true = BDD.true(manager)
     false = BDD.false(manager)
     init = fsm.init
     
     self.assertTrue(~true == -true)
     self.assertTrue(~false == -false)
     self.assertTrue(~true == false)
     self.assertTrue(~false == true)
     self.assertTrue(false < ~init < true)

 def test_dup(self):
     (fsm, enc, manager) = self.init_model()
     
     false = BDD.false(manager)
     true = BDD.true(manager)
     init = fsm.init
     
     self.assertEqual(false, false.dup())
     self.assertEqual(true, true.dup())
     self.assertEqual(init, init.dup())
     
     self.assertNotEqual(true, init.dup())
     self.assertNotEqual(init, false.dup())

 def test_true_false_and(self):
     (fsm, enc, manager) = self.init_model()
     
     true = BDD.true(manager)
     false = BDD.false(manager)
     init = fsm.init
     
     self.assertTrue((true & false) == (true * false))
     self.assertTrue(true & false == false)
     self.assertTrue(true & true == true)
     self.assertTrue(false & false == false)
     self.assertTrue(init & true == init)
     self.assertTrue(init & false == false)

 def test_init_equalities(self):
     (fsm, enc, manager) = self.init_model()
     
     true = BDD.true(manager)
     false = BDD.false(manager)
     init = fsm.init
     
     self.assertIsNotNone(init)
     
     self.assertTrue(init != true)
     self.assertTrue(init != false)
     self.assertFalse(init == true)
     self.assertFalse(init == false)