An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
This PR implements a corrected wrapper around itertools::multi_cartesian_product.
I added a CI lint that forbids the string multi_cartesian_product (as a standalone word, not a substring, as decided by grep -w) from the code base. Use the wrapper multi_cartesian_product_fixed instead.
I ported all existing call sites to use the fixed version. I considered each call site manually and convinced myself that either the iterator was never empty or that the old code did not correctly handle that case already. I also removed some obvious workarounds that handled the empty iterator case separately to avoid the bug.
This PR implements a corrected wrapper around
itertools::multi_cartesian_product.I added a CI lint that forbids the string
multi_cartesian_product(as a standalone word, not a substring, as decided bygrep -w) from the code base. Use the wrappermulti_cartesian_product_fixedinstead.I ported all existing call sites to use the fixed version. I considered each call site manually and convinced myself that either the iterator was never empty or that the old code did not correctly handle that case already. I also removed some obvious workarounds that handled the empty iterator case separately to avoid the bug.
Fixes #73