Certificador de ordem causal
Descreva quem sinaliza para quem entre as partes. O certificador decide se a ordem causal é definida (acíclica, com função-tempo) ou indefinida (laço causal) e emite um certificado Lean que você pode verificar com `lake`.
Exemplos:
Uma por linha ou separadas por vírgula, no formato i->j (ex.: 0->1, 1->2).