Refactor: Use appropriate control configurations in trace checks #692

maul-esel · 2024-11-08T10:08:05Z

As discussed internally, this is an attempt at fixing the detection of perfect interpolant sequences, and some other usages of the control locations (or in the case of concurrent programs, control configurations) visited along a counterexample trace.

Motivation

At various points of the code, we either used the IcfgLocation returned by IIcfgTransition::getSource (usually via TraceCheckUtils::getSequenceOfProgramPoints) or the predicate in the IRun for the counterexample.

The IcfgLocations do not make sense in the context of concurrent programs, we want the whole control configuration, i.e., the locations of all threads.
The run predicates are typically not what is intended either. If the run is a run of the difference automaton between program and interpolant automata, and is found by DFS or BFS, it will never contain any repeated state, and is thus useless for determining isPerfect.

Changes

In places where the control configurations / states of the run are not needed at all, I have replaced IRun by Word.
1.1 This includes usages in LassoChecker, where, according to @Heizmann, any emphasis on the usage of "perfect" proofs was unintentional.
In other places, I have replaced an IRun by a new class Counterexample<L>, which bundles the trace (a Word<L>) and an optional List<Object> controlConfigurationSequences.

2.1 The type of configurations is Object, any type will do -- we only care about equality of instances (as defined by Object::equals).
2.2 It is easier to pass some list rather than creating an IRun on the original program (e.g. a CEGAR loop's initial abstraction).

As a lot of these changes touch code I am unfamiliar with, I would appreciate it if someone with more knowledge could take a look, in particular for accelerated interpolation and assert order modulation. @danieldietsch?

Evaluation

The nightly tests look fine: https://jenkins.sopranium.de/job/Ultimate/job/Ultimate%20Nightly/job/wip%252Fdk%252Fperfect-tracechecks/4/testReport/

Once the current evaluations are finished, I will run a fast SV-COMP run on this branch to stress-test these changes, and also to see if the "correct" notion of perfect proofs for concurrent programs has any positive impact.

Update: SV-COMP evaluation is currently running.

…ecks

maul-esel · 2024-11-08T10:22:13Z

The conflict is with the addition of the new Fox refinement strategy. I'll rebase after I have run the SV-COMP evaluation, because the current base is our reference point for the comparison.

danieldietsch

I did not find the place where we really see a benefit from the removal of IRun. Can you point me to it so that I can have a closer look?

In contrast, I see many places that become more convoluted and difficult to understand, in particular because word and sequence of control locations is now separated.
This leads to passing null or returning pairs, having even more parameters, and generally obfuscating the relation between things.
It was a major concern for me to not let that happen.

Please introduce some wrapper class that combines both and perhaps provides helpful abstractions. In contrast to IRun, it can make its control location sequence optional, but then we should ensure that we fail early, i.e., that strategy modules that require control sequences fail if they are not provided with them.

It would also be nice if we could reduce these pesky casts even further, but I am not sure that this is easy.

.../uni_freiburg/informatik/ultimate/lib/acceleratedinterpolation/AcceleratedInterpolation.java

...anker/src/de/uni_freiburg/informatik/ultimate/lassoranker/nontermination/FixpointCheck2.java

trunk/source/Library-PDR/src/de/uni_freiburg/informatik/ultimate/lib/pdr/Pdr.java

...c/de/uni_freiburg/informatik/ultimate/lib/acceleratedinterpolation/MetaTraceTransformer.java

danieldietsch · 2024-11-08T20:19:36Z

...freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/AnnotateAndAsserter.java

@@ -51,6 +52,7 @@ public class AnnotateAndAsserter<L extends IAction> {

 	protected final ManagedScript mMgdScriptTc;
 	protected final NestedWord<L> mTrace;
+	protected final List<?> mControlConfigurationSequence;


Why is it called mControlConfiugrationSequence instead of mControlLocationSequence?

For concurrent programs we do not have sequences of locations but sequence of SomethingElse. We do not yet know what SomethingElse should be.

One good choice for SomethingElse is a set of locations, one location per active thread.

Another choice might be that we additionally states of a monitor automaton.

To add to this: In GemCutter, the SomethingElse has yet another type: it is a pair of a set of locations (one location per active thread) and a sleeo set (a set of letters).

configuration just seems awfully close to the mixing of concepts we want to avoid.
For GemCutter, I would argue that the pair of sets of location and the set of letters is the location of the explicit product automaton, so here location would be ok. I think that location is in general closer to the "something" we want to describe than configuration. But right now I don't know a better name.

...rator/traceabstraction/pathinvariants/InterpolatingTraceCheckPathInvariantsWithFallback.java

danieldietsch · 2024-11-08T21:29:29Z

...e/plugins/generator/traceabstraction/tracehandling/IpAbStrategyModuleTotalInterpolation.java

@@ -94,7 +92,7 @@ public IpAbStrategyModuleResult<LETTER> buildInterpolantAutomaton(final List<Qua
 			final INestedWordAutomaton<LETTER, IPredicate> castedAbstraction =
 					(INestedWordAutomaton<LETTER, IPredicate>) mAbstraction;
 			@SuppressWarnings("unchecked")
-			final NestedRun<LETTER, IPredicate> castedCex = (NestedRun<LETTER, IPredicate>) mCounterexample;
+			final List<IPredicate> castedCex = (List<IPredicate>) mCounterexampleRun;


Would be nice if we could get rid of these casts

...e/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/Mcr.java

...rg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/StrategyFactory.java

Heizmann · 2024-11-09T18:26:19Z

I did not find the place where we really see a benefit from the removal of IRun. Can you point me to it so that I can have a closer look?

TraceChecks were made for for sequences of IActions. Perfect Interpolants and Assert Orders and an additional bonus that are sometimes desired and that require and additional sequence of control configurations.

We must separate the sequence of IActions from the sequence of control configurations in order to maintain support for applications that provide only a sequence of IActions.
A run is a concept from automata theory. It is misleading to utilize a object with this name for other applications. (Would you use ComplexNumber for storing temperature and humidity only because the ComplexNumber can store two reals?)

In contrast, I see many places that become more convoluted and difficult to understand, in particular because word and sequence of control locations is now separated. This leads to passing null or returning pairs, having even more parameters, and generally obfuscating the relation between things. It was a major concern for me to not let that happen.

Please introduce some wrapper class that combines both and perhaps provides helpful abstractions. In contrast to IRun, it can make its control location sequence optional, but then we should ensure that we fail early, i.e., that strategy modules that require control sequences fail if they are not provided with them.

Our TraceChecks are work in progress. We have to try to keep them as simple and as modular as possible. Let us pass null for the sequence of control configurations if there is no sequence of control configurations.
Wrapper classes and additional abstractions will make our TraceChecks even more convoluted.

danieldietsch · 2024-11-09T20:15:23Z

I am not arguing for keeping IRun. I am arguing for adding a new type that describes a trace and optional metadata.

...r/traceabstraction/interpolantautomata/builders/AbsIntNonSmtInterpolantAutomatonBuilder.java

…terexample

…mCounterexample

…nces of the counterexample's set of ControlConfigurations exceed a given threshold Implementation of getControlConfigurationsFromCounterexample needs to be replaced when merging #692 Threshold is currently hardcoded to 1 and might be adjusted later on

schuessf

Thanks for your work. I don't have much to add here, just some minor comment.

Jenkinsfile

...e/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/Mcr.java

...rg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/StrategyFactory.java

This was omitted in PR #692 due to a misunderstanding. That omission broke assert order modulation for termination analysis, which was thus disabled in commit 240d0f7. According to mattermost discussion [1], control configurations should indeed be used in termination analysis as well. https://chat.sopranium.de/swt/pl/muq4okgsutnnbrm43jnysz9uxw

maul-esel requested review from Heizmann, danieldietsch and schuessf November 8, 2024 10:08

maul-esel added 2 commits November 8, 2024 11:17

begin fixing usage of IRun / IcfgLocations in strategies and trace ch…

09348e3

…ecks

pass control locations to assert orders and use them there

613d0d7

maul-esel force-pushed the wip/dk/perfect-tracechecks branch from df46ce8 to 613d0d7 Compare November 8, 2024 10:18

danieldietsch requested changes Nov 8, 2024

View reviewed changes

maul-esel and others added 2 commits November 10, 2024 00:49

group trace and control configurations in class Counterexample

7a12730

pin jdk and maven versions

4a4e67f

maul-esel force-pushed the wip/dk/perfect-tracechecks branch from c657d13 to 4a4e67f Compare November 9, 2024 23:50

maul-esel added 6 commits November 10, 2024 01:24

small improvements

7f0b44e

minor simplification

bbbc7d1

simplify terminology

5c6749a

minor improvements

1de881a

remove accidentally committed file

faeaae6

Move documentation to the right place

b1e93a2

danieldietsch reviewed Nov 10, 2024

View reviewed changes

...r/traceabstraction/interpolantautomata/builders/AbsIntNonSmtInterpolantAutomatonBuilder.java Outdated Show resolved Hide resolved

danieldietsch approved these changes Nov 10, 2024

View reviewed changes

maul-esel added 3 commits November 10, 2024 17:37

minor changes and documentation for #getControlConfigurationsFromCoun…

2cb1046

…terexample

AcceleratedTraceCheck requires control configurations

fd4be16

properly implement PartialOrderCegarLoop::getControlConfigurationsFro…

8be7027

…mCounterexample

add check: Counterexample should never have the empty word

e800f60

schuessf approved these changes Nov 11, 2024

View reviewed changes

maul-esel added 3 commits November 11, 2024 22:01

clarify MCR todo

739ff48

update doc comments

abdcca6

Merge branch 'dev' into wip/dk/perfect-tracechecks

402d187

Merge branch 'dev' into wip/dk/perfect-tracechecks

95ba0fe

maul-esel merged commit 5e0bc53 into dev Nov 13, 2024
3 of 4 checks passed

maul-esel added a commit that referenced this pull request Nov 13, 2024

custom trace check strategies are no longer needed as of #692

760bb2f

maul-esel deleted the wip/dk/perfect-tracechecks branch November 17, 2024 09:29

schuessf mentioned this pull request Dec 3, 2024

Refactor assert orders #699

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor: Use appropriate control configurations in trace checks #692

Refactor: Use appropriate control configurations in trace checks #692

maul-esel commented Nov 8, 2024 •

edited

Loading

maul-esel commented Nov 8, 2024

danieldietsch left a comment

danieldietsch Nov 8, 2024

Heizmann Nov 9, 2024

maul-esel Nov 10, 2024

danieldietsch Nov 10, 2024

danieldietsch Nov 8, 2024

Heizmann commented Nov 9, 2024 •

edited

Loading

danieldietsch commented Nov 9, 2024

schuessf left a comment

Refactor: Use appropriate control configurations in trace checks #692

Refactor: Use appropriate control configurations in trace checks #692

Conversation

maul-esel commented Nov 8, 2024 • edited Loading

Motivation

Changes

Evaluation

maul-esel commented Nov 8, 2024

danieldietsch left a comment

Choose a reason for hiding this comment

danieldietsch Nov 8, 2024

Choose a reason for hiding this comment

Heizmann Nov 9, 2024

Choose a reason for hiding this comment

maul-esel Nov 10, 2024

Choose a reason for hiding this comment

danieldietsch Nov 10, 2024

Choose a reason for hiding this comment

danieldietsch Nov 8, 2024

Choose a reason for hiding this comment

Heizmann commented Nov 9, 2024 • edited Loading

danieldietsch commented Nov 9, 2024

schuessf left a comment

Choose a reason for hiding this comment

maul-esel commented Nov 8, 2024 •

edited

Loading

Heizmann commented Nov 9, 2024 •

edited

Loading