Skip to content

Commit e86bd9f

Browse files
mondokmmondokm
authored
Merge pull request #377 from ftsrg/mddtracegen
MDD counterexample generation and implicit CEGAR
2 parents e91ef32 + 4fe41a4 commit e86bd9f

File tree

23 files changed

+1052
-116
lines changed

23 files changed

+1052
-116
lines changed

‎build.gradle.kts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ buildscript {
2929

3030
allprojects {
3131
group = "hu.bme.mit.theta"
32-
version = "6.16.1"
32+
version = "6.17.0"
3333

3434

3535
apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))

‎lib/hu.bme.mit.delta-0.0.1-all.jar

-84 Bytes
Binary file not shown.

‎subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,17 +18,19 @@
1818
import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Domain.*;
1919
import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement.*;
2020

21+
import hu.bme.mit.theta.analysis.Trace;
2122
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
22-
import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex;
2323
import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker;
2424
import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof;
2525
import hu.bme.mit.theta.analysis.expr.ExprAction;
26+
import hu.bme.mit.theta.analysis.expr.ExprState;
2627
import hu.bme.mit.theta.cfa.CFA;
2728
import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
2829
import hu.bme.mit.theta.common.OsHelper;
2930
import hu.bme.mit.theta.common.logging.ConsoleLogger;
3031
import hu.bme.mit.theta.common.logging.Logger;
3132
import hu.bme.mit.theta.common.logging.NullLogger;
33+
import hu.bme.mit.theta.core.model.Valuation;
3234
import hu.bme.mit.theta.solver.SolverFactory;
3335
import hu.bme.mit.theta.solver.SolverManager;
3436
import hu.bme.mit.theta.solver.SolverPool;
@@ -90,15 +92,18 @@ public void test() throws Exception {
9092
CFA cfa = CfaDslManager.createCfa(new FileInputStream(filePath));
9193
var monolithicExpr = CfaToMonolithicExprKt.toMonolithicExpr(cfa);
9294

93-
final SafetyResult<MddProof, MddCex> status;
95+
final SafetyResult<MddProof, Trace<ExprState, ExprAction>> status;
9496
try (var solverPool = new SolverPool(solverFactory)) {
95-
final MddChecker<ExprAction> checker =
97+
final MddChecker<ExprState, ExprAction> checker =
9698
MddChecker.create(
9799
monolithicExpr,
98100
monolithicExpr.getVars(),
99101
solverPool,
100102
logger,
101-
MddChecker.IterationStrategy.GSAT);
103+
MddChecker.IterationStrategy.GSAT,
104+
valuation -> monolithicExpr.getValToState().invoke(valuation),
105+
(Valuation v1, Valuation v2) ->
106+
monolithicExpr.getBiValToAction().invoke(v1, v2));
102107
status = checker.check(null);
103108
}
104109

‎subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java

Lines changed: 73 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -27,41 +27,45 @@
2727
import hu.bme.mit.delta.java.mdd.MddVariableOrder;
2828
import hu.bme.mit.delta.mdd.MddInterpreter;
2929
import hu.bme.mit.delta.mdd.MddVariableDescriptor;
30+
import hu.bme.mit.theta.analysis.Trace;
3031
import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
3132
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
3233
import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
3334
import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor;
34-
import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeInitializer;
35-
import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.MddNodeNextStateDescriptor;
36-
import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.OnTheFlyReachabilityNextStateDescriptor;
35+
import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.*;
3736
import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition;
37+
import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExplicitRepresentationExtractor;
3838
import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.MddExpressionTemplate;
39-
import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.BfsProvider;
40-
import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.GeneralizedSaturationProvider;
41-
import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.SimpleSaturationProvider;
42-
import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.StateSpaceEnumerationProvider;
39+
import hu.bme.mit.theta.analysis.algorithm.mdd.fixedpoint.*;
4340
import hu.bme.mit.theta.analysis.expr.ExprAction;
41+
import hu.bme.mit.theta.analysis.expr.ExprState;
4442
import hu.bme.mit.theta.analysis.unit.UnitPrec;
4543
import hu.bme.mit.theta.common.container.Containers;
4644
import hu.bme.mit.theta.common.logging.Logger;
4745
import hu.bme.mit.theta.common.logging.Logger.Level;
4846
import hu.bme.mit.theta.core.decl.Decl;
4947
import hu.bme.mit.theta.core.decl.VarDecl;
48+
import hu.bme.mit.theta.core.model.Valuation;
5049
import hu.bme.mit.theta.core.type.Expr;
5150
import hu.bme.mit.theta.core.type.booltype.BoolType;
5251
import hu.bme.mit.theta.core.utils.PathUtils;
5352
import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
5453
import hu.bme.mit.theta.solver.SolverPool;
5554
import java.util.ArrayList;
5655
import java.util.List;
56+
import java.util.function.BiFunction;
57+
import java.util.function.Function;
5758

58-
public class MddChecker<A extends ExprAction> implements SafetyChecker<MddProof, MddCex, UnitPrec> {
59+
public class MddChecker<S extends ExprState, A extends ExprAction>
60+
implements SafetyChecker<MddProof, Trace<S, A>, UnitPrec> {
5961

6062
private final MonolithicExpr monolithicExpr;
6163
private final List<VarDecl<?>> variableOrdering;
6264
private final SolverPool solverPool;
6365
private final Logger logger;
64-
private IterationStrategy iterationStrategy = IterationStrategy.GSAT;
66+
private final IterationStrategy iterationStrategy;
67+
private final Function<Valuation, S> valToState;
68+
private final BiFunction<Valuation, Valuation, A> biValToAction;
6569

6670
public enum IterationStrategy {
6771
BFS,
@@ -74,35 +78,55 @@ private MddChecker(
7478
List<VarDecl<?>> variableOrdering,
7579
SolverPool solverPool,
7680
Logger logger,
77-
IterationStrategy iterationStrategy) {
81+
IterationStrategy iterationStrategy,
82+
Function<Valuation, S> valToState,
83+
BiFunction<Valuation, Valuation, A> biValToAction) {
7884
this.monolithicExpr = monolithicExpr;
7985
this.variableOrdering = variableOrdering;
8086
this.solverPool = solverPool;
8187
this.logger = logger;
8288
this.iterationStrategy = iterationStrategy;
89+
this.valToState = valToState;
90+
this.biValToAction = biValToAction;
8391
}
8492

85-
public static <A extends ExprAction> MddChecker<A> create(
93+
public static <S extends ExprState, A extends ExprAction> MddChecker<S, A> create(
8694
MonolithicExpr monolithicExpr,
8795
List<VarDecl<?>> variableOrdering,
8896
SolverPool solverPool,
89-
Logger logger) {
90-
return new MddChecker<A>(
91-
monolithicExpr, variableOrdering, solverPool, logger, IterationStrategy.GSAT);
97+
Logger logger,
98+
Function<Valuation, S> valToState,
99+
BiFunction<Valuation, Valuation, A> biValToAction) {
100+
return new MddChecker<S, A>(
101+
monolithicExpr,
102+
variableOrdering,
103+
solverPool,
104+
logger,
105+
IterationStrategy.GSAT,
106+
valToState,
107+
biValToAction);
92108
}
93109

94-
public static <A extends ExprAction> MddChecker<A> create(
110+
public static <S extends ExprState, A extends ExprAction> MddChecker<S, A> create(
95111
MonolithicExpr monolithicExpr,
96112
List<VarDecl<?>> variableOrdering,
97113
SolverPool solverPool,
98114
Logger logger,
99-
IterationStrategy iterationStrategy) {
100-
return new MddChecker<A>(
101-
monolithicExpr, variableOrdering, solverPool, logger, iterationStrategy);
115+
IterationStrategy iterationStrategy,
116+
Function<Valuation, S> valToState,
117+
BiFunction<Valuation, Valuation, A> biValToAction) {
118+
return new MddChecker<S, A>(
119+
monolithicExpr,
120+
variableOrdering,
121+
solverPool,
122+
logger,
123+
iterationStrategy,
124+
valToState,
125+
biValToAction);
102126
}
103127

104128
@Override
105-
public SafetyResult<MddProof, MddCex> check(UnitPrec prec) {
129+
public SafetyResult<MddProof, Trace<S, A>> check(UnitPrec prec) {
106130

107131
final MddGraph<Expr> mddGraph =
108132
JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr());
@@ -223,11 +247,39 @@ public SafetyResult<MddProof, MddCex> check(UnitPrec prec) {
223247
// var explTrans = MddExplicitRepresentationExtractor.INSTANCE.transform(transitionNode,
224248
// transSig.getTopVariableHandle());
225249

226-
final SafetyResult<MddProof, MddCex> result;
250+
final SafetyResult<MddProof, Trace<S, A>> result;
227251
if (violatingSize != 0) {
252+
final var explTrans =
253+
MddExplicitRepresentationExtractor.INSTANCE.transform(
254+
transitionNode, transSig.getTopVariableHandle());
255+
final var reversed = ReverseNextStateDescriptor.of(stateSpace, explTrans);
256+
257+
final TraceProvider traceProvider = new TraceProvider(stateSig.getVariableOrder());
258+
final var mddTrace =
259+
traceProvider.compute(
260+
propViolating, reversed, initNode, stateSig.getTopVariableHandle());
261+
final var valuations =
262+
mddTrace.stream()
263+
.map(
264+
it ->
265+
PathUtils.extractValuation(
266+
MddValuationCollector.collect(it).stream()
267+
.findFirst()
268+
.orElseThrow(),
269+
0))
270+
.toList();
271+
final List<S> states = new ArrayList<>();
272+
final List<A> actions = new ArrayList<>();
273+
for (int i = 0; i < valuations.size(); ++i) {
274+
states.add(valToState.apply(valuations.get(i)));
275+
if (i > 0) {
276+
actions.add(biValToAction.apply(valuations.get(i - 1), valuations.get(i)));
277+
}
278+
}
279+
228280
result =
229281
SafetyResult.unsafe(
230-
MddCex.of(propViolating), MddProof.of(stateSpace), statistics);
282+
Trace.of(states, actions), MddProof.of(stateSpace), statistics);
231283
} else {
232284
result = SafetyResult.safe(MddProof.of(stateSpace), statistics);
233285
}

‎subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddSinglePathExtractor.kt

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
/*
2+
* Copyright 2025 Budapest University of Technology and Economics
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package hu.bme.mit.theta.analysis.algorithm.mdd
17+
18+
import com.google.common.base.Preconditions
19+
import hu.bme.mit.delta.java.mdd.JavaMddFactory
20+
import hu.bme.mit.delta.java.mdd.MddHandle
21+
import hu.bme.mit.delta.java.mdd.impl.MddStructuralTemplate
22+
23+
object MddSinglePathExtractor {
24+
25+
fun transform(node: MddHandle): MddHandle {
26+
27+
if (node.isTerminal) {
28+
Preconditions.checkState(!node.isTerminalZero)
29+
return node
30+
} else {
31+
32+
val templateBuilder = JavaMddFactory.getDefault().createUnsafeTemplateBuilder()
33+
34+
if (!node.defaultValue().isTerminalZero) {
35+
templateBuilder.set(0, transform(node.defaultValue()).node)
36+
} else {
37+
val cursor = node.cursor()
38+
cursor.moveNext()
39+
templateBuilder.set(cursor.key(), transform(cursor.value()).node)
40+
}
41+
42+
return node.variableHandle.checkInNode(
43+
MddStructuralTemplate.of(templateBuilder.buildAndReset())
44+
)
45+
}
46+
}
47+
}

‎subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/OrNextStateDescriptor.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,7 @@ public IntObjMapView<IntObjMapView<AbstractNextStateDescriptor>> getOffDiagonal(
180180

181181
@Override
182182
public Optional<Iterable<AbstractNextStateDescriptor>> split() {
183+
// TODO flatmap to handle hierarchical splitting
183184
return Optional.of(operands);
184185
}
185186

0 commit comments

Comments
 (0)