diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties index efb2dbd0eb..144d0ea9d7 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 @@ -41,4 +41,5 @@ javasmtVersion=4.1.1 sosylabVersion=0.3000-569-g89796f98 cliktVersion=4.4.0 spotlessVersion=6.25.0 -kamlVersion=0.59.0 \ No newline at end of file +kamlVersion=0.59.0 +nuprocessVersion=2.0.6 diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt index 5fc6cc9b53..9c869af882 100644 --- a/buildSrc/src/main/kotlin/Deps.kt +++ b/buildSrc/src/main/kotlin/Deps.kt @@ -81,4 +81,6 @@ object Deps { val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}" val kaml = "com.charleskorn.kaml:kaml:${Versions.kaml}" + + val nuprocess = "com.zaxxer:nuprocess:${Versions.nuprocess}" } 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/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..87da3778b6 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,16 +22,18 @@ 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.*; import hu.bme.mit.theta.common.visualization.Shape; 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 { @@ -51,10 +44,10 @@ 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() { - } + private CfaVisualizer() {} public static Graph visualize(final CFA cfa) { final Graph graph = new Graph(CFA_ID, CFA_LABEL); @@ -64,7 +57,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; } @@ -74,16 +67,20 @@ private static void addVars(final Graph graph, final CFA cfa) { for (final VarDecl var : cfa.getVars()) { sb.append('\n').append(var.getName()).append(": ").append(var.getType()); } - final NodeAttributes attrs = NodeAttributes.builder().label(sb.toString()) - .shape(Shape.RECTANGLE) - .fillColor(FILL_COLOR).lineColor(LINE_COLOR).lineStyle(LineStyle.DASHED) - .alignment(Alignment.LEFT) - .build(); + final NodeAttributes attrs = + NodeAttributes.builder() + .label(sb.toString()) + .shape(Shape.RECTANGLE) + .fillColor(FILL_COLOR) + .lineColor(LINE_COLOR) + .lineStyle(LineStyle.DASHED) + .alignment(Alignment.LEFT) + .build(); graph.addNode(CFA_ID + "_vars", attrs); } - private static void addLocation(final Graph graph, final CFA cfa, final Loc loc, - final Map ids) { + private static void addLocation( + final Graph graph, final CFA cfa, final Loc loc, final Map ids) { final String id = LOC_ID_PREFIX + ids.size(); ids.put(loc, id); String label = loc.getName(); @@ -96,21 +93,34 @@ private static void addLocation(final Graph graph, final CFA cfa, final Loc loc, label += " (error)"; } final int peripheries = isError ? 2 : 1; - final NodeAttributes nAttrs = NodeAttributes.builder().label(label).fillColor(FILL_COLOR) - .lineColor(LINE_COLOR) - .lineStyle(LOC_LINE_STYLE).peripheries(peripheries).build(); + final NodeAttributes nAttrs = + NodeAttributes.builder() + .label(label) + .fillColor(FILL_COLOR) + .lineColor(LINE_COLOR) + .lineStyle(LOC_LINE_STYLE) + .peripheries(peripheries) + .build(); graph.addNode(id, nAttrs); } - private static void addEdge(final Graph graph, final Edge edge, 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(); + 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(accepting ? ACC_EDGE_LINE_STYLE : EDGE_LINE_STYLE) + .font(EDGE_FONT) + .build(); graph.addEdge(ids.get(edge.getSource()), ids.get(edge.getTarget()), eAttrs); } - public static void printTraceTable(final Trace, CfaAction> trace, - final TableWriter writer) { + public static void printTraceTable( + final Trace, CfaAction> trace, final TableWriter writer) { final Set> allVars = new LinkedHashSet<>(); for (final CfaState state : trace.getStates()) { allVars.addAll(state.getState().getDecls()); @@ -132,7 +142,8 @@ public static void printTraceTable(final Trace, CfaAction> t writer.newRow(); if (i < trace.getActions().size()) { final StringBuilder sb = new StringBuilder(); - trace.getAction(i).getStmts() + trace.getAction(i) + .getStmts() .forEach(s -> sb.append(s.toString()).append(System.lineSeparator())); writer.cell(sb.toString(), nCols); writer.newRow(); 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..ecd5e3fa90 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,22 +15,18 @@ */ 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.base.Preconditions.*; 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.*; /** * Represents an immutable Control Flow Automata (CFA). Use the builder class to create a new @@ -45,6 +41,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; @@ -52,14 +49,18 @@ private CFA(final Builder builder) { errorLoc = Optional.ofNullable(builder.errorLoc); locs = ImmutableSet.copyOf(builder.locs); edges = ImmutableList.copyOf(builder.edges); - vars = edges.stream().flatMap(e -> StmtUtils.getVars(e.getStmt()).stream()) - .collect(toImmutableSet()); + vars = + edges.stream() + .flatMap(e -> StmtUtils.getVars(e.getStmt()).stream()) + .collect(toImmutableSet()); Set varNames = Containers.createSet(); for (var v : vars) { - checkArgument(!varNames.contains(v.getName()), + checkArgument( + !varNames.contains(v.getName()), "Variable with name '" + v.getName() + "' already exists in the CFA."); varNames.add(v.getName()); } + acceptingEdges = builder.acceptingEdges; } public Loc getInitLoc() { @@ -74,9 +75,7 @@ public Optional getErrorLoc() { return errorLoc; } - /** - * Get the variables appearing on the edges of the CFA. - */ + /** Get the variables appearing on the edges of the CFA. */ public Collection> getVars() { return vars; } @@ -89,15 +88,23 @@ public Collection getEdges() { return edges; } + public Collection getAcceptingEdges() { + return acceptingEdges; + } + public static Builder builder() { return new Builder(); } @Override public String toString() { - return Utils.lispStringBuilder("process").aligned().addAll(vars).body() + return Utils.lispStringBuilder("process") + .aligned() + .addAll(vars) + .body() .addAll(locs.stream().map(this::locToString)) - .addAll(edges.stream().map(this::edgeToString)).toString(); + .addAll(edges.stream().map(this::edgeToString)) + .toString(); } private String locToString(final Loc loc) { @@ -113,9 +120,11 @@ private String locToString(final Loc loc) { } private String edgeToString(final Edge edge) { - return Utils.lispStringBuilder("edge").add(edge.getSource().getName()) + return Utils.lispStringBuilder("edge") + .add(edge.getSource().getName()) .add(edge.getTarget().getName()) - .add(edge.getStmt()).toString(); + .add(edge.getStmt()) + .toString(); } public static final class Loc { @@ -185,6 +194,7 @@ public static final class Builder { private final Collection locs; private final Collection edges; + private final Collection acceptingEdges; private final Set locNames; @@ -196,6 +206,7 @@ private Builder() { locs = Containers.createSet(); locNames = Containers.createSet(); edges = new LinkedList<>(); + acceptingEdges = Containers.createSet(); built = false; } @@ -240,7 +251,8 @@ public void setErrorLoc(final Loc errorLoc) { public Loc createLoc(final String name) { checkNotBuilt(); - checkArgument(!locNames.contains(name), + checkArgument( + !locNames.contains(name), "Location with name '" + name + "' already exists in the CFA."); final Loc loc = new Loc(name); locs.add(loc); @@ -264,14 +276,23 @@ 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) { - checkState(finalLoc.getOutEdges().isEmpty(), + checkState( + finalLoc.getOutEdges().isEmpty(), "Final location cannot have outgoing edges."); } if (errorLoc != null) { - checkState(errorLoc.getOutEdges().isEmpty(), + checkState( + errorLoc.getOutEdges().isEmpty(), "Error location cannot have outgoing edges."); } built = true; @@ -282,5 +303,4 @@ private void checkNotBuilt() { checkState(!built, "A CFA was already built."); } } - } diff --git a/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFAVarChanger.kt similarity index 57% rename from subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt rename to subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFAVarChanger.kt index e3260c6bce..5a58186c9a 100644 --- a/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFAVarChanger.kt @@ -13,29 +13,27 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.cfa import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.utils.changeVars /** - * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable whose name is present in - * the parameter gets replaced to the associated instance. + * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable + * whose name is present in the parameter gets replaced to the associated instance. */ fun CFA.copyWithReplacingVars(variableMapping: Map>): CFA { - val builder = CFA.builder() - val locationMap: Map = locs.associate { it.name to builder.createLoc(it.name) } - builder.initLoc = locationMap[initLoc.name] - if (errorLoc.isPresent) - builder.errorLoc = locationMap[errorLoc.get().name] - if (finalLoc.isPresent) - builder.finalLoc = locationMap[finalLoc.get().name] - edges.forEach { - builder.createEdge( - locationMap[it.source.name], locationMap[it.target.name], - it.stmt.changeVars(variableMapping) - ) - } - return builder.build() + val builder = CFA.builder() + val locationMap: Map = locs.associate { it.name to builder.createLoc(it.name) } + builder.initLoc = locationMap[initLoc.name] + if (errorLoc.isPresent) builder.errorLoc = locationMap[errorLoc.get().name] + if (finalLoc.isPresent) builder.finalLoc = locationMap[finalLoc.get().name] + edges.forEach { + builder.createEdge( + locationMap[it.source.name], + locationMap[it.target.name], + it.stmt.changeVars(variableMapping), + ) + } + return builder.build() } diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/Ltl2BuchiTransformer.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/Ltl2BuchiTransformer.kt new file mode 100644 index 0000000000..94ba395919 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/Ltl2BuchiTransformer.kt @@ -0,0 +1,23 @@ +/* + * 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.cfa.buchi + +import hu.bme.mit.theta.cfa.CFA + +fun interface Ltl2BuchiTransformer { + + fun transform(ltl: String): CFA +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/APGeneratorVisitor.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/APGeneratorVisitor.kt new file mode 100644 index 0000000000..532f595d8c --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/APGeneratorVisitor.kt @@ -0,0 +1,190 @@ +/* + * 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.cfa.buchi.hoa + +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarBaseVisitor +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarParser +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.abstracttype.AbstractExprs +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.EnumLitExpr +import hu.bme.mit.theta.core.type.enumtype.EnumType +import hu.bme.mit.theta.core.type.inttype.IntExprs +import hu.bme.mit.theta.core.type.inttype.IntType + +class APGeneratorVisitor( + private val vars: Map>, + private val enumTypes: Map, +) : LTLGrammarBaseVisitor?>() { + + override fun visitModel(ctx: ModelContext): Expr<*> { + return super.visitModel(ctx)!! + } + + override fun visitImplyExpression(ctx: ImplyExpressionContext): Expr<*> { + return if (ctx.ops.size > 1) { + BoolExprs.Imply( + visitOrExpr(ctx.ops[0]) as Expr, + visitOrExpr(ctx.ops[1]) as Expr, + ) + } else visitOrExpr(ctx.ops[0]) + } + + override fun visitOrExpr(ctx: LTLGrammarParser.OrExprContext): Expr<*> { + if (ctx.ops.size == 1) return visitAndExpr(ctx.ops[0]) + val ops: MutableList> = ArrayList() + for (child in ctx.ops) { + ops.add(visitAndExpr(child)) + } + return BoolExprs.Or(ops) + } + + override fun visitAndExpr(ctx: LTLGrammarParser.AndExprContext): Expr { + if (ctx.ops.size == 1) return visitNotExpr(ctx.ops[0]) + val ops: MutableList> = ArrayList() + for (child in ctx.ops) { + ops.add(visitNotExpr(child)) + } + return BoolExprs.And(ops) + } + + override fun visitNotExpr(ctx: LTLGrammarParser.NotExprContext): Expr { + return if (ctx.ops.size > 0) BoolExprs.Not(visitNotExpr(ctx.ops[0])) + else visitBinaryLtlExpr(ctx.binaryLtlExpr()) as Expr + } + + override fun visitBinaryLtlExpr(ctx: BinaryLtlExprContext): Expr<*> { + return visitLtlExpr(ctx.ltlExpr()) + } + + override fun visitBinaryLtlOp(ctx: BinaryLtlOpContext): Expr<*> { + return super.visitBinaryLtlOp(ctx)!! + } + + override fun visitLtlExpr(ctx: LtlExprContext): Expr<*> { + return visitEqExpr(ctx.eqExpr()) + } + + override fun visitLtlOp(ctx: LtlOpContext): Expr<*> { + return super.visitLtlOp(ctx)!! + } + + override fun visitEqExpr(ctx: EqExprContext): Expr<*> { + return if (ctx.ops.size > 1) { + if (ctx.oper.EQ() != null) + AbstractExprs.Eq(visitRelationExpr(ctx.ops[0]), visitRelationExpr(ctx.ops[1])) + else AbstractExprs.Neq(visitRelationExpr(ctx.ops[0]), visitRelationExpr(ctx.ops[1])) + } else visitRelationExpr(ctx.ops[0]) + } + + override fun visitEqOperator(ctx: EqOperatorContext): Expr<*> { + return super.visitEqOperator(ctx)!! + } + + override fun visitRelationExpr(ctx: LTLGrammarParser.RelationExprContext): Expr<*> { + return if (ctx.ops.size > 1) { + if (ctx.oper.LEQ() != null) { + AbstractExprs.Leq(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else if (ctx.oper.GEQ() != null) { + AbstractExprs.Geq(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else if (ctx.oper.LT() != null) { + AbstractExprs.Lt(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else AbstractExprs.Gt(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else visitAdditiveExpr(ctx.ops[0]) + } + + override fun visitRelationOperator(ctx: RelationOperatorContext): Expr<*> { + return super.visitRelationOperator(ctx)!! + } + + override fun visitAdditiveExpr(ctx: LTLGrammarParser.AdditiveExprContext): Expr<*> { + var res = visitMultiplicativeExpr(ctx.ops[0]) + for (i in 1 until ctx.ops.size) { + res = + if (ctx.opers[i - 1].PLUS() != null) { + AbstractExprs.Add(res, visitMultiplicativeExpr(ctx.ops[i])) + } else { + AbstractExprs.Sub(res, visitMultiplicativeExpr(ctx.ops[i])) + } + } + return res + } + + override fun visitAdditiveOperator(ctx: AdditiveOperatorContext): Expr<*> { + return super.visitAdditiveOperator(ctx)!! + } + + override fun visitMultiplicativeExpr(ctx: LTLGrammarParser.MultiplicativeExprContext): Expr<*> { + var res = visitNegExpr(ctx.ops[0]) + for (i in 1 until ctx.ops.size) { + res = + if (ctx.opers[i - 1].DIV() != null) { + AbstractExprs.Div(res, visitNegExpr(ctx.ops[i])) + } else if (ctx.opers[i - 1].MOD() != null) { + IntExprs.Mod(res as Expr, visitNegExpr(ctx.ops[i]) as Expr) + } else { + AbstractExprs.Mul(res, visitNegExpr(ctx.ops[i])) + } + } + return res + } + + override fun visitMultiplicativeOperator(ctx: MultiplicativeOperatorContext): Expr<*> { + return super.visitMultiplicativeOperator(ctx)!! + } + + override fun visitNegExpr(ctx: LTLGrammarParser.NegExprContext): Expr<*> { + return if (ctx.ops.size > 0) { + AbstractExprs.Neg(visitNegExpr(ctx.ops[0])) + } else visitPrimaryExpr(ctx.primaryExpr()) + } + + override fun visitPrimaryExpr(ctx: LTLGrammarParser.PrimaryExprContext): Expr<*> { + return if (ctx.boolLitExpr() != null) { + visitBoolLitExpr(ctx.boolLitExpr()) + } else if (ctx.intLitExpr() != null) { + visitIntLitExpr(ctx.intLitExpr()) + } else if (ctx.enumLitExpr() != null) { + visitEnumLitExpr(ctx.enumLitExpr()) + } else visitParenExpr(ctx.parenExpr()) + } + + override fun visitBoolLitExpr(ctx: BoolLitExprContext): Expr<*> { + return if (ctx.value.text == "true") BoolExprs.True() else BoolExprs.False() + } + + override fun visitParenExpr(ctx: LTLGrammarParser.ParenExprContext): Expr<*> { + return if (ctx.variable() != null) visitVariable(ctx.variable()) + else visitImplyExpression(ctx.ops[0]) + } + + override fun visitIntLitExpr(ctx: LTLGrammarParser.IntLitExprContext): Expr<*> { + return IntExprs.Int(ctx.value.text.toInt()) + } + + override fun visitEnumLitExpr(ctx: EnumLitExprContext): Expr<*> { + return EnumLitExpr.of(enumTypes[ctx.type.text], ctx.lit.text) + } + + override fun visitVariable(ctx: LTLGrammarParser.VariableContext): Expr<*> { + val decl = vars[ctx.name.text] + if (decl == null) println("Variable [" + ctx.name.text + "] not found") + return decl!!.ref + } +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/BuchiBuilder.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/BuchiBuilder.kt new file mode 100644 index 0000000000..ebe3e6d949 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/BuchiBuilder.kt @@ -0,0 +1,189 @@ +/* + * 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.cfa.buchi.hoa + +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.common.logging.Logger +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 java.util.function.Consumer +import jhoafparser.ast.AtomAcceptance +import jhoafparser.ast.AtomLabel +import jhoafparser.ast.BooleanExpression +import jhoafparser.consumer.HOAConsumer +import jhoafparser.consumer.HOAConsumerException + +class BuchiBuilder +internal constructor( + private val logger: Logger, + private val swappedExpressions: Map>, +) : HOAConsumer { + + private val builder: CFA.Builder = CFA.builder() + private var initLocNumber: Int? = null + private var aps: MutableList? = null + private val locations: MutableMap = HashMap() + + fun build(): CFA { + return builder.build() + } + + private fun getOrCreateLocation(locName: Int): CFA.Loc { + return locations.computeIfAbsent(locName) { i: Int -> builder.createLoc(i.toString()) } + } + + private fun apBoolExpressionToInternal( + booleanExpression: BooleanExpression + ): Expr { + return when (booleanExpression.type) { + BooleanExpression.Type.EXP_AND -> + BoolExprs.And( + apBoolExpressionToInternal(booleanExpression.left), + apBoolExpressionToInternal(booleanExpression.right), + ) + + BooleanExpression.Type.EXP_OR -> + BoolExprs.Or( + apBoolExpressionToInternal(booleanExpression.left), + apBoolExpressionToInternal(booleanExpression.right), + ) + + BooleanExpression.Type.EXP_NOT -> + BoolExprs.Not(apBoolExpressionToInternal(booleanExpression.left)) + BooleanExpression.Type.EXP_TRUE -> BoolExprs.True() + BooleanExpression.Type.EXP_ATOM -> + swappedExpressions[aps!![booleanExpression.atom.toString().toInt()]]!! + else -> BoolExprs.False() + } + } + + override fun parserResolvesAliases(): Boolean { + return false + } + + override fun notifyHeaderStart(s: String) { + logger.write(Logger.Level.VERBOSE, "HOA consumer header: %s%n", s) + } + + override fun setNumberOfStates(i: Int) { + logger.write(Logger.Level.VERBOSE, "HOA automaton has %d states%n", i) + } + + @Throws(HOAConsumerException::class) + override fun addStartStates(list: List) { + if (list.isEmpty()) return + if (list.size != 1 || initLocNumber != null) + throw HOAConsumerException("HOA automaton should have exactly 1 starting location%n") + initLocNumber = list[0] + } + + override fun addAlias(s: String, booleanExpression: BooleanExpression) { + // currently does not get called by the Owl library + } + + override fun setAPs(list: List) { + if (aps == null) aps = java.util.List.copyOf(list) else aps!!.addAll(list) + } + + @Throws(HOAConsumerException::class) + override fun setAcceptanceCondition( + i: Int, + booleanExpression: BooleanExpression, + ) { + logger.write(Logger.Level.VERBOSE, "Acceptance condition: %s%n", booleanExpression) + } + + override fun provideAcceptanceName(s: String, list: List) { + logger.write(Logger.Level.VERBOSE, "Acceptance name received: %s%n", s) + list.forEach( + Consumer { o: Any? -> + logger.write(Logger.Level.VERBOSE, "\tobject under acceptance: %s%n", o) + } + ) + } + + @Throws(HOAConsumerException::class) + override fun setName(s: String) { + logger.write(Logger.Level.VERBOSE, "Automaton named {}%n", s) + } + + override fun setTool(s: String, s1: String) { + logger.write(Logger.Level.VERBOSE, "Tool named %s %s%n", s, s1) + } + + override fun addProperties(list: List) { + if (list.isEmpty()) return + logger.write(Logger.Level.VERBOSE, "Properties:%n") + list.forEach(Consumer { prop: String? -> logger.write(Logger.Level.VERBOSE, "%s", prop) }) + logger.write(Logger.Level.VERBOSE, "%n") + } + + override fun addMiscHeader(s: String, list: List) { + // we don't really care for these yet + } + + override fun notifyBodyStart() { + // no action needed + } + + override fun addState( + i: Int, + s: String?, + booleanExpression: BooleanExpression?, + list: List?, + ) { + getOrCreateLocation(i) + } + + override fun addEdgeImplicit(i: Int, list: List, list1: List) { + TODO("This should only be called for state-based acceptance which is not yet supported") + } + + @Throws(HOAConsumerException::class) + override fun addEdgeWithLabel( + i: Int, + booleanExpression: BooleanExpression, + list: List, + list1: List?, + ) { + val from = getOrCreateLocation(i) + val to = getOrCreateLocation(list[0]) + val edge = + builder.createEdge(from, to, Stmts.Assume(apBoolExpressionToInternal(booleanExpression))) + if (list1 != null && !list1.isEmpty()) builder.setAcceptingEdge(edge) + } + + override fun notifyEndOfState(i: Int) { + // no action needed + } + + @Throws(HOAConsumerException::class) + override fun notifyEnd() { + if (initLocNumber == null) throw HOAConsumerException("No initial location named") + builder.initLoc = locations[initLocNumber] + } + + override fun notifyAbort() { + // never gets called yet + } + + @Throws(HOAConsumerException::class) + override fun notifyWarning(s: String) { + throw HOAConsumerException(s) + } +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/ExternalLtl2Hoaf.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/ExternalLtl2Hoaf.kt new file mode 100644 index 0000000000..02cc810f18 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/ExternalLtl2Hoaf.kt @@ -0,0 +1,25 @@ +/* + * 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.cfa.buchi.hoa + +import hu.bme.mit.theta.common.process.SimpleProcessRunner + +class ExternalLtl2Hoaf(private val cmd: String) : Ltl2Hoaf { + + override fun transform(ltl: String): String { + return SimpleProcessRunner.run("$cmd '$ltl'", 20) + } +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/LTLExprVisitor.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/LTLExprVisitor.kt new file mode 100644 index 0000000000..c0339f9c5f --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/LTLExprVisitor.kt @@ -0,0 +1,233 @@ +/* + * 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.cfa.buchi.hoa + +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarBaseVisitor +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarParser +import hu.bme.mit.theta.cfa.dsl.gen.LTLGrammarParser.* +import org.antlr.v4.runtime.ParserRuleContext + +/** + * 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. + */ +object LTLExprVisitor : LTLGrammarBaseVisitor() { + + var ltl: HashMap = HashMap() + + override fun visitModel(ctx: ModelContext): Boolean { + return super.visitModel(ctx)!! + } + + override fun visitImplyExpression(ctx: ImplyExpressionContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitOrExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitAndExpr(ctx: LTLGrammarParser.AndExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNotExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitNotExpr(ctx: LTLGrammarParser.NotExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNotExpr(op)) { + ltl[ctx] = true + return true + } + } + if (ctx.binaryLtlExpr() != null && visitBinaryLtlExpr(ctx.binaryLtlExpr())) { + ltl[ctx] = true + return true + } + ltl[ctx] = false + return false + } + + override fun visitBinaryLtlExpr(ctx: BinaryLtlExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + if (ctx.type != null) { + ltl[ctx] = true + return true + } + val child = visitLtlExpr(ctx.ltlExpr()) + ltl[ctx] = child + return child + } + + override fun visitBinaryLtlOp(ctx: BinaryLtlOpContext): Boolean { + return false + } + + override fun visitLtlExpr(ctx: LtlExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + if (ctx.type != null) { + ltl[ctx] = true + return true + } + val child = visitEqExpr(ctx.eqExpr()) + ltl[ctx] = child + return child + } + + override fun visitLtlOp(ctx: LtlOpContext): Boolean { + return false + } + + override fun visitEqExpr(ctx: EqExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitRelationExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitEqOperator(ctx: EqOperatorContext): Boolean { + return false + } + + override fun visitRelationExpr(ctx: LTLGrammarParser.RelationExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitAdditiveExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitRelationOperator(ctx: RelationOperatorContext): Boolean { + return false + } + + override fun visitAdditiveExpr(ctx: LTLGrammarParser.AdditiveExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitMultiplicativeExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitAdditiveOperator(ctx: AdditiveOperatorContext): Boolean { + return false + } + + override fun visitMultiplicativeExpr(ctx: LTLGrammarParser.MultiplicativeExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNegExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitMultiplicativeOperator(ctx: MultiplicativeOperatorContext): Boolean { + return false + } + + override fun visitNegExpr(ctx: LTLGrammarParser.NegExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNegExpr(op)) { + ltl[ctx] = true + return true + } + } + if (ctx.primaryExpr() != null && visitPrimaryExpr(ctx.primaryExpr())) { + ltl[ctx] = true + return true + } + ltl[ctx] = false + return false + } + + override fun visitPrimaryExpr(ctx: LTLGrammarParser.PrimaryExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + var 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[ctx] = child + return child + } + + override fun visitBoolLitExpr(ctx: BoolLitExprContext): Boolean { + return false + } + + override fun visitParenExpr(ctx: LTLGrammarParser.ParenExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitImplyExpression(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitIntLitExpr(ctx: LTLGrammarParser.IntLitExprContext): Boolean { + return false + } + + override fun visitVariable(ctx: LTLGrammarParser.VariableContext): Boolean { + return false + } + + override fun visitOrExpr(ctx: LTLGrammarParser.OrExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitAndExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2BuchiThroughHoaf.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2BuchiThroughHoaf.kt new file mode 100644 index 0000000000..26f10bc865 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2BuchiThroughHoaf.kt @@ -0,0 +1,49 @@ +/* + * 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.cfa.buchi.hoa + +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.buchi.Ltl2BuchiTransformer +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.VarDecl +import hu.bme.mit.theta.core.type.enumtype.EnumType +import jhoafparser.parser.HOAFParser +import org.antlr.v4.runtime.CharStreams +import org.antlr.v4.runtime.CommonTokenStream + +class Ltl2BuchiThroughHoaf( + private val converter: Ltl2Hoaf, + private val variables: Collection>, + private val logger: Logger, +) : Ltl2BuchiTransformer { + + override fun transform(ltl: String): CFA { + val modelContext = + LTLGrammarParser(CommonTokenStream(LTLGrammarLexer(CharStreams.fromString(ltl)))).model() + val namedVariables: Map> = variables.associateBy { it.name } + val enumTypes: Map = + variables.mapNotNull { it.type as? EnumType }.associateBy { it.name } + val toStringVisitor = ToStringVisitor(APGeneratorVisitor(namedVariables, enumTypes)) + val swappedLtl = toStringVisitor.visitModel(modelContext) + val negatedLtl = "!($swappedLtl)" + val hoafExpression = converter.transform(negatedLtl) + val buchiBuilder = BuchiBuilder(logger, toStringVisitor.aps) + HOAFParser.parseHOA(hoafExpression.byteInputStream(), buchiBuilder) + return buchiBuilder.build() + } +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2Hoaf.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2Hoaf.kt new file mode 100644 index 0000000000..601f0dc2c8 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2Hoaf.kt @@ -0,0 +1,21 @@ +/* + * 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.cfa.buchi.hoa + +fun interface Ltl2Hoaf { + + fun transform(ltl: String): String +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2HoafFromDir.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2HoafFromDir.kt new file mode 100644 index 0000000000..f1213c2cc2 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/Ltl2HoafFromDir.kt @@ -0,0 +1,30 @@ +/* + * 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.cfa.buchi.hoa + +import java.net.URLEncoder +import java.nio.file.Path + +/** + * Provide a directory which contains HOAF files named as their respective LTL expression .hoa. E.g. + * if you have the hoaf representation of `F a` as `/tmp/ltls/F a.hoa`, create this class with + * `/tmp/ltls` and simply call the transform with the ltl expression. + */ +class Ltl2HoafFromDir(private val dir: String) : Ltl2Hoaf { + + override fun transform(ltl: String) = + Path.of("""$dir/${URLEncoder.encode(ltl, "UTF-8")}.hoa""").toFile().readText() +} diff --git a/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/ToStringVisitor.kt b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/ToStringVisitor.kt new file mode 100644 index 0000000000..b3fae7b415 --- /dev/null +++ b/subprojects/cfa/cfa/src/main/kotlin/cfa/buchi/hoa/ToStringVisitor.kt @@ -0,0 +1,298 @@ +/* + * 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.cfa.buchi.hoa + +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 + +class ToStringVisitor(private val apGeneratorVisitor: APGeneratorVisitor) : + LTLGrammarBaseVisitor() { + + var aps: HashMap> = HashMap() + private var counter = 0 + + override fun visitModel(ctx: ModelContext): String { + return visitImplyExpression(ctx.implyExpression) + } + + override fun visitImplyExpression(ctx: ImplyExpressionContext): String { + if (!LTLExprVisitor.visitImplyExpression(ctx)) { + val name = generateApName() + val expr = apGeneratorVisitor.visitImplyExpression(ctx) + aps[name] = expr as Expr + return name + } + return if (ctx.ops.size > 1) { + visitOrExpr(ctx.ops[0]) + " -> " + visitOrExpr(ctx.ops[1]) + } else { + visitOrExpr(ctx.ops[0]) + } + } + + override fun visitOrExpr(ctx: OrExprContext): String { + if (!LTLExprVisitor.visitOrExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitOrExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitAndExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(" | ") + builder.append(visitAndExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitAndExpr(ctx: AndExprContext): String { + if (!LTLExprVisitor.visitAndExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitAndExpr(ctx) + return name + } + val builder = StringBuilder() + builder.append(visitNotExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(" & ") + builder.append(visitNotExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitNotExpr(ctx: NotExprContext): String { + if (!LTLExprVisitor.visitNotExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitNotExpr(ctx) + return name + } + return if (ctx.ops.isNotEmpty()) { + "! " + visitNotExpr(ctx.ops[0]) + } else { + visitBinaryLtlExpr(ctx.binaryLtlExpr()) + } + } + + override fun visitBinaryLtlExpr(ctx: BinaryLtlExprContext): String { + if (!LTLExprVisitor.visitBinaryLtlExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitBinaryLtlExpr(ctx) as Expr + return name + } + return if (ctx.type != null) { + (visitBinaryLtlExpr(ctx.ops[0]) + + " " + + visitBinaryLtlOp(ctx.type) + + " " + + visitBinaryLtlExpr(ctx.ops[1])) + } else { + visitLtlExpr(ctx.ltlExpr()) + } + } + + override fun visitBinaryLtlOp(ctx: BinaryLtlOpContext): String { + return if (ctx.U_OP() != null) { + "U" + } else if (ctx.M_OP() != null) { + "M" + } else if (ctx.W_OP() != null) { + "W" + } else { + "R" + } + } + + override fun visitLtlExpr(ctx: LtlExprContext): String { + if (!LTLExprVisitor.visitLtlExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitLtlExpr(ctx) as Expr + return name + } + return if (ctx.ops.size > 0) { + visitLtlOp(ctx.type) + " " + visitLtlExpr(ctx.ops[0]) + } else { + visitEqExpr(ctx.eqExpr()) + } + } + + override fun visitLtlOp(ctx: LtlOpContext): String { + return if (ctx.F_OP() != null) { + "F" + } else if (ctx.G_OP() != null) { + "G" + } else { + "X" + } + } + + override fun visitEqExpr(ctx: EqExprContext): String { + if (!LTLExprVisitor.visitEqExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitEqExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitRelationExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitEqOperator(ctx.oper)) + builder.append(visitRelationExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitEqOperator(ctx: EqOperatorContext): String { + return if (ctx.EQ() != null) { + "=" + } else { + "/=" + } + } + + override fun visitRelationExpr(ctx: RelationExprContext): String { + if (!LTLExprVisitor.visitRelationExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitRelationExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitAdditiveExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitRelationOperator(ctx.oper)) + builder.append(visitAdditiveExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitRelationOperator(ctx: RelationOperatorContext): String { + return if (ctx.LT() != null) { + "<" + } else if (ctx.GT() != null) { + ">" + } else if (ctx.LEQ() != null) { + "<=" + } else ">=" + } + + override fun visitAdditiveExpr(ctx: AdditiveExprContext): String { + if (!LTLExprVisitor.visitAdditiveExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitAdditiveExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitMultiplicativeExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitAdditiveOperator(ctx.opers[i - 1])) + builder.append(visitMultiplicativeExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitAdditiveOperator(ctx: AdditiveOperatorContext): String { + return if (ctx.PLUS() != null) { + "+" + } else "-" + } + + override fun visitMultiplicativeExpr(ctx: MultiplicativeExprContext): String { + if (!LTLExprVisitor.visitMultiplicativeExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitMultiplicativeExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitNegExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitMultiplicativeOperator(ctx.opers[i - 1])) + builder.append(visitNegExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitMultiplicativeOperator(ctx: MultiplicativeOperatorContext): String { + return if (ctx.MUL() != null) { + "*" + } else if (ctx.MOD() != null) { + "%" + } else "/" + } + + override fun visitNegExpr(ctx: NegExprContext): String { + if (!LTLExprVisitor.visitNegExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitNegExpr(ctx) as Expr + return name + } + return if (ctx.ops.size > 0) { + "- " + visitNegExpr(ctx.ops[0]) + } else { + visitPrimaryExpr(ctx.primaryExpr()) + } + } + + override fun visitPrimaryExpr(ctx: PrimaryExprContext): String { + if (!LTLExprVisitor.visitPrimaryExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitPrimaryExpr(ctx) as Expr + return name + } + return if (ctx.parenExpr() != null) { + visitParenExpr(ctx.parenExpr()) + } else if (ctx.intLitExpr() != null) { + visitIntLitExpr(ctx.intLitExpr()) + } else visitBoolLitExpr(ctx.boolLitExpr()) + } + + override fun visitBoolLitExpr(ctx: BoolLitExprContext): String { + return ctx.value.text + } + + override fun visitParenExpr(ctx: ParenExprContext): String { + if (!LTLExprVisitor.visitParenExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitParenExpr(ctx) as Expr + return name + } + return if (ctx.variable() != null) { + visitVariable(ctx.variable()) + } else { + "(" + visitImplyExpression(ctx.ops[0]) + ")" + } + } + + override fun visitIntLitExpr(ctx: IntLitExprContext): String { + if (!LTLExprVisitor.visitIntLitExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitIntLitExpr(ctx) as Expr + return name + } + return ctx.value.text + } + + override fun visitVariable(ctx: VariableContext): String { + if (!LTLExprVisitor.visitVariable(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitVariable(ctx) as Expr + return name + } + return ctx.name.text + } + + private fun generateApName(): String { + return "ap" + (counter++) + } +} diff --git a/subprojects/common/common/build.gradle.kts b/subprojects/common/common/build.gradle.kts index 5f55ec589f..971b6106d4 100644 --- a/subprojects/common/common/build.gradle.kts +++ b/subprojects/common/common/build.gradle.kts @@ -15,4 +15,9 @@ */ plugins { id("java-common") + id("kotlin-common") +} + +dependencies { + implementation(Deps.nuprocess) } diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/process/SimpleProcessRunner.kt b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/process/SimpleProcessRunner.kt new file mode 100644 index 0000000000..a7964e735e --- /dev/null +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/process/SimpleProcessRunner.kt @@ -0,0 +1,66 @@ +/* + * 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.process + +import com.zaxxer.nuprocess.NuAbstractProcessHandler +import com.zaxxer.nuprocess.NuProcessBuilder +import java.nio.ByteBuffer +import java.util.concurrent.TimeUnit + +object SimpleProcessRunner { + + fun run(cmd: String, timeout: Long = 0): String { + val processBuilder = NuProcessBuilder(cmd.split(" ")) + val handler = ProcessHandler() + processBuilder.setProcessListener(handler) + processBuilder.start().waitFor(timeout, TimeUnit.SECONDS) + return handler.output + } + + class ProcessHandler : NuAbstractProcessHandler() { + var output: String = "" + var error: String = "" + + override fun onStdout(buffer: ByteBuffer?, closed: Boolean) { + if (!closed && buffer != null) { + val bytes = ByteArray(buffer.remaining()) + buffer[bytes] + output = String(bytes) + } + } + + override fun onStderr(buffer: ByteBuffer?, closed: Boolean) { + if (!closed && buffer != null) { + val bytes = ByteArray(buffer.remaining()) + buffer[bytes] + error = "$error\n${String(bytes)}" + } + } + + override fun onExit(statusCode: Int) { + if (statusCode == Integer.MIN_VALUE) { + throw ProcessException("Nuprocess launch error") + } + if (statusCode != 0) { + throw ProcessException( + if (error != "") error else "Process exit with non-zero code: $statusCode" + ) + } + } + } +} + +class ProcessException(err: String) : Exception(err)