def all_equiv_sat(fsm, winning, agents):
    """
    Return the states s of winning such that all states indistinguishable
    from s by agents are in winning.
    
    fsm -- a MAS representing the system;
    winning -- a BDD representing a set of states of fsm;
    agents -- a set of agents.
    
    """
    nwinning = ~winning & fsm.bddEnc.statesInputsMask
    return ~fsm.equivalent_states(nwinning & fsm.reachable_states,
        frozenset(agents)) & winning
