Я определил следующую модель Alloy, которая использует один объект State для указания на корни двух деревьев State.a и State.b . sig N { children: set N } fact { let p = ~children | ~p.p in iden and no iden & ^p } one sig...