Trying to model a protocol, in particular that a message is associated with a correlation ID. The cut-down version is below.
If I use , var correlationIDs : Message -> one CorrelationID then I get the dreaded No instance found
If I use , var correlationIDs : Message -> CorrelationID then I get this sort of thing, and I don’t understand how the Receiver can be associated
Thanks all
abstract sig Subscriber {
, var correlationIDs : Message -> one CorrelationID
}
one sig Sender extends Subscriber {}
one sig Receiver extends Subscriber {}
enum Status { New, Started }
sig CorrelationID {}
sig Message {
, var status : one Status
}
pred start[message: Message] {
one id: CorrelationID - Subscriber.correlationIDs[Message] | {
Sender.correlationIDs' = Sender.correlationIDs ++ (message -> id)
}
message.status = Started
all s: Subscriber - Sender | s.correlationIDs' = s.correlationIDs
}
pred skip {
status' = status
correlationIDs' = correlationIDs
}
pred init {
no correlationIDs
some Message
some CorrelationID
Message.status = New
}
fact traces {
init
always (lone message: Message | start[message] or skip)
}
pred correlationIDs_used_once {
all message: Message | lone Subscriber.correlationIDs[message]
}
check correlationIDs_used_once {
always correlationIDs_used_once
}
pred show {
eventually some m: Message | m.status = Started and one Sender.correlationIDs[m]
}
run show {}
This one gives you a no instance found because it requires that at all times all subscribers (including receivers) have one CorrelationID for every possible Message. This is not possible because your init predicate directly contradicts that. I think the multiplicity you want is lone.
I believe this lone is responsible for the second problem. This constraint can be made true by having no Message satisfying start, which will happen in a “random” trace where the first step does not satisfy start and leads to a bogus second state, like the one you depict. You should use some instead.
Btw, I also don’t think you specification of start is not correct:
it allows status to change freely.
the correlationIDs can change freely between senders. Notice that Sender.correlationIDs' = Sender.correlationIDs would still be true in a state where Message0->CorrelationIDs0 is associated with Sender0 and in the next state is associated with Sender1.
Here is a specification of start I believe captures your intention:
pred start[message: Message] {
some id: CorrelationID - Subscriber.correlationIDs[Message], s : Sender {
correlationIDs' = correlationIDs + (s -> message -> id)
}
status' = status ++ message->Started
all s: Subscriber - Sender | s.correlationIDs' = s.correlationIDs
}
Thanks for responding. I applied your changes, which made the code better but I’m still not there.
I find this confusing, as I was hoping that this relationship would say that a Subscriber has some Messages, each associated with a single CorrelationID.
I’m now wondering if I should model this differently: either by reversing to Subscriber → CorrelationID → Message, or by introducing an Exchange, with a CorrelationID and some messages.
Reworked. Once again, coding in relationships improves things. But I still can’t force the creation of a correlation relationship.
abstract sig Subscriber {
, var correlationIDs : CorrelationID -> Message
}
one sig Sender extends Subscriber {}
one sig Receiver extends Subscriber {}
enum Status { New, Started }
sig CorrelationID {}
sig Message {
, var status : one Status
}
fun freeCorrelationIDs[] : set CorrelationID {
CorrelationID - ternary/mid[correlationIDs]
}
pred start[message: Message] {
some freeCorrelationIDs
one id: freeCorrelationIDs | correlationIDs' = correlationIDs + (Sender -> id -> message)
status' = status ++ message->Started
}
pred skip {
status' = status
correlationIDs' = correlationIDs
}
pred init {
no correlationIDs
some Message
some CorrelationID
Message.status = New
}
fact traces {
init
always (some message: Message | start[message] or skip)
}
