Язык моделирования Alloy

Укажите ограничения, которые характеризуют двоичное красное-черное дерево.
задание:
sig Node {
children : set Node
}
sig Leaf extends Node {}
one sig Root in Node {}
sig Red, Black in Node {}
pred Invs {
// Specify the properties that characterize
// red-black binary trees inside this predicate.
// The number of points you will get is proportional to the number of correct properties.
// To check how many points you have so far you can use the different commands.
// The maximum is 5 points.

// Be careful to not overspecify!
// If some of your properties are not valid in a red-black tree you get 0 points,
// even if you have some correct properties.
// To check if you are not overspecifying you can use command NoOverspecification.
// If you are overspecifying this command will return a tree that should be possible
// but that you spec is not accepting.
}