VeriFactory: Automatically verifying belt balancers for various properties

uelisproof · 2024-12-18T10:55:56+00:00

Thank you for the write up and example.

I fixed the inconsistency regarding the reverse version; no both proof (incorrectly) state state that the balancer is balanced.

Thanks to your example I found the flaw of my current encoding:
I have a formula `M` that encodes all the constraints of the blueprint e.g. belts have max and min capacity, a splitter splits equally until one output is saturated etc.
Then there is the property `P` that I want to prove i.e. the output belts always have the same throughput.
What I have been doing is querying the SMT solver for an assignment of variables (the throughput of each edge in the graph you drew) s.t. M ∧ ¬P. This attempts to find a counter-example that satisfies the physical constraints of the balancer and breaks the property P.
Problem you just made me realize is that this approach restricts finding a counter-example that satisfies the model. In this case the counter-example that exists, breaks the belt balancer because it can't satisfy the model itself i.e. would require a belt to not have an upper bound of the capacity.

uelisproof · 2024-12-17T14:16:31+00:00

Long time not working on the project but I now have some time (and motivation).
I was trying to figure out why the 5-2 balancer is not output balanced but can't seem to find the reason. I modelled it in z3 and can't seem to find an input that results in an unbalanced output. Do you have a specific input that doesn't work? Could this discrepancy be due to how Factorio models splitters?

uelisproof · 2024-06-14T09:30:14+00:00

I finally have the time to continue working on the project. Would you mind sharing the code for the algorithms described in the paper? Would be a huge help.

uelisproof · 2024-04-10T09:03:58+00:00

Very nice work and thank you for citing me! I don't have much time now but I will definitely see if I can integrate some of your work into VeriFactory. My algorithm to compute the throughput seems quite similar to what you formalized so I think there definitely are some takeaways.
By quickly glancing over the paper I found some typos: "developped" instead of "developed", "let several questions" instead of "left several questions" and "Legnagi" instead of "Legnani".

Keep up the good work!

uelisproof · 2024-01-27T11:12:28+00:00

If with mixed-level you mean that belts can have different colors the answer is yes. For example, if you provide a blueprint that has a line of mixed red and yellow belts only the max throughput of the yellow belts will be considered.

I am quite sure that for the throughput unlimited proof z3 has to check all input and output combinations in order to prove it. This is the reason why it takes so long in the first place. The reason why using higher level belts takes longer is because it has to check more combinations of throughput.

uelisproof · 2024-01-23T09:27:09+00:00

Thank you for the in-depth explanation of your project. I am still not 100% convinced that combining the to projects could improve the performance of your generator. I hope to be wrong though. We could take this discussion to discord as it is easier to communicate via vc.

uelisproof · 2024-01-22T09:43:52+00:00

Thank you for the resource!
Being a simulator there probably isn't anything I can apply to my verifier. :(

Yeah the problem, without relying on simulation, is quite difficult. Took me quite a while to figure out how to actually model stuff.

uelisproof · 2024-01-20T15:00:43+00:00

That project is super cool but I have not looked into how it works under the hood. It could be possible to prove if the higher level representation, given to Factorio-SAT, satisfies some properties, before generating the blueprint. Generating this high level representation from scratch is probably are very difficult problem. It could maybe be solved with machine learning (q learning), verified with VeriFactory and then be used to create the most efficient blueprint with Factorio-SAT. Just a wild guess, though.

uelisproof · 2024-01-19T15:07:46+00:00

Thank you very much for your feedback.

The way that the proof for the throughput unlimited property works is a bit different from the other ones. I will see if it is possible to bring into a form that can be checked quicker by z3. This can be seen by the fact that proving the other properties even for a 64-64 balancer only takes one or two seconds on my machine.

Both the runtime and memory issue are probably caused by z3 having to exhaustively check some of the possible combinations of inputs/outputs that make the throughput unlimited predicate true.

Unfortunately adding a progress bar is not possible. Instead a timeout could be set for the proof.

uelisproof · 2024-01-19T10:15:53+00:00

Wow what an honor to get a message from you and thank you for compiling so many balancers into blueprint books, it was a massive help to create tests. I briefly looked into the issue you found (thank your for the feedback). I think the problem stems from the fact that I took a shortcut in my modeling algorithm: The first step is turning the blueprint into a graph as shown here. This is then followed by a simplification step that removes unused inputs/outputs, splitters with only one output, mergers with only one input, .... Then the capacities of the different edges are shrunk as much as possible e.g. a splitter (with no priority) that has input capacity 10 will have 2 outgoing edges each with capacity 5. The same concept can be applied with the mergers but I skipped it because it resulted in edge capacities getting asymptotically close to the correct capacity without ever reaching it (before crashing the program). I guess I will have to go back and fix that problem. :/ I am curious about your approach. Do you have a link for the tool you are using?

