(XCFA) trace builder #457
Description
Currently, traces can be built from a sequence of states and actions. However, this more-or-less assumes an analysis that uses actions (i.e., the LTS), but we have quite some analyses not relying on the LTS (OC checker, monolithic expression-based analyses), and it's a pain to assemble actions in some (many) cases just for the sake of having a counterexample trace.
E.g., OC checker returns infeasible traces because some info related to pointer states and actions are not updated even though the actual sequence of XCFA edges is a feasible counterexample and most parts of the states (unrelated to the memory state management) are correct. Clearly, this should not be fixed on the OC checker side (and potentially the monolithic expression side).
We should at least create a trace builder that accepts a sequence of states and edges or edges and some solver valuation (and some interpreter for the valuation) and creates an action-trace.
We should have a discussion about this at some point.