Struggling with multi relations

I’m sure this is all very stupid, but…

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
image

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 {}

Hi,

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
}

Best,
Alcino

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)
}

So, after some experimentation, this works:

one id: freeCorrelationIDs | {
  Sender.correlationIDs' = Sender.correlationIDs + id -> m
}
Receiver.correlationIDs' = Receiver.correlationIDs

but this doesn’t find an instance

one id: freeCorrelationIDs | {
  correlationIDs' = correlationIDs + Sender->id -> m
}

Can anyone explain why?

Thx
S

Woah! This works.

Subscriber <: correlationIDs' = Subscriber <: correlationIDs + Sender -> id -> m

Confused.

Hi,

I can create correlationIDs with this model, so I don’t understand what you mean by

Here is an example of trace where two correlation ids were added to relation correlationIDs.

Best,
Alcino

I think I may have found it. There’s

run pred and run { constraint }.

What happens with run pred { constraint }?

I had assumed it would apply the predicate and add the constraint, but the Green Book and @hwayne’s docs imply that it’s one or the other.

Hi.

Yes, once you pass a formula to a run command the first parameter becomes just a label for that command (the same applies with checks and asserts).

That seems like a serious usability flaw to me. At least there should be a warning if the label is the same as a predicate name.

S

Written with thumbs. Please excuse autocorrections and errors