Skip to content

Commit

Permalink
correction after rebase
Browse files Browse the repository at this point in the history
  • Loading branch information
mondokm committed Jul 8, 2024
1 parent 05e568b commit 89d4db8
Show file tree
Hide file tree
Showing 30 changed files with 27 additions and 2,388 deletions.
2 changes: 2 additions & 0 deletions buildSrc/src/main/kotlin/kotlin-common.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,13 @@
*/
import org.jetbrains.kotlin.gradle.plugin.KotlinPlatformJvmPlugin
import org.jetbrains.kotlin.gradle.tasks.KotlinCompile

apply(plugin = "java-common")
apply<KotlinPlatformJvmPlugin>()
dependencies {
val implementation: Configuration by configurations
implementation(Deps.Kotlin.stdlib)
implementation(Deps.Kotlin.reflect)
}
tasks {
withType<KotlinCompile>() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ private CheckMethod(final P prec) {
reachedSet = ImpactReachedSet.create(partitioning);
}

private SafetyResult<S, A> run() {
private SafetyResult<ARG<S, A>, Trace<S, A>> run() {
final Optional<ArgNode<S, A>> unsafeNode = unwind();

if (unsafeNode.isPresent()) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -303,11 +303,11 @@ private void printResult(final SafetyResult<? extends ARG<?, ?>, ? extends Trace
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());
writer.cell(status.getWitness().size());
writer.cell(status.getWitness().getDepth());
writer.cell(status.getWitness().getMeanBranchingFactor());
if (status.isUnsafe()) {
writer.cell(status.asUnsafe().getTrace().length() + "");
writer.cell(status.asUnsafe().getCex().length() + "");
} else {
writer.cell("");
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -65,11 +65,8 @@ public static <W extends Witness, C extends Cex> Unsafe<W, C> unsafe(final C cex
return new Unsafe<>(cex, witness, Optional.of(stats));
}

// Factory methods

public static <S extends State, A extends Action> Safe<S, A> safe(final ARG<S, A> arg,
final Statistics stats) {
return new Safe<>(arg, Optional.of(stats));
public static <W extends Witness, C extends Cex> Unknown<W, C> unknown() {
return new Unknown<>();
}

public abstract boolean isSafe();
Expand Down Expand Up @@ -164,47 +161,16 @@ public boolean isSafe() {

@Override
public boolean isUnsafe() {
return true;
}

@Override
public Safe<S, A> asSafe() {
throw new ClassCastException(
"Cannot cast " + Unsafe.class.getSimpleName() + " to "
+ Safe.class.getSimpleName());
}

@Override
public Unsafe<S, A> asUnsafe() {
return this;
}

@Override
public String toString() {
return Utils.lispStringBuilder(SafetyResult.class.getSimpleName())
.add(Unsafe.class.getSimpleName())
.add("Trace length: " + cex.map(Trace::length).orElse(-1)).toString();
}
}

public static final class Unknown<S extends State, A extends Action> extends SafetyResult<S, A> {
@Override
public boolean isSafe() {
return false;
}

@Override
public boolean isUnsafe() {
return false;
}

@Override
public Safe<S, A> asSafe() {
public Safe<W, C> asSafe() {
return null;
}

@Override
public Unsafe<S, A> asUnsafe() {
public Unsafe<W, C> asUnsafe() {
return null;
}

Expand Down

This file was deleted.

Loading

0 comments on commit 89d4db8

Please sign in to comment.