LTL checking capability

Add possibility of checking LTL properties with CEGAR.
CFA is now extended with optional accepting edges. Classes are available that convert LTL string to such CFA.

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java

@@ -15,13 +15,12 @@
  */
 package hu.bme.mit.theta.analysis.unit;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import com.google.common.collect.ImmutableList;
 import hu.bme.mit.theta.analysis.InitFunc;
-
 import java.util.Collection;
 
-import static com.google.common.base.Preconditions.checkNotNull;
-
 public final class UnitInitFunc implements InitFunc<UnitState, UnitPrec> {
 
     private static final UnitInitFunc INSTANCE = new UnitInitFunc();

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java

@@ -15,8 +15,6 @@
  */
 package hu.bme.mit.theta.analysis.algorithm.loopchecker;
 
-import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
-
 import hu.bme.mit.theta.analysis.Analysis;
 import hu.bme.mit.theta.analysis.LTS;
 import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult;
@@ -45,18 +43,21 @@
 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.function.Predicate;
-import kotlin.Unit;
-import org.junit.Assert;
-import org.junit.Test;
-import org.junit.runner.RunWith;
-import org.junit.runners.Parameterized;
+
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
 
 @RunWith(Parameterized.class)
 public class LDGAbstractorCheckingTest {
@@ -80,7 +81,6 @@ public static Collection<Object[]> data() {
                     {"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},

subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt

@@ -21,12 +21,12 @@ 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
-import java.util.function.Consumer
 
 class BuchiBuilder
 internal constructor(

subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt

@@ -33,12 +33,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 LtlCheckTestWithCfaExpl(

subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt

@@ -30,12 +30,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(

subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt

@@ -32,12 +32,12 @@ import hu.bme.mit.theta.xsts.analysis.XstsState
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder
 import hu.bme.mit.theta.xsts.dsl.XstsDslManager
 import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass
+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 LtlCheckTestWithXstsExpl(

subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt

@@ -29,12 +29,12 @@ 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 hu.bme.mit.theta.xsts.passes.XstsNormalizerPass
+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(