formatting

RipplB · Oct 30, 2024 · 930c58d · 930c58d
1 parent 8756c32
commit 930c58d
Show file tree

Hide file tree

Showing 11 changed files with 23 additions and 30 deletions.
diff --git a/...cts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java b/...cts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java
@@ -24,12 +24,11 @@
 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.Shape;
 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;

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
@@ -15,20 +15,19 @@
  */
 package hu.bme.mit.theta.cfa;
 
+import static com.google.common.base.Preconditions.*;
+import static com.google.common.collect.ImmutableSet.toImmutableSet;
+import static java.lang.String.format;
+
 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.

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
@@ -15,23 +15,22 @@
  */
 package hu.bme.mit.theta.cfa.buchi;
 
+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;
+
 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<Expr> {
 
     private final Map<String, VarDecl<?>> vars;

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
@@ -26,6 +26,11 @@
 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 java.util.Collection;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.stream.Collectors;
 import jhoafparser.ast.AtomAcceptance;
 import jhoafparser.ast.AtomLabel;
 import jhoafparser.ast.BooleanExpression;
@@ -43,12 +48,6 @@
 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;

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
@@ -17,9 +17,8 @@
 
 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;
+import org.antlr.v4.runtime.ParserRuleContext;
 
 /**
  * Returns whether an AST element represents an LTL expression that has no temporal operators. We

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
@@ -19,7 +19,6 @@
 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<String> {

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
@@ -15,19 +15,18 @@
  */
 package hu.bme.mit.theta.cfa.buchi;
 
+import static hu.bme.mit.theta.core.decl.Decls.Var;
+
 import hu.bme.mit.theta.cfa.CFA;
 import hu.bme.mit.theta.common.logging.ConsoleLogger;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import java.util.List;
 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;

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
@@ -37,12 +37,12 @@ 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 java.io.FileInputStream
 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(

diff --git a/...rojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt b/...rojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt
@@ -36,12 +36,12 @@ 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 java.io.FileInputStream
 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(

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
@@ -23,12 +23,12 @@ 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 java.io.FileInputStream
 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(

diff --git a/...ojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt b/...ojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt
@@ -30,12 +30,12 @@ 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 java.io.FileInputStream
 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(