lot of memory is needed onnfa-3.dot

[Numero7]

@pazz lot of memory is needed onnfa-3.dot , I will investigate

Originally posted by @Numero7 in #93 (comment)

[Numero7]

@pazz on this branch the computation avoids the memory shortage.
The new problem is a never-ending iteration over a very large cartesian product of approximately 5 billion elements (precisely 5 159 780 352). Check it with

./target/release/shepherd -f dot examples/iterated-majority/nfa-3.dot -vvv

[pazz]

I can confirm that shepherd does not die here, yes. It is still vasly slower than prism because that process only requires 8 iterations but hey :)

I propose to merge the example into main, because that should be safe.
If you want to keep thisheuristic, it'd be great if you could add some inline docs explaining what it is and why it works.

Was the issue that correct caching is costly? If so, would it be better to (optionally) disable that?

Also, what is the status of this alternative solution to the decision problem only, which avoids computing the winning strategies?

[Numero7]

@pazz currently buggy, working on it

[Numero7]

@pazz better, answer in less than two minutes on iterated-majority with n = 3 . All tests are ok, does the maximal strategy computed seems correct to you?

nfa-3.pdf

[Numero7]

in topological order (computation slightly longer but easier to read)

[Numero7]

@pazz I did drop the cache system, it is useless now. The heuristic is a not totally naive iteration of possible ideals when computing the presafe image by a letter. Two principles: when finding a good ideal, avoid iterating in smaller ideals. Also when iterating on a coordinate 0 first, then omega, then finite coordinates by descending order. If it is losing for 0, there is no need to push further the exploration with other coordinates larger or equal.

[pazz]

Nice! I still have the previous version running, since 9am this morning.

I believe the strategy outputted above is correct. I had to stare at it for a while but cannot fault it.
It's a little surprising to see it include some unreachable configurations, for instance that have tokens both at 0 and 1, but it is true that those are still in the winning region and the proposed letter is safe.

[pazz]

@pazz I did drop the cache system, it is useless now. The heuristic is a not totally naive iteration of possible ideals when computing the presafe image by a letter. Two principles: when finding a good ideal, avoid iterating in smaller ideals. Also when iterating on a coordinate 0 first, then omega, then finite coordinates by descending order.

Would it improve if you use binary search here in the heuristic?
We know that largest finite value below $\omega$ right? So try $0$, then $\omega$, then $C_\max/2$ etc.

[Numero7]

It's a little surprising to see it include some unreachable configurations, for instance that have tokens both at 0 and 1, but it is true that those are still in the winning region and the proposed letter is ssafe.

Yes, when computing the maximal strategy, the initial configuration is not considered at all. It is only used at the end of the computation to answer "yes" or "no".

I am not sure whether introducing the combinatorics of "reachable supports" in the computation would be good for execution time, I would say sometimes yes and sometimes not.

[Numero7]

@pazz I did drop the cache system, it is useless now. The heuristic is a not totally naive iteration of possible ideals when computing the presafe image by a letter. Two principles: when finding a good ideal, avoid iterating in smaller ideals. Also when iterating on a coordinate 0 first, then omega, then finite coordinates by descending order.

Would it improve if you use binary search here in the heuristic? We know that largest finite value below ω right? So try 0 , then ω , then C max / 2 etc.

yes possibly, it used to be done in the "sad story" version of the safe pre image computation, feel free to try to implement it on the current version?

since you give positive feedback on the current heuristic, I will merge it in main