Skip to content

Commit 18a9805

Browse files
HeizmannHeizmann
committed
Add statistics for accelerated trace check
1 parent 4913422 commit 18a9805

File tree

4 files changed

+214
-2
lines changed

4 files changed

+214
-2
lines changed

‎trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/acceleratedtracecheck/AcceleratedTraceCheck.java‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,9 @@ public class AcceleratedTraceCheck<L extends IIcfgTransition<?>> implements IInt
109109
private boolean mTraceCheckFinishedNormally;
110110
private final PredicateFactory mPredicateFactory;
111111

112+
private final AcceleratedTraceCheckStatisticsGenerator mStatisticsGenerator;
113+
114+
112115
public AcceleratedTraceCheck(final IUltimateServiceProvider services, final ILogger logger,
113116
final TaCheckAndRefinementPreferences<L> prefs, final ManagedScript script,
114117
final IPredicateUnifier predicateUnifier, final IRun<L, IPredicate> counterexample,
@@ -125,11 +128,11 @@ public AcceleratedTraceCheck(final IUltimateServiceProvider services, final ILog
125128
mIcfg = mPrefs.getIcfgContainer();
126129
mPredicateUnifier = predicateUnifier;
127130
mInterpolants = null;
131+
mStatisticsGenerator = new AcceleratedTraceCheckStatisticsGenerator();
128132

129133
final TreeMap<Integer, AcceleratedSegment> acceleratedSegments = constructAcceleratedSegments(mServices,
130134
mLogger, script, counterexample);
131135
if (acceleratedSegments.isEmpty()) {
132-
133136
final TraceCheckSpWp<L> tc = checkTrace(mPrecondition, mPostcondition, mCounterexample);
134137
mIsTraceCorrect = tc.isCorrect();
135138
switch (tc.isCorrect()) {
@@ -146,7 +149,6 @@ public AcceleratedTraceCheck(final IUltimateServiceProvider services, final ILog
146149
} else {
147150
throw new UnsupportedOperationException("Acceleration-free interpolant computation failed.");
148151
}
149-
150152
break;
151153
default:
152154
throw new AssertionError();
@@ -172,6 +174,11 @@ public AcceleratedTraceCheck(final IUltimateServiceProvider services, final ILog
172174
default:
173175
throw new AssertionError();
174176
}
177+
mStatisticsGenerator.reportSatisfiability(tc.isCorrect());
178+
final StatisticsData stats = new StatisticsData();
179+
stats.aggregateBenchmarkData(mStatisticsGenerator);
180+
services.getResultService().reportResult(Activator.PLUGIN_ID,
181+
new StatisticsResult<>(Activator.PLUGIN_NAME, "AcceleratedTraceCheckStatistics", stats));
175182
}
176183
}
177184

@@ -329,6 +336,7 @@ private TreeMap<Integer, AcceleratedSegment> constructAcceleratedSegments(final
329336
final HashTreeRelation<IcfgLocation, Integer> similarProgramPoints = findSimilarProgramPoints(
330337
counterexample.getStateSequence());
331338
final TreeRelation<Integer, Integer> loopPositions = computeMaximalCrossFreeLoopPositions(similarProgramPoints);
339+
332340
for (int i = 0; i < counterexample.getLength(); i++) {
333341
final TreeSet<Integer> positionsWithSimilarProgramPoint = loopPositions
334342
.getImage(i);
@@ -337,7 +345,9 @@ private TreeMap<Integer, AcceleratedSegment> constructAcceleratedSegments(final
337345
final NestedWord<L> nestedWord = (NestedWord<L>) counterexample.getWord();
338346
final NestedWord<L> subWord = nestedWord.getSubWord(i, nextPosition);
339347
final UnmodifiableTransFormula transitiveClosure = accelerate(services, logger, mgdScript, subWord);
348+
mStatisticsGenerator.reportAccelerationAttempt();
340349
if (transitiveClosure != null) {
350+
mStatisticsGenerator.reportSuccessfullAcceleration();
341351
result.put(i, new AcceleratedSegment(i, nextPosition - 1, transitiveClosure));
342352
i = nextPosition - 1;
343353
}

‎trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/acceleratedtracecheck/AcceleratedTraceCheckStatisticsGenerator.java‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
/*
2+
* Copyright (C) 2021 Matthias Heizmann ([email protected])
3+
* Copyright (C) 2021 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE TraceAbstraction plug-in.
6+
*
7+
* The ULTIMATE TraceAbstraction plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE TraceAbstraction plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE TraceAbstraction plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE TraceAbstraction plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE TraceAbstraction plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
27+
package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.acceleratedtracecheck;
28+
29+
import java.util.Collection;
30+
31+
import de.uni_freiburg.informatik.ultimate.logic.Script.LBool;
32+
import de.uni_freiburg.informatik.ultimate.util.statistics.IStatisticsDataProvider;
33+
import de.uni_freiburg.informatik.ultimate.util.statistics.IStatisticsType;
34+
35+
public class AcceleratedTraceCheckStatisticsGenerator implements IStatisticsDataProvider {
36+
37+
private int mSuccessfullAccelerations;
38+
private int mAccelerationAttempts;
39+
private LBool mSatisfiability;
40+
41+
public AcceleratedTraceCheckStatisticsGenerator() {
42+
super();
43+
mSuccessfullAccelerations = 0;
44+
mAccelerationAttempts = 0;
45+
mSatisfiability = null;
46+
}
47+
48+
@Override
49+
public Object getValue(final String key) {
50+
final AcceleratedTraceCheckStatsticsDefinitions keyEnum = Enum
51+
.valueOf(AcceleratedTraceCheckStatsticsDefinitions.class, key);
52+
switch (keyEnum) {
53+
case SuccessfullAccelerations:
54+
return mSuccessfullAccelerations;
55+
case AccelerationAttempts:
56+
return mAccelerationAttempts;
57+
case Satisfiability:
58+
return mSatisfiability;
59+
default:
60+
throw new AssertionError("unknown data");
61+
}
62+
}
63+
64+
@Override
65+
public IStatisticsType getBenchmarkType() {
66+
return AcceleratedTracecheckStatisticsType.getInstance();
67+
}
68+
69+
@Override
70+
public Collection<String> getKeys() {
71+
return getBenchmarkType().getKeys();
72+
}
73+
74+
public void reportAccelerationAttempt() {
75+
mAccelerationAttempts++;
76+
}
77+
78+
public void reportSuccessfullAcceleration() {
79+
mSuccessfullAccelerations++;
80+
}
81+
82+
public void reportSatisfiability(final LBool lbool) {
83+
if (mSatisfiability != null) {
84+
throw new AssertionError("Satisfiability already set");
85+
}
86+
mSatisfiability = lbool;
87+
}
88+
89+
@Override
90+
public String toString() {
91+
return getBenchmarkType().prettyprintBenchmarkData(this);
92+
}
93+
94+
}

‎trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/acceleratedtracecheck/AcceleratedTraceCheckStatsticsDefinitions.java‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
/*
2+
* Copyright (C) 2021 Matthias Heizmann ([email protected])
3+
* Copyright (C) 2021 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE TraceAbstraction plug-in.
6+
*
7+
* The ULTIMATE TraceAbstraction plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE TraceAbstraction plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE TraceAbstraction plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE TraceAbstraction plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE TraceAbstraction plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
27+
package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.acceleratedtracecheck;
28+
29+
import java.util.Objects;
30+
import java.util.function.Function;
31+
32+
import de.uni_freiburg.informatik.ultimate.logic.Script.LBool;
33+
import de.uni_freiburg.informatik.ultimate.util.statistics.IStatisticsElement;
34+
import de.uni_freiburg.informatik.ultimate.util.statistics.StatisticsType;
35+
36+
public enum AcceleratedTraceCheckStatsticsDefinitions implements IStatisticsElement {
37+
38+
AccelerationAttempts(Integer.class, StatisticsType.INTEGER_ADDITION, StatisticsType.DATA_BEFORE_KEY),
39+
40+
SuccessfullAccelerations(Integer.class, StatisticsType.INTEGER_ADDITION, StatisticsType.DATA_BEFORE_KEY),
41+
42+
Satisfiability(LBool.class, StatisticsType.INTEGER_ADDITION, StatisticsType.KEY_BEFORE_DATA),
43+
44+
;
45+
46+
private final Class<?> mClazz;
47+
private final Function<Object, Function<Object, Object>> mAggr;
48+
private final Function<String, Function<Object, String>> mPrettyprinter;
49+
50+
AcceleratedTraceCheckStatsticsDefinitions(final Class<?> clazz, final Function<Object, Function<Object, Object>> aggr,
51+
final Function<String, Function<Object, String>> prettyprinter) {
52+
mClazz = Objects.requireNonNull(clazz);
53+
mAggr = Objects.requireNonNull(aggr);
54+
mPrettyprinter = Objects.requireNonNull(prettyprinter);
55+
}
56+
57+
@Override
58+
public Object aggregate(final Object o1, final Object o2) {
59+
return mAggr.apply(o1).apply(o2);
60+
}
61+
62+
@Override
63+
public String prettyprint(final Object o) {
64+
return mPrettyprinter.apply(name()).apply(o);
65+
}
66+
}

‎trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/acceleratedtracecheck/AcceleratedTracecheckStatisticsType.java‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
/*
2+
* Copyright (C) 2021 Matthias Heizmann ([email protected])
3+
* Copyright (C) 2021 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE Automata Library.
6+
*
7+
* The ULTIMATE Automata Library is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE Automata Library is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE Automata Library. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE Automata Library, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE Automata Library grant you additional permission
25+
* to convey the resulting work.
26+
*/
27+
package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.acceleratedtracecheck;
28+
29+
import de.uni_freiburg.informatik.ultimate.util.statistics.StatisticsType;
30+
31+
public final class AcceleratedTracecheckStatisticsType extends StatisticsType<AcceleratedTraceCheckStatsticsDefinitions> {
32+
33+
private static final AcceleratedTracecheckStatisticsType INSTANCE = new AcceleratedTracecheckStatisticsType();
34+
35+
private AcceleratedTracecheckStatisticsType() {
36+
super(AcceleratedTraceCheckStatsticsDefinitions.class);
37+
}
38+
39+
public static AcceleratedTracecheckStatisticsType getInstance() {
40+
return INSTANCE;
41+
}
42+
}

0 commit comments

Comments
 (0)