Draft: Creating a branch for TerminationToReachCPA
This merge request summarizes changes made to implement new TerminationToReachCPA. It implements a new analysis that is based on the idea from A. Biere's et. al. paper about transformation of liveness properties to safety property.
The analysis keeps a map in its states (stored values) that maps the loop heads to a list of constraints. The list of constraints contains assignment formulas of each variable to a variable with a SSA index that was seen at some point in the loop head. The list of constraints may for instance look like this:
[__Q__x@0 = x@2 and __Q__y@0 = y@3, __Q__x@1 = x@3 and __Q__y@2 = y@4, __Q__x@2 = x@4 and __Q__y@2 = y@5]
The auxiliary variables have always the following form __Q__[name of the variable]@[number of iteration of the loop]
Every time the analysis applies precision operator in a loop-head, we check for satisfiability so called lasso-shaped formula. The lasso-shaped formula is composed of a path formula and a loop constraints. For instance, let's say we entered a loop-head for the 4th time, then we iteratively check for satisfiability of
path formula and (__Q__x@0 = x@2 and __Q__y@0 = y@3) and (__Q__x@0 = x@5 and __Q__y@0 = y@6)
path formula and (__Q__x@1 = x@3 and __Q__y@1 = y@4) and (__Q__x@1 = x@5 and __Q__y@1 = y@6)
path formula and (__Q__x@2 = x@4 and __Q__y@2 = y@5) and (__Q__x@2 = x@5 and __Q__y@2 = y@6)
If some of the queries is satisfiable, we have found a non-terminating loop. If the analysis is able to explore the whole underlying state-space, there is no non-terminating loop.
TerminationToReachCPA can be run only in CompositeCPA with PredicateCPA and LocationCPA. Moreover, the option cpa.predicate.enableSharedInformation=true must be set because TerminationToReachCPA must get information about FormulaManagerView of PredicateCPA because of the satisfiability checks in its precision adjustment operator.
git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/terminationCPA@44862 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c