Skip to content

Commit

Permalink
Reformatted code
Browse files Browse the repository at this point in the history
  • Loading branch information
@thetabotmaintainer @leventeBajczi
thetabotmaintainer[bot] authored and leventeBajczi committed Nov 16, 2023
1 parent aff754c commit ebaf60d
Show file tree
Hide file tree
Showing 11 changed files with 182 additions and 176 deletions.
10 changes: 5 additions & 5 deletions ...cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,12 +93,12 @@

public class CfaConfigBuilder {

public enum Algorithm {
CEGAR,
KINDUCTION,
public enum Algorithm {
CEGAR,
KINDUCTION,
IMC
}
}

public enum Domain {
EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT
}
Expand Down
76 changes: 38 additions & 38 deletions subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,11 +80,11 @@ public class CfaCli {
private static final String JAR_NAME = "theta-cfa-cli.jar";
private final String[] args;
private final TableWriter writer;
@Parameter(names = {"--algorithm"}, description = "Algorithm")
Algorithm algorithm = Algorithm.CEGAR;
@Parameter(names = {"--algorithm"}, description = "Algorithm")
Algorithm algorithm = Algorithm.CEGAR;

@Parameter(names = "--domain", description = "Abstract domain")
Domain domain = Domain.PRED_CART;
@Parameter(names = "--domain", description = "Abstract domain")
Domain domain = Domain.PRED_CART;

@Parameter(names = "--refinement", description = "Refinement strategy")
Refinement refinement = Refinement.SEQ_ITP;
Expand Down Expand Up @@ -236,7 +236,7 @@ private void run() {
refinementSolverFactory = SolverManager.resolveSolverFactory(solver);
}

final SafetyResult<?, ?> status;
final SafetyResult<?, ?> status;
if (algorithm == Algorithm.CEGAR) {
final CfaConfig<?, ?, ?> configuration = buildConfiguration(cfa, errLoc, abstractionSolverFactory, refinementSolverFactory);
status = check(configuration);
Expand All @@ -254,18 +254,18 @@ private void run() {
logger.write(Logger.Level.RESULT, "%s%n", status);
sw.stop();
} else {
throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported");
}

printResult(status, sw.elapsed(TimeUnit.MILLISECONDS));
if (status.isUnsafe() && cexfile != null) {
writeCex(status.asUnsafe());
}
} catch (final Throwable ex) {
printError(ex);
System.exit(1);
}
}
throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported");
}

printResult(status, sw.elapsed(TimeUnit.MILLISECONDS));
if (status.isUnsafe() && cexfile != null) {
writeCex(status.asUnsafe());
}
} catch (final Throwable ex) {
printError(ex);
System.exit(1);
}
}

private void printHeader() {
Stream.of("Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations",
Expand Down Expand Up @@ -308,27 +308,27 @@ private CFA loadModel() throws Exception {
}
}

private void printResult(final SafetyResult<?, ?> status, final long totalTimeMs) {
final CegarStatistics stats = (CegarStatistics)
status.getStats().orElse(new CegarStatistics(0, 0, 0, 0));
if (benchmarkMode) {
writer.cell(status.isSafe());
writer.cell(totalTimeMs);
writer.cell(stats.getAlgorithmTimeMs());
writer.cell(stats.getAbstractorTimeMs());
writer.cell(stats.getRefinerTimeMs());
writer.cell(stats.getIterations());
writer.cell(status.getArg().size());
writer.cell(status.getArg().getDepth());
writer.cell(status.getArg().getMeanBranchingFactor());
if (status.isUnsafe()) {
writer.cell(status.asUnsafe().getTrace().length() + "");
} else {
writer.cell("");
}
writer.newRow();
}
}
private void printResult(final SafetyResult<?, ?> status, final long totalTimeMs) {
final CegarStatistics stats = (CegarStatistics)
status.getStats().orElse(new CegarStatistics(0, 0, 0, 0));
if (benchmarkMode) {
writer.cell(status.isSafe());
writer.cell(totalTimeMs);
writer.cell(stats.getAlgorithmTimeMs());
writer.cell(stats.getAbstractorTimeMs());
writer.cell(stats.getRefinerTimeMs());
writer.cell(stats.getIterations());
writer.cell(status.getArg().size());
writer.cell(status.getArg().getDepth());
writer.cell(status.getArg().getMeanBranchingFactor());
if (status.isUnsafe()) {
writer.cell(status.asUnsafe().getTrace().length() + "");
} else {
writer.cell("");
}
writer.newRow();
}
}

private void printError(final Throwable ex) {
final String message = ex.getMessage() == null ? "" : ex.getMessage();
Expand Down
42 changes: 21 additions & 21 deletions ...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/imc/ImcChecker.java
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
package hu.bme.mit.theta.analysis.algorithm.imc;

import hu.bme.mit.theta.analysis.Trace;
import hu.bme.mit.theta.analysis.algorithm.ARG;
import hu.bme.mit.theta.analysis.algorithm.MonolithicTransFunc;
Expand Down Expand Up @@ -27,7 +28,7 @@
import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*;


public class ImcChecker<S extends ExprState, A extends StmtAction> implements SafetyChecker<S, A, UnitPrec> {
public class ImcChecker<S extends ExprState, A extends StmtAction> implements SafetyChecker<S, A, UnitPrec> {
final Expr<BoolType> trans;
final Expr<BoolType> init;
final Expr<BoolType> prop;
Expand All @@ -42,7 +43,7 @@ public class ImcChecker<S extends ExprState, A extends StmtAction> implements S
public ImcChecker(MonolithicTransFunc transFunc,
int upperBound,
ItpSolver solver,
Function<Valuation,S> valToState,
Function<Valuation, S> valToState,
Collection<VarDecl<?>> vars,
boolean interpolateForward1) {
this.trans = transFunc.getTransExpr();
Expand All @@ -54,63 +55,62 @@ public ImcChecker(MonolithicTransFunc transFunc,
this.offset = transFunc.getOffsetIndexing();
this.valToState = valToState;
this.vars = vars;
interpolateForward =interpolateForward1;
interpolateForward = interpolateForward1;
}



@Override
public SafetyResult<S, A> check(UnitPrec prec) {
int i=0;
var exprsFromStart=new ArrayList<>(List.of(PathUtils.unfold(init,VarIndexingFactory.indexing(0))));
int i = 0;
var exprsFromStart = new ArrayList<>(List.of(PathUtils.unfold(init, VarIndexingFactory.indexing(0))));
var listOfIndexes = new ArrayList<>(List.of(firstIndexing));

final ItpMarker a = solver.createMarker();
final ItpMarker b = solver.createMarker();
final ItpPattern pattern = solver.createBinPattern(a, b);

while(i<upperBound){
while (i < upperBound) {
i++;
var newIndex = listOfIndexes.get(i-1).add(offset);
var expression = PathUtils.unfold(trans,listOfIndexes.get(i-1));
var newIndex = listOfIndexes.get(i - 1).add(offset);
var expression = PathUtils.unfold(trans, listOfIndexes.get(i - 1));

exprsFromStart.add(expression);
listOfIndexes.add(newIndex);

var unfoldedProp = Not(PathUtils.unfold(prop,newIndex));
var unfoldedProp = Not(PathUtils.unfold(prop, newIndex));

solver.push();
solver.add(a,And(exprsFromStart.subList(0, 2)));
solver.add(b,And(And(exprsFromStart.subList(2, exprsFromStart.size())), unfoldedProp));
solver.add(a, And(exprsFromStart.subList(0, 2)));
solver.add(b, And(And(exprsFromStart.subList(2, exprsFromStart.size())), unfoldedProp));


var img = exprsFromStart.get(0);

var status = solver.check();
if(status.isSat()){
if (status.isSat()) {
S initial = null;
for (int j = 0; j < listOfIndexes.size(); j++) {
var valuation = PathUtils.extractValuation(solver.getModel(), listOfIndexes.get(j), vars);

S st = valToState.apply(valuation);
if(initial == null)
if (initial == null)
initial = st;
}
Trace<S, A> trace = Trace.of(List.of(initial), List.of());
return SafetyResult.unsafe(trace,ARG.create(null));
return SafetyResult.unsafe(trace, ARG.create(null));
}
// reached fixed point
while(status.isUnsat()){
while (status.isUnsat()) {
var interpolant = solver.getInterpolant(pattern);
var itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), listOfIndexes.get(1)),listOfIndexes.get(0));
var itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), listOfIndexes.get(1)), listOfIndexes.get(0));
solver.pop();
try (var pps = new WithPushPop(solver)){
solver.add(a,And(itpFormula,Not(img)));
if(solver.check().isUnsat()){
try (var pps = new WithPushPop(solver)) {
solver.add(a, And(itpFormula, Not(img)));
if (solver.check().isUnsat()) {
return SafetyResult.safe(ARG.create((state1, state2) -> false));
}
}
img = Or(img,itpFormula);
img = Or(img, itpFormula);

solver.push();
solver.add(a, And(itpFormula, exprsFromStart.get(1)));
Expand Down
47 changes: 23 additions & 24 deletions ...s/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@
import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not;


public class KIndChecker<S extends ExprState, A extends ExprAction> implements SafetyChecker<S, A, UnitPrec> {
public class KIndChecker<S extends ExprState, A extends ExprAction> implements SafetyChecker<S, A, UnitPrec> {
final Expr<BoolType> trans;
final Expr<BoolType> init;
final Expr<BoolType> prop;
Expand All @@ -61,7 +61,7 @@ public KIndChecker(MonolithicTransFunc transFunc,
int upperBound,
Solver solver1,
Solver solver2,
Function<Valuation,S> valToState,
Function<Valuation, S> valToState,
Collection<VarDecl<?>> vars) {
this.trans = transFunc.getTransExpr();
this.init = transFunc.getInitExpr();
Expand All @@ -76,23 +76,22 @@ public KIndChecker(MonolithicTransFunc transFunc,
}



@Override
public SafetyResult<S, A> check(UnitPrec prec) {
//var trans = action.toExpr();
//var offset = action.nextIndexing();

int i=0;
int i = 0;
var currIndex = firstIndexing;


var exprsFromStart=new ArrayList<Expr<BoolType>>();
var exprsForInductivity=new ArrayList<Expr<BoolType>>();
var exprsFromStart = new ArrayList<Expr<BoolType>>();
var exprsForInductivity = new ArrayList<Expr<BoolType>>();
var listOfIndexes = new ArrayList<VarIndexing>();

solver1.add(PathUtils.unfold(init, VarIndexingFactory.indexing(0))); // VarIndexingFactory.indexing(0)?
var eqList= new ArrayList<Expr<BoolType>>();
while(i<upperBound){
var eqList = new ArrayList<Expr<BoolType>>();
while (i < upperBound) {


solver1.add(PathUtils.unfold(trans, currIndex));
Expand Down Expand Up @@ -125,30 +124,30 @@ public SafetyResult<S, A> check(UnitPrec prec) {

if (solver1.check().isUnsat()) {

return SafetyResult.safe(ARG.create(null));
}
return SafetyResult.safe(ARG.create(null));
}
solver1.pop();

// Counterexample feasibility check

// I1 and T1-2 and T2-3 and ... and Tk-1-k
// I1 and T1-2 and T2-3 and ... and Tk-1-k

// Not Pk
// Not Pk
solver1.push();
solver1.add(PathUtils.unfold(Not(prop), currIndex));

if (solver1.check().isSat()) {
S initial = null;
for (int j = 0; j < listOfIndexes.size(); j++) {
var valuation = PathUtils.extractValuation(solver1.getModel(), listOfIndexes.get(j), vars);

S st = valToState.apply(valuation);
if(initial == null)
initial = st;
}
Trace<S, A> trace = Trace.of(List.of(initial), List.of());
return SafetyResult.unsafe(trace,ARG.create(null));
S initial = null;
for (int j = 0; j < listOfIndexes.size(); j++) {
var valuation = PathUtils.extractValuation(solver1.getModel(), listOfIndexes.get(j), vars);

S st = valToState.apply(valuation);
if (initial == null)
initial = st;
}
Trace<S, A> trace = Trace.of(List.of(initial), List.of());
return SafetyResult.unsafe(trace, ARG.create(null));
}
solver1.pop();


Expand All @@ -161,8 +160,8 @@ public SafetyResult<S, A> check(UnitPrec prec) {
solver2.add(PathUtils.unfold(Not(prop), currIndex.sub(firstIndexing)));

if (solver2.check().isUnsat()) {
return SafetyResult.safe(ARG.create(null));
}
return SafetyResult.safe(ARG.create(null));
}
solver2.pop();
i++;
}
Expand Down
Loading

0 comments on commit ebaf60d

Please sign in to comment.