Termination analysis works only from specific directories
As reported on the mailing list, the termination analysis currently only works if CPAchecker is executed with the current working dir being the project's base directory. This is not desired, CPAchecker should always work regardless of the working directory.
The reason for this is the constant
TerminationAlgorithm.SPEC_FILE, that is resolved against the working directory instead of the base directory. The cleanest way is to make a configuration option out of this constant, because for configuration options input files are automatically treated correctly.
To do this, several steps seems to be necessary.
- The constructor of
SPEC_FILEto reconstruct the termination specification
termSpec, which is then passed to
TerminationStatisticsfor used in the witness export. This is weird because
SPEC_FILEdoes precisely not point to the termination specification. Shouldn't or couldn't we just use the original specification for the witness export? But note that this would be different, it could include input witnesses and it would point to different files. The related commit is b8ef4dbb.
- Some code in
TerminationAlgorithmstores the specification read from
SPEC_FILEin a static field
terminationSpecification. From there it is used by
CoreComponentsFactory, and in the constructor it is checked that the passed specification equals the one in the field. As always, static state is bad though, and in this case prevents the constant
SPEC_FILEfrom being turned into an option.
For the latter, I suggest the following solution:
- Remove the static field
terminationSpecificationand the check using
requiredSpecificationin the constructor.
- In the constructor of
CoreComponentsFactory, convert the specification from termination into "termination as reach" using the code in
TerminationAlgorithm.loadTerminationSpecification, but moved to
SPEC_FILEwould be replaced by an option in
CoreComponentsFactory. Both specifications would be stored in fields of
CoreComponentsFactoryand used appropriately in
@mjakobs @masp Does this seem to work for you, especially related to what ends up as specification in the exported witness? Would the original specification be a valid substitute for the one that is created as
termSpec when passed to