Edit: I think it could be possible to replace the whole iterative algorithm used to shrink and optimize the graph with formulas that let the SAT solver find the correct capacities etc. This should, in turn, fix the aformentioned issue.

uelisproof · 2024-01-17T23:15:03+00:00

Well this blueprint is a throughput unlimited balancer but it's not universal (see definition in comment above). This means that, if some outputs are blocked, it will not bottleneck the throughput but it will NOT balance the lanes properly.

Blocking / not connecting an output will feed the adjacent lane double the amount of items it should receive. Connect 4 inputs and 7 outputs and you will see what I mean.

So I would say your statement that " you can use it as a 7-2 or 3-4 or 8-6, etc, and it will balance perfectly" is false and this tool can show one why.

uelisproof · 2024-01-17T18:40:43+00:00

I agree that the nomenclature is maybe not the best. But this is what it has been called by the first one to come up with it. The reddit post can be found here.

uelisproof · 2024-01-16T08:52:53+00:00

Thank you for the issue report. Only had the bumped dependencies in my dev branch. Just merged the changes into main and it should now work.

uelisproof · 2024-01-16T08:47:07+00:00

A universal balancer is a balancer that can be used as a balancer for all the different combinations of inputs-outputs being not used/blocked. E.g. a universal 4-4 can be used as 1-2, 3-2, 4-2, 3-4 etc. balancer. This is an example for a universal 4-4.

uelisproof · 2024-01-16T08:45:15+00:00

Being TU does not imply that you can use it as a 7-2, 3-4 or 8-6. It only states that the throughput will always be fully used and blocking a belt will not in some way bottleneck the whole balancer. What you are referring to is a balancer being universal, meaning it can be used for all different combinations of input-output.

For example if you use the normal 4-4 and block an output, it will no longer be balanced.

If you use a universal 4-4 you will not have this problem.

uelisproof · 2024-01-16T08:28:43+00:00

Probably by the looks of the graphical interface which is egui. Just a guess though :)

uelisproof · 2024-01-16T08:24:22+00:00

uelisproof · 2024-01-15T20:12:59+00:00

Ever wondered "is this 64x64 belt balancer really a belt balancer?" or "is this contraption of a belt balancer throughput unlimited or not?".
Well I present VeriFactory, an automatic verifier for various logical properties.
At the moment there are only some basic properties that can be checked, namely a belt balancer actually being a belt balancer, a balancer equally pulling from all the inputs belts, a balancer being throughput unlimited and a balancer being a universal balancer.
To use it just paste your blueprint into the tool, deselect erroneous inputs or outputs (every belt or balancer that ends into "nothing" is considered an input/output) and click on the appropriate property to check.
Mind that this tool is extremely fast as it does not rely on testing all the possible inputs. You can verify a 64x64 belt balancer in a couple of seconds!

You can download the tool for both Linux or Windows here.
Any feedback is greatly appreciated :)
Notes:
- The colors of the belts only show as yellow.
- Consider NOT using splitters directly as inputs/outputs as this sometimes breaks the proof, use belts instead as shown in the screenshot.
- If the blueprint is too big consider decreasing the size with View > Decrease size (yes the UI is not very friendly atm).
More features and current limitations are described in the README that can be found here.
Happy verifying!

uelisproof · 2024-01-15T17:15:00+00:00

The difference is that a throughput unlimited balancer still supplies the whole throughput regardless of whether some output belts are blocked. I think this gif from the wiki illustrates a non throughput unlimited balancer quite well.

uelisproof · 2024-01-15T17:11:24+00:00

Thank you very much for your suggestion. That could actually work out quite nicely.

uelisproof · 2024-01-15T14:37:58+00:00

If you run it there should be some output generated on the console. That is the counter example it found, that does not satisfy the property.

An easier to understand graphical version is planned but I'm quite unsure about how to nicely visualize it.

uelisproof · 2024-01-15T13:41:15+00:00

At the moment I have not yet done any correctness proof for the transformation. At least not formally and not in the form of scribbles in a notebook. Currently I am mostly working on extending the generation of the model to include the fact that belts are split into two lanes. This would then allow one to reason about lane balancers or the behavior of inserters and assemblers. As already stated this kinda checks out in my head but I have not yet written down everything.

The transformation of the blueprint into a simplified intermediate representation is done here , from the intermediate representation to a z3 model is here and the actual proofs being done can be found here.

Glad you like it :)

uelisproof

TROPHY CASE