Отображение производных отношений

Рассмотрим простую графическую структуру G, которая определяет пару отношений (r1 и r2) над набором X узлов. Я хочу поговорить о том, есть ли у моих графиков определенное свойство под названием wf_G. Это свойство определяется путем получения дополнительного отношения r3 из r1 и r2, а затем ограничения r3.

sig X {}

sig G { r1, r2 : X -> X }

pred wf_G [g : G] {
  let r3 = (g.r1 - iden) . (g.r2 - iden) . (g.r2 - iden) |
  one r3
}

run wf_G for 1 G, 2 X

(Я должен сказать: это очень игрушечный пример.)

Дело в том, что r3 не отображается в визуализаторе, потому что это отношение, определенное let. Я хотел бы, чтобы он отображался в визуализаторе, потому что иначе мне пришлось бы выводить его вручную в своей голове. Есть ли способ (например) аннотировать оператор let, чтобы указать визуализатору включить производное отношение, например. как следующее?

let {show} r3 = (g.r1 - iden) . (g.r2 - iden) . (g.r2 - iden) |

Мой текущий обходной путь заключается в том, чтобы включить r3 в подпись G, а затем ограничить r3 в соответствии с его определением с точки зрения r1 и r2. То есть я писал:

sig X {}

sig G { r1, r2, r3 : X -> X }

pred wf_G [g : G] {
  (g.r3) = (g.r1 - iden) . (g.r2 - iden) . (g.r2 - iden) 
  && 
  one (g.r3)
}

run wf_G for 1 G, 2 X

Это менее привлекательно, чем мой исходный код, потому что

• он объединяет примитивные отношения r1 и r2 с производным отношением r3, и

• кажется менее эффективным с вычислительной точки зрения, если сначала разрешить r3 быть любым отношением, а затем ограничить его определенным отношением (хотя я не запускал временные тесты, чтобы проверить, так ли это).

Изменить. Дэниел предложил закодировать r3 как 0-арную функцию. Я не понимаю, как это можно сделать, но я вижу, как будет работать одномерная функция:

sig X {}

sig G { r1, r2 : X -> X }

fun r3 [g : G] : X -> X {
  (g.r1 - iden) . (g.r2 - iden) . (g.r2 - iden)
}

pred wf_G [g : G] {
  one r3[g]
}

run wf_G for 1 G, 2 X

Если r3 кодируется как такая функция, можно ли показать это в визуализаторе? Это, безусловно, очень удовлетворительно решило бы мою проблему.