OwlTest.scala 1.74 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.workflows.tests
2 3 4 5 6 7

import java.util
import java.util.EnumSet

import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
8
import de.tum.workflows.owltransformer.OwlTransformer
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import owl.automaton.algorithms.{EmptinessCheck, LanguageAnalysis}
import owl.ltl.parser.LtlParser
import owl.run.{DefaultEnvironment, RunUtil}
import owl.translations.SimpleTranslations
import owl.translations.ltl2dra.LTL2DRAFunction
import owl.translations.ltl2ldba.LTL2LDBAFunction
import owl.translations.ltl2ldba.LTL2LDBAFunction.Configuration

class OwlTest  extends FlatSpec with LazyLogging {


  "OwlTransformer" should "go to owl formulas" in {

    val tests = List(
      (Next(Or(Var("x"), Var("y"))), "X(x | y)"),
      (And(Var("x"), Var("y")), "(x & y)"),
      (Globally(Finally(Var("y"))), "GF y"),
Christian Müller's avatar
Christian Müller committed
29
      (Next(Finally(Equiv(Var("y"), Var("z")))), "XF (y <-> z)")
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
    )

    for (t <- tests) {
      val owlform = OwlTransformer.toOwl(t._1)
      val parsedform = LtlParser.parse(t._2)

      owlform shouldEqual (parsedform)
    }
  }

  "OWLFormulas" should "identify satisfiability" in {

    val tests = List(
      (Next(Or(Var("x"), Var("y"))), false)
//      (And(Var("x"), Var("y")), true),
//      (Globally(Finally(Var("y"))), true),
//      (Next(Finally(Eq(Var("y"), Neg(Var("y"))))), false),
//      (And(Globally(Var("y")), Finally(Neg(Var("y")))), false)
    )

    for (t <- tests) {
      val owlform = OwlTransformer.toOwl(t._1)

      val env = DefaultEnvironment.of(true, false, false)
      val trans = SimpleTranslations.buildSafety(owlform, env)
      val empty = EmptinessCheck.isEmpty(trans)

      empty should be (t._2)
    }

  }
}