diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties index 77da25281b..d4ddb17d8d 100644 --- a/buildSrc/gradle.properties +++ b/buildSrc/gradle.properties @@ -17,7 +17,7 @@ javaVersion=17 kotlinVersion=1.9.25 shadowVersion=7.1.2 -antlrVersion=4.9.2 +antlrVersion=4.12.0 guavaVersion=31.1-jre jcommanderVersion=1.72 z3Version=4.5.0 @@ -40,4 +40,5 @@ gsonVersion=2.9.1 javasmtVersion=4.1.1 sosylabVersion=0.3000-569-g89796f98 cliktVersion=4.4.0 -spotlessVersion=6.25.0 \ No newline at end of file +spotlessVersion=6.25.0 +jbddVersion=0.5.2 diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt index 642499ed8f..d74ff82b57 100644 --- a/buildSrc/src/main/kotlin/Deps.kt +++ b/buildSrc/src/main/kotlin/Deps.kt @@ -79,4 +79,6 @@ object Deps { } val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}" + + val jbdd = "de.tum.in:jbdd:${Versions.jbdd}" } diff --git a/lib/jhoafparser-1.1.1.jar b/lib/jhoafparser-1.1.1.jar new file mode 100644 index 0000000000..750256100b Binary files /dev/null and b/lib/jhoafparser-1.1.1.jar differ diff --git a/lib/owl-21.0.jar b/lib/owl-21.0.jar new file mode 100644 index 0000000000..2e9916bcbb Binary files /dev/null and b/lib/owl-21.0.jar differ diff --git a/settings.gradle.kts b/settings.gradle.kts index 5421f34ea0..c66e3b4fe6 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -21,6 +21,7 @@ include( "common/core", "common/grammar", "common/multi-tests", + "common/ltl", "frontends/c-frontend", "frontends/petrinet-frontend/petrinet-model", diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java index 213fafdd07..6ce50146b5 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java @@ -15,15 +15,6 @@ */ package hu.bme.mit.theta.cfa.analysis.utils; -import java.awt.Color; - -import hu.bme.mit.theta.common.container.Containers; - -import java.util.LinkedHashSet; -import java.util.Map; -import java.util.Optional; -import java.util.Set; - import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.cfa.CFA; @@ -31,17 +22,20 @@ import hu.bme.mit.theta.cfa.CFA.Loc; import hu.bme.mit.theta.cfa.analysis.CfaAction; import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.common.table.TableWriter; -import hu.bme.mit.theta.common.visualization.Alignment; -import hu.bme.mit.theta.common.visualization.EdgeAttributes; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.LineStyle; -import hu.bme.mit.theta.common.visualization.NodeAttributes; import hu.bme.mit.theta.common.visualization.Shape; +import hu.bme.mit.theta.common.visualization.*; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.dsl.CoreDslManager; +import java.awt.*; +import java.util.LinkedHashSet; +import java.util.Map; +import java.util.Optional; +import java.util.Set; + public final class CfaVisualizer { private static final String CFA_LABEL = ""; @@ -51,6 +45,7 @@ public final class CfaVisualizer { private static final Color LINE_COLOR = Color.BLACK; private static final LineStyle LOC_LINE_STYLE = LineStyle.NORMAL; private static final LineStyle EDGE_LINE_STYLE = LineStyle.NORMAL; + private static final LineStyle ACC_EDGE_LINE_STYLE = LineStyle.DASHED; private static final String EDGE_FONT = "courier"; private CfaVisualizer() { @@ -64,7 +59,7 @@ public static Graph visualize(final CFA cfa) { addLocation(graph, cfa, loc, ids); } for (final Edge edge : cfa.getEdges()) { - addEdge(graph, edge, ids); + addEdge(graph, edge, cfa.getAcceptingEdges().contains(edge), ids); } return graph; } @@ -102,10 +97,10 @@ private static void addLocation(final Graph graph, final CFA cfa, final Loc loc, graph.addNode(id, nAttrs); } - private static void addEdge(final Graph graph, final Edge edge, final Map ids) { + private static void addEdge(final Graph graph, final Edge edge, final boolean accepting, final Map ids) { final EdgeAttributes eAttrs = EdgeAttributes.builder() .label(new CoreDslManager().writeStmt(edge.getStmt())) - .color(LINE_COLOR).lineStyle(EDGE_LINE_STYLE).font(EDGE_FONT).build(); + .color(LINE_COLOR).lineStyle(accepting ? ACC_EDGE_LINE_STYLE : EDGE_LINE_STYLE).font(EDGE_FONT).build(); graph.addEdge(ids.get(edge.getSource()), ids.get(edge.getTarget()), eAttrs); } diff --git a/subprojects/cfa/cfa/build.gradle.kts b/subprojects/cfa/cfa/build.gradle.kts index 25854d3935..cbbc376301 100644 --- a/subprojects/cfa/cfa/build.gradle.kts +++ b/subprojects/cfa/cfa/build.gradle.kts @@ -22,4 +22,5 @@ plugins { dependencies { implementation(project(":theta-common")) implementation(project(":theta-core")) + implementation(Deps.jbdd) } diff --git a/subprojects/cfa/cfa/src/main/antlr/LTLGrammar.g4 b/subprojects/cfa/cfa/src/main/antlr/LTLGrammar.g4 new file mode 100644 index 0000000000..e133f146ff --- /dev/null +++ b/subprojects/cfa/cfa/src/main/antlr/LTLGrammar.g4 @@ -0,0 +1,138 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +grammar LTLGrammar; + +model: + rules+=implyExpression*; + +implyExpression: + ops+=orExpr (IMPLIES ops+=orExpr)? +; + +orExpr: + ops+=andExpr (OR ops+=andExpr)* +; + +andExpr: + ops+=notExpr (AND ops+=notExpr)* +; + +notExpr: + binaryLtlExpr| + NOT ops+=notExpr +; + +binaryLtlExpr: + ltlExpr | + ops+=binaryLtlExpr type=binaryLtlOp ops+=binaryLtlExpr; + +binaryLtlOp: + M_OP | W_OP | U_OP | R_OP; + +ltlExpr: + eqExpr | + type=ltlOp ops+=ltlExpr +; + +ltlOp: + F_OP|G_OP|X_OP + ; + +eqExpr: + ops+=relationExpr (oper=eqOperator ops+=relationExpr)? +; + +eqOperator: + EQ|NEQ +; + +relationExpr: + ops+=additiveExpr (oper=relationOperator ops+=additiveExpr)? +; + +relationOperator: + LT|GT|LEQ|GEQ +; + +additiveExpr: + ops+=multiplicativeExpr (opers+=additiveOperator ops+=multiplicativeExpr)* +; + +additiveOperator: + PLUS|MINUS +; + +multiplicativeExpr: + ops+=negExpr (opers+=multiplicativeOperator ops+=negExpr)* +; + +multiplicativeOperator: + MUL|DIV|MOD +; + +negExpr: + primaryExpr| + MINUS ops+=negExpr +; + +primaryExpr: + boolLitExpr| + intLitExpr| + enumLitExpr| + parenExpr +; + +boolLitExpr: + value=BOOLLIT +; + +parenExpr: + LPAREN ops+=implyExpression RPAREN | variable +; + +intLitExpr: + value=INTLIT +; + +enumLitExpr: + type=ID DOT lit=ID +; + +variable: + name=ID +; + +AND: 'and' | '&&'; +OR: 'or' | '|' | '||'; +IMPLIES: '->' | '=>'; +NOT: 'not' | '!'; +EQ: '=' | '=='; +NEQ: '/=' | '!='; +LT: '<'; +GT: '>'; +LEQ: '<='; +GEQ: '>='; +PLUS: '+'; +MINUS: '-'; +MUL: '*'; +DIV: '/'; +MOD: '%'; +LPAREN: '('; +RPAREN: ')'; +F_OP: 'F'; +G_OP: 'G'; +U_OP: 'U'; +W_OP: 'W'; +M_OP: 'M'; +R_OP: 'R'; +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/CFA.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java index 49c2dc1efc..42c68fdd24 100644 --- a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java @@ -15,23 +15,20 @@ */ package hu.bme.mit.theta.cfa; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static com.google.common.base.Preconditions.checkState; -import static com.google.common.collect.ImmutableSet.toImmutableSet; -import static java.lang.String.format; - -import java.util.*; - import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; - import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.utils.StmtUtils; +import java.util.*; + +import static com.google.common.base.Preconditions.*; +import static com.google.common.collect.ImmutableSet.toImmutableSet; +import static java.lang.String.format; + /** * Represents an immutable Control Flow Automata (CFA). Use the builder class to create a new * instance. @@ -45,6 +42,7 @@ public final class CFA { private final Collection> vars; private final Collection locs; private final Collection edges; + private final Collection acceptingEdges; private CFA(final Builder builder) { initLoc = builder.initLoc; @@ -60,6 +58,7 @@ private CFA(final Builder builder) { "Variable with name '" + v.getName() + "' already exists in the CFA."); varNames.add(v.getName()); } + acceptingEdges = builder.acceptingEdges; } public Loc getInitLoc() { @@ -89,6 +88,10 @@ public Collection getEdges() { return edges; } + public Collection getAcceptingEdges() { + return acceptingEdges; + } + public static Builder builder() { return new Builder(); } @@ -185,6 +188,7 @@ public static final class Builder { private final Collection locs; private final Collection edges; + private final Collection acceptingEdges; private final Set locNames; @@ -196,6 +200,7 @@ private Builder() { locs = Containers.createSet(); locNames = Containers.createSet(); edges = new LinkedList<>(); + acceptingEdges = Containers.createSet(); built = false; } @@ -264,6 +269,13 @@ public Edge createEdge(final Loc source, final Loc target, final Stmt stmt) { return edge; } + public void setAcceptingEdge(final Edge acceptingEdge) { + checkNotBuilt(); + checkNotNull(acceptingEdge); + checkArgument(edges.contains(acceptingEdge), "Accepting edge not present in CFA."); + acceptingEdges.add(acceptingEdge); + } + public CFA build() { checkState(initLoc != null, "Initial location must be set."); if (finalLoc != null) { 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 new file mode 100644 index 0000000000..3d02359887 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/APGeneratorVisitor.java @@ -0,0 +1,221 @@ +/* + * 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.cfa.buchi; + +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarBaseVisitor; +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarParser; +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; +import java.util.Map; + +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Mod; + +public class APGeneratorVisitor extends LTLGrammarBaseVisitor { + + private final Map> vars; + private final Map enumTypes; + + public APGeneratorVisitor(Map> vars, Map enumTypes) { + this.vars = vars; + this.enumTypes = enumTypes; + } + + @Override + public Expr visitModel(LTLGrammarParser.ModelContext ctx) { + return super.visitModel(ctx); + } + + @Override + public Expr visitImplyExpression(LTLGrammarParser.ImplyExpressionContext ctx) { + if (ctx.ops.size() > 1) { + return Imply(visitOrExpr(ctx.ops.get(0)), visitOrExpr(ctx.ops.get(1))); + } else return visitOrExpr(ctx.ops.get(0)); + } + + @Override + public Expr visitOrExpr(LTLGrammarParser.OrExprContext ctx) { + if (ctx.ops.size() == 1) return visitAndExpr(ctx.ops.get(0)); + List> ops = new ArrayList>(); + for (LTLGrammarParser.AndExprContext child : ctx.ops) { + ops.add(visitAndExpr(child)); + } + return Or(ops); + } + + @Override + public Expr visitAndExpr(LTLGrammarParser.AndExprContext ctx) { + if (ctx.ops.size() == 1) return visitNotExpr(ctx.ops.get(0)); + List> ops = new ArrayList>(); + for (LTLGrammarParser.NotExprContext child : ctx.ops) { + ops.add(visitNotExpr(child)); + } + return And(ops); + } + + @Override + public Expr visitNotExpr(LTLGrammarParser.NotExprContext ctx) { + if (ctx.ops.size() > 0) return Not(visitNotExpr(ctx.ops.get(0))); + else return visitBinaryLtlExpr(ctx.binaryLtlExpr()); + } + + @Override + public Expr visitBinaryLtlExpr(LTLGrammarParser.BinaryLtlExprContext ctx) { + return visitLtlExpr(ctx.ltlExpr()); + } + + @Override + public Expr visitBinaryLtlOp(LTLGrammarParser.BinaryLtlOpContext ctx) { + return super.visitBinaryLtlOp(ctx); + } + + @Override + public Expr visitLtlExpr(LTLGrammarParser.LtlExprContext ctx) { + return visitEqExpr(ctx.eqExpr()); + } + + @Override + public Expr visitLtlOp(LTLGrammarParser.LtlOpContext ctx) { + return super.visitLtlOp(ctx); + } + + @Override + public Expr visitEqExpr(LTLGrammarParser.EqExprContext ctx) { + if (ctx.ops.size() > 1) { + if (ctx.oper.EQ() != null) return Eq(visitRelationExpr(ctx.ops.get(0)), visitRelationExpr(ctx.ops.get(1))); + else return Neq(visitRelationExpr(ctx.ops.get(0)), visitRelationExpr(ctx.ops.get(1))); + } else return visitRelationExpr(ctx.ops.get(0)); + } + + @Override + public Expr visitEqOperator(LTLGrammarParser.EqOperatorContext ctx) { + return super.visitEqOperator(ctx); + } + + @Override + public Expr visitRelationExpr(LTLGrammarParser.RelationExprContext ctx) { + if (ctx.ops.size() > 1) { + if (ctx.oper.LEQ() != null) { + return Leq(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1))); + } else if (ctx.oper.GEQ() != null) { + return Geq(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1))); + } else if (ctx.oper.LT() != null) { + return Lt(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1))); + } else return Gt(visitAdditiveExpr(ctx.ops.get(0)), visitAdditiveExpr(ctx.ops.get(1))); + } else return visitAdditiveExpr(ctx.ops.get(0)); + } + + @Override + public Expr visitRelationOperator(LTLGrammarParser.RelationOperatorContext ctx) { + return super.visitRelationOperator(ctx); + } + + @Override + public Expr visitAdditiveExpr(LTLGrammarParser.AdditiveExprContext ctx) { + Expr res = visitMultiplicativeExpr(ctx.ops.get(0)); + for (int i = 1; i < ctx.ops.size(); i++) { + if (ctx.opers.get(i - 1).PLUS() != null) { + res = Add(res, visitMultiplicativeExpr(ctx.ops.get(i))); + } else { + res = Sub(res, visitMultiplicativeExpr(ctx.ops.get(i))); + } + } + return res; + + } + + @Override + public Expr visitAdditiveOperator(LTLGrammarParser.AdditiveOperatorContext ctx) { + return super.visitAdditiveOperator(ctx); + } + + @Override + public Expr visitMultiplicativeExpr(LTLGrammarParser.MultiplicativeExprContext ctx) { + Expr res = visitNegExpr(ctx.ops.get(0)); + for (int i = 1; i < ctx.ops.size(); i++) { + if (ctx.opers.get(i - 1).DIV() != null) { + res = Div(res, visitNegExpr(ctx.ops.get(i))); + } else if (ctx.opers.get(i - 1).MOD() != null) { + res = Mod(res, visitNegExpr(ctx.ops.get(i))); + } else { + res = Mul(res, visitNegExpr(ctx.ops.get(i))); + } + } + return res; + } + + @Override + public Expr visitMultiplicativeOperator(LTLGrammarParser.MultiplicativeOperatorContext ctx) { + return super.visitMultiplicativeOperator(ctx); + } + + @Override + public Expr visitNegExpr(LTLGrammarParser.NegExprContext ctx) { + if (ctx.ops.size() > 0) { + return Neg(visitNegExpr(ctx.ops.get(0))); + } else return visitPrimaryExpr(ctx.primaryExpr()); + } + + @Override + public Expr visitPrimaryExpr(LTLGrammarParser.PrimaryExprContext ctx) { + if (ctx.boolLitExpr() != null) { + 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()); + } + + @Override + public Expr visitBoolLitExpr(LTLGrammarParser.BoolLitExprContext ctx) { + if (ctx.value.getText().equals("true")) return True(); + else return False(); + } + + @Override + public Expr visitParenExpr(LTLGrammarParser.ParenExprContext ctx) { + if (ctx.variable() != null) return visitVariable(ctx.variable()); + else return visitImplyExpression(ctx.ops.get(0)); + } + + @Override + 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) { + 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 new file mode 100644 index 0000000000..7d4499eab8 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/BuchiBuilder.java @@ -0,0 +1,217 @@ +/* + * 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.cfa.buchi; + +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarLexer; +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarParser; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.stmt.Stmts; +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; +import jhoafparser.consumer.HOAConsumer; +import jhoafparser.consumer.HOAConsumerException; +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.CommonTokenStream; +import owl.automaton.Automaton; +import owl.automaton.acceptance.BuchiAcceptance; +import owl.automaton.hoa.HoaWriter; +import owl.collections.Either; +import owl.ltl.Formula; +import owl.ltl.LabelledFormula; +import owl.ltl.parser.LtlParser; +import owl.translations.ltl2nba.ProductState; +import owl.translations.ltl2nba.SymmetricNBAConstruction; + +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.stream.Collectors; + +public final class BuchiBuilder implements HOAConsumer { + + private final CFA.Builder builder; + private final Logger logger; + private Integer initLocNumber = null; + private List aps; + private final Map locations; + private Map> swappedExpressions; + + private BuchiBuilder(final Logger logger) { + builder = CFA.builder(); + this.logger = logger; + locations = new HashMap<>(); + } + + public static CFA of(String ltlExpression, Collection> variables, final Logger logger) throws HOAConsumerException { + LTLGrammarParser.ModelContext modelContext = new LTLGrammarParser( + new CommonTokenStream( + new LTLGrammarLexer(CharStreams.fromString(ltlExpression)) + ) + ).model(); + Map> namedVariables = variables.stream().collect(Collectors.toMap(Decl::getName, v -> v)); + Map 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, BuchiAcceptance> oautomaton = SymmetricNBAConstruction.of(BuchiAcceptance.class).apply(negatedLtl); + BuchiBuilder buchiBuilder = new BuchiBuilder(logger); + buchiBuilder.swappedExpressions = toStringVisitor.aps; + HoaWriter.write(oautomaton, buchiBuilder, false); + return buchiBuilder.builder.build(); + } + + private CFA.Loc getOrCreateLocation(int locName) { + return locations.computeIfAbsent(locName, i -> builder.createLoc(String.valueOf(i))); + } + + private Expr apBoolExpressionToInternal(BooleanExpression booleanExpression) { + return switch (booleanExpression.getType()) { + case EXP_AND -> BoolExprs.And(apBoolExpressionToInternal(booleanExpression.getLeft()), apBoolExpressionToInternal(booleanExpression.getRight())); + case EXP_OR -> BoolExprs.Or(apBoolExpressionToInternal(booleanExpression.getLeft()), apBoolExpressionToInternal(booleanExpression.getRight())); + case EXP_NOT -> BoolExprs.Not(apBoolExpressionToInternal(booleanExpression.getLeft())); + case EXP_TRUE -> BoolExprs.True(); + case EXP_ATOM -> swappedExpressions.get(aps.get(Integer.parseInt(booleanExpression.getAtom().toString()))); + default -> BoolExprs.False(); + }; + } + + @Override + public boolean parserResolvesAliases() { + return false; + } + + @Override + public void notifyHeaderStart(String s) { + logger.write(Logger.Level.VERBOSE, "HOA consumer header: %s%n", s); + } + + @Override + public void setNumberOfStates(int i) { + logger.write(Logger.Level.VERBOSE, "HOA automaton has %d states%n", i); + } + + @Override + public void addStartStates(List list) throws HOAConsumerException { + if (list.isEmpty() || list.get(0) == null) + return; + if (list.size() != 1 || initLocNumber != null) + throw new HOAConsumerException("HOA automaton should have exactly 1 starting location%n"); + initLocNumber = list.get(0); + } + + @Override + public void addAlias(String s, BooleanExpression booleanExpression) { + // currently does not get called by the Owl library + } + + @Override + public void setAPs(List list) { + if (aps == null) + aps = List.copyOf(list); + else + aps.addAll(list); + } + + @Override + public void setAcceptanceCondition(int i, BooleanExpression booleanExpression) throws HOAConsumerException { + logger.write(Logger.Level.VERBOSE, "Acceptance condition: %s%n", booleanExpression); + } + + @Override + public void provideAcceptanceName(String s, List list) { + logger.write(Logger.Level.VERBOSE, "Acceptance name received: %s%n", s); + list.forEach(o -> logger.write(Logger.Level.VERBOSE, "\tobject under acceptance: %s%n", o)); + } + + @Override + public void setName(String s) throws HOAConsumerException { + logger.write(Logger.Level.VERBOSE, "Automaton named {}%n", s); + } + + @Override + public void setTool(String s, String s1) { + logger.write(Logger.Level.VERBOSE, "Tool named %s %s%n", s, s1); + } + + @Override + public void addProperties(List list) { + if (list.isEmpty()) + return; + logger.write(Logger.Level.VERBOSE, "Properties:%n"); + list.forEach(prop -> logger.write(Logger.Level.VERBOSE, "%s", prop)); + logger.write(Logger.Level.VERBOSE, "%n"); + } + + @Override + public void addMiscHeader(String s, List list) { + // we don't really care of these yet + } + + @Override + public void notifyBodyStart() { + // no action needed + } + + @Override + public void addState(int i, String s, BooleanExpression booleanExpression, List list) { + getOrCreateLocation(i); + } + + @Override + public void addEdgeImplicit(int i, List list, List list1) { + // currently does not get called by the Owl library + } + + @Override + public void addEdgeWithLabel(int i, BooleanExpression booleanExpression, List list, List list1) throws HOAConsumerException { + CFA.Loc from = getOrCreateLocation(i); + CFA.Loc to = getOrCreateLocation(list.get(0)); + CFA.Edge edge = builder.createEdge(from, to, Stmts.Assume(apBoolExpressionToInternal(booleanExpression))); + if (list1 != null && !list1.isEmpty()) + builder.setAcceptingEdge(edge); + } + + @Override + public void notifyEndOfState(int i) { + // no action needed + } + + @Override + public void notifyEnd() throws HOAConsumerException { + if (initLocNumber == null) + throw new HOAConsumerException("No initial location named"); + builder.setInitLoc(locations.get(initLocNumber)); + } + + @Override + public void notifyAbort() { + // never gets called yet + } + + @Override + public void notifyWarning(String s) throws HOAConsumerException { + throw new HOAConsumerException(s); + } +} diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/LTLExprVisitor.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/LTLExprVisitor.java new file mode 100644 index 0000000000..adfdb354f9 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/LTLExprVisitor.java @@ -0,0 +1,271 @@ +/* + * 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.cfa.buchi; + +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarBaseVisitor; +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarParser; +import org.antlr.v4.runtime.ParserRuleContext; + +import java.util.HashMap; + +/** + * Returns whether an AST element represents an LTL expression that has no temporal operators. + * We need to convert all these into atomic propositions that Spot can interpret. + * So in the AST, the F G(not err), the largest expression (not err) will be converted to atomic proposition ap0. + * The resulting LTL expression, which now Spot can interpret, is F G ap0. + * Whether there is an LTL expression, is returned by LTLExprVisitor. + * The link is stored in APGeneratorVisitor's result. + */ +public class LTLExprVisitor extends LTLGrammarBaseVisitor { + + private static LTLExprVisitor instance = new LTLExprVisitor(); + + private LTLExprVisitor() { + } + + ; + + public static LTLExprVisitor getInstance() { + return instance; + } + + HashMap ltl = new HashMap(); + + @Override + public Boolean visitModel(LTLGrammarParser.ModelContext ctx) { + return super.visitModel(ctx); + } + + @Override + public Boolean visitImplyExpression(LTLGrammarParser.ImplyExpressionContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.OrExprContext op : ctx.ops) { + if (visitOrExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitAndExpr(LTLGrammarParser.AndExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.NotExprContext op : ctx.ops) { + if (visitNotExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitNotExpr(LTLGrammarParser.NotExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.NotExprContext op : ctx.ops) { + if (visitNotExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + if (ctx.binaryLtlExpr() != null && visitBinaryLtlExpr(ctx.binaryLtlExpr())) { + ltl.put(ctx, true); + return true; + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitBinaryLtlExpr(LTLGrammarParser.BinaryLtlExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + if (ctx.type != null) { + ltl.put(ctx, true); + return true; + } + boolean child = visitLtlExpr(ctx.ltlExpr()); + ltl.put(ctx, child); + return child; + } + + @Override + public Boolean visitBinaryLtlOp(LTLGrammarParser.BinaryLtlOpContext ctx) { + return false; + } + + @Override + public Boolean visitLtlExpr(LTLGrammarParser.LtlExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + if (ctx.type != null) { + ltl.put(ctx, true); + return true; + } + boolean child = visitEqExpr(ctx.eqExpr()); + ltl.put(ctx, child); + return child; + } + + @Override + public Boolean visitLtlOp(LTLGrammarParser.LtlOpContext ctx) { + return false; + } + + @Override + public Boolean visitEqExpr(LTLGrammarParser.EqExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.RelationExprContext op : ctx.ops) { + if (visitRelationExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitEqOperator(LTLGrammarParser.EqOperatorContext ctx) { + return false; + } + + @Override + public Boolean visitRelationExpr(LTLGrammarParser.RelationExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.AdditiveExprContext op : ctx.ops) { + if (visitAdditiveExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitRelationOperator(LTLGrammarParser.RelationOperatorContext ctx) { + return false; + } + + @Override + public Boolean visitAdditiveExpr(LTLGrammarParser.AdditiveExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.MultiplicativeExprContext op : ctx.ops) { + if (visitMultiplicativeExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitAdditiveOperator(LTLGrammarParser.AdditiveOperatorContext ctx) { + return false; + } + + @Override + public Boolean visitMultiplicativeExpr(LTLGrammarParser.MultiplicativeExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.NegExprContext op : ctx.ops) { + if (visitNegExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitMultiplicativeOperator(LTLGrammarParser.MultiplicativeOperatorContext ctx) { + return false; + } + + @Override + public Boolean visitNegExpr(LTLGrammarParser.NegExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.NegExprContext op : ctx.ops) { + if (visitNegExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + if (ctx.primaryExpr() != null && visitPrimaryExpr(ctx.primaryExpr())) { + ltl.put(ctx, true); + return true; + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitPrimaryExpr(LTLGrammarParser.PrimaryExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + boolean child = false; + if (ctx.boolLitExpr() != null) child = visitBoolLitExpr(ctx.boolLitExpr()); + if (ctx.intLitExpr() != null) child = visitIntLitExpr(ctx.intLitExpr()); + if (ctx.parenExpr() != null) child = visitParenExpr(ctx.parenExpr()); + ltl.put(ctx, child); + return child; + } + + @Override + public Boolean visitBoolLitExpr(LTLGrammarParser.BoolLitExprContext ctx) { + return false; + } + + @Override + public Boolean visitParenExpr(LTLGrammarParser.ParenExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.ImplyExpressionContext op : ctx.ops) { + if (visitImplyExpression(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + } + + @Override + public Boolean visitIntLitExpr(LTLGrammarParser.IntLitExprContext ctx) { + return false; + } + + @Override + public Boolean visitVariable(LTLGrammarParser.VariableContext ctx) { + return false; + } + + @Override + public Boolean visitOrExpr(LTLGrammarParser.OrExprContext ctx) { + if (ltl.get(ctx) != null) return ltl.get(ctx); + for (LTLGrammarParser.AndExprContext op : ctx.ops) { + if (visitAndExpr(op)) { + ltl.put(ctx, true); + return true; + } + } + ltl.put(ctx, false); + return false; + + } + +} diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/ToStringVisitor.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/ToStringVisitor.java new file mode 100644 index 0000000000..b6732e0523 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/buchi/ToStringVisitor.java @@ -0,0 +1,329 @@ +/* + * 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.cfa.buchi; + +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarBaseVisitor; +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarParser; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; + +import java.util.HashMap; + +public class ToStringVisitor extends LTLGrammarBaseVisitor { + + HashMap> aps = new HashMap>(); + private int counter = 0; + private APGeneratorVisitor apGeneratorVisitor; + + public ToStringVisitor(APGeneratorVisitor apGeneratorVisitor) { + this.apGeneratorVisitor = apGeneratorVisitor; + } + + public HashMap> getAps() { + return aps; + } + + @Override + public String visitModel(LTLGrammarParser.ModelContext ctx) { + return visitImplyExpression(ctx.implyExpression); + } + + @Override + public String visitImplyExpression(LTLGrammarParser.ImplyExpressionContext ctx) { + if (!LTLExprVisitor.getInstance().visitImplyExpression(ctx)) { + String name = generateApName(); + Expr expr = apGeneratorVisitor.visitImplyExpression(ctx); + aps.put(name, expr); + return name; + } + if (ctx.ops.size() > 1) { + return visitOrExpr(ctx.ops.get(0)) + " -> " + visitOrExpr(ctx.ops.get(1)); + } else { + return visitOrExpr(ctx.ops.get(0)); + } + } + + @Override + public String visitOrExpr(LTLGrammarParser.OrExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitOrExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitOrExpr(ctx)); + return name; + } + StringBuilder builder = new StringBuilder(); + builder.append(visitAndExpr(ctx.ops.get(0))); + for (int i = 1; i < ctx.ops.size(); i++) { + builder.append(" | "); + builder.append(visitAndExpr(ctx.ops.get(i))); + } + return builder.toString(); + } + + @Override + public String visitAndExpr(LTLGrammarParser.AndExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitAndExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitAndExpr(ctx)); + return name; + } + StringBuilder builder = new StringBuilder(); + builder.append(visitNotExpr(ctx.ops.get(0))); + for (int i = 1; i < ctx.ops.size(); i++) { + builder.append(" & "); + builder.append(visitNotExpr(ctx.ops.get(i))); + } + return builder.toString(); + } + + @Override + public String visitNotExpr(LTLGrammarParser.NotExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitNotExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitNotExpr(ctx)); + return name; + } + if (ctx.ops.size() > 0) { + return "! " + visitNotExpr(ctx.ops.get(0)); + } else { + return visitBinaryLtlExpr(ctx.binaryLtlExpr()); + } + } + + @Override + public String visitBinaryLtlExpr(LTLGrammarParser.BinaryLtlExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitBinaryLtlExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitBinaryLtlExpr(ctx)); + return name; + } + if (ctx.type != null) { + return visitBinaryLtlExpr(ctx.ops.get(0)) + " " + visitBinaryLtlOp(ctx.type) + " " + visitBinaryLtlExpr(ctx.ops.get(1)); + + } else { + return visitLtlExpr(ctx.ltlExpr()); + } + } + + @Override + public String visitBinaryLtlOp(LTLGrammarParser.BinaryLtlOpContext ctx) { + if (ctx.U_OP() != null) { + return "U"; + } else if (ctx.M_OP() != null) { + return "M"; + } else if (ctx.W_OP() != null) { + return "W"; + } else { + return "R"; + } + } + + @Override + public String visitLtlExpr(LTLGrammarParser.LtlExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitLtlExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitLtlExpr(ctx)); + return name; + } + if (ctx.ops.size() > 0) { + return visitLtlOp(ctx.type) + " " + visitLtlExpr(ctx.ops.get(0)); + + } else { + return visitEqExpr(ctx.eqExpr()); + } + } + + @Override + public String visitLtlOp(LTLGrammarParser.LtlOpContext ctx) { + if (ctx.F_OP() != null) { + return "F"; + } else if (ctx.G_OP() != null) { + return "G"; + } else { + return "X"; + } + } + + @Override + public String visitEqExpr(LTLGrammarParser.EqExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitEqExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitEqExpr(ctx)); + return name; + } + StringBuilder builder = new StringBuilder(); + builder.append(visitRelationExpr(ctx.ops.get(0))); + for (int i = 1; i < ctx.ops.size(); i++) { + builder.append(visitEqOperator(ctx.oper)); + builder.append(visitRelationExpr(ctx.ops.get(i))); + } + return builder.toString(); + } + + @Override + public String visitEqOperator(LTLGrammarParser.EqOperatorContext ctx) { + if (ctx.EQ() != null) { + return "="; + } else { + return "/="; + } + } + + @Override + public String visitRelationExpr(LTLGrammarParser.RelationExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitRelationExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitRelationExpr(ctx)); + return name; + } + StringBuilder builder = new StringBuilder(); + builder.append(visitAdditiveExpr(ctx.ops.get(0))); + for (int i = 1; i < ctx.ops.size(); i++) { + builder.append(visitRelationOperator(ctx.oper)); + builder.append(visitAdditiveExpr(ctx.ops.get(i))); + } + return builder.toString(); + } + + @Override + public String visitRelationOperator(LTLGrammarParser.RelationOperatorContext ctx) { + if (ctx.LT() != null) { + return "<"; + } else if (ctx.GT() != null) { + return ">"; + } else if (ctx.LEQ() != null) { + return "<="; + } else return ">="; + } + + @Override + public String visitAdditiveExpr(LTLGrammarParser.AdditiveExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitAdditiveExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitAdditiveExpr(ctx)); + return name; + } + StringBuilder builder = new StringBuilder(); + builder.append(visitMultiplicativeExpr(ctx.ops.get(0))); + for (int i = 1; i < ctx.ops.size(); i++) { + builder.append(visitAdditiveOperator(ctx.opers.get(i - 1))); + builder.append(visitMultiplicativeExpr(ctx.ops.get(i))); + } + return builder.toString(); + } + + @Override + public String visitAdditiveOperator(LTLGrammarParser.AdditiveOperatorContext ctx) { + if (ctx.PLUS() != null) { + return "+"; + } else return "-"; + } + + @Override + public String visitMultiplicativeExpr(LTLGrammarParser.MultiplicativeExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitMultiplicativeExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitMultiplicativeExpr(ctx)); + return name; + } + StringBuilder builder = new StringBuilder(); + builder.append(visitNegExpr(ctx.ops.get(0))); + for (int i = 1; i < ctx.ops.size(); i++) { + builder.append(visitMultiplicativeOperator(ctx.opers.get(i - 1))); + builder.append(visitNegExpr(ctx.ops.get(i))); + } + return builder.toString(); + } + + @Override + public String visitMultiplicativeOperator(LTLGrammarParser.MultiplicativeOperatorContext ctx) { + if (ctx.MUL() != null) { + return "*"; + } else if (ctx.MOD() != null) { + return "%"; + } else return "/"; + } + + @Override + public String visitNegExpr(LTLGrammarParser.NegExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitNegExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitNegExpr(ctx)); + return name; + } + if (ctx.ops.size() > 0) { + return "- " + visitNegExpr(ctx.ops.get(0)); + } else { + return visitPrimaryExpr(ctx.primaryExpr()); + } + } + + @Override + public String visitPrimaryExpr(LTLGrammarParser.PrimaryExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitPrimaryExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitPrimaryExpr(ctx)); + return name; + } + if (ctx.parenExpr() != null) { + return visitParenExpr(ctx.parenExpr()); + } else if (ctx.intLitExpr() != null) { + return visitIntLitExpr(ctx.intLitExpr()); + } else return visitBoolLitExpr(ctx.boolLitExpr()); + } + + @Override + public String visitBoolLitExpr(LTLGrammarParser.BoolLitExprContext ctx) { + return ctx.value.getText(); + } + + @Override + public String visitParenExpr(LTLGrammarParser.ParenExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitParenExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitParenExpr(ctx)); + return name; + } + if (ctx.variable() != null) { + return visitVariable(ctx.variable()); + } else { + return "(" + visitImplyExpression(ctx.ops.get(0)) + ")"; + } + } + + @Override + public String visitIntLitExpr(LTLGrammarParser.IntLitExprContext ctx) { + if (!LTLExprVisitor.getInstance().visitIntLitExpr(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitIntLitExpr(ctx)); + return name; + } + return ctx.value.getText(); + } + + @Override + public String visitVariable(LTLGrammarParser.VariableContext ctx) { + if (!LTLExprVisitor.getInstance().visitVariable(ctx)) { + String name = generateApName(); + aps.put(name, apGeneratorVisitor.visitVariable(ctx)); + return name; + } + return ctx.name.getText(); + } + + private String generateApName() { + return "ap" + (counter++); + } +} diff --git a/subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/buchi/BuchiBuilderTest.java b/subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/buchi/BuchiBuilderTest.java new file mode 100644 index 0000000000..786ac24352 --- /dev/null +++ b/subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/buchi/BuchiBuilderTest.java @@ -0,0 +1,49 @@ +/* + * 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.cfa.buchi; + +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import jhoafparser.consumer.HOAConsumerException; +import org.junit.Assert; +import org.junit.Test; + +import java.util.List; + +import static hu.bme.mit.theta.core.decl.Decls.Var; + +public class BuchiBuilderTest { + + private static final Logger.Level LOGLEVEL = Logger.Level.VERBOSE; + + @Test + public void testSimpleExpression() throws HOAConsumerException { + Logger logger = new ConsoleLogger(LOGLEVEL); + String ltlExpression = "not G(F(p))"; + VarDecl p = Var("p", BoolType.getInstance()); + CFA cfa = BuchiBuilder.of(ltlExpression, List.of(p), logger); + logger.write(Logger.Level.VERBOSE, GraphvizWriter.getInstance().writeString(CfaVisualizer.visualize(cfa))); + Assert.assertEquals(1, cfa.getLocs().size()); + Assert.assertEquals(2, cfa.getEdges().size()); + Assert.assertEquals(1, cfa.getAcceptingEdges().size()); + } + +} diff --git a/subprojects/common/analysis/build.gradle.kts b/subprojects/common/analysis/build.gradle.kts index f8205f008d..4bb71e0bfe 100644 --- a/subprojects/common/analysis/build.gradle.kts +++ b/subprojects/common/analysis/build.gradle.kts @@ -31,4 +31,8 @@ dependencies { testImplementation(project(":theta-solver-z3-legacy")) testImplementation(project(":theta-solver-z3")) implementation("com.corundumstudio.socketio:netty-socketio:2.0.6") + testImplementation(project(mapOf("path" to ":theta-xsts-analysis"))) + testImplementation(project(mapOf("path" to ":theta-xsts"))) + testImplementation(project(mapOf("path" to ":theta-cfa-analysis"))) + testImplementation(project(mapOf("path" to ":theta-cfa"))) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt new file mode 100644 index 0000000000..b0c0e85fb5 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt @@ -0,0 +1,46 @@ +/* + * 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.loopchecker + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import java.util.function.Predicate + + +class AcceptancePredicate( + private val statePredicate: ((S?) -> Boolean)? = null, + private val actionPredicate: ((A?) -> Boolean)? = null, +) : Predicate> { + + constructor(statePredicate: (S?) -> Boolean = { _ -> true }, a: Unit) : this(statePredicate) + + fun testState(state: S): Boolean { + return statePredicate?.invoke(state) ?: false + } + + fun testAction(action: A) = actionPredicate?.invoke(action) ?: false + + override fun test(t: Pair): Boolean { + val state = t.first + val action = t.second + if (statePredicate == null && action == null) return false + return (statePredicate == null || statePredicate.invoke( + state + )) && (actionPredicate == null || (action != null && actionPredicate.invoke(action))) + } + +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt new file mode 100644 index 0000000000..19622193f6 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt @@ -0,0 +1,68 @@ +/* + * 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.loopchecker + +import hu.bme.mit.theta.analysis.Cex +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.Logger.Level + +class LDGTrace( + val tail: List>, + val honda: LDGNode, + val loop: List>, +) : Cex { + + val edges by lazy { tail + loop } + + constructor(edges: List>, honda: LDGNode) : this( + edges.takeWhile { it.source != honda }, honda, edges.dropWhile { it.source != honda }) + + init { + check( + (1 until tail.size).none { tail[it - 1].target != tail[it].source }) { "The edges of the tail have to connect into each other" } + check(tail.isEmpty() || tail.last().target == honda) { "The tail has to finish in the honda" } + check(loop.first().source == honda) { "The loop has to start in the honda" } + check( + (1 until loop.size).none { loop[it - 1].target != loop[it].source }) { "The edges of the loop have to connect into each other" } + check(loop.last().target == honda) { "The loop has to finish in the honda" } + } + + override fun length() = edges.size + + fun getEdge(index: Int): LDGEdge { + check(index >= 0) { "Can't get negative indexed edge (${index})" } + check(index < length()) { "Index out of range $index < ${length()}" } + return if (index < tail.size) tail[index] else loop[index - tail.size] + } + + fun getAction(index: Int) = getEdge(index).action + + fun getState(index: Int) = if (index < length()) getEdge(index).source!!.state else honda.state + + fun toTrace(): Trace = Trace.of(edges.map { it.source!!.state } + honda.state, edges.map { it.action!! }) + + fun print(logger: Logger, level: Level) { + tail.forEach { logger.write(level, "%s%n---through action:---%n%s%n--------->%n", it.source?.state, it.action) } + logger.write(level, "---HONDA:---%n{ %s }---------%n", honda.state) + loop.forEach { logger.write(level, "---through action:---%n%s%n--------->%n%s%n", it.action, it.target.state) } + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt new file mode 100644 index 0000000000..fe53d1b6ed --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt @@ -0,0 +1,129 @@ +/* + * 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.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger + + +typealias BacktrackResult = Pair>?, List>?> + +fun combineLassos(results: Collection>) = + Pair(setOf>(), results.flatMap { it.second ?: emptyList() }) + +abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { + + internal fun expandFromInitNodeUntilTarget( + initNode: LDGNode, stopAtLasso: Boolean, expand: NodeExpander, + logger: Logger + ): Collection> { + return expandThroughNode( + emptyMap(), LDGEdge(null, initNode, null, false), emptyList(), 0, stopAtLasso, expand, + logger + ).second!! + } + + private fun expandThroughNode( + pathSoFar: Map, Int>, incomingEdge: LDGEdge, + edgesSoFar: List>, targetsSoFar: Int, stopAtLasso: Boolean, expand: NodeExpander, + logger: Logger + ): BacktrackResult { + val expandingNode: LDGNode = incomingEdge.target + logger.write( + Logger.Level.VERBOSE, "Expanding through %s edge to %s node with state %s%n", + if (incomingEdge.accepting) "accepting" else "not accepting", + if (expandingNode.accepting) "accepting" else "not accepting", expandingNode.state + ) + if (expandingNode.state.isBottom()) { + logger.write(Logger.Level.VERBOSE, "Node is a dead end since its bottom%n") + return BacktrackResult(null, null) + } + val totalTargets = + if (expandingNode.accepting || incomingEdge.accepting) targetsSoFar + 1 else targetsSoFar + if (pathSoFar.containsKey(expandingNode) && pathSoFar[expandingNode]!! < totalTargets) { + logger.write(Logger.Level.SUBSTEP, "Found trace with a length of %d, building lasso...%n", pathSoFar.size) + logger.write(Logger.Level.DETAIL, "Honda should be: %s", expandingNode.state) + pathSoFar.forEach { (node, targetsThatFar) -> + logger.write( + Logger.Level.VERBOSE, "Node state %s | targets that far: %d%n", node.state, targetsThatFar + ) + } + val lasso: LDGTrace = LDGTrace(edgesSoFar + incomingEdge, expandingNode) + logger.write(Logger.Level.DETAIL, "Built the following lasso:%n") + lasso.print(logger, Logger.Level.DETAIL) + return BacktrackResult(null, listOf(lasso)) + } + if (pathSoFar.containsKey(expandingNode)) { + logger.write(Logger.Level.VERBOSE, "Reached loop but no acceptance inside%n") + return BacktrackResult(setOf(expandingNode), null) + } + val needsTraversing = !expandingNode.expanded || expandingNode + .validLoopHondas + .filter(pathSoFar::containsKey) + .any { + pathSoFar[it]!! < targetsSoFar + } + val expandStrategy: NodeExpander = if (needsTraversing + ) expand + else { _ -> mutableSetOf() } + val outgoingEdges: Collection> = expandStrategy(expandingNode) + val results: MutableList> = mutableListOf() + for (newEdge in outgoingEdges) { + val result: BacktrackResult = + expandThroughNode(pathSoFar + (expandingNode to totalTargets), newEdge, if (incomingEdge.source != null) edgesSoFar.plus(incomingEdge) else edgesSoFar, totalTargets, stopAtLasso, expand, logger) + results.add(result) + if (stopAtLasso && result.second?.isNotEmpty() == true) break + } + val result: BacktrackResult = combineLassos(results) + if (result.second != null) return result + val validLoopHondas: Collection> = results.flatMap { it.first ?: emptyList() } + expandingNode.validLoopHondas.addAll(validLoopHondas) + return BacktrackResult(validLoopHondas.toSet(), null) + } +} + +object GdfsSearchStrategy : AbstractSearchStrategy() { + + override fun search( + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, + logger: Logger + ): Collection> { + for (initNode in initNodes) { + val possibleTraces: Collection> = + expandFromInitNodeUntilTarget(initNode, true, expand, logger) + if (!possibleTraces.isEmpty()) { + return possibleTraces + } + } + return emptyList() + } + +} + +object FullSearchStrategy : AbstractSearchStrategy() { + + override fun search( + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, + logger: Logger + ) = initNodes.flatMap { expandFromInitNodeUntilTarget(it, false, expand, logger) } + +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt new file mode 100644 index 0000000000..cd2c4fc1f5 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt @@ -0,0 +1,59 @@ +/* + * 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.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.Analysis +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger + +class LDGAbstractor( + private val analysis: Analysis, private val lts: LTS, + private val acceptancePredicate: AcceptancePredicate, + private val searchStrategy: LoopcheckerSearchStrategy, private val logger: Logger +) : Abstractor> { + + override fun createProof() = LDG(acceptancePredicate) + + override fun check(ldg: LDG, prec: P): AbstractorResult { + if (ldg.isUninitialised()) { + ldg.initialise(analysis.initFunc.getInitStates(prec)) + ldg.traces = emptyList() + } + val expander: NodeExpander = fun (node : LDGNode) : Collection> { + if (node.expanded) { + return node.outEdges + } + node.expanded = true + return lts.getEnabledActionsFor(node.state).flatMap { action -> + analysis.transFunc.getSuccStates(node.state, action, prec).map(ldg::getOrCreateNode) + .map { ldg.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) } + } + } + val searchResult = searchStrategy.search(ldg, acceptancePredicate, expander, logger) + ldg.traces = searchResult.toList() + return AbstractorResult(searchResult.isEmpty()) + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt new file mode 100644 index 0000000000..66306d96e8 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt @@ -0,0 +1,51 @@ +/* + * 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.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.NullLogger + +typealias NodeExpander = (LDGNode) -> Collection> + +enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStrategy) { + GDFS(GdfsSearchStrategy), NDFS(NdfsSearchStrategy), FULL(FullSearchStrategy); + + companion object { + + val default = GDFS + } + + fun search( + ldg: LDG, target: AcceptancePredicate, expand: NodeExpander, + logger: Logger = NullLogger.getInstance() + ): Collection> = strategy.search(ldg.initNodes, target, expand, logger) +} + +interface ILoopcheckerSearchStrategy { + + fun search( + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, + logger: Logger + ): Collection> +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt new file mode 100644 index 0000000000..6ff054cfc1 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt @@ -0,0 +1,93 @@ +/* + * 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.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger + + +object NdfsSearchStrategy : ILoopcheckerSearchStrategy { + + override fun search( + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, + logger: Logger + ): Collection> { + for (node in initNodes) { + for (edge in expand(node)) { + val result = blueSearch(edge, emptyList(), mutableSetOf(), mutableSetOf(), target, expand) + if (!result.isEmpty()) return result + } + } + return emptyList() + } + + private fun redSearch( + seed: LDGNode, edge: LDGEdge, trace: List>, + redNodes: MutableSet>, target: AcceptancePredicate, expand: NodeExpander + ): List> { + val targetNode = edge.target + if (targetNode.state.isBottom) { + return emptyList() + } + if (targetNode == seed) { + return trace + edge + } + if (redNodes.contains(targetNode)) { + return emptyList() + } + redNodes.add(edge.target) + for (nextEdge in expand(targetNode)) { + val redSearch: List> = redSearch(seed, nextEdge, trace + edge, redNodes, target, expand) + if (redSearch.isNotEmpty()) return redSearch + } + return emptyList() + } + + private fun blueSearch( + edge: LDGEdge, trace: List>, blueNodes: MutableSet>, + redNodes: Set>, target: AcceptancePredicate, expand: NodeExpander + ): Collection> { + val targetNode = edge.target + if (targetNode.state.isBottom) { + return emptyList() + } + if (target.test(Pair(targetNode.state, edge.action))) { + // Edge source can only be null artificially, and is only used when calling other search strategies + val accNode = + if (targetNode.accepting) targetNode else edge.source!! + val redSearch: List> = + redSearch(accNode, edge, trace, mutableSetOf(), target, expand) + if (redSearch.isNotEmpty()) return setOf(LDGTrace(redSearch, accNode)) + } + if (blueNodes.contains(targetNode)) { + return emptyList() + } + blueNodes.add(edge.target) + for (nextEdge in expand(targetNode)) { + val blueSearch: Collection> = + blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand) + if (!blueSearch.isEmpty()) return blueSearch + } + return emptyList() + } + +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/InvalidPathException.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/InvalidPathException.kt new file mode 100644 index 0000000000..5f2e1cff81 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/InvalidPathException.kt @@ -0,0 +1,19 @@ +/* + * 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.loopchecker.exception + +class InvalidPathException : RuntimeException("The path given is not a lasso") \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/TraceCheckingFailedException.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/TraceCheckingFailedException.kt new file mode 100644 index 0000000000..002ccb9d33 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/TraceCheckingFailedException.kt @@ -0,0 +1,20 @@ +/* + * 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.loopchecker.exception + +class TraceCheckingFailedException(reason: String) : + Exception("The trace checker was unable to check the trace because of:\n$reason") \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt new file mode 100644 index 0000000000..2d12f9c5ef --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt @@ -0,0 +1,99 @@ +/* + * 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.loopchecker.ldg + +import hu.bme.mit.theta.analysis.algorithm.Proof +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState + +class LDG( + private val acceptancePredicate: AcceptancePredicate +) : Proof { + + val nodes: MutableMap> = mutableMapOf() + val initNodes: MutableList> = mutableListOf() + var traces: List> = emptyList() + + fun isUninitialised() = initNodes.isEmpty() + + fun pruneAll() { + initNodes.clear() + nodes.clear() + traces = emptyList() + } + + fun initialise(initStates: Collection) { + check(initStates.isNotEmpty()) + initNodes.addAll(initStates.map(this::getOrCreateNode)) + } + + fun getOrCreateNode(state: S): LDGNode = nodes.computeIfAbsent(state) { s -> + LDGNode( + s, acceptancePredicate.test(Pair(s, null)) + ) + } + + fun containsNode(state: S) = nodes.containsKey(state) + + fun drawEdge( + source: LDGNode, + target: LDGNode, + action: A?, + accepting: Boolean + ): LDGEdge { + val edge = LDGEdge(source, target, action, accepting) + source.addOutEdge(edge) + target.addInEdge(edge) + return edge + } + +} + +data class LDGEdge( + val source: LDGNode?, + val target: LDGNode, + val action: A?, + val accepting: Boolean +) + +class LDGNode(val state: S, val accepting: Boolean) { + companion object { + + var idCounter: Long = 0 + } + + val inEdges: MutableList> = mutableListOf() + val outEdges: MutableList> = mutableListOf() + val id = idCounter++ + var validLoopHondas: MutableSet> = hashSetOf() + var expanded: Boolean = false + set(value) { + if (!value) { + throw IllegalArgumentException("Can't set expanded to false") + } + field = true + } + + fun addInEdge(edge: LDGEdge) = inEdges.add(edge) + + fun addOutEdge(edge: LDGEdge) = outEdges.add(edge) + + fun smallerEdgeCollection() = if (inEdges.size > outEdges.size) inEdges else outEdges + +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt new file mode 100644 index 0000000000..73ddc6969b --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt @@ -0,0 +1,153 @@ +/* + * 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.loopchecker.refinement + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException +import hu.bme.mit.theta.analysis.algorithm.loopchecker.util.VarCollectorStmtVisitor +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.ExprStates +import hu.bme.mit.theta.analysis.expr.StmtAction +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.DomainSize +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.PathUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory +import hu.bme.mit.theta.solver.ItpMarker +import hu.bme.mit.theta.solver.SolverFactory +import java.util.function.Consumer + + +class BoundedUnrollingLDGTraceCheckerStrategy( + private val trace: LDGTrace, private val solverFactory: SolverFactory, + init: Expr, private val bound: Int, private val logger: Logger +) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { + + override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { + val indexingBeforeLoop = indexings[trace.tail.size] + val indexingAfterLoop = indexings[trace.length()] + val deltaIndexing = indexingAfterLoop.sub(indexingBeforeLoop) + val usedVariablesPrecision = ExplPrec.of(expandUsedVariables(emptySet())) + val requiredLoops: Int = findSmallestAbstractState(0, bound + 1, usedVariablesPrecision) + if (requiredLoops == bound + 1) { + throw TraceCheckingFailedException("Required number of unrolling is above $bound") + } + logger.write(Logger.Level.INFO, "Unrolling loop of trace at most %d times%n", requiredLoops) + solver.reset() + var loopIndexing = VarIndexingFactory.indexing(0) + for (i in 0 until requiredLoops) { + solver.push() + putLoopOnSolver(satMarker, loopIndexing) + if (solver.check().isUnsat) { + solver.pop() + putLoopOnSolver(unreachableMarker, loopIndexing) + logger.write(Logger.Level.INFO, "Unrolled loop of trace %d times%n", i + 1) + return infeasibleThroughInterpolant(trace.tail.size, loopIndexing) + } + loopIndexing = loopIndexing.add(deltaIndexing) + solver.push() + val finalLoopIndexing = loopIndexing + variables.forEach( + Consumer { variable: VarDecl<*> -> + solver.add( + unreachableMarker, Eq( + PathUtils.unfold(variable.ref, VarIndexingFactory.indexing(0)), + PathUtils.unfold(variable.ref, finalLoopIndexing) + ) + ) + }) + if (solver.check().isSat) { + logger.write(Logger.Level.INFO, "Unrolled loop of trace %d times%n", i + 1) + return getItpRefutationFeasible() + } + solver.pop() + } + val finalLoopIndexing = loopIndexing + variables.forEach { variable -> + solver.add( + unreachableMarker, Eq( + PathUtils.unfold(variable.ref, VarIndexingFactory.indexing(0)), + PathUtils.unfold(variable.ref, finalLoopIndexing) + ) + ) + } + return infeasibleThroughInterpolant(trace.tail.size, loopIndexing.sub(deltaIndexing)) + } + + private fun findSmallestAbstractState(i: Int, bound: Int, usedVariablesPrecision: ExplPrec): Int { + val loop = trace.loop + if (i == loop.size) return bound + val expr: Expr = loop[i].source!!.state.toExpr() + val statesForExpr: Collection = ExprStates.createStatesForExpr( + solverFactory.createSolver(), expr, 0, usedVariablesPrecision::createState, VarIndexingFactory.indexing(0), + bound + ) + val currentSize: DomainSize = statesForExpr + .map { state -> + val filtVars = usedVariablesPrecision + .vars + .filter(ExprUtils.getVars(state.toExpr())::contains) + val types = filtVars.map(VarDecl<*>::getType) + val sizes = types.map(Type::getDomainSize) + val res = sizes.fold(DomainSize.ONE, DomainSize::multiply) + res + } + .fold(DomainSize.ZERO, DomainSize::add) + return if (currentSize.isInfinite || currentSize.isBiggerThan(bound.toLong())) findSmallestAbstractState( + i + 1, bound, usedVariablesPrecision + ) + else findSmallestAbstractState(i + 1, currentSize.finiteSize.toInt(), usedVariablesPrecision) + } + + fun expandUsedVariables(usedVariables: Set>): Set> { + val expanded = trace.loop.fold(emptySet>()) { acc, edge -> + if (edge.action is StmtAction) VarCollectorStmtVisitor.visitAll( + edge.action.getStmts(), acc + ) else emptySet() + } + + return if (expanded.size > usedVariables.size) expandUsedVariables(expanded) + else usedVariables + } + + private fun putLoopOnSolver(marker: ItpMarker, startIndexing: VarIndexing) { + var loopIndexing = startIndexing + for (ldgEdge in trace.loop) { + solver.add(marker, PathUtils.unfold(ldgEdge.source!!.state.toExpr(), loopIndexing)) + val action = ldgEdge.action!! + solver.add(marker, PathUtils.unfold(action.toExpr(), loopIndexing)) + loopIndexing = loopIndexing.add(action.nextIndexing()) + } + solver.add( + marker, PathUtils.unfold( + trace.loop[trace.loop.size - 1].target.state.toExpr(), loopIndexing + ) + ) + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt new file mode 100644 index 0000000000..dd68069e6e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt @@ -0,0 +1,144 @@ +/* + * 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.loopchecker.refinement + +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException +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.ExprTraceStatus.Feasible +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.NullLogger +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.PathUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory +import hu.bme.mit.theta.solver.* + +enum class LDGTraceCheckerStrategy { + MILANO { + + override fun check( + trace: LDGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger + ) = MilanoLDGTraceCheckerStrategy(trace, solverFactory, init, logger).check() + }, BOUNDED_UNROLLING { + + override fun check( + trace: LDGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger + ): ExprTraceStatus { + try { + return BoundedUnrollingLDGTraceCheckerStrategy(trace, solverFactory, init, 100, logger).check() + } catch (t: TraceCheckingFailedException) { + logger.write(Logger.Level.INFO, "${t.message}\n") + logger.write(Logger.Level.INFO, "Falling back to default strategy $default\n") + return default.check(trace, solverFactory, init, logger) + } + } + }; + + companion object { + + val default = MILANO + } + abstract fun check(trace: LDGTrace, solverFactory: SolverFactory, init : Expr = True(), logger: Logger = NullLogger.getInstance()): ExprTraceStatus +} + +abstract class AbstractLDGTraceCheckerStrategy(private val trace: LDGTrace, solverFactory: SolverFactory, private val init : Expr, private val logger: Logger) { + protected val solver: ItpSolver = solverFactory.createItpSolver() + protected val stateCount = trace.length() + 1 + protected val indexings = mutableListOf() + protected val satMarker: ItpMarker = solver.createMarker() + protected val unreachableMarker: ItpMarker = solver.createMarker() + protected val pattern: ItpPattern = solver.createBinPattern(satMarker, unreachableMarker) + protected val variables = trace.edges.flatMap { ExprUtils.getVars(it.source?.state?.toExpr() ?: True()) + ExprUtils.getVars(it.action?.toExpr() ?: True()) } + + private fun findSatIndex(): Int { + for (i in 1 until stateCount) { + solver.push() + indexings.add(indexings[i - 1].add(trace.getAction(i - 1)!!.nextIndexing())) + solver.add(satMarker, PathUtils.unfold(trace.getState(i).toExpr(), indexings[i])) + solver.add( + satMarker, PathUtils.unfold( + trace.getAction(i - 1)!!.toExpr(), + indexings[i - 1] + ) + ) + if (solver.check().isUnsat) { + solver.pop() + return i - 1 + } + } + return stateCount - 1 + } + + abstract fun evaluateLoop(valuation: Valuation) : ExprTraceStatus + + fun check(): ExprTraceStatus { + solver.push() + indexings.add(VarIndexingFactory.indexing(0)) + solver.add(satMarker, PathUtils.unfold(init, indexings[0])) + solver.add(satMarker, PathUtils.unfold(trace.getState(0).toExpr(), indexings[0])) + + val satIndex = findSatIndex() + if (satIndex < stateCount - 1) return infeasibleAsLoopIsUnreachable(satIndex) + return evaluateLoop(solver.model) + } + + private fun infeasibleAsLoopIsUnreachable(satPrefix: Int): ExprTraceStatus { + logger.write(Logger.Level.INFO, "Loop was unreachable%n") + solver.add( + unreachableMarker, PathUtils.unfold( + trace.getState(satPrefix + 1).toExpr(), + indexings[satPrefix + 1] + ) + ) + solver.add( + unreachableMarker, PathUtils.unfold( + trace.getAction(satPrefix)!!.toExpr(), + indexings[satPrefix] + ) + ) + return infeasibleThroughInterpolant(satPrefix, indexings[satPrefix]) + } + + protected fun infeasibleThroughInterpolant(satPrefix: Int, indexing: VarIndexing): ExprTraceStatus { + solver.check() + val interpolant: Interpolant = solver.getInterpolant(pattern) + val interpolantExpr: Expr = interpolant.eval(satMarker) + logInterpolant(interpolantExpr) + try { + val itpFolded: Expr = PathUtils.foldin(interpolantExpr, indexing) + return ExprTraceStatus.infeasible(ItpRefutation.binary(itpFolded, satPrefix, stateCount)) + } catch (e: IllegalArgumentException) { + logger.write(Logger.Level.INFO, "Interpolant expression: %s; indexing: %s%n", interpolantExpr, indexing) + throw e + } + } + + protected fun getItpRefutationFeasible(): Feasible = ExprTraceStatus.feasible(Trace.of(indexings.map { PathUtils.extractValuation(solver.model, it) }, (trace.tail + trace.loop).map { it.action })) + + protected fun logInterpolant(expr: Expr) { + logger.write(Logger.Level.INFO, "Interpolant : $expr%n") + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt new file mode 100644 index 0000000000..a5641e867b --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt @@ -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.loopchecker.refinement + +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState + +interface LDGTraceRefiner : + Refiner, LDGTrace> { +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt new file mode 100644 index 0000000000..98eff1596c --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt @@ -0,0 +1,76 @@ +/* + * 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.loopchecker.refinement + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +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.common.logging.Logger +import hu.bme.mit.theta.core.decl.IndexedConstDecl +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq +import hu.bme.mit.theta.core.type.anytype.Exprs.Prime +import hu.bme.mit.theta.core.type.anytype.RefExpr +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.PathUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.solver.Interpolant +import hu.bme.mit.theta.solver.SolverFactory + + +class MilanoLDGTraceCheckerStrategy(private val trace: LDGTrace, solverFactory: SolverFactory, init : Expr, logger: Logger) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { + + override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { + for (variable in variables) { + solver.add( + unreachableMarker, Eq( + PathUtils.unfold( + variable.ref, + indexings[trace.tail.size] + ), PathUtils.unfold(variable.ref, indexings[stateCount - 1]) + ) + ) + if (solver.check().isSat) continue + val interpolant: Interpolant = solver.getInterpolant(pattern) + val interpolantExpr: Expr = ExprUtils.simplify(foldIn(interpolant.eval(satMarker), indexings[stateCount - 1], valuation)) + logInterpolant(interpolantExpr) + return ExprTraceStatus.infeasible(ItpRefutation.binary(interpolantExpr, stateCount - 1, stateCount)) + } + return getItpRefutationFeasible() + } + + private fun foldIn(expr: Expr, indexing: VarIndexing, valuation: Valuation): Expr { + if (expr is RefExpr) { + val decl = expr.decl + if (decl is IndexedConstDecl) { + val varDecl = decl.varDecl + val nPrimes = decl.index - indexing[varDecl] + val varRef = varDecl.ref + if (nPrimes == 0) return varRef + if (nPrimes > 0) return Prime(varRef, nPrimes) + return expr.eval(valuation) + } + } + + return expr.map { foldIn(it, indexing, valuation) } + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt new file mode 100644 index 0000000000..255d8be70e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt @@ -0,0 +1,55 @@ +/* + * 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.loopchecker.refinement + +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +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.common.logging.Logger +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.solver.SolverFactory + + +class SingleLDGTraceRefiner( + private val strategy: LDGTraceCheckerStrategy, private val solverFactory: SolverFactory, + private val refiner: JoiningPrecRefiner, + private val logger: Logger, private val init: Expr = True() +) : LDGTraceRefiner { + + override fun refine(witness: LDG, prec: P): RefinerResult> { + val ldgTraces = witness.traces + check(ldgTraces.isNotEmpty()) { "${this.javaClass.simpleName} needs at least one trace!" } + val ldgTrace = ldgTraces[0] + val refutation: ExprTraceStatus = + strategy.check(ldgTrace, solverFactory, init, logger) + if (refutation.isInfeasible) { + val refinedPrecision: P = + refiner.refine(prec, ldgTrace.toTrace(), refutation.asInfeasible().refutation) + witness.pruneAll() + return RefinerResult.spurious(refinedPrecision) + } + return RefinerResult.unsafe(ldgTrace) + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt new file mode 100644 index 0000000000..9e3226fc61 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt @@ -0,0 +1,70 @@ +/* + * 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.loopchecker.util + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.utils.ExprUtils + + +class VarCollectorStmtVisitor : StmtVisitor>, Set>> { + + companion object { + + fun visitAll(stmts: Collection, vars: Set>): Set> { + val visitor = VarCollectorStmtVisitor() + val expanded: Set> = stmts.fold(emptySet()) { acc, stmt -> acc + stmt.accept(visitor, vars) } + return if (expanded.size > vars.size) visitAll(stmts, expanded) else expanded + } + + } + + override fun visit(stmt: SkipStmt, param: Set>) = param + + override fun visit(stmt: AssumeStmt, param: Set>) = param + + override fun visit(stmt: AssignStmt, param: Set>): Set> { + val rightVars: Collection> = ExprUtils.getVars(stmt.expr) + val leftVar = stmt.varDecl + for (rightVar in rightVars) { + if (rightVar == leftVar || param.contains(rightVar)) { + return param.plus(leftVar) + } + } + return param + } + + override fun visit(stmt: HavocStmt, param: Set>) = param + stmt.varDecl + + override fun visit(stmt: SequenceStmt, param: Set>) = param + visitAll(stmt.stmts, param) + + override fun visit(stmt: NonDetStmt, param: Set>) = param + visitAll(stmt.stmts, param) + + override fun visit(stmt: OrtStmt, param: Set>) = param + visitAll(stmt.stmts, param) + + override fun visit(stmt: LoopStmt, param: Set>) = param + stmt.stmt.accept(this, param) + + override fun visit(stmt: IfStmt, param: Set>) = + param + stmt.then.accept(this, param) + stmt.elze.accept(this, param) + + override fun visit( + stmt: MemoryAssignStmt?, param: Set>? + ): Set> { + TODO("Not yet implemented") + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt new file mode 100644 index 0000000000..038f4cb026 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt @@ -0,0 +1,121 @@ +/* + * 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.utils + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.visualization.* +import hu.bme.mit.theta.common.visualization.Alignment.LEFT +import hu.bme.mit.theta.common.visualization.Shape.RECTANGLE +import java.awt.Color + + +class LdgVisualizer ( + private val stateToString: (S) -> String, + private val actionToString: (A) -> String +) : ProofVisualizer> { + + private var traceNodes: MutableSet> = mutableSetOf() + private var traceEdges: MutableSet> = mutableSetOf() + + override fun visualize(ldg: LDG): Graph { + traceNodes = mutableSetOf() + traceEdges = mutableSetOf() + return createVisualization(ldg) + } + + fun visualize(ldg: LDG, trace: LDGTrace): Graph { + traceEdges = mutableSetOf() + traceEdges.addAll(trace.edges) + traceNodes = mutableSetOf() + trace.edges.map{it.source!!}.forEach(traceNodes::add) + return createVisualization(ldg) + } + + private fun createVisualization(ldg: LDG): Graph { + val graph = Graph(LDG_ID, LDG_LABEL) + + val traversed: MutableSet> = mutableSetOf() + + for (initNode in ldg.initNodes) { + traverse(graph, initNode, traversed) + val nAttributes = NodeAttributes.builder().label("") + .fillColor(FILL_COLOR) + .lineColor(FILL_COLOR).lineStyle(SUCC_EDGE_STYLE).peripheries(1).build() + graph.addNode(PHANTOM_INIT_ID + initNode.id, nAttributes) + val eAttributes = EdgeAttributes.builder().label("") + .color(if (traceNodes.contains(initNode)) TARGET_COLOR else LINE_COLOR) + .lineStyle(SUCC_EDGE_STYLE).build() + graph.addEdge( + PHANTOM_INIT_ID + initNode.id, NODE_ID_PREFIX + initNode.id, + eAttributes + ) + } + + return graph + } + + private fun traverse( + graph: Graph, node: LDGNode, + traversed: MutableSet> + ) { + if (traversed.contains(node)) { + return + } else { + traversed.add(node) + } + val nodeId = NODE_ID_PREFIX + node.id + val peripheries = if (node.accepting) 2 else 1 + + val nAttributes = NodeAttributes.builder() + .label(stateToString(node.state)) + .alignment(LEFT).shape(RECTANGLE).font(FONT).fillColor(FILL_COLOR) + .lineColor(if (traceNodes.contains(node)) TARGET_COLOR else LINE_COLOR) + .lineStyle(SUCC_EDGE_STYLE).peripheries(peripheries).build() + + graph.addNode(nodeId, nAttributes) + + for (edge in node.outEdges) { + traverse(graph, edge.target, traversed) + val sourceId = NODE_ID_PREFIX + edge.source?.id + val targetId = NODE_ID_PREFIX + edge.target.id + val eAttributes = EdgeAttributes.builder() + .label(actionToString(edge.action!!)) + .alignment(LEFT).font(FONT) + .color(if (traceEdges.contains(edge)) TARGET_COLOR else LINE_COLOR) + .lineStyle(if (edge.accepting) LineStyle.DASHED else SUCC_EDGE_STYLE).build() + graph.addEdge(sourceId, targetId, eAttributes) + } + } + + companion object { + + private val SUCC_EDGE_STYLE = LineStyle.NORMAL + private const val LDG_LABEL = "" + private const val LDG_ID = "ldg" + private const val FONT = "courier" + private const val NODE_ID_PREFIX = "node_" + private val FILL_COLOR: Color = Color.WHITE + private val LINE_COLOR: Color = Color.BLACK + private val TARGET_COLOR: Color = Color.RED + private const val PHANTOM_INIT_ID = "phantom_init" + } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java new file mode 100644 index 0000000000..fc2a05025a --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java @@ -0,0 +1,133 @@ +/* + * 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.loopchecker; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; +import hu.bme.mit.theta.analysis.expl.ExplPrec; +import hu.bme.mit.theta.analysis.expl.ExplState; +import hu.bme.mit.theta.analysis.expl.ExplStatePredicate; +import hu.bme.mit.theta.analysis.expl.ExplStmtAnalysis; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.CfaAction; +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; +import hu.bme.mit.theta.cfa.analysis.CfaPrec; +import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec; +import hu.bme.mit.theta.cfa.dsl.CfaDslManager; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; +import java.util.Arrays; +import java.util.Collection; +import java.util.List; +import java.util.function.Predicate; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; + +@RunWith(Parameterized.class) +public class LDGAbstractorCheckingTest { + + @Parameterized.Parameter + public String fileName; + + @Parameterized.Parameter(1) + public String propFileName; + + @Parameterized.Parameter(2) + public String acceptingLocationName; + + @Parameterized.Parameter(3) + public boolean isLassoPresent; + + @Parameterized.Parameters + public static Collection data() { + return Arrays.asList(new Object[][]{ + {"counter6to7.cfa", "", "IS6", true}, + {"counter6to7.xsts", "x_eq_7.prop", "", true}, + {"counter6to7.xsts", "x_eq_6.prop", "", true}, + {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, + {"colors.xsts", "currentColor_eq_Green.prop", "", true}, + {"counter5.xsts", "x_eq_5.prop", "", true}, + {"forever5.xsts", "x_eq_5.prop", "", true}, + {"counter6to7.xsts", "x_eq_5.prop", "", false}, + {"weather.xsts", "isWet_eq_true.prop", "", false}, + {"weather.xsts", "waterproof.prop", "", true} + }); + } + + @Test + public void test() throws IOException { + if (propFileName.isBlank() && !acceptingLocationName.isBlank()) + testWithCfa(); + if (!propFileName.isBlank() && acceptingLocationName.isBlank()) + testWithXsts(); + } + + private void testWithXsts() throws IOException { + XSTS xsts; + try (InputStream inputStream = new SequenceInputStream(new FileInputStream(String.format("src/test/resources/xsts/%s", fileName)), new FileInputStream(String.format("src/test/resources/prop/%s", propFileName)))) { + xsts = XstsDslManager.createXsts(inputStream); + } + final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + final Analysis, XstsAction, ExplPrec> analysis = XstsAnalysis.create(ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), 250)); + final LTS, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + final Predicate> statePredicate = new XstsStatePredicate<>(new ExplStatePredicate(xsts.getProp(), abstractionSolver)); + final AcceptancePredicate, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + final ExplPrec precision = new XstsAllVarsInitPrec().createExpl(xsts); + var abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), new ConsoleLogger(Logger.Level.DETAIL)); + LDG, XstsAction> ldg = new LDG<>(target); + ldg.initialise(List.of()); + AbstractorResult result = abstractor.check(ldg, precision); + Assert.assertEquals(isLassoPresent, result.isUnsafe()); + } + + private void testWithCfa() throws IOException { + final CFA cfa = CfaDslManager.createCfa(new FileInputStream(String.format("src/test/resources/cfa/%s", fileName))); + final CfaLts lts = CfaConfigBuilder.Encoding.SBE.getLts(cfa.getInitLoc()); + final Analysis, CfaAction, CfaPrec> analysis = CfaAnalysis + .create(cfa.getInitLoc(), ExplStmtAnalysis.create(Z3LegacySolverFactory.getInstance().createSolver(), True(), 250)); + final CfaPrec precision = GlobalCfaPrec.create(ExplPrec.of(cfa.getVars())); + Predicate> statePredicate = cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); + AcceptancePredicate, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + LDGAbstractor, CfaAction, CfaPrec> abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), new ConsoleLogger(Logger.Level.DETAIL)); + LDG, CfaAction> ldg = new LDG<>(target); + ldg.initialise(List.of()); + AbstractorResult result = abstractor.check(ldg, precision); + Assert.assertEquals(isLassoPresent, result.isUnsafe()); + } + +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java new file mode 100644 index 0000000000..ecb03f3f9c --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java @@ -0,0 +1,150 @@ +/* + * 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.loopchecker; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; +import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; +import hu.bme.mit.theta.analysis.pred.*; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +import hu.bme.mit.theta.analysis.utils.LdgVisualizer; +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.CfaAction; +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; +import hu.bme.mit.theta.cfa.analysis.CfaPrec; +import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec; +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec; +import hu.bme.mit.theta.cfa.dsl.CfaDslManager; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.BeforeClass; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; +import java.util.Arrays; +import java.util.Collection; +import java.util.function.Predicate; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; + +@RunWith(Parameterized.class) +public class LDGCegarVerifierTest { + + private static Solver abstractionSolver; + private static ItpSolver itpSolver; + private static Logger logger; + + @BeforeClass + public static void init() { + abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); + logger = new ConsoleLogger(Logger.Level.INFO); + } + + @Parameterized.Parameter + public String fileName; + + @Parameterized.Parameter(1) + public String propFileName; + + @Parameterized.Parameter(2) + public String acceptingLocationName; + + @Parameterized.Parameter(3) + public boolean result; + + @Parameterized.Parameters + public static Collection data() { + return Arrays.asList(new Object[][]{ + {"counter3.xsts", "x_eq_3.prop", "", false} + , {"counter6to7.xsts", "x_eq_7.prop", "", true} + , {"counter6to7.cfa", "", "IS6", true} + , {"counter2to3.cfa", "", "IS3", true} + , {"counter6to7.xsts", "x_eq_6.prop", "", true} + , {"infinitehavoc.xsts", "x_eq_7.prop", "", true} + , {"colors.xsts", "currentColor_eq_Green.prop", "", true} + , {"counter5.xsts", "x_eq_5.prop", "", true} + , {"forever5.xsts", "x_eq_5.prop", "", true} + , {"counter6to7.xsts", "x_eq_5.prop", "", false} + }); + } + + @Test + public void test() throws IOException { + if (propFileName.isBlank() && !acceptingLocationName.isBlank()) + testWithCfa(); + if (!propFileName.isBlank() && acceptingLocationName.isBlank()) + testWithXsts(); + } + + private void testWithXsts() throws IOException { + XSTS xsts; + try (InputStream inputStream = new SequenceInputStream(new FileInputStream(String.format("src/test/resources/xsts/%s", fileName)), new FileInputStream(String.format("src/test/resources/prop/%s", propFileName)))) { + xsts = XstsDslManager.createXsts(inputStream); + } + final Analysis, XstsAction, PredPrec> analysis = XstsAnalysis.create(PredAnalysis.create(abstractionSolver, PredAbstractors.booleanSplitAbstractor(abstractionSolver), xsts.getInitFormula())); + final LTS, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + final Predicate> statePredicate = new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); + final AcceptancePredicate, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp()); + var abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger); + final Refiner, XstsAction>, LDGTrace, XstsAction>> refiner = BasicLDGTraceRefiner.create(itpSolver, new ItpRefToPredPrec(ExprSplitters.atoms()), RefinerStrategy.defaultValue(), logger); + final CegarChecker, XstsAction>, LDGTrace, XstsAction>> verifier = CegarChecker.create(abstractor, refiner, logger, LdgVisualizer.getDefault()); + + final PredPrec precision = PredPrec.of(); + var result = verifier.check(precision); + Assert.assertEquals(this.result, result.isUnsafe()); + } + + private void testWithCfa() throws IOException { + final CFA cfa = CfaDslManager.createCfa(new FileInputStream(String.format("src/test/resources/cfa/%s", fileName))); + final CfaLts lts = CfaConfigBuilder.Encoding.SBE.getLts(null); + final Analysis, CfaAction, CfaPrec> analysis = CfaAnalysis + .create(cfa.getInitLoc(), PredAnalysis.create(abstractionSolver, PredAbstractors.booleanSplitAbstractor(abstractionSolver), True())); + final Predicate> statePredicate = cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); + final AcceptancePredicate, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + final RefutationToPrec refToPrec = new ItpRefToPredPrec(ExprSplitters.atoms()); + final RefutationToGlobalCfaPrec cfaRefToPrec = new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc()); + var abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger); + final Refiner, LDG, CfaAction>, LDGTrace, CfaAction>> refiner = BasicLDGTraceRefiner.create(itpSolver, cfaRefToPrec, RefinerStrategy.defaultValue(), logger); + final CegarChecker, LDG, CfaAction>, LDGTrace, CfaAction>> verifier = CegarChecker.create(abstractor, refiner, logger, LdgVisualizer.getDefault()); + + final GlobalCfaPrec prec = GlobalCfaPrec.create(PredPrec.of()); + var res = verifier.check(prec); + Assert.assertEquals(result, res.isUnsafe()); + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java new file mode 100644 index 0000000000..e20227ce13 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java @@ -0,0 +1,72 @@ +/* + * 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.loopchecker; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; +import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.pred.PredAbstractors; +import hu.bme.mit.theta.analysis.pred.PredAnalysis; +import hu.bme.mit.theta.analysis.pred.PredPrec; +import hu.bme.mit.theta.analysis.pred.PredState; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.Test; + +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; +import java.util.List; +import java.util.function.Predicate; + +public class LDGTraceCheckerTest { + @Test + public void testWithCounter3() throws IOException { + XSTS xsts; + try (InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/xsts/counter3.xsts"), new FileInputStream("src/test/resources/prop/x_eq_3.prop"))) { + xsts = XstsDslManager.createXsts(inputStream); + } + final ItpSolver itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); + final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + final Analysis, XstsAction, PredPrec> analysis = XstsAnalysis.create(PredAnalysis.create(abstractionSolver, PredAbstractors.booleanAbstractor(abstractionSolver), xsts.getInitFormula())); + final LTS, XstsAction> lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + final Predicate> statePredicate = new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); + final AcceptancePredicate, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + final PredPrec precision = PredPrec.of(); + final Logger logger = new ConsoleLogger(Logger.Level.DETAIL); + final LDGAbstractor, XstsAction, PredPrec> abstractor = LDGAbstractor.create(analysis, lts, target, SearchStrategy.defaultValue(), logger); + LDG, XstsAction> ldg = new LDG<>(target); + ldg.initialise(List.of()); + abstractor.check(ldg, precision); + LDGTrace, XstsAction> trace = abstractor.getLdg().getTraces().iterator().next(); + + ExprTraceStatus status = LDGTraceChecker.check(trace, itpSolver, RefinerStrategy.MILANO, logger); + Assert.assertTrue(status.isInfeasible()); + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGAbstractorTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGAbstractorTest.java new file mode 100644 index 0000000000..6cdd277ddc --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGAbstractorTest.java @@ -0,0 +1,61 @@ +/* + * 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.loopchecker.ldg; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.Prec; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.SearchStrategy; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; +import hu.bme.mit.theta.common.logging.NullLogger; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.mockito.Mock; +import org.mockito.junit.MockitoJUnitRunner; + +import static org.mockito.Mockito.mock; + +@RunWith(MockitoJUnitRunner.class) +public class LDGAbstractorTest { + + @Mock + public ExprState fromState; + @Mock + public ExprState toState; + @Mock + public ExprAction actionFromTo; + + @Test + @SuppressWarnings("unchecked") + public void testConnectTwoNodes() { + LDGNode from = LDGNode.of(fromState, true); + LDGNode to = LDGNode.of(toState, true); + LDGAbstractor abstractor = LDGAbstractor.create((Analysis) mock(Analysis.class), (LTS) mock(LTS.class), new AcceptancePredicate<>(), SearchStrategy.defaultValue(), NullLogger.getInstance()); + + LDGEdge edge = abstractor.connectTwoNodes(from, to, actionFromTo); + + Assert.assertEquals(from, edge.source()); + Assert.assertEquals(to, edge.target()); + Assert.assertEquals(1, from.getOutEdges().size()); + Assert.assertEquals(1, to.getInEdges().size()); + Assert.assertTrue(from.getOutEdges().contains(edge)); + Assert.assertTrue(to.getInEdges().contains(edge)); + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java new file mode 100644 index 0000000000..002697069f --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java @@ -0,0 +1,63 @@ +/* + * 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.ldg; + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.mockito.junit.MockitoJUnitRunner; + +import java.util.List; + +import static org.mockito.Mockito.mock; + +@RunWith(MockitoJUnitRunner.class) +public class LDGTraceTest { + + @Test + public void testSimpleLasso() { + LDGNode initNode = LDGNode.of(mock(ExprState.class), false); + LDGNode hondaNode = LDGNode.of(mock(ExprState.class), true); + LDGNode loopNode = LDGNode.of(mock(ExprState.class), false); + Assert.assertNotEquals(initNode, hondaNode); + Assert.assertNotEquals(initNode, loopNode); + Assert.assertNotEquals(loopNode, hondaNode); + LDGEdge firstEdge = new LDGEdge<>(initNode, hondaNode, mock(ExprAction.class), false); + LDGEdge secondEdge = new LDGEdge<>(hondaNode, loopNode, mock(ExprAction.class), false); + LDGEdge thirdEdge = new LDGEdge<>(loopNode, hondaNode, mock(ExprAction.class), false); + initNode.addOutEdge(firstEdge); + hondaNode.addInEdge(firstEdge); + hondaNode.addOutEdge(secondEdge); + loopNode.addInEdge(secondEdge); + loopNode.addOutEdge(thirdEdge); + hondaNode.addInEdge(thirdEdge); + + LDGTrace trace = LDGTrace.lassoFromIteratorWithHonda(List.of(initNode, hondaNode, loopNode).iterator(), hondaNode); + + Assert.assertEquals(1, trace.getTail().size()); + Assert.assertEquals(2, trace.getLoop().size()); + Assert.assertEquals(initNode, trace.getTail().get(0).source()); + Assert.assertEquals(hondaNode, trace.getTail().get(0).target()); + Assert.assertEquals(hondaNode, trace.getLoop().get(0).source()); + Assert.assertEquals(loopNode, trace.getLoop().get(0).target()); + Assert.assertEquals(loopNode, trace.getLoop().get(1).source()); + Assert.assertEquals(hondaNode, trace.getLoop().get(1).target()); + } + +} diff --git a/subprojects/common/analysis/src/test/resources/cfa/counter2to3.cfa b/subprojects/common/analysis/src/test/resources/cfa/counter2to3.cfa new file mode 100644 index 0000000000..b5b2867b4f --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/cfa/counter2to3.cfa @@ -0,0 +1,16 @@ +main process cfa { + var x : int + + init loc I + loc L0 + loc L1 + loc IS2 + loc IS3 + + I -> L0 { x := 0 } + L0 -> L1 { assume x < 2 } + L1 -> L0 { x := x + 1 } + L0 -> IS2 { assume x = 2 } + IS2 -> IS3 { x := x + 1 } + IS3 -> IS2 { x := x - 1 } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/cfa/counter6to7.cfa b/subprojects/common/analysis/src/test/resources/cfa/counter6to7.cfa new file mode 100644 index 0000000000..3063a76786 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/cfa/counter6to7.cfa @@ -0,0 +1,19 @@ +main process cfa { + var x : int + + init loc L0 + loc L1 + loc L2 + loc L3 + loc IS6 + loc IS7 + error loc ERR + + L0 -> L1 { x := 0 } + L1 -> L2 { assume x < 5 } + L1 -> L3 { assume not (x < 5) } + L2 -> L1 { x := x + 1 } + L3 -> IS6 { x := x + 1 } + IS6 -> IS7 { x := x + 1 } + IS7 -> IS6 { x := x - 1 } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/currentColor_eq_Green.prop b/subprojects/common/analysis/src/test/resources/prop/currentColor_eq_Green.prop new file mode 100644 index 0000000000..eeb441d7a5 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/currentColor_eq_Green.prop @@ -0,0 +1,3 @@ +prop { + currentColor == Green +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/isWet_eq_true.prop b/subprojects/common/analysis/src/test/resources/prop/isWet_eq_true.prop new file mode 100644 index 0000000000..b7ab97c829 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/isWet_eq_true.prop @@ -0,0 +1,3 @@ +prop { + isWet == true +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/waterproof.prop b/subprojects/common/analysis/src/test/resources/prop/waterproof.prop new file mode 100644 index 0000000000..bd2560743f --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/waterproof.prop @@ -0,0 +1,3 @@ +prop { + clothing == Waterproof +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_3.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_3.prop new file mode 100644 index 0000000000..02cceee940 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_3.prop @@ -0,0 +1,3 @@ +prop{ + x==3 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_5.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_5.prop new file mode 100644 index 0000000000..5fd56522e8 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_5.prop @@ -0,0 +1,3 @@ +prop{ + x==5 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_6.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_6.prop new file mode 100644 index 0000000000..46ab62325d --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_6.prop @@ -0,0 +1,3 @@ +prop{ + x==6 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_7.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_7.prop new file mode 100644 index 0000000000..c9b549c899 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_7.prop @@ -0,0 +1,3 @@ +prop{ + x==7 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/colors.xsts b/subprojects/common/analysis/src/test/resources/xsts/colors.xsts new file mode 100644 index 0000000000..ee68377924 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/colors.xsts @@ -0,0 +1,35 @@ +type Color : { Red , Green , Blue } +type Mood : { Happy, Angry, Depressed } +var currentColor : Color = Red +var currentMood : Mood = Happy + +trans { + assume currentColor == Red; + choice { + assume currentMood == Happy; + currentColor := Green; + } or { + assume currentMood == Angry; + } or { + assume currentMood == Depressed; + currentColor := Blue; + } +} or { + assume currentColor == Green; + choice { + assume (currentMood == Happy || currentMood == Depressed); + currentColor := Blue; + } or { + assume currentMood == Angry; + currentColor := Red; + } +} or { + assume currentColor == Blue; + if (currentMood == Angry) currentColor := Red; +} + +init{} + +env { + havoc currentMood; +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/counter3.xsts b/subprojects/common/analysis/src/test/resources/xsts/counter3.xsts new file mode 100644 index 0000000000..3b7909e1db --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/counter3.xsts @@ -0,0 +1,10 @@ +var x: integer = 0 + +trans { + assume x<3; + x:=x+1; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/counter5.xsts b/subprojects/common/analysis/src/test/resources/xsts/counter5.xsts new file mode 100644 index 0000000000..ed7b207596 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/counter5.xsts @@ -0,0 +1,12 @@ +ctrl var x: integer = 0 + +trans { + assume x<5; + x:=x+1; +} or { + x:=x; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/counter6to7.xsts b/subprojects/common/analysis/src/test/resources/xsts/counter6to7.xsts new file mode 100644 index 0000000000..300a73f31a --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/counter6to7.xsts @@ -0,0 +1,13 @@ +ctrl var x: integer = 0 + +trans { + assume x<=6; + x:=x+1; +} or { + assume x==7; + x:=x-1; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/forever5.xsts b/subprojects/common/analysis/src/test/resources/xsts/forever5.xsts new file mode 100644 index 0000000000..d80dcaff9d --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/forever5.xsts @@ -0,0 +1,9 @@ +ctrl var x: integer = 5 + +trans { + x:=x; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/infinitehavoc.xsts b/subprojects/common/analysis/src/test/resources/xsts/infinitehavoc.xsts new file mode 100644 index 0000000000..d53b11cf4b --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/infinitehavoc.xsts @@ -0,0 +1,14 @@ +ctrl var x: integer = 0 +var y: integer = 0 + +trans { + havoc y; +} + +init { + x:=7; +} + +env { + havoc y; +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/weather.xsts b/subprojects/common/analysis/src/test/resources/xsts/weather.xsts new file mode 100644 index 0000000000..36d3e79442 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/weather.xsts @@ -0,0 +1,106 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { __init__, Morning , Noon, Afternoon, Night } +type Clothing : { Shorts, Warm, Waterproof } +var isWet : boolean = false +var looksOut : boolean = false +var isClever : boolean = false +var weather : Weather = Sunny +var time : TimeOfDay = __init__ +var clothing : Clothing = Shorts + +trans { + choice { + assume time == Morning; + choice { + assume (looksOut == false && isClever == false); + havoc clothing; + } or { + assume (looksOut == true && isClever == false); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Foggy); + clothing := Warm; + } or { + assume weather == Rainy; + clothing := Waterproof; + } + } or { + assume (isClever == true); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Rainy); + clothing := Waterproof; + } or { + assume weather == Foggy; + clothing := Warm; + } + } + } or { + assume time == Noon; + if (isWet == true) looksOut := true; + } or { + assume time == Afternoon; + } or { + assume time == Night; + if (isWet == true) isClever := true; + } +} + +init { + havoc weather; +} + +env { + choice { + assume time == __init__; + time := Morning; + } or { + assume time != __init__; + if (clothing != Waterproof && weather == Rainy) isWet := true; + if (time == Noon || time == Night) isWet := false; + choice { + assume time == Morning; + time := Noon; + } or { + assume time == Noon; + time := Afternoon; + } or { + assume time == Afternoon; + time := Night; + } or { + assume time == Night; + time := Morning; + } + + choice { + assume time != Noon; + choice { + assume (weather == Sunny || weather == Cloudy || weather == Foggy); + choice { + weather := Cloudy; + } or { + weather := Sunny; + } or { + assume weather == Cloudy; + weather := Rainy; + } + } or { + assume (weather == Rainy); + choice { + weather := Rainy; + } or { + weather := Sunny; + } + } or { + assume time == Morning; + weather := Foggy; + } + } or { + assume time == Noon; + } + } +} \ No newline at end of file diff --git a/subprojects/common/ltl/build.gradle.kts b/subprojects/common/ltl/build.gradle.kts new file mode 100644 index 0000000000..7ba6367682 --- /dev/null +++ b/subprojects/common/ltl/build.gradle.kts @@ -0,0 +1,31 @@ +/* + * 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. + */ +plugins { + id("java-common") + id("kotlin-common") +} + +dependencies { + implementation(project(":theta-common")) + implementation(project(":theta-core")) + implementation(project(":theta-solver")) + implementation(project(":theta-analysis")) + implementation(project(mapOf("path" to ":theta-cfa"))) + implementation(project(mapOf("path" to ":theta-cfa-analysis"))) + testImplementation(project(":theta-solver-z3-legacy")) + testImplementation(project(mapOf("path" to ":theta-xsts-analysis"))) + testImplementation(project(mapOf("path" to ":theta-xsts"))) +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/BuchiUtils.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/BuchiUtils.kt new file mode 100644 index 0000000000..0b725c3d02 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/BuchiUtils.kt @@ -0,0 +1,57 @@ +/* + * 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.common.ltl + +import hu.bme.mit.theta.analysis.InitFunc +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.StmtAction +import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState +import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.CfaAction +import hu.bme.mit.theta.cfa.analysis.CfaState + +class BuchiInitFunc

(private val initLoc: CFA.Loc) : InitFunc, P> { + + override fun getInitStates(prec: P) = mutableListOf(CfaState.of(initLoc, UnitState.getInstance())) +} + +class BuchiLts : LTS, CfaAction> { + + override fun getEnabledActionsFor(state: CfaState) = state.loc.outEdges.map(CfaAction::create) +} + +fun buchiPredicate( + buchiAutomaton: CFA +): AcceptancePredicate, D>, StmtMultiAction> = AcceptancePredicate( + actionPredicate = { a -> + (a?.rightAction != null && a.rightAction.edges.any { e -> + buchiAutomaton.acceptingEdges.contains( + e + ) + }) + }) + +fun combineBlankBuchiStateWithData(buchiState: CfaState, dataState: D) = + CfaState.of(buchiState.loc, dataState) + +fun stripDataFromBuchiState(buchiState: CfaState) = + CfaState.of(buchiState.loc, UnitState.getInstance()) \ No newline at end of file diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt new file mode 100644 index 0000000000..c986d106ae --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt @@ -0,0 +1,108 @@ +/* + * 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.common.ltl + +import hu.bme.mit.theta.analysis.Analysis +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleLDGTraceRefiner +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.StmtAction +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.analysis.multi.* +import hu.bme.mit.theta.analysis.multi.builder.stmt.StmtMultiBuilder +import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState +import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction +import hu.bme.mit.theta.analysis.unit.UnitPrec +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.analysis.utils.LdgVisualizer +import hu.bme.mit.theta.cfa.analysis.CfaAction +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis +import hu.bme.mit.theta.cfa.analysis.CfaPrec +import hu.bme.mit.theta.cfa.analysis.CfaState +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.buchi.BuchiBuilder +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.solver.SolverFactory + +class LtlChecker( + multiSide: MultiAnalysisSide, + lts: LTS, + refToPrec: RefutationToPrec, + dataRefToPrec: RefutationToPrec, + dataAnalysis: Analysis, + variables: Collection>, + ltl: String, + solverFactory: SolverFactory, + logger: Logger, + searchStrategy: LoopcheckerSearchStrategy, + refinerStrategy: LDGTraceCheckerStrategy, + initExpr: Expr = True() +) : SafetyChecker, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>, MultiPrec, DataP>> { + val checker: CegarChecker, DataP>, LDG, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>> + + init { + val buchiAutomaton = BuchiBuilder.of(ltl, variables, logger) + val cfaAnalysis: Analysis, CfaAction, CfaPrec> = + CfaAnalysis.create(buchiAutomaton.initLoc, dataAnalysis) + val buchiSide = MultiAnalysisSide( + cfaAnalysis, BuchiInitFunc(buchiAutomaton.initLoc), ::combineBlankBuchiStateWithData, + ::stripDataFromBuchiState, { it.state }, { _ -> GlobalCfaPrec.create(UnitPrec.getInstance()) }) + val product = StmtMultiBuilder(multiSide, lts).addRightSide( + buchiSide, BuchiLts() + ).build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val buchiRefToPrec = + RefutationToGlobalCfaPrec(dataRefToPrec, buchiAutomaton.initLoc) + val multiRefToPrec = RefToMultiPrec(refToPrec, buchiRefToPrec, dataRefToPrec) + val multiAnalysis = product.side.analysis + val abstractor = + LDGAbstractor(multiAnalysis, product.lts, buchiPredicate(buchiAutomaton), searchStrategy, logger) + val refiner : SingleLDGTraceRefiner, DataS>, StmtMultiAction, MultiPrec, DataP>> = + SingleLDGTraceRefiner(refinerStrategy, solverFactory, JoiningPrecRefiner.create(multiRefToPrec), logger, initExpr) + val visualizer = + LdgVisualizer, DataS>, StmtMultiAction>( + { it.toString() }, + { it.toString() } + ) + checker = CegarChecker.create(abstractor, refiner, logger, visualizer) + } + + override fun check( + input: MultiPrec, DataP> + ): SafetyResult, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>> { + return checker.check(input) + } + + fun check(prec: P, dataPrec: DataP): SafetyResult, DataS>, StmtMultiAction>, LDGTrace, DataS>, StmtMultiAction>> { + return check(MultiPrec(prec, GlobalCfaPrec.create(dataPrec), dataPrec)) + } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt new file mode 100644 index 0000000000..e3e2b8c755 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfa.kt @@ -0,0 +1,115 @@ +/* + * 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.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expl.ExplAnalysis +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec +import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis +import hu.bme.mit.theta.cfa.analysis.CfaPrec +import hu.bme.mit.theta.cfa.analysis.CfaState +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts +import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.dsl.CfaDslManager +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@RunWith(Parameterized::class) +class LtlCheckTestWithCfa( + private val cfaName: String, + private val ltlExpr: String, + private val result: Boolean +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE) + + companion object { + @JvmStatic + @Parameterized.Parameters + fun data() = listOf( + arrayOf("counter2inf", "G(x=1)", false), + arrayOf("counter2inf", "G(x=2)", false), + arrayOf("counter2inf", "F G(x=2)", true), + arrayOf("counter2inf", "F(x=1)", true), + arrayOf("counter2inf", "F(x=3)", false), + ) + } + + @Test + fun test() { + abstractionSolver.reset() + var cfaI: CFA? + FileInputStream(String.format("src/test/resources/cfa/%s.cfa", cfaName)).use { inputStream -> + cfaI = CfaDslManager.createCfa(inputStream) + } + if (cfaI == null) + fail("Couldn't read cfa $cfaName") + val cfa = cfaI!! + val dataAnalysis = ExplAnalysis.create( + abstractionSolver, + True() + ) + val analysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis) + val lts: CfaLts = CfaSbeLts.getInstance() + val refToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) + val initFunc = { _: CfaPrec -> listOf>(CfaState.of(cfa.initLoc, UnitState.getInstance())) } + val variables = cfa.vars + val dataInitPrec = ExplPrec.of(variables) + val initPrec:CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val combineStates = { c: CfaState, d: ExplState -> CfaState.of(c.loc, d) } + val stripState = { c: CfaState -> CfaState.of(c.loc, UnitState.getInstance()) } + val extractFromState = { c: CfaState -> c.state } + val stripPrec = { p: CfaPrec -> p } + val multiSide = MultiAnalysisSide(analysis, initFunc, combineStates, stripState, extractFromState, stripPrec) + + val checker = LtlChecker( + multiSide, + lts, + refToPrec, + ItpRefToExplPrec(), + dataAnalysis, + variables, + ltlExpr, + itpSolverFactory, + logger, + LoopcheckerSearchStrategy.GDFS, + LDGTraceCheckerStrategy.MILANO + ) + + Assert.assertEquals(result, checker.check(initPrec, dataInitPrec).isSafe) + } + +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt new file mode 100644 index 0000000000..123da55d6a --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt @@ -0,0 +1,138 @@ +/* + * 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.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide +import hu.bme.mit.theta.analysis.pred.* +import hu.bme.mit.theta.analysis.unit.UnitPrec +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis +import hu.bme.mit.theta.cfa.analysis.CfaPrec +import hu.bme.mit.theta.cfa.analysis.CfaState +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts +import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.dsl.CfaDslManager +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@RunWith(Parameterized::class) +class LtlCheckTestWithCfaPred( + private val cfaName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: LDGTraceCheckerStrategy +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.INFO) + + companion object { + fun data() = listOf( + arrayOf("wave_flags", "F G(x)", false), + arrayOf("wave_flags", "F G(x and y)", false), + arrayOf("wave_flag", "G F(x)", true), + arrayOf("wave_flag", "G(x)", false), + arrayOf("wave_flag", "F G(x)", false), + arrayOf("counter5inf", "G(not(x=6))", true), + arrayOf("counter5inf", "G(x=1)", false), + arrayOf("counter5inf", "G(x=5)", false), + arrayOf("counter5inf", "F G(x=5)", true), + arrayOf("counter5inf", "F(x=1)", true), + arrayOf("counter5inf", "F(x=5)", true), + arrayOf("wave_flags", "G F(y)", true), + arrayOf("wave_flags", "F G(x)", false), + arrayOf("indicator", "G (x -> y)", true), +// arrayOf("indicator_multiassign", "G (x -> y)", true), + arrayOf("indicator", "G (x -> X (not x))", true), + arrayOf("indicator", "G (y -> X (not y))", false), + ) + + @JvmStatic + @Parameterized.Parameters(name = "{3}-{4}: {0}") + fun params() = + listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> + listOf(LDGTraceCheckerStrategy.MILANO, LDGTraceCheckerStrategy.BOUNDED_UNROLLING).flatMap { ref -> + data().map { + arrayOf(*it, search, ref) + } + } + } + } + + @Test + fun test() { + abstractionSolver.reset() + var cfaI: CFA? + FileInputStream(String.format("src/test/resources/cfa/%s.cfa", cfaName)).use { inputStream -> + cfaI = CfaDslManager.createCfa(inputStream) + } + if (cfaI == null) + fail("Couldn't read cfa $cfaName") + val cfa = cfaI!! + val dataAnalysis = PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + True() + ) + val analysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis) + val lts: CfaLts = CfaSbeLts.getInstance() + val refToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) + val initFunc = { _: CfaPrec -> listOf>(CfaState.of(cfa.initLoc, UnitState.getInstance())) } + val variables = cfa.vars + val dataInitPrec = PredPrec.of() + val initPrec : CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val combineStates = { c: CfaState, d: PredState -> CfaState.of(c.loc, d) } + val stripState = { c: CfaState -> CfaState.of(c.loc, UnitState.getInstance()) } + val extractFromState = { c: CfaState -> c.state } + val stripPrec = { p: CfaPrec -> GlobalCfaPrec.create(UnitPrec.getInstance()) } + val multiSide = MultiAnalysisSide(analysis, initFunc, combineStates, stripState, extractFromState, stripPrec) + + val checker = LtlChecker( + multiSide, + lts, + refToPrec, + ItpRefToPredPrec(ExprSplitters.atoms()), + dataAnalysis, + variables, + ltlExpr, + itpSolverFactory, + logger, + searchStrategy, + refinerStrategy + ) + + Assert.assertEquals(result, checker.check(initPrec, dataInitPrec).isSafe) + } + +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt new file mode 100644 index 0000000000..22f0674e96 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXsts.kt @@ -0,0 +1,89 @@ +/* + * 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.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@RunWith(Parameterized::class) +class LtlCheckTestWithXsts( + private val xstsName: String, + private val ltlExpr: String, + private val result: Boolean +) { + + private val solverFactory = Z3LegacySolverFactory.getInstance() + private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE) + + companion object { + @JvmStatic + @Parameterized.Parameters + fun data() = listOf( + arrayOf("counter3inf", "F G(x=3)", true), + arrayOf("counter3inf", "F(x=2)", true), + arrayOf("counter3inf", "G(x<4)", true), + arrayOf("counter3inf", "G(x=1)", false), + arrayOf("counter6to7", "G(x=1)", false), + arrayOf("counter6to7", "G(x=7)", false), + arrayOf("counter6to7", "G F(x=7)", true), + ) + } + + @Test + fun test() { + var xstsI: XSTS? + FileInputStream(String.format("src/test/resources/xsts/%s.xsts", xstsName)) + .use { inputStream -> + xstsI = XstsDslManager.createXsts(inputStream) + } + if (xstsI == null) + fail("Couldn't read xsts $xstsName") + val xsts = xstsI!! + val configBuilder = XstsConfigBuilder(XstsConfigBuilder.Domain.EXPL, XstsConfigBuilder.Refinement.SEQ_ITP, solverFactory, solverFactory).initPrec(XstsConfigBuilder.InitPrec.EMPTY).ExplStrategy(xsts) + val initPrec = configBuilder.initPrec + + val checker = LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + configBuilder.itpRefToPrec, + configBuilder.itpRefToPrec, + configBuilder.dataAnalysis, + xsts.vars, + ltlExpr, + solverFactory, + logger, + LoopcheckerSearchStrategy.GDFS, + LDGTraceCheckerStrategy.MILANO + ) + val checkResult = checker.check(initPrec, initPrec) + + Assert.assertEquals(result, checkResult.isSafe) + } + +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt new file mode 100644 index 0000000000..a3a528505f --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt @@ -0,0 +1,153 @@ +/* + * 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.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide +import hu.bme.mit.theta.analysis.pred.* +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.* +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import hu.bme.mit.theta.xsts.normalize +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@RunWith(Parameterized::class) +class LtlCheckTestWithXstsPred( + private val xstsName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: LDGTraceCheckerStrategy +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE) + + companion object { + private fun data() = listOf( + arrayOf("simple_types", "F G(color = Colors.Red)", false), + arrayOf("counter3inf", "F G(x=3)", true), + arrayOf("counter3inf", "F(x=2)", true), + arrayOf("counter3inf", "G(x<4)", true), + arrayOf("counter3inf", "G(x=1)", false), + arrayOf("counter6to7", "G(x=1)", false), + arrayOf("counter6to7", "G(x=7)", false), + arrayOf("counter6to7", "G F(x=7)", true), +// arrayOf("counter50", "G(x<49)", false), + arrayOf("trafficlight_v2", "G(LightCommands_displayRed -> X(not LightCommands_displayGreen))", true), + arrayOf("trafficlight_v2", "G((normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle) -> X(normal = Normal.Green))", true), + arrayOf("trafficlight_v2", "G(PoliceInterrupt_police -> F(LightCommands_displayYellow))", true), + arrayOf("forever5", "G(x=5)", true), + arrayOf("forever5", "F(x=6)", false), + arrayOf("randomincreasingeven", "not F(x=1)", true), + arrayOf("randomincreasingeven", "F(x>10)", true), + arrayOf("randomincreasingeven", "G(x>=0)", true), + arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Blue))", true), + arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Green))", false), + arrayOf("simple_color", "F G(envColor = modelColor)", false), + arrayOf("weather", "G F(isClever and isWet)", false), + arrayOf("weather", "F G(not isWet)", true), + arrayOf("weather", "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))", true), +// arrayOf("weather", "F G(weather = Weather.Foggy -> (clothing = Clothing.Nothing or clothing = Clothing.Warm))", true), +// arrayOf("weather_noinit", "G F(isClever and isWet)", false), +// arrayOf("weather_noinit", "F G(not isWet)", true), +// arrayOf("weather_noinit", "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))", true), +// arrayOf("weather_noinit", "F G(weather = Weather.Foggy -> (clothing = Clothing.Nothing or clothing = Clothing.Warm))", true), + ) + + @JvmStatic + @Parameterized.Parameters(name = "{3}-{4}: {0}") + fun params() = + listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> + LDGTraceCheckerStrategy.entries.flatMap { ref -> + data().map { + arrayOf(*it, search, ref) + } + } + } + } + + @Test + fun test() { + var xstsI: XSTS? + FileInputStream(String.format("src/test/resources/xsts/%s.xsts", xstsName)).use { inputStream -> + xstsI = XstsDslManager.createXsts(inputStream) + } + if (xstsI == null) + fail("Couldn't read xsts $xstsName") + val xsts = normalize(xstsI) + val dataAnalysis = PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + xsts.initFormula + ) + val analysis = XstsAnalysis.create( + dataAnalysis + ) + val lts = XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())) + val refToPrec = ItpRefToPredPrec(ExprSplitters.atoms()) + val initFunc = XstsInitFunc.create{ _: PredPrec -> listOf(UnitState.getInstance()) } + val initPrec = PredPrec.of() + val variables = xsts.vars + val combineStates = { x: XstsState, d: PredState -> XstsState.of(d, x.lastActionWasEnv(), true) } + val stripState = { x: XstsState -> XstsState.of(UnitState.getInstance(), x.lastActionWasEnv(), true) } + val extractFromState = { x: XstsState -> x.state } + val stripPrec = { p: PredPrec -> p } + + val multiAnalysisSide = MultiAnalysisSide( + analysis, + initFunc, + combineStates, + stripState, + extractFromState, + stripPrec + + ) + + val checker = LtlChecker( + multiAnalysisSide, + lts, + refToPrec, + refToPrec, + dataAnalysis, + variables, + ltlExpr, + itpSolverFactory, + logger, + searchStrategy, + refinerStrategy, + xsts.initFormula + ) + + Assert.assertEquals(result, checker.check(initPrec, initPrec).isSafe) + } + +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa b/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa new file mode 100644 index 0000000000..81e578cc5d --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa @@ -0,0 +1,12 @@ +main process cfa { + var x : int + + init loc I + loc L0 + loc L1 + + I -> L0 { x := 0 } + L0 -> L1 { assume x < 2 } + L1 -> L0 { x := x + 1 } + L0 -> L0 { assume x = 2 } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa b/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa new file mode 100644 index 0000000000..6fb102aaf8 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa @@ -0,0 +1,12 @@ +main process cfa { + var x : int + + init loc I + loc L0 + loc L1 + + I -> L0 { x := 0 } + L0 -> L1 { assume x < 5 } + L1 -> L0 { x := x + 1 } + L0 -> L0 { assume x = 5 } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa b/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa new file mode 100644 index 0000000000..c8a7062768 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa @@ -0,0 +1,14 @@ +main process cfa { + var x : bool + var y : bool + + loc L0 + loc L1 + init loc L2 + loc L3 + + L0 -> L1 { y := true } + L1 -> L2 { x := true } + L2 -> L3 { x := false } + L3 -> L0 { y := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa b/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa new file mode 100644 index 0000000000..8330500158 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa @@ -0,0 +1,12 @@ +main process cfa { + var x : bool + var y : bool + + loc L0 + loc L1 + init loc L2 + + L0 -> L1 { y := true } + L1 -> L2 { x := true } + L2 -> L0 { y := false x := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa b/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa new file mode 100644 index 0000000000..77322ac49d --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa @@ -0,0 +1,9 @@ +main process cfa { + var x : bool + + init loc L0 + loc L1 + + L0 -> L1 { x := true } + L1 -> L0 { x := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa b/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa new file mode 100644 index 0000000000..dc192bb7e5 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa @@ -0,0 +1,18 @@ +main process cfa { + var x : bool + var y : bool + + init loc I0 + loc I1 + loc L0 + loc L1 + loc L2 + loc L3 + + I0 -> I1 { x := false } + I1 -> L0 { y := false } + L0 -> L1 { y := true } + L1 -> L2 { y := false x := true } + L2 -> L3 { y := true } + L3 -> L0 { y := false x := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts new file mode 100644 index 0000000000..af2080f290 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts @@ -0,0 +1,12 @@ +var x: integer = 0 + +trans { + assume x<3; + x:=x+1; +} or { + assume x>=3; +} + +init {} +env {} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts new file mode 100644 index 0000000000..ffed019bc4 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts @@ -0,0 +1,16 @@ +ctrl var x: integer = 0 + +trans { + choice { + assume x<50; + x:=x+1; + } or { + assume x == 50; + } +} + +init {} + +env {} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts new file mode 100644 index 0000000000..f331be2ee6 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts @@ -0,0 +1,13 @@ +var x: integer = 0 + +trans { + assume x<=6; + x:=x+1; +} or { + assume x==7; + x:=x-1; +} + +init {} +env {} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts b/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts new file mode 100644 index 0000000000..975cfc8f93 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts @@ -0,0 +1,9 @@ +var x: integer = 5 + +trans { + x:=x; +} + +init {} +env {} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts b/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts new file mode 100644 index 0000000000..d6f9c53796 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts @@ -0,0 +1,14 @@ +var x: integer = 0 +var y: integer = 0 + +trans { + if (y < 0) y := -y; + if (y == 0) y := 1; + if (y % 2 == 1) y := y + 1; + x:= x + y; +} +init {} +env { + havoc y; +} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts b/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts new file mode 100644 index 0000000000..6443992dff --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts @@ -0,0 +1,24 @@ +type Colors : { Red, Green, Blue} +var envColor : Colors = Red +var modelColor : Colors = Red + +trans { + choice { + assume envColor == Red; + modelColor := Green; + } or { + assume envColor == Green; + modelColor := Blue; + } or { + assume envColor == Blue; + modelColor := Red; + } +} + +init{} + +env { + havoc envColor; +} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts b/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts new file mode 100644 index 0000000000..3f1dda287f --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts @@ -0,0 +1,16 @@ +type Abc : { A, B, C, D} +type Colors : { Red, Green, Blue} +var letter : Abc = A +var color : Colors = Red + +trans { + havoc letter; +} + +init{} + +env { + havoc color; +} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts b/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts new file mode 100644 index 0000000000..e2f50cef51 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts @@ -0,0 +1,169 @@ +type Main_region : { __Inactive__, Interrupted, Normal} +type Normal : { __Inactive__, Green, Red, Yellow} +type Interrupted : { __Inactive__, Black, BlinkingYellow} +var PoliceInterrupt_police : boolean = false +var LightCommands_displayRed : boolean = false +var Control_toggle : boolean = false +var LightCommands_displayYellow : boolean = false +var LightCommands_displayNone : boolean = false +var LightCommands_displayGreen : boolean = false +ctrl var main_region : Main_region = __Inactive__ +ctrl var normal : Normal = __Inactive__ +ctrl var interrupted : Interrupted = __Inactive__ +ctrl var BlackTimeout3 : integer = 500 +ctrl var BlinkingYellowTimeout4 : integer = 500 +var c : boolean = true +var b : integer = 0 +var asd : integer = 0 +var a : boolean = false + +trans { + choice { + assume ((!(((main_region == Interrupted) && (PoliceInterrupt_police == true)))) && (((main_region == Interrupted) && (interrupted == BlinkingYellow)) && (500 <= BlinkingYellowTimeout4))); + assume (interrupted == BlinkingYellow); + interrupted := Black; + assume (interrupted == Black); + BlackTimeout3 := 0; + LightCommands_displayNone := true; + } or { + assume ((!(((main_region == Interrupted) && (PoliceInterrupt_police == true)))) && (((main_region == Interrupted) && (interrupted == Black)) && (500 <= BlackTimeout3))); + assume (interrupted == Black); + interrupted := BlinkingYellow; + assume (interrupted == BlinkingYellow); + BlinkingYellowTimeout4 := 0; + LightCommands_displayYellow := true; + } or { + assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Green)) && (Control_toggle == true))); + assume (normal == Green); + b := 4; + normal := Yellow; + assume (normal == Yellow); + LightCommands_displayYellow := true; + } or { + assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Red)) && (Control_toggle == true))); + assume (normal == Red); + a := true; + normal := Green; + assume (normal == Green); + LightCommands_displayGreen := true; + } or { + assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Yellow)) && (Control_toggle == true))); + assume (normal == Yellow); + normal := Red; + assume (normal == Red); + LightCommands_displayRed := true; + } or { + assume (((main_region == Interrupted) && (PoliceInterrupt_police == true))); + assume (main_region == Interrupted); + interrupted := __Inactive__; + main_region := Normal; + choice { + assume (normal == __Inactive__); + normal := Red; + } or { + assume !((normal == __Inactive__)); + } + assume (main_region == Normal); + choice { + assume (normal == Green); + LightCommands_displayGreen := true; + } or { + assume (normal == Red); + LightCommands_displayRed := true; + } or { + assume (normal == Yellow); + LightCommands_displayYellow := true; + } + } or { + assume (((main_region == Normal) && (PoliceInterrupt_police == true))); + assume (main_region == Normal); + choice { + assume (normal == Green); + } or { + assume (normal == Red); + a := true; + } or { + assume (normal == Yellow); + } + asd := 321; + main_region := Interrupted; + interrupted := BlinkingYellow; + assume (main_region == Interrupted); + choice { + assume (interrupted == Black); + BlackTimeout3 := 0; + LightCommands_displayNone := true; + } or { + assume (interrupted == BlinkingYellow); + BlinkingYellowTimeout4 := 0; + LightCommands_displayYellow := true; + } + } +} + +init { + c := true; + b := 0; + a := false; + asd := 0; + BlackTimeout3 := 500; + BlinkingYellowTimeout4 := 500; + normal := __Inactive__; + interrupted := __Inactive__; + PoliceInterrupt_police := false; + Control_toggle := false; + LightCommands_displayRed := false; + LightCommands_displayYellow := false; + LightCommands_displayNone := false; + LightCommands_displayGreen := false; + main_region := Normal; + choice { + assume (normal == __Inactive__); + normal := Red; + } or { + assume !((normal == __Inactive__)); + } + choice { + assume (main_region == Interrupted); + choice { + assume (interrupted == Black); + BlackTimeout3 := 0; + LightCommands_displayNone := true; + } or { + assume (interrupted == BlinkingYellow); + BlinkingYellowTimeout4 := 0; + LightCommands_displayYellow := true; + } + } or { + assume (main_region == Normal); + choice { + assume (normal == Green); + LightCommands_displayGreen := true; + } or { + assume (normal == Red); + LightCommands_displayRed := true; + } or { + assume (normal == Yellow); + LightCommands_displayYellow := true; + } + } +} + +env { + choice { + PoliceInterrupt_police := true; + } or { + PoliceInterrupt_police := false; + } + choice { + Control_toggle := true; + } or { + Control_toggle := false; + } + LightCommands_displayYellow := false; + LightCommands_displayRed := false; + LightCommands_displayNone := false; + LightCommands_displayGreen := false; +} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather.xsts new file mode 100644 index 0000000000..b5d9da75dc --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/weather.xsts @@ -0,0 +1,104 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { Morning , Noon, Afternoon, Night } +type Clothing : { Nothing, Shorts, Warm, Waterproof } +var isWet : boolean = false +var looksOut : boolean = false +var isClever : boolean = false +var weather : Weather = Sunny +var time : TimeOfDay +var clothing : Clothing = Nothing + +trans { + choice { + assume time == Morning; + choice { + assume (looksOut == false && isClever == false); + havoc clothing; + } or { + assume (looksOut == true && isClever == false); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Foggy); + clothing := Warm; + } or { + assume weather == Rainy; + clothing := Waterproof; + } + } or { + assume (isClever == true); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Rainy); + clothing := Waterproof; + } or { + assume weather == Foggy; + clothing := Warm; + } + } + } or { + assume time == Noon; + if (isWet == true) looksOut := true; + } or { + assume time == Afternoon; + } or { + assume time == Night; + if (isWet == true) isClever := true; + clothing := Nothing; + } +} + +init { + havoc weather; + time := Morning; +} + +env { + if (clothing != Waterproof && weather == Rainy) isWet := true; + if (time == Noon || time == Night) isWet := false; + choice { + assume time == Morning; + time := Noon; + } or { + assume time == Noon; + time := Afternoon; + } or { + assume time == Afternoon; + time := Night; + } or { + assume time == Night; + time := Morning; + } + + choice { + assume time != Noon; + choice { + assume (weather == Sunny || weather == Cloudy || weather == Foggy); + choice { + weather := Cloudy; + } or { + weather := Sunny; + } or { + assume weather == Cloudy; + weather := Rainy; + } + } or { + assume (weather == Rainy); + choice { + weather := Rainy; + } or { + weather := Sunny; + } + } or { + assume time == Morning; + weather := Foggy; + } + } or { + assume time == Noon; + } + +} +prop {true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts new file mode 100644 index 0000000000..78f5efe332 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts @@ -0,0 +1,106 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { __init__, Morning , Noon, Afternoon, Night } +type Clothing : { Nothing, Shorts, Warm, Waterproof } +var isWet : boolean = false +var looksOut : boolean = false +var isClever : boolean = false +var weather : Weather = Sunny +var time : TimeOfDay = __init__ +var clothing : Clothing = Nothing + +trans { + choice { + assume time == Morning; + choice { + assume (looksOut == false && isClever == false); + havoc clothing; + } or { + assume (looksOut == true && isClever == false); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Foggy); + clothing := Warm; + } or { + assume weather == Rainy; + clothing := Waterproof; + } + } or { + assume (isClever == true); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Rainy); + clothing := Waterproof; + } or { + assume weather == Foggy; + clothing := Warm; + } + } + } or { + assume time == Noon; + if (isWet == true) looksOut := true; + } or { + assume time == Afternoon; + } or { + assume time == Night; + if (isWet == true) isClever := true; + clothing := Nothing; + } +} + +init { } + +env { + choice { + assume time == __init__; + time := Morning; + } or { + assume time != __init__; + if (clothing != Waterproof && weather == Rainy) isWet := true; + if (time == Noon || time == Night) isWet := false; + choice { + assume time == Morning; + time := Noon; + } or { + assume time == Noon; + time := Afternoon; + } or { + assume time == Afternoon; + time := Night; + } or { + assume time == Night; + time := Morning; + } + + choice { + assume time != Noon; + choice { + assume (weather == Sunny || weather == Cloudy || weather == Foggy); + choice { + weather := Cloudy; + } or { + weather := Sunny; + } or { + assume weather == Cloudy; + weather := Rainy; + } + } or { + assume (weather == Rainy); + choice { + weather := Rainy; + } or { + weather := Sunny; + } + } or { + assume time == Morning; + weather := Foggy; + } + } or { + assume time == Noon; + } + } +} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts new file mode 100644 index 0000000000..4cdde5291a --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts @@ -0,0 +1,105 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { Morning , Noon, Afternoon, Night } +type Clothing : { Nothing, Shorts, Warm, Waterproof } +var isWet : boolean = false +var looksOut : boolean = false +var isClever : boolean = false +var weather : Weather = Sunny +var time : TimeOfDay +var clothing : Clothing = Nothing + +trans { + choice { + assume time == Morning; + choice { + assume (looksOut == false && isClever == false); + havoc clothing; + } or { + assume (looksOut == true && isClever == false); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Foggy); + clothing := Warm; + } or { + assume weather == Rainy; + clothing := Waterproof; + } + } or { + assume (isClever == true); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Rainy); + clothing := Waterproof; + } or { + assume weather == Foggy; + clothing := Warm; + } + } + } or { + assume time == Noon; + if (isWet == true) looksOut := true; + } or { + assume time == Afternoon; + } or { + assume time == Night; + if (isWet == true) isClever := true; + clothing := Nothing; + } +} + +init { + havoc weather; + time := Morning; +} + +env { + if (clothing != Waterproof && weather == Rainy) isWet := true; + if (time == Noon || time == Night) isWet := false; + choice { + assume time == Morning; + time := Noon; + } or { + assume time == Noon; + time := Afternoon; + } or { + assume time == Afternoon; + time := Night; + } or { + assume time == Night; + time := Morning; + } + + choice { + assume time != Noon; + choice { + assume (weather == Sunny || weather == Cloudy || weather == Foggy); + choice { + weather := Cloudy; + } or { + weather := Sunny; + } or { + assume weather == Cloudy; + weather := Rainy; + } + } or { + assume (weather == Rainy); + choice { + weather := Rainy; + } or { + weather := Sunny; + } + } or { + assume time == Morning; + weather := Foggy; + } + } or { + assume time == Noon; + } + +} +prop{true} +ltl{G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))} \ No newline at end of file diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XstsTransformer.kt b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XstsTransformer.kt new file mode 100644 index 0000000000..cf6213067d --- /dev/null +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XstsTransformer.kt @@ -0,0 +1,71 @@ +/* + * 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.xsts + +import com.google.common.base.Preconditions.checkArgument +import hu.bme.mit.theta.core.stmt.NonDetStmt +import hu.bme.mit.theta.core.stmt.SequenceStmt +import hu.bme.mit.theta.core.stmt.SkipStmt +import hu.bme.mit.theta.core.stmt.Stmt + +fun normalize(rawXsts: XSTS?) : XSTS { + checkArgument(rawXsts != null, "Can't normalize null") + val xstsInput = rawXsts!! + + val normalizedInit = normalize(xstsInput.init) + val normalizedTran = normalize(xstsInput.tran) + val normalizedEnv = normalize(xstsInput.env) + + return XSTS( + xstsInput.ctrlVars, + normalizedInit, + normalizedTran, + normalizedEnv, + xstsInput.initFormula, + xstsInput.prop + ) +} + + + +private fun normalize(stmt: Stmt): NonDetStmt { + val collector = mutableListOf>() + collector.add(mutableListOf()) + normalize(stmt, collector) + return NonDetStmt.of(collector.map { SequenceStmt.of(it) }.toList()) +} + +private fun normalize(stmt: Stmt, collector: MutableList>) { + when (stmt) { + is SequenceStmt -> stmt.stmts.forEach { normalize(it, collector) } + is NonDetStmt -> { + val newCollector = mutableListOf>() + stmt.stmts.forEach { nondetBranch -> + val copy = collector.copy() + normalize(nondetBranch, copy) + newCollector.addAll(copy) + } + collector.clear() + collector.addAll(newCollector) + } + + is SkipStmt -> {} + else -> collector.forEach { it.add(stmt) } + } +} + +private fun MutableList>.copy() = map { it.toMutableList() }.toMutableList() \ No newline at end of file