Skip to content

Commit

Permalink
Generalize abstractor, refiner, cegarchecker, visualizer
Browse files Browse the repository at this point in the history
These classes/interfaces depended on ARG and Trace before, which heavily limits reusability. They are now generalized over Witness and Cex. To ease the switch, the old entry points are replicated in "Arg..." classes, so a lot of these changes are just renames.
  • Loading branch information
RipplB committed Oct 21, 2024
1 parent 55c083c commit 292dd94
Show file tree
Hide file tree
Showing 30 changed files with 2,536 additions and 1,614 deletions.
2 changes: 1 addition & 1 deletion build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ buildscript {

allprojects {
group = "hu.bme.mit.theta"
version = "6.6.3"
version = "6.6.4"

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

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -15,31 +15,23 @@
*/
package hu.bme.mit.theta.analysis.algorithm.cegar;

import hu.bme.mit.theta.analysis.Action;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
import hu.bme.mit.theta.analysis.algorithm.Witness;

/**
* Common interface for the abstractor component. It can create an initial ARG and check an ARG with
* Common interface for the abstractor component. It can create an initial witness and check a witness with
* a given precision.
*/
public interface Abstractor<S extends State, A extends Action, P extends Prec> {
public interface Abstractor<P extends Prec, W extends Witness> {

/**
* Create initial ARG.
*
* @return
* Create initial witness
*/
ARG<S, A> createArg();
W createWitness();

/**
* Check ARG with given precision.
*
* @param arg
* @param prec
* @return
* Check witness with given precision
*/
AbstractorResult check(ARG<S, A> arg, P prec);
AbstractorResult check(W witness, P prec);

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package hu.bme.mit.theta.analysis.algorithm.cegar;

import hu.bme.mit.theta.analysis.Action;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;

/**
* Common interface for the abstractor component. It can create an initial ARG and check an ARG with
* a given precision.
*/
public interface ArgAbstractor<S extends State, A extends Action, P extends Prec>
extends Abstractor<P, ARG<S, A>> {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package hu.bme.mit.theta.analysis.algorithm.cegar;

import hu.bme.mit.theta.analysis.Action;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.Trace;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.NullLogger;

/**
* Counterexample-Guided Abstraction Refinement (CEGAR) loop implementation,
* that uses an Abstractor to explore the abstract state space and a Refiner to
* check counterexamples and refine them if needed. It also provides certain
* statistics about its execution.
*/
public final class ArgCegarChecker {

private ArgCegarChecker() {
}

public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P, ARG<S, A>, Trace<S, A>> create(
final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner) {
return create(abstractor, refiner, NullLogger.getInstance());
}

public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P, ARG<S, A>, Trace<S, A>> create(
final ArgAbstractor<S, A, P> abstractor, final ArgRefiner<S, A, P> refiner, final Logger logger) {
return CegarChecker.create(abstractor, refiner, logger, ArgVisualizer.getDefault());
}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
/*
* Copyright 2024 Budapest University of Technology and Economics
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
package hu.bme.mit.theta.analysis.algorithm.cegar;

import hu.bme.mit.theta.analysis.Action;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.Trace;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;

/**
* Common interface for refiners. It takes an ARG and a precision, checks if the counterexample in
* the ARG is feasible and if not, it refines the precision and may also prune the ARG.
*/
public interface ArgRefiner<S extends State, A extends Action, P extends Prec> extends Refiner<S, A, P, ARG<S, A>, Trace<S, A>> {
}
Original file line number Diff line number Diff line change
Expand Up @@ -41,16 +41,16 @@
/**
* Basic implementation for the abstractor, relying on an ArgBuilder.
*/
public class BasicAbstractor<S extends State, A extends Action, P extends Prec> implements Abstractor<S, A, P> {
public class BasicArgAbstractor<S extends State, A extends Action, P extends Prec> implements ArgAbstractor<S, A, P> {

protected final ArgBuilder<S, A, P> argBuilder;
protected final Function<? super S, ?> projection;
protected final Waitlist<ArgNode<S, A>> waitlist;
protected final StopCriterion<S, A> stopCriterion;
protected final Logger logger;

protected BasicAbstractor(final ArgBuilder<S, A, P> argBuilder, final Function<? super S, ?> projection,
final Waitlist<ArgNode<S, A>> waitlist, final StopCriterion<S, A> stopCriterion, final Logger logger) {
protected BasicArgAbstractor(final ArgBuilder<S, A, P> argBuilder, final Function<? super S, ?> projection,
final Waitlist<ArgNode<S, A>> waitlist, final StopCriterion<S, A> stopCriterion, final Logger logger) {
this.argBuilder = checkNotNull(argBuilder);
this.projection = checkNotNull(projection);
this.waitlist = checkNotNull(waitlist);
Expand All @@ -64,7 +64,7 @@ public static <S extends State, A extends Action, P extends Prec> Builder<S, A,
}

@Override
public ARG<S, A> createArg() {
public ARG<S, A> createWitness() {
return argBuilder.createArg();
}

Expand Down Expand Up @@ -174,8 +174,8 @@ public Builder<S, A, P> logger(final Logger logger) {
return this;
}

public BasicAbstractor<S, A, P> build() {
return new BasicAbstractor<>(argBuilder, projection, waitlist, stopCriterion, logger);
public BasicArgAbstractor<S, A, P> build() {
return new BasicArgAbstractor<>(argBuilder, projection, waitlist, stopCriterion, logger);
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,19 +17,18 @@

import com.google.common.base.Stopwatch;
import hu.bme.mit.theta.analysis.Action;
import hu.bme.mit.theta.analysis.Cex;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.Trace;
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
import hu.bme.mit.theta.analysis.algorithm.Witness;
import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint;
import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
import hu.bme.mit.theta.analysis.utils.WitnessVisualizer;
import hu.bme.mit.theta.common.Utils;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.Logger.Level;
import hu.bme.mit.theta.common.logging.NullLogger;

import hu.bme.mit.theta.common.visualization.writer.JSONWriter;
import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger;

Expand All @@ -43,42 +42,44 @@
* check counterexamples and refine them if needed. It also provides certain
* statistics about its execution.
*/
public final class CegarChecker<S extends State, A extends Action, P extends Prec> implements SafetyChecker<ARG<S, A>, Trace<S, A>, P> {
public final class CegarChecker<S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> implements SafetyChecker<W, C, P> {

private final Abstractor<S, A, P> abstractor;
private final Refiner<S, A, P> refiner;
private final Abstractor<P, W> abstractor;
private final Refiner<S, A, P, W, C> refiner;
private final Logger logger;
private final ARG<S, A> arg; // TODO I don't think putting the ARG up here from check below causes any issues, but keep it in mind, that it might
private final W witness;
private final WitnessVisualizer<? super W> witnessVisualizer;

private CegarChecker(final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner, final Logger logger) {
private CegarChecker(final Abstractor<P, W> abstractor, final Refiner<S, A, P, W, C> refiner, final Logger logger, final WitnessVisualizer<? super W> witnessVisualizer) {
this.abstractor = checkNotNull(abstractor);
this.refiner = checkNotNull(refiner);
this.logger = checkNotNull(logger);
arg = abstractor.createArg();
witness = abstractor.createWitness();
this.witnessVisualizer = checkNotNull(witnessVisualizer);
}

public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P> create(
final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner) {
return new CegarChecker<>(abstractor, refiner, NullLogger.getInstance());
public static <S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> CegarChecker<S, A, P, W, C> create(
final Abstractor<P, W> abstractor, final Refiner<S, A, P, W, C> refiner, final WitnessVisualizer<W> witnessVisualizer) {
return create(abstractor, refiner, NullLogger.getInstance(), witnessVisualizer);
}

public static <S extends State, A extends Action, P extends Prec> CegarChecker<S, A, P> create(
final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner, final Logger logger) {
return new CegarChecker<>(abstractor, refiner, logger);
public static <S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> CegarChecker<S, A, P, W, C> create(
final Abstractor<P, W> abstractor, final Refiner<S, A, P, W, C> refiner, final Logger logger, final WitnessVisualizer<? super W> witnessVisualizer) {
return new CegarChecker<>(abstractor, refiner, logger, witnessVisualizer);
}

public ARG<S, A> getArg() {
return arg;
public W getWitness() {
return witness;
}

@Override
public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
public SafetyResult<W, C> check(final P initPrec) {
logger.write(Level.INFO, "Configuration: %s%n", this);
final Stopwatch stopwatch = Stopwatch.createStarted();
long abstractorTime = 0;
long refinerTime = 0;
RefinerResult<S, A, P> refinerResult = null;
AbstractorResult abstractorResult = null;
RefinerResult<S, A, P, C> refinerResult = null;
AbstractorResult abstractorResult;
P prec = initPrec;
int iteration = 0;
WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
Expand All @@ -88,12 +89,12 @@ public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
logger.write(Level.MAINSTEP, "Iteration %d%n", iteration);
logger.write(Level.MAINSTEP, "| Checking abstraction...%n");
final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);
abstractorResult = abstractor.check(arg, prec);
abstractorResult = abstractor.check(witness, prec);
abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime;
logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult);

if (WebDebuggerLogger.enabled()) {
String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg));
String argGraph = JSONWriter.getInstance().writeString(witnessVisualizer.visualize(witness));
String precString = prec.toString();
wdl.addIteration(iteration, argGraph, precString);
}
Expand All @@ -104,7 +105,7 @@ public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
P lastPrec = prec;
logger.write(Level.MAINSTEP, "| Refining abstraction...%n");
final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);
refinerResult = refiner.refine(arg, prec);
refinerResult = refiner.refine(witness, prec);
refinerTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - refinerStartTime;
logger.write(Level.MAINSTEP, "Refining abstraction done, result: %s%n", refinerResult);

Expand All @@ -123,16 +124,16 @@ public SafetyResult<ARG<S, A>, Trace<S, A>> check(final P initPrec) {
} while (!abstractorResult.isSafe() && !refinerResult.isUnsafe());

stopwatch.stop();
SafetyResult<ARG<S, A>, Trace<S, A>> cegarResult = null;
SafetyResult<W, C> cegarResult = null;
final CegarStatistics stats = new CegarStatistics(stopwatch.elapsed(TimeUnit.MILLISECONDS), abstractorTime,
refinerTime, iteration);

assert abstractorResult.isSafe() || (refinerResult != null && refinerResult.isUnsafe());
assert abstractorResult.isSafe() || refinerResult.isUnsafe();

if (abstractorResult.isSafe()) {
cegarResult = SafetyResult.safe(arg, stats);
cegarResult = SafetyResult.safe(witness, stats);
} else if (refinerResult.isUnsafe()) {
cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), arg, stats);
cegarResult = SafetyResult.unsafe(refinerResult.asUnsafe().getCex(), witness, stats);
}

assert cegarResult != null;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,23 +16,19 @@
package hu.bme.mit.theta.analysis.algorithm.cegar;

import hu.bme.mit.theta.analysis.Action;
import hu.bme.mit.theta.analysis.Cex;
import hu.bme.mit.theta.analysis.Prec;
import hu.bme.mit.theta.analysis.State;
import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
import hu.bme.mit.theta.analysis.algorithm.Witness;

/**
* Common interface for refiners. It takes an ARG and a precision, checks if the counterexample in
* the ARG is feasible and if not, it refines the precision and may also prune the ARG.
* Common interface for refiners. It takes a witness and a precision, checks if the counterexample in
* the witness is feasible and if not, it refines the precision
*/
public interface Refiner<S extends State, A extends Action, P extends Prec> {
public interface Refiner<S extends State, A extends Action, P extends Prec, W extends Witness, C extends Cex> {

/**
* Checks if the counterexample in the ARG is feasible. If not, refines the precision and prunes
* the ARG.
*
* @param arg
* @param prec
* @return
* Checks if the counterexample in the witness is feasible. If not, refines the precision
*/
RefinerResult<S, A, P> refine(ARG<S, A> arg, P prec);
RefinerResult<S, A, P, C> refine(W witness, P prec);
}
Loading

0 comments on commit 292dd94

Please sign in to comment.