def pre_univ(mas, agents, states, moves):
    """
    Return the set of states q of mas such that for all moves in moves
    specifying an action for agents in q, all successors are in states.
    
    mas -- a multi-agent system;
    agents -- a subset of agents of mas;
    states -- a subset of states of mas;
    moves -- a set of moves for agents.
    """
    agents_cube = mas.inputs_cube_for_agents(agents)
    others_cube = mas.bddEnc.inputsCube - agents_cube
    states = states.forsome(mas.bddEnc.inputsCube)
    moves = moves.forsome(others_cube)
    states = states & mas.bddEnc.statesMask
    nstates = ~states & mas.bddEnc.statesMask
    moves = moves & mas.bddEnc.statesInputsMask
    res = ~((mas.weak_pre(nstates) & moves).forsome(mas.bddEnc.inputsCube) &
        mas.bddEnc.statesMask) & moves.forsome(mas.bddEnc.inputsCube)
    return res
