Type Error in Alloy specification

Question

In the Requirements Engineering (2007) article, "Requirement Progression In Problem Frames", there is a worked example on a traffic lights problem that I have transcribed into the Alloy editor. Unfortunately, I get the following error when testing the code.

Starting the solver...

A type error has occurred: This must be a set or relation. Instead, it has the following possible type(s): {PrimitiveBoolean}

The error is triggered by the following predicate:

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

referencing the NGPulse predicate below:

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}

Exactly. I explain on page 137 of my book why boolean is not a type in Alloy. — Daniel Jackson
Thanks to both Loic and Daniel for follow-ups and clarifications - much appreciated. — matekus

Loïc Gammaitoni Loïc Gammaitoni · Accepted Answer · 2015-07-09T08:02:02

My guess is that a set-valued expression is expected between the square brackets of odd instead of calls to the NGPulse or SGPulse predicates. Indeed, predicates are boolean-valued and not set/relation valued expressions, hence the error.

Type Error in Alloy specification

1 Answers