Commit 7df195e7 authored by Christian Müller's avatar Christian Müller

fix merge

parent 294da866
...@@ -32,6 +32,7 @@ results/*.ltl ...@@ -32,6 +32,7 @@ results/*.ltl
results/*.ppltl results/*.ppltl
results/*.foltl results/*.foltl
results/*.png results/*.png
results/*.metrics
# aalta # aalta
cnf.dimacs cnf.dimacs
......
...@@ -9,9 +9,9 @@ class Test { ...@@ -9,9 +9,9 @@ class Test {
public static void main(String[] args) { public static void main(String[] args) {
System.out.println("Test"); System.out.println("Test");
var owlform = BooleanConstant.FALSE; BooleanConstant owlform = BooleanConstant.FALSE;
var checksat = LanguageAnalysis.isSatisfiable(owlform); boolean checksat = LanguageAnalysis.isSatisfiable(owlform);
System.out.println(checksat); System.out.println(checksat);
} }
......
...@@ -4,7 +4,7 @@ import foltl.FOLTL._ ...@@ -4,7 +4,7 @@ import foltl.FOLTL._
import blocks.Workflow._ import blocks.Workflow._
import Implicits._ import Implicits._
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.FOTransformers import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.Utils._ import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties import de.tum.workflows.foltl.Properties
...@@ -30,7 +30,7 @@ object InvariantInspector extends App with LazyLogging { ...@@ -30,7 +30,7 @@ object InvariantInspector extends App with LazyLogging {
logger.info(s"Encoding Spec:\n$spec") logger.info(s"Encoding Spec:\n$spec")
def invariant = def invariant =
InvariantGenerator.invariantNoninterStubbornSingleBS _ InvariantGenerator.invariantNoninterSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _ // InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _ // InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _ // InvariantChecker.invariantAllEqual _
...@@ -51,7 +51,7 @@ object InvariantInspector extends App with LazyLogging { ...@@ -51,7 +51,7 @@ object InvariantInspector extends App with LazyLogging {
} }
} }
inspect("omitting/conference") // inspect("omitting/conference")
// generateExample("tests/loopexampleNoOracle") inspect("tests/loopexampleNoOracle")
// generateAllExamples() // generateAllExamples()
} }
\ No newline at end of file
...@@ -7,10 +7,10 @@ import de.tum.workflows.Utils._ ...@@ -7,10 +7,10 @@ import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Properties import de.tum.workflows.foltl.Properties
import de.tum.workflows.blocks.Spec import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.owltransformer.OwlTransformer import de.tum.workflows.owltransformer.OwlTransformer
import owl.ltl.algorithms.LanguageAnalysis import owl.ltl.algorithms.LanguageAnalysis
import owl.ltl.rewriter.SimplifierFactory import owl.ltl.rewriter.SimplifierFactory
import de.tum.workflows.ltl.FOTransformers
object MainLTL extends App with LazyLogging { object MainLTL extends App with LazyLogging {
......
...@@ -10,7 +10,6 @@ import com.typesafe.scalalogging.LazyLogging ...@@ -10,7 +10,6 @@ import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils import de.tum.workflows.Utils
import de.tum.workflows.foltl.FOTransformers import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.foltl.FormulaFunctions import de.tum.workflows.foltl.FormulaFunctions
import it.unimi.dsi.fastutil.longs.Long2BooleanArrayMap
object Z3QFree extends LazyLogging { object Z3QFree extends LazyLogging {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment