Skip to content

Commit

Permalink
Improve XTA property parsing, add combined to CLI
Browse files Browse the repository at this point in the history
  • Loading branch information
@as3810t @kopero2000
as3810t authored and kopero2000 committed Oct 25, 2022
1 parent 846c636 commit d308fc2
Show file tree
Hide file tree
Showing 10 changed files with 357 additions and 36 deletions.
206 changes: 206 additions & 0 deletions ...me/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,206 @@
package hu.bme.mit.theta.xta.analysis.combinedlazycegar;

import hu.bme.mit.theta.analysis.*;
import hu.bme.mit.theta.analysis.algorithm.SearchStrategy;
import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker;
import hu.bme.mit.theta.analysis.algorithm.lazy.*;
import hu.bme.mit.theta.analysis.algorithm.lazy.itp.*;
import hu.bme.mit.theta.analysis.expl.*;
import hu.bme.mit.theta.analysis.expr.refinement.*;
import hu.bme.mit.theta.analysis.prod2.Prod2Analysis;
import hu.bme.mit.theta.analysis.prod2.Prod2Prec;
import hu.bme.mit.theta.analysis.prod2.Prod2State;
import hu.bme.mit.theta.analysis.zone.*;
import hu.bme.mit.theta.common.Tuple3;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.NullLogger;
import hu.bme.mit.theta.core.utils.Lens;
import hu.bme.mit.theta.solver.SolverFactory;
import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
import hu.bme.mit.theta.xta.XtaSystem;
import hu.bme.mit.theta.xta.analysis.*;
import hu.bme.mit.theta.xta.analysis.lazy.ClockStrategy;
import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaLensUtils;
import hu.bme.mit.theta.xta.analysis.zone.XtaZoneAnalysis;
import hu.bme.mit.theta.xta.analysis.zone.XtaZoneInvTransFunc;
import hu.bme.mit.theta.xta.analysis.zone.XtaZoneTransFunc;

import java.util.function.Function;

import static com.google.common.base.Preconditions.checkNotNull;
import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
import static hu.bme.mit.theta.xta.analysis.combinedlazycegar.CombinedLazyCegarXtaUtils.forceCast;
import static hu.bme.mit.theta.xta.analysis.lazy.LazyXtaLensUtils.createConcrProd2Lens;

public class CombinedLazyCegarXtaCheckerConfigFactory {
private final XtaSystem system;
private final Logger logger;
private final SolverFactory solverFactory;

private CombinedLazyCegarXtaCheckerConfigFactory(final XtaSystem system, final Logger logger, final SolverFactory solverFactory) {
this.system = system;
this.logger = logger;
this.solverFactory = solverFactory;
}

private CombinedLazyCegarXtaCheckerConfigFactory(final XtaSystem system) {
this(system, NullLogger.getInstance(), Z3SolverFactory.getInstance());
}

public static CombinedLazyCegarXtaCheckerConfigFactory create(final XtaSystem system, final Logger logger, final SolverFactory solverFactory) {
return new CombinedLazyCegarXtaCheckerConfigFactory(system, logger, solverFactory);
}

public static CombinedLazyCegarXtaCheckerConfigFactory create(final XtaSystem system) {
return new CombinedLazyCegarXtaCheckerConfigFactory(system);
}

public CombinedLazyCegarXtaCheckerConfig<ExplState, ZoneState, ExplState, ZoneState, ExplPrec, ZonePrec> build() {
final var lazyStrategy = createLazyStrategy(ClockStrategy.BWITP);

final var lazyAnalysis = createLazyAnalysis(
solverFactory,
lazyStrategy.getPartialOrd(),
lazyStrategy.getInitAbstractor()
);

final var prec = createConcrPrec();

final var cegarChecker = CegarChecker.create(
new LazyAbstractor<>(
forceCast(XtaLts.create(system)),
SearchStrategy.BFS,
lazyStrategy,
lazyAnalysis,
XtaState::isError,
createConcrProd2Lens()
),
SingleExprTraceRefiner.create(
new CombinedLazyCegarExprTraceChecker<>(
ExprTraceSeqItpChecker.create(True(), True(), solverFactory.createItpSolver()),
createConcrProd2Lens(),
system),
new CombinedLazyCegarXtaPrecRefiner<>(new ItpRefToExplPrec()),
PruneStrategy.FULL,
logger
),
logger
);

return new CombinedLazyCegarXtaCheckerConfig<>(cegarChecker, prec);
}

private LazyAnalysis<XtaState<Prod2State<ExplState, ZoneState>>, XtaState<Prod2State<ExplState, ZoneState>>, XtaAction, Prod2Prec<ExplPrec, ZonePrec>>
createLazyAnalysis(final SolverFactory solverFactory,
final PartialOrd<Prod2State<ExplState, ZoneState>> abstrPartialOrd,
final InitAbstractor<Prod2State<ExplState, ZoneState>, Prod2State<ExplState, ZoneState>> initAbstractor) {
final Prod2Analysis<ExplState, ZoneState, XtaAction, ExplPrec, ZonePrec>
prod2ConcrAnalysis = createConcrAnalysis(solverFactory);
final XtaAnalysis<Prod2State<ExplState, ZoneState>, Prod2Prec<ExplPrec, ZonePrec>>
xtaConcrAnalysis = XtaAnalysis.create(system, prod2ConcrAnalysis);

return LazyAnalysis.create(
XtaOrd.create(abstrPartialOrd),
xtaConcrAnalysis.getInitFunc(),
xtaConcrAnalysis.getTransFunc(),
XtaInitAbstractor.create(initAbstractor)
);
}

private Prod2Analysis<ExplState, ZoneState, XtaAction, ExplPrec, ZonePrec> createConcrAnalysis(final SolverFactory solverFactory) {
return Prod2Analysis.create(
createConcrDataAnalysis(solverFactory),
createConcrClockAnalysis()
);
}

private Analysis<ExplState, XtaAction, ExplPrec> createConcrDataAnalysis(final SolverFactory solverFactory) {
return CombinedLazyCegarXtaAnalysis.create(
ExplAnalysis.create(
solverFactory.createSolver(),
system.getInitVal().toExpr()
)
);
}

private Analysis<ZoneState, XtaAction, ZonePrec> createConcrClockAnalysis() {
return XtaZoneAnalysis.getInstance();
}

private LazyStrategy<Prod2State<ExplState, ZoneState>, Prod2State<ExplState, ZoneState>, LazyState<XtaState<Prod2State<ExplState, ZoneState>>, XtaState<Prod2State<ExplState, ZoneState>>>, XtaAction>
createLazyStrategy(final ClockStrategy clockStrategy) {
final LazyStrategy<ExplState, ExplState, LazyState<XtaState<Prod2State<ExplState, ZoneState>>, XtaState<Prod2State<ExplState, ZoneState>>>, XtaAction>
dataLazyStrategy = forceCast(createDataStrategy2());

final LazyStrategy<ZoneState, ZoneState, LazyState<XtaState<Prod2State<ExplState, ZoneState>>, XtaState<Prod2State<ExplState, ZoneState>>>, XtaAction>
clockLazyStrategy = forceCast(createClockStrategy(clockStrategy));

final Function<LazyState<XtaState<Prod2State<ExplState, ZoneState>>, XtaState<Prod2State<ExplState, ZoneState>>>, ?> projection = s -> Tuple3.of(
s.getConcrState().getLocs(),
dataLazyStrategy.getProjection().apply(s),
clockLazyStrategy.getProjection().apply(s)
);

final Lens<LazyState<XtaState<Prod2State<ExplState, ZoneState>>, XtaState<Prod2State<ExplState, ZoneState>>>, Prod2State<ExplState, ZoneState>>
lens = createConcrProd2Lens();
return new Prod2LazyStrategy<>(lens, dataLazyStrategy, clockLazyStrategy, projection);
}

private LazyStrategy<ExplState, ExplState, LazyState<XtaState<Prod2State<ExplState, ?>>, XtaState<Prod2State<ExplState, ?>>>, XtaAction> createDataStrategy2() {
return new BasicLazyStrategy<>(
createDataLens(),
createDataConcretizer()
);
}

private Lens<LazyState<XtaState<Prod2State<ExplState, ?>>, XtaState<Prod2State<ExplState, ?>>>, ExplState> createDataLens() {
return LazyXtaLensUtils.createConcrDataLens();
}

private Concretizer<ExplState, ExplState> createDataConcretizer() {
return BasicConcretizer.create(ExplOrd.getInstance());
}

private LazyStrategy<ZoneState, ZoneState, LazyState<XtaState<Prod2State<?, ZoneState>>, XtaState<Prod2State<?, ZoneState>>>, XtaAction> createClockStrategy(final ClockStrategy clockStrategy) {
return switch (clockStrategy) {
case BWITP, FWITP -> createLazyZoneStrategy(clockStrategy);
case LU -> throw new AssertionError();
};
}

private LazyStrategy<ZoneState, ZoneState, LazyState<XtaState<Prod2State<?, ZoneState>>, XtaState<Prod2State<?, ZoneState>>>, XtaAction>
createLazyZoneStrategy(final ClockStrategy clockStrategy) {

final Lens<LazyState<XtaState<Prod2State<?, ZoneState>>, XtaState<Prod2State<?, ZoneState>>>, LazyState<ZoneState, ZoneState>>
lens = LazyXtaLensUtils.createLazyClockLens();
final Lattice<ZoneState> lattice = ZoneLattice.getInstance();
final Interpolator<ZoneState, ZoneState> interpolator = ZoneInterpolator.getInstance();
final PartialOrd<ZoneState> partialOrd = ZoneOrd.getInstance();
final Concretizer<ZoneState, ZoneState> concretizer = BasicConcretizer.create(partialOrd);
final InvTransFunc<ZoneState, XtaAction, ZonePrec> zoneInvTransFunc = XtaZoneInvTransFunc.getInstance();
final ZonePrec prec = ZonePrec.of(system.getClockVars());

switch (clockStrategy){
case BWITP:
return new BwItpStrategy<>(lens, lattice, interpolator, concretizer, zoneInvTransFunc, prec);
case FWITP:
final TransFunc<ZoneState, XtaAction, ZonePrec> zoneTransFunc = XtaZoneTransFunc.getInstance();
return new FwItpStrategy<>(lens, lattice, interpolator, concretizer, zoneInvTransFunc, prec, zoneTransFunc, prec);
default:
throw new AssertionError();
}
}

private Prod2Prec<ExplPrec, ZonePrec> createConcrPrec() {
return Prod2Prec.of(createConcrDataPrec(), createConcrZonePrec());
}

private ExplPrec createConcrDataPrec() {
return ExplPrec.empty();
}

private ZonePrec createConcrZonePrec() {
return ZonePrec.of(system.getClockVars());
}

}
100 changes: 87 additions & 13 deletions subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,9 @@
import hu.bme.mit.theta.common.logging.ConsoleLogger;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.NullLogger;
import hu.bme.mit.theta.common.logging.ConsoleLogger;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.NullLogger;
import hu.bme.mit.theta.common.table.BasicTableWriter;
import hu.bme.mit.theta.common.table.TableWriter;
import hu.bme.mit.theta.common.visualization.Graph;
Expand All @@ -47,9 +50,12 @@
import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
import hu.bme.mit.theta.solver.z3.Z3SolverManager;
import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
import hu.bme.mit.theta.xta.XtaSystem;
import hu.bme.mit.theta.xta.XtaVisualizer;
import hu.bme.mit.theta.xta.analysis.XtaAction;
import hu.bme.mit.theta.xta.analysis.combinedlazycegar.CombinedLazyCegarXtaCheckerConfigFactory;
import hu.bme.mit.theta.xta.analysis.lazy.*;
import hu.bme.mit.theta.xta.analysis.XtaState;
import hu.bme.mit.theta.xta.analysis.config.XtaConfig;
import hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder;
Expand All @@ -58,28 +64,44 @@
import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaCheckerFactory;
import hu.bme.mit.theta.xta.analysis.lazy.LazyXtaStatistics;
import hu.bme.mit.theta.xta.dsl.XtaDslManager;
import hu.bme.mit.theta.xta.utils.CTLOperatorNotSupportedException;
import hu.bme.mit.theta.xta.utils.MixedDataTimeNotSupportedException;

import javax.sound.sampled.AudioFormat;

import static com.google.common.base.Preconditions.checkNotNull;
import static hu.bme.mit.theta.xta.analysis.config.XtaConfigBuilder.*;

public final class XtaCli {

public enum Algorithm {
LAZY, EXPERIMENTAL_EAGERLAZY
}

private static final String JAR_NAME = "theta-xta.jar";
private final String[] args;
private final TableWriter writer;

@Parameter(names = {"--model", "-m"}, description = "Path of the input model", required = true)
String model;

@Parameter(names = {"--discrete", "-d"}, description = "Refinement strategy for discrete variables", required = false)
DataStrategy dataStrategy = DataStrategy.NONE;
@Parameter(names = {"--discreteconcr", "-dc"}, description = "Concrete domain for discrete variables", required = false)
DataStrategy2.ConcrDom concrDataDom = DataStrategy2.ConcrDom.EXPL;

@Parameter(names = {"--clock", "-c"}, description = "Refinement strategy for clock variables", required = true)
ClockStrategy clockStrategy;
@Parameter(names = {"--discreteabstr", "-da"}, description = "Abstract domain for discrete variables", required = false)
DataStrategy2.AbstrDom abstrDataDom = DataStrategy2.AbstrDom.EXPL;

@Parameter(names = {"--search", "-s"}, description = "Search strategy", required = true)
SearchStrategy searchStrategy;
@Parameter(names = {"--discreteitp", "-di"}, description = "Interpolation strategy for discrete variables", required = false)
DataStrategy2.ItpStrategy dataItpStrategy = DataStrategy2.ItpStrategy.BIN_BW;

@Parameter(names = {"--meet", "-me"}, description = "Meet strategy for expressions", required = false)
ExprMeetStrategy exprMeetStrategy = ExprMeetStrategy.BASIC;

@Parameter(names = {"--clock", "-c"}, description = "Refinement strategy for clock variables", required = false)
ClockStrategy clockStrategy = ClockStrategy.BWITP;

@Parameter(names = {"--search", "-s"}, description = "Search strategy", required = false)
SearchStrategy searchStrategy = SearchStrategy.BFS;

@Parameter(names = {"--benchmark", "-b"}, description = "Benchmark mode (only print metrics)")
Boolean benchmarkMode = false;
Expand All @@ -93,6 +115,9 @@ public final class XtaCli {
@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
boolean stacktrace = false;

@Parameter(names = "--loglevel", description = "Detailedness of logging")
Logger.Level logLevel = Logger.Level.MAINSTEP;

@Parameter(names = "--version", description = "Display version", help = true)
boolean versionInfo = false;

Expand Down Expand Up @@ -195,19 +220,60 @@ private void run() {

try {
final XtaSystem system = loadModel();
final SafetyChecker<?, ?, UnitPrec> checker = LazyXtaCheckerFactory.create(system, dataStrategy,
clockStrategy, searchStrategy);
final SafetyResult<?, ?> result = check(checker);
printResult(result);
if (dotfile != null) {
writeVisualStatus(result, dotfile);
switch (algorithm) {
case LAZY -> runLazy(system);
case EXPERIMENTAL_EAGERLAZY -> runCombined(system);
case EAGER -> runEager(system);
}
} catch (final Throwable ex) {
printError(ex);
System.exit(1);
}
}

private void runLazy(final XtaSystem system) {
final LazyXtaAbstractorConfig<?, ?, ?> abstractor = LazyXtaAbstractorConfigFactory.create(
system, new DataStrategy2(concrDataDom, abstrDataDom, dataItpStrategy),
clockStrategy, searchStrategy, exprMeetStrategy
);
final var result = abstractor.check();
resultPrinter(result.isSafe(), result.isUnsafe(), system);
}

private void runCombined(final XtaSystem system) {
final var config = CombinedLazyCegarXtaCheckerConfigFactory.create(system, NullLogger.getInstance(), Z3SolverFactory.getInstance()).build();
final var result = config.check();
resultPrinter(result.isSafe(), result.isUnsafe(), system);
}

private void runEager(XtaSystem system){
final SafetyChecker<?, ?, UnitPrec> checker = LazyXtaCheckerFactory.create(system, dataStrategy,
clockStrategy, searchStrategy);
final SafetyResult<?, ?> result = check(checker);
resultPrinter(result.isSafe(), result.isUnsafe(), system);
if (dotfile != null) {
writeVisualStatus(result, dotfile);
}
}

private void resultPrinter(final boolean isSafe, final boolean isUnsafe, final XtaSystem system) {
if (isSafe) {
switch (system.getPropertyKind()) {
case AG -> System.out.println("(SafetyResult Safe)");
case EF -> System.out.println("(SafetyResult Unsafe)");
default -> throw new UnsupportedOperationException();
}
} else if (isUnsafe) {
switch (system.getPropertyKind()) {
case AG -> System.out.println("(SafetyResult Unsafe)");
case EF -> System.out.println("(SafetyResult Safe)");
default -> throw new UnsupportedOperationException();
}
} else {
throw new UnsupportedOperationException();
}
}

private SafetyResult<?, ?> check(SafetyChecker<?, ?, UnitPrec> checker) throws Exception {
try {
return checker.check(UnitPrec.getInstance());
Expand All @@ -222,9 +288,17 @@ private XtaSystem loadModel() throws Exception {
try (InputStream inputStream = new FileInputStream(model)) {
return XtaDslManager.createSystem(inputStream);
}
} catch (CTLOperatorNotSupportedException ex) {
ex.printStackTrace();
System.exit(11);
} catch (MixedDataTimeNotSupportedException ex) {
ex.printStackTrace();
System.exit(12);
} catch (Exception ex) {
throw new Exception("Could not parse XTA: " + ex.getMessage(), ex);
ex.printStackTrace();
System.exit(10);
}
throw new AssertionError();
}

private void printResult(final SafetyResult<?, ?> result) {
Expand Down
Loading

0 comments on commit d308fc2

Please sign in to comment.