LTLSatTests.scala 871 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
package de.tum.niwo.tests.papertests

import java.io.File

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.invariants.InvariantGenerator.genEq
import de.tum.niwo.{Examples, MainLTLWorkflows, Utils}
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.parser.{TransitionSystemParser, WorkflowParser}
import de.tum.niwo.tests.TestUtils.{checkSafe, checkSafeCausalElim}
import org.scalatest.FlatSpec

class LTLSatTests extends FlatSpec with LazyLogging {

  def generate(name:String) = {
    MainLTLWorkflows.generateExample(name)
  }

  "Nonomitting Easychair" should "be generated" in {
    val names = List(
      "nonomitting/conference_stubborn"
    )

    names.foreach(generate)
  }

}