How to find first relation *not* of a type

Questions
1

Say I have

abstract sig Node {
  , next: lone Node
}

fact list {
  some root: Node |
    root.*next = Node
}

sig Red, Blue extends Node {}

For each red node, I want to find the next red node. So if the model is red1 -> blue1 -> blue2 -> red2 -> red3, the relationship next_red_node should be red1 -> red2 + red2 -> red3. Ideally I want this to also be fast, since my production model already takes almost a minute to write the CFG.

I’m open to adding an extra field if that’s the fastest way.

2

Hi,

Your lists currently allow circularity. If that was not the case (that is, if fact list included constraint no x : Node | x in x.^next) I think you could derive next_red_node as follows:

fun next_red_node : Node -> Node {
	{ x,y : Red | y in x.^next and no Red & x.^next & ^next.y}
}

Best,
Alcino

1 Like
3

With circularity this one seems to work:

fun next_red_node : Node -> Node {
	{ x, y : Red | x->y in next or x->y in ^(next :> Blue + Blue <: next) }
}

Either the next red node is directly connect or can be reached via a blue path.

Best,
Alcino

1 Like
4

Yeah, I meant it to be noncircular. The first works magnificently, thank you!

5

Another idea: go from red to red, with zero or more steps to a blue and then one step:

fun next_red_node : Node -> Node {
	Red -> Red & *(next :> Blue).next
}
2 Likes
6

This ended up being a LOT faster!