CCSSubmissionTest.scala 3.54 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
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 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 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
package de.tum.niwo.tests.papertests

import de.tum.niwo.foltl.FOLTL.{Forall, Var}
import de.tum.niwo.invariants.InvariantGenerator.genEq
import de.tum.niwo.{Examples, Utils}
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.tests.TestUtils.checkSafe
import org.scalatest.FlatSpec

class CCSSubmissionTest extends FlatSpec {

  def checkTS(name:String, properties:InvProperties):Boolean = {
    val spec = Examples.parseExampleTS(name).get
    Utils.check(name, "", spec, properties)
  }

  val properties = InvProperties(stubborn = true, eliminateA = true, eliminateB = true)

  "Single trace Easychair" should "be proven safe" in {
    val name = "tstests/easychair_singletrace"

    assert(checkTS(name, properties))
  }

  "Deterministic Leader election" should "be proven safe" in {
    val name = "tstests/leaderelection_inductive"

    assert(checkTS(name, properties))
  }


  it should "be proven safe with Bs" in {
    val name = "tstests/leaderelection_inductive_withB"

    assert(checkTS(name, properties))
  }

  it should "be proven safe with easier B" in {
    val name = "tstests/leaderelection_inductive_withB2"

    assert(checkTS(name, properties))
  }

  "Easychair" should "prove stubborn conference" in {
    val name = "omitting/conference_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = false
    ))
  }

  it should "prove stubborn conference with B" in {
    val name = "omitting/conference_stubborn_withB"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = false
    ))
  }

  it should "prove linear causal stuff with B safe" in {
    val name = "tests/conference_linear_small_withB"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
    assert(checkSafe(name, "", _ => inv,
      InvProperties(stubborn = false, approxElim = false)))
  }

//  it should "fail to prove causal conference with approxElim" in {
//    val name = "omitting/conference"
//    val inv = InvariantGenerator.invariantNoninterSingleBS _
//    assert(checkSafe(name, "", inv, InvProperties(
//      stubborn = false,
//      approxElim = true
//    )))
//  }

  it should "prove causal unrolled conference with approxElim" in {
    val name = "omitting/conference_unrolled_withB"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = false,
      approxElim = true
    )))
  }

  // terminates, but gives strategy False
  it should "prove causal conference with approxElim" in {
    val name = "omitting/conference_withB"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = false,
      approxElim = true
    )))
  }

  it should "prove stubborn omitting/conference_linear_fixed" in {
    val name = "omitting/conference_linear_fixed"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = false
    )))
  }

  it should "prove causal omitting/conference_linear_fixed" in {
    val name = "omitting/conference_linear_fixed"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = false,
      approxElim = false
    )))
  }
}