Z3 Timing Out

[cscaff]

Hello!

I've been using this tool for reactive synthesis with TSLMT and it's been great! I had a question though regarding Z3.
I'm working on synthesizing a cops and robber's style game played on a finite grid. We have a cop (system player) that is formally guaranteed to catch a robber (environment player).

The following specification works!

var Int cop_x
var Int cop_y

var Int robber_x
var Int robber_y

SPECIFICATION

assume {
  gte cop_x i0() && lte cop_x i6();
  gte cop_y i0() && lte cop_y i6();

  gte robber_x i0() && gte robber_y i0();
  lte robber_x i6() && lte robber_y i6();
  
}

always guarantee {
  gte cop_x i0() && lte cop_x i6();
  gte cop_y i0() && lte cop_y i6();

  ([cop_x <- cop_x] || [cop_x <- add cop_x i1()] || [cop_x <- sub cop_x i1()]);
  ([cop_y <- cop_y] || [cop_y <- add cop_y i1()] || [cop_y <- sub cop_y i1()]);

  F (eq cop_x robber_x && eq cop_y robber_y);
}

However, when I try to play with adding a third input "Robber_two", I note my Z3 times out and I'm unsure why.

var Int cop_x
var Int cop_y

var Int robber_x
var Int robber_y

var Int robber_two_x
var Int robber_two_y


SPECIFICATION

assume {
  gte cop_x i0() && lte cop_x i5();
  gte cop_y i0() && lte cop_y i5();

  eq robber_x i0() && eq robber_y i0();
  eq robber_two_x i4() && eq robber_two_y i4();
}

always guarantee {
  gte cop_x i0() && lte cop_x i5();
  gte cop_y i0() && lte cop_y i5();

  ([cop_x <- cop_x] || [cop_x <- add cop_x i1()] || [cop_x <- sub cop_x i1()]);
  ([cop_y <- cop_y] || [cop_y <- add cop_y i1()] || [cop_y <- sub cop_y i1()]);

  (F (eq cop_x robber_x && eq cop_y robber_y)) || (F (eq cop_x robber_two_x && eq cop_y robber_two_y));
}

This following spec seems trivial given the first spec. The core difference is we have a third input player (Both players are assumed to be static in this case) and we now guarantee the system player has an option to pursue either static environment player. However, when I run Issy, it looks like I get stuck in Z3.

Is this an issue with Z3 or a subtle error I am misinterpreting? Any help is appreciated. Thanks for the great tool again!

[phheim]

Hello!

I am glad to hear that you find this useful.

First, I think that I could reproduce your issue, but to be sure, could you maybe let me know the following.

• How do you use Issy (container or self-build)?
• With which options did you run the benchmarks?
• With which versions of Z3 and Spot did you run them (if not in the container)?
• And maybe on which kind of machine did you run them?

However, as you noticed, this is probably an "issue" of Z3, where it gets stuck doing quantifier elimination. In this case, it seems that the generated query gets more "complex" in the second benchmark, maybe as there are more inputs.

Unfortunately, there is no straightforward answer to this. Determining what is "complex" for Z3 is not really easy.
Also, Z3 performs differently on different machines (e.g., we noticed that some versions of it perform really well on some Macs), which in turn, as we use timeouts for some of the queries to Z3, can lead to a very different global behavior.

One option that you could try is to use a different/newer version of Z3. This can sometimes help with this, but be aware that newer is not necessarily better.

Also, if you have more questions or interesting problems you want to discuss, feel free to reach out to me.

Best,
Philippe

[cscaff]

Thanks for the help!

I built Issy from source. My Z3 and Spot were installed via HomeBrew on MacOS 15.6.1 on an M4 chip. Z3 is at Version 4.15.4. I could probably roll it back 4.13.3. Spot is at 2.14.3. I am running the benchmarks with the following options: issy --tslmt --solve --synt. Thanks again for your help!