ton of changes

RipplB · Oct 24, 2023 · 5ae2e10 · 5ae2e10
1 parent f97ee3c
commit 5ae2e10
Show file tree

Hide file tree

Showing 47 changed files with 1,789 additions and 494 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "4.4.4"
+    version = "21.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/cfa/cfa/src/main/antlr/LTLGrammar.g4 b/subprojects/cfa/cfa/src/main/antlr/LTLGrammar.g4
@@ -82,6 +82,7 @@ negExpr:
 primaryExpr:
 	boolLitExpr|
 	intLitExpr|
+	enumLitExpr|
 	parenExpr
 ;
 
@@ -97,6 +98,10 @@ intLitExpr:
 	value=INTLIT
 ;
 
+enumLitExpr:
+    type=ID DOT lit=ID
+;
+
 variable:
 	name=ID
 ;
@@ -128,5 +133,6 @@ X_OP: 'X';
 INTLIT: [0-9]+;
 BOOLLIT: 'true' | 'false';
 ID: [a-zA-Z][a-zA-Z0-9_]*;
+DOT: '.';
 WS: (' '| '\t' | '\n' | '\r') -> skip;
 
diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/APGeneratorVisitor.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/APGeneratorVisitor.java
@@ -20,6 +20,8 @@
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr;
+import hu.bme.mit.theta.core.type.enumtype.EnumType;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -32,12 +34,12 @@
 
 public class APGeneratorVisitor extends LTLGrammarBaseVisitor<Expr> {
 
-	Map<String, VarDecl<?>> vars;
-	Map<String, Integer> literals;
+	private final Map<String, VarDecl<?>> vars;
+	private final Map<String, EnumType> enumTypes;
 
-	public APGeneratorVisitor(Map<String, VarDecl<?>> vars, Map<String, Integer> literals) {
+	public APGeneratorVisitor(Map<String, VarDecl<?>> vars, Map<String, EnumType> enumTypes) {
 		this.vars = vars;
-		this.literals = literals;
+		this.enumTypes = enumTypes;
 	}
 
 	@Override
@@ -181,6 +183,8 @@ public Expr visitPrimaryExpr(LTLGrammarParser.PrimaryExprContext ctx) {
 			return visitBoolLitExpr(ctx.boolLitExpr());
 		} else if (ctx.intLitExpr() != null) {
 			return visitIntLitExpr(ctx.intLitExpr());
+		} else if (ctx.enumLitExpr() != null) {
+			return visitEnumLitExpr(ctx.enumLitExpr());
 		} else return visitParenExpr(ctx.parenExpr());
 	}
 
@@ -201,9 +205,13 @@ public Expr visitIntLitExpr(LTLGrammarParser.IntLitExprContext ctx) {
 		return Int(Integer.parseInt(ctx.value.getText()));
 	}
 
+	@Override
+	public Expr visitEnumLitExpr(LTLGrammarParser.EnumLitExprContext ctx) {
+		return EnumLitExpr.of(enumTypes.get(ctx.type.getText()), ctx.lit.getText());
+	}
+
 	@Override
 	public Expr visitVariable(LTLGrammarParser.VariableContext ctx) {
-		if (literals.containsKey(ctx.name.getText())) return Int(literals.get(ctx.name.getText()));
 		VarDecl decl = vars.get(ctx.name.getText());
 		if (decl == null) System.out.println("Variable [" + ctx.name.getText() + "] not found");
 		return decl.getRef();

diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/BuchiBuilder.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/BuchiBuilder.java
@@ -25,6 +25,7 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolExprs;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.enumtype.EnumType;
 import jhoafparser.ast.AtomAcceptance;
 import jhoafparser.ast.AtomLabel;
 import jhoafparser.ast.BooleanExpression;
@@ -70,8 +71,8 @@ public static CFA of(String ltlExpression, Collection<VarDecl<?>> variables, fin
                 )
         ).model();
         Map<String, VarDecl<?>> namedVariables = variables.stream().collect(Collectors.toMap(Decl::getName, v -> v));
-        Map<String, Integer> literalToIntMap = new HashMap<>();
-        ToStringVisitor toStringVisitor = new ToStringVisitor(new APGeneratorVisitor(namedVariables, literalToIntMap));
+        Map<String, EnumType> enumTypes = variables.stream().map(VarDecl::getType).filter(EnumType.class::isInstance).map(t -> (EnumType) t).distinct().collect(Collectors.toMap(EnumType::getName, t -> t));
+        ToStringVisitor toStringVisitor = new ToStringVisitor(new APGeneratorVisitor(namedVariables, enumTypes));
         String swappedLtl = toStringVisitor.visitModel(modelContext);
         LabelledFormula negatedLtl = LtlParser.parse(swappedLtl).not();
         Automaton<Either<Formula, ProductState>, BuchiAcceptance> oautomaton = SymmetricNBAConstruction.of(BuchiAcceptance.class).apply(negatedLtl);

diff --git a/...s/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/BasicLDGTraceRefiner.java b/...s/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/BasicLDGTraceRefiner.java
@@ -0,0 +1,69 @@
+/*
+ *  Copyright 2023 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.loopchecker;
+
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult;
+import hu.bme.mit.theta.analysis.expr.ExprAction;
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus;
+import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation;
+import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner;
+import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec;
+import hu.bme.mit.theta.common.logging.Logger;
+import hu.bme.mit.theta.common.logging.NullLogger;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.solver.ItpSolver;
+
+import java.util.Collection;
+
+import static com.google.common.base.Preconditions.checkArgument;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+
+public final class BasicLDGTraceRefiner<S extends ExprState, A extends ExprAction, P extends Prec> implements LDGTraceRefiner<S, A, P> {
+	private final ItpSolver solver;
+	private final Expr<BoolType> init;
+	private final JoiningPrecRefiner<S, A, P, ItpRefutation> refiner;
+	private final Logger logger;
+
+	private BasicLDGTraceRefiner(ItpSolver solver, Expr<BoolType> init, RefutationToPrec<P, ItpRefutation> refToPrec, Logger logger) {
+		this.solver = solver;
+		this.init = init;
+		this.logger = logger != null ? logger : NullLogger.getInstance();
+		refiner = JoiningPrecRefiner.create(refToPrec);
+	}
+
+	public static <S extends ExprState, A extends ExprAction, P extends Prec> BasicLDGTraceRefiner<S, A, P> create(ItpSolver solver, Expr<BoolType> init, RefutationToPrec<P, ItpRefutation> refToPrec, Logger logger) {
+		return new BasicLDGTraceRefiner<>(solver, init, refToPrec, logger);
+	}
+
+	public static <S extends ExprState, A extends ExprAction, P extends Prec> BasicLDGTraceRefiner<S, A, P> create(ItpSolver solver, RefutationToPrec<P, ItpRefutation> refToPrec, Logger logger) {
+		return create(solver, True(), refToPrec, logger);
+	}
+
+	public RefinerResult<S, A, P> check(final Collection<LDGTrace<S, A>> ldgTraces, final P currentPrecision, RefinerStrategy refinerStrategy) {
+		checkArgument(!ldgTraces.isEmpty(), "%s needs at least one trace!", getClass().getSimpleName());
+		var ldgTrace = ldgTraces.iterator().next();
+		ExprTraceStatus<ItpRefutation> refutation = LDGTraceChecker.check(ldgTrace, solver, init, refinerStrategy, logger);
+		if (refutation.isInfeasible()) {
+			P refinedPrecision = refiner.refine(currentPrecision, ldgTrace.toTrace(), refutation.asInfeasible().getRefutation());
+			return RefinerResult.spurious(refinedPrecision);
+		}
+		return RefinerResult.unsafe(ldgTrace.toTrace());
+	}
+
+}