[Libre-soc-dev] daily kan-ban update 14nov2020

[Luke Kenneth Casson Leighton]

On Sat, Nov 14, 2020 at 1:43 PM Cesar Strauss <cestrauss at gmail.com> wrote:

> Interestingly, you can find such loops with a normal bounded model
> checker, by a clever addition to the model. It saves a visited state, at
> random, and asserts "I was already here, and that signal did not become
> active, not once". See:
> http://fmv.jku.at/papers/BiereArthoSchuppan-FMICS02.pdf.

thank you, Cesar, for a fascinating and valuable report.

l.