package de.tum.workflows.ltl.tests

import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._

import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
import de.tum.workflows.blocks._
import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker

class NonOmittingInvariantFilesTest extends FlatSpec {

  "InvariantChecker" should "prove simple things safe" in {
    val name = "tests/simpleNoChoice2"
    val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
    assert(checkSafe(name, inv))
  }

  it should "prove simple loops safe" in {
    val name = "tests/loopexampleNoOracle"
    val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
    assert(checkSafe(name, inv))
  }
  
  it should "prove simple loops safe and iterate" in {
    val name = "tests/loopexampleNoOracle"
    val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
    assert(checkSafe(name, inv))
  }

  it should "fail on oracly things" in {
    val name = "tests/simpleChoice"
    val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
    assert(!checkSafe(name, inv))
  }
  
  it should "fail on loopy oracly things" in {
    val name = "tests/loopexample"
    val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
    assert(!checkSafe(name, inv))
  }

  def checkSafe(name: String, inv: Formula) = {
    val spec = ExampleWorkflows.parseExample(name).get
    val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
    Utils.write(s"${name}.dot", dot)
    res
  }

  def genEq(name: String, params: List[Var]) = {
    val o1 = Fun(name, Some("t1"), params)
    val o2 = Fun(name, Some("t2"), params)
    Eq(o1, o2)
  }
}