From d308fc283a809dd432a6e28b2eca81b8d2e8d503 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= <3751182+as3810t@users.noreply.github.com> Date: Tue, 25 Oct 2022 11:22:58 +0200 Subject: [PATCH] Improve XTA property parsing, add combined to CLI --- ...binedLazyCegarXtaCheckerConfigFactory.java | 206 ++++++++++++++++++ .../java/hu/bme/mit/theta/xta/cli/XtaCli.java | 100 +++++++-- subprojects/xta/xta/src/main/antlr/XtaDsl.g4 | 13 +- .../java/hu/bme/mit/theta/xta/XtaProcess.java | 3 +- .../java/hu/bme/mit/theta/xta/XtaSystem.java | 15 +- .../mit/theta/xta/dsl/XtaProcessSymbol.java | 4 +- .../mit/theta/xta/dsl/XtaSpecification.java | 10 +- .../bme/mit/theta/xta/dsl/XtaTransition.java | 28 ++- .../CTLOperatorNotSupportedException.java | 7 + .../MixedDataTimeNotSupportedException.java | 7 + 10 files changed, 357 insertions(+), 36 deletions(-) create mode 100644 subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java create mode 100644 subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/CTLOperatorNotSupportedException.java create mode 100644 subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/MixedDataTimeNotSupportedException.java diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java new file mode 100644 index 0000000000..b192b554fd --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/combinedlazycegar/CombinedLazyCegarXtaCheckerConfigFactory.java @@ -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 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>, XtaAction, Prod2Prec> + createLazyAnalysis(final SolverFactory solverFactory, + final PartialOrd> abstrPartialOrd, + final InitAbstractor, Prod2State> initAbstractor) { + final Prod2Analysis + prod2ConcrAnalysis = createConcrAnalysis(solverFactory); + final XtaAnalysis, Prod2Prec> + xtaConcrAnalysis = XtaAnalysis.create(system, prod2ConcrAnalysis); + + return LazyAnalysis.create( + XtaOrd.create(abstrPartialOrd), + xtaConcrAnalysis.getInitFunc(), + xtaConcrAnalysis.getTransFunc(), + XtaInitAbstractor.create(initAbstractor) + ); + } + + private Prod2Analysis createConcrAnalysis(final SolverFactory solverFactory) { + return Prod2Analysis.create( + createConcrDataAnalysis(solverFactory), + createConcrClockAnalysis() + ); + } + + private Analysis createConcrDataAnalysis(final SolverFactory solverFactory) { + return CombinedLazyCegarXtaAnalysis.create( + ExplAnalysis.create( + solverFactory.createSolver(), + system.getInitVal().toExpr() + ) + ); + } + + private Analysis createConcrClockAnalysis() { + return XtaZoneAnalysis.getInstance(); + } + + private LazyStrategy, Prod2State, LazyState>, XtaState>>, XtaAction> + createLazyStrategy(final ClockStrategy clockStrategy) { + final LazyStrategy>, XtaState>>, XtaAction> + dataLazyStrategy = forceCast(createDataStrategy2()); + + final LazyStrategy>, XtaState>>, XtaAction> + clockLazyStrategy = forceCast(createClockStrategy(clockStrategy)); + + final Function>, XtaState>>, ?> projection = s -> Tuple3.of( + s.getConcrState().getLocs(), + dataLazyStrategy.getProjection().apply(s), + clockLazyStrategy.getProjection().apply(s) + ); + + final Lens>, XtaState>>, Prod2State> + lens = createConcrProd2Lens(); + return new Prod2LazyStrategy<>(lens, dataLazyStrategy, clockLazyStrategy, projection); + } + + private LazyStrategy>, XtaState>>, XtaAction> createDataStrategy2() { + return new BasicLazyStrategy<>( + createDataLens(), + createDataConcretizer() + ); + } + + private Lens>, XtaState>>, ExplState> createDataLens() { + return LazyXtaLensUtils.createConcrDataLens(); + } + + private Concretizer createDataConcretizer() { + return BasicConcretizer.create(ExplOrd.getInstance()); + } + + private LazyStrategy>, XtaState>>, XtaAction> createClockStrategy(final ClockStrategy clockStrategy) { + return switch (clockStrategy) { + case BWITP, FWITP -> createLazyZoneStrategy(clockStrategy); + case LU -> throw new AssertionError(); + }; + } + + private LazyStrategy>, XtaState>>, XtaAction> + createLazyZoneStrategy(final ClockStrategy clockStrategy) { + + final Lens>, XtaState>>, LazyState> + lens = LazyXtaLensUtils.createLazyClockLens(); + final Lattice lattice = ZoneLattice.getInstance(); + final Interpolator interpolator = ZoneInterpolator.getInstance(); + final PartialOrd partialOrd = ZoneOrd.getInstance(); + final Concretizer concretizer = BasicConcretizer.create(partialOrd); + final InvTransFunc 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 zoneTransFunc = XtaZoneTransFunc.getInstance(); + return new FwItpStrategy<>(lens, lattice, interpolator, concretizer, zoneInvTransFunc, prec, zoneTransFunc, prec); + default: + throw new AssertionError(); + } + } + + private Prod2Prec createConcrPrec() { + return Prod2Prec.of(createConcrDataPrec(), createConcrZonePrec()); + } + + private ExplPrec createConcrDataPrec() { + return ExplPrec.empty(); + } + + private ZonePrec createConcrZonePrec() { + return ZonePrec.of(system.getClockVars()); + } + +} diff --git a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java index a2d9725b13..f451222c4d 100644 --- a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java +++ b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java @@ -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; @@ -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; @@ -58,6 +64,8 @@ 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; @@ -65,6 +73,11 @@ 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; @@ -72,14 +85,23 @@ public final class XtaCli { @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; @@ -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; @@ -195,12 +220,10 @@ private void run() { try { final XtaSystem system = loadModel(); - final SafetyChecker 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); @@ -208,6 +231,49 @@ private void run() { } } + 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 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 checker) throws Exception { try { return checker.check(UnitPrec.getInstance()); @@ -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) { diff --git a/subprojects/xta/xta/src/main/antlr/XtaDsl.g4 b/subprojects/xta/xta/src/main/antlr/XtaDsl.g4 index 6903533eed..8b6b7fab49 100644 --- a/subprojects/xta/xta/src/main/antlr/XtaDsl.g4 +++ b/subprojects/xta/xta/src/main/antlr/XtaDsl.g4 @@ -53,7 +53,7 @@ functionDecl ; processDecl - : PROCESS fId=ID fParameterList=parameterList LBRAC fProcessBody=processBody RBRAC + : PROCESS fId=ID fParameterList=parameterList? LBRAC fProcessBody=processBody RBRAC ; processBody @@ -105,7 +105,7 @@ select ; guard - : GUARD fExpression=expression SEMICOLON + : GUARD fExpressions+=expression (COMMA fExpressions+=expression)* SEMICOLON ; sync: SYNC fExpression=expression (fEmit=EXCL | fRecv=QUEST) SEMICOLON @@ -738,7 +738,7 @@ structSelectOp quantifier - : AG | EF + : AG | EF | AF | EG ; FORALL @@ -972,6 +972,13 @@ RARROW AG : 'A[]' ; + +AF + : 'A<>' + ; +EG + : 'E[]' + ; EF : 'E<>' ; diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java index e52eeb4037..c8b3956682 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java @@ -27,6 +27,7 @@ import hu.bme.mit.theta.core.type.rattype.RatType; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.StmtUtils; +import hu.bme.mit.theta.xta.utils.MixedDataTimeNotSupportedException; import java.util.*; import java.util.stream.Collectors; @@ -158,7 +159,7 @@ private Collection createGuards(final Collection> exprs) { } else if (!dataExpr && clockExpr) { guard = Guard.clockGuard(expr); } else { - throw new UnsupportedOperationException(); + throw new MixedDataTimeNotSupportedException(expr.toString()); } builder.add(guard); } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java index c80c3a12ae..b7babb7e15 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaSystem.java @@ -23,6 +23,7 @@ import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.xta.XtaProcess.Loc; import java.lang.management.LockInfo; @@ -44,6 +45,7 @@ public final class XtaSystem { private Expr prop; + private PropertyKind propertyKind = PropertyKind.NONE; private XtaSystem() { processes = new ArrayList<>(); @@ -107,18 +109,21 @@ public Expr getProp(){ return prop; } + public PropertyKind getPropertyKind() { + return propertyKind; + } - - public void setProp(final Expr _prop){ + public void setProp(final Expr _prop, final PropertyKind _propertyKind){ prop = _prop; + propertyKind = _propertyKind; //ErrorProcess XtaProcess process = createProcess("ErrorProc"); final Collection> invars = Collections.emptySet(); Loc initloc = process.createLoc("InitLoc", XtaProcess.LocKind.NORMAL, invars); process.setInitLoc(initloc); Loc errorLoc = process.createLoc("ErrorLoc", XtaProcess.LocKind.ERROR, invars); - final Collection> guards = Set.of(prop); + final Collection> guards = ExprUtils.getConjuncts(ExprUtils.simplify(prop)); process.createEdge(initloc, errorLoc, guards, Optional.empty(), Collections.emptyList()); //Edges to ErrorLocations from COMMITTED locations @@ -137,4 +142,8 @@ public void setProp(final Expr _prop){ } } + + public enum PropertyKind { + AG, AF, EG, EF, NONE + } } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java index 40cac0db24..9b5032d9ef 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaProcessSymbol.java @@ -73,7 +73,9 @@ public XtaProcessSymbol(final XtaSpecification scope, final ProcessDeclContext c transitions = context.fProcessBody.fTransitions.fTransitions.stream().map(t -> new XtaTransition(this, t)) .collect(toList()); - declareAllParameters(context.fParameterList.fParameterDecls); + if (context.fParameterList != null) { + declareAllParameters(context.fParameterList.fParameterDecls); + } declareAllTypes(context.fProcessBody.fTypeDecls); declareAllVariables(context.fProcessBody.fVariableDecls); declareAllFunctions(context.fProcessBody.fFunctionDecls); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java index 210d381e08..bd72505b1f 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaSpecification.java @@ -30,6 +30,7 @@ import hu.bme.mit.theta.xta.XtaSystem; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.*; +import hu.bme.mit.theta.xta.utils.CTLOperatorNotSupportedException; import org.antlr.v4.runtime.Token; import java.util.*; @@ -127,11 +128,13 @@ private XtaSystem instantiate() { if(context.fProperty.q.children.get(0).toString().equals("A[]")) { prop = BoolExprs.Not(prop); + system.setProp(prop, XtaSystem.PropertyKind.AG); + } else if (context.fProperty.q.children.get(0).toString().equals("E<>")) { + system.setProp(prop, XtaSystem.PropertyKind.EF); + } else { + throw new CTLOperatorNotSupportedException(context.fProperty.q.children.get(0).toString()); } //if(context.fProperty.neg != null) prop = BoolExprs.Not(prop); - - - system.setProp(prop); } return system; } @@ -278,7 +281,6 @@ public Optional resolve(final String name) { } - //// } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaTransition.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaTransition.java index 1acd198aba..bb5be018a0 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaTransition.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaTransition.java @@ -25,6 +25,7 @@ import java.util.Collection; import java.util.List; import java.util.Optional; +import java.util.stream.Collectors; import hu.bme.mit.theta.common.dsl.Env; import hu.bme.mit.theta.common.dsl.Scope; @@ -38,6 +39,8 @@ import hu.bme.mit.theta.xta.Sync; import hu.bme.mit.theta.xta.XtaProcess; import hu.bme.mit.theta.xta.XtaProcess.Loc; +import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser; +import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.GuardContext; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.IteratorDeclContext; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.SelectContext; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.TransitionContext; @@ -49,7 +52,7 @@ final class XtaTransition implements Scope { private final String sourceState; private final String targetState; private final List selections; - private final Optional guard; + private final List guards; private final Optional sync; private final List updates; @@ -62,19 +65,25 @@ public XtaTransition(final XtaProcessSymbol scope, final TransitionContext conte targetState = context.fTargetId.getText(); selections = new ArrayList<>(); - guard = extractGuard(context); + guards = new ArrayList<>(); sync = extractSync(context); updates = extractUpdates(context); declareAllSelections(context.fTransitionBody.fSelect); + extractGuards(context.fTransitionBody.fGuard); } private Optional extractSync(final TransitionContext context) { return Optional.ofNullable(context.fTransitionBody.fSync).map(s -> new XtaSync(this, s)); } - private Optional extractGuard(final TransitionContext context) { - return Optional.ofNullable(context.fTransitionBody.fGuard).map(g -> new XtaExpression(this, g.fExpression)); + private void extractGuards(final GuardContext context) { + if (context != null) { + if (context.fExpressions != null) { + context.fExpressions.forEach(e -> guards.add(new XtaExpression(this, e))); + + } + } } private List extractUpdates(final TransitionContext context) { @@ -110,15 +119,12 @@ public void instantiate(final XtaProcess process, final Env env) { final Loc source = (Loc) env.eval(sourceSymbol); final Loc target = (Loc) env.eval(targetSymbol); - final Collection> guards; - if (guard.isPresent()) { - final Expr expr = guard.get().instantiate(env); + final Collection> guards = this.guards.stream().flatMap(guard -> { + final Expr expr = guard.instantiate(env); final Expr guardExpr = TypeUtils.cast(expr, Bool()); final Collection> conjuncts = ExprUtils.getConjuncts(guardExpr); - guards = conjuncts.stream().map(e -> e).collect(toList()); - } else { - guards = emptySet(); - } + return conjuncts.stream(); + }).collect(Collectors.toSet()); final List assignments = updates.stream().map(u -> u.instantiate(env)).collect(toList()); final Optional label = sync.map(s -> s.instantiate(env)); diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/CTLOperatorNotSupportedException.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/CTLOperatorNotSupportedException.java new file mode 100644 index 0000000000..06420178f8 --- /dev/null +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/CTLOperatorNotSupportedException.java @@ -0,0 +1,7 @@ +package hu.bme.mit.theta.xta.utils; + +public class CTLOperatorNotSupportedException extends RuntimeException { + public CTLOperatorNotSupportedException(final String operator) { + super(operator + " is not supported"); + } +} diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/MixedDataTimeNotSupportedException.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/MixedDataTimeNotSupportedException.java new file mode 100644 index 0000000000..5dc9ced6e5 --- /dev/null +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/MixedDataTimeNotSupportedException.java @@ -0,0 +1,7 @@ +package hu.bme.mit.theta.xta.utils; + +public class MixedDataTimeNotSupportedException extends RuntimeException { + public MixedDataTimeNotSupportedException(final String guard) { + super("Mixing data and clock variables inside one guard is not supported: " + guard); + } +}