This PR adds an alternative means of fully automatic tests for ARGs. This is similar to the CFG tests: a GraphViz graph is rendered as ASCII using graph-easy and expected outputs are in the repository.
The tests are very similar to Cram tests: if something changes, the tests will fail with a diff that can be promoted if intended. However, they aren't Cram tests but just dune expectation tests using rule generation.
The mechanism is somewhat complex (at least without dune 3.14), but nobody other than me will probably ever have to deal with these anyway (because they should just keep passing).
TODO
[x] Manually check that all current outputs are correct to begin with.
[x] Fix small bugs in ARG generation revealed by manual inspection.
Like in #1462, I'm always afraid of doing any modifications in the ARG generation because it's very fragile and there have been no tests so far.
At some point I added https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/scripts/sv-comp/witness-isomorphism.py to semi-automatically check if two sets of GraphML witnesses are isomorphic. But that requires a set of reference witnesses (which we don't have in the repository) and the networkx Python library that implements graph isomorphism algorithms.
This PR adds an alternative means of fully automatic tests for ARGs. This is similar to the CFG tests: a GraphViz graph is rendered as ASCII using
graph-easyand expected outputs are in the repository. The tests are very similar to Cram tests: if something changes, the tests will fail with a diff that can be promoted if intended. However, they aren't Cram tests but just dune expectation tests using rule generation.The mechanism is somewhat complex (at least without dune 3.14), but nobody other than me will probably ever have to deal with these anyway (because they should just keep passing).
TODO