Тип Ошибка в спецификации сплава

Question

В статье «Технические требования» (2007) «Требование прогрессирования в проблемных кадрах» есть обработанный пример проблемы светофора, которую я переписал в редакторе Alloy. К сожалению, при тестировании кода я получаю следующую ошибку.

Запуск решателя ...

Произошла ошибка типа: Это должен быть набор или отношения. Вместо этого, он имеет следующий возможный тип (ы): {PrimitiveBoolean}

ошибка вызвана следующим предикатом:

pred LightUnitBreadcrumb [] { 
    all t: Time | 
     NGObserve [t] <=> 
      odd [NGPulse [t]] and 
     SGObserve [t] <=> 
      odd [SGPulse [t]] } 

ссылающегося предикат NGPulse ниже:

sig NGP, SGP, NRP, SRP in Time {} 
pred NGPulse [t: Time] {t in NGP} 
pred SGPulse [t: Time] {t in SGP} 
pred NRPulse [t: Time] {t in NRP} 
pred SRPulse [t: Time] {t in SRP} 

Answer 1

Точно. Я объясняю на стр. 137 моего book, почему boolean не является типом в сплаве.

Answer 2

Мое предположение заключается в том, что ожидается, что выражено множество значений между квадратными скобками odd вместо вызовов предикатов NGPulse или SGPulse. Действительно, предикаты являются булевозначными и не заданными/связанными отношениями выражениями, следовательно, ошибкой.