This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

TacasBenchmarks.scala 5.31 KB
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 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 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
package de.bbisping.coupledsim.flink

import org.apache.flink.api.scala.ExecutionEnvironment

import scala.collection.Seq

/**
  * Runs the coupled simulation flink algorithm on a number of VLTS samples
  * in order to produce the benchmarking results as reported in our TACAS 2019
  * paper.
  */
object TacasBenchmarks {
  
  val tacasSamples = Seq(
    "shared/src/test/assets/csv/coupled-sim-phil.csv",
    "shared/src/test/assets/csv/ltbts.csv",
    "shared/src/test/assets/vlts/vasy_0_1.csv", //   289,   1224,  no tau,  2
    "shared/src/test/assets/vlts/vasy_1_4.csv", //  1183,   4464,    1213,  6
    "shared/src/test/assets/vlts/vasy_5_9.csv",
    "shared/src/test/assets/vlts/cwi_1_2.csv", //  1952,   2387,    2215, 26
    "shared/src/test/assets/vlts/cwi_3_14.csv",//  3996,  14552,   14551,  2
    "shared/src/test/assets/vlts/vasy_8_24.csv",
    "shared/src/test/assets/vlts/vasy_8_38.csv",
    "shared/src/test/assets/vlts/vasy_10_56.csv",
    "shared/src/test/assets/vlts/vasy_25_25.csv"
  )

  val systemPathToTacasHandle = Map(
    "shared/src/test/assets/csv/coupled-sim-phil.csv" -> "phil",
    "shared/src/test/assets/csv/ltbts.csv" -> "ltbts"
  ).withDefault(s => s.slice(s.lastIndexOf('/') + 1, s.lastIndexOf('.')))

  def runSizeMark(cfgPreminimization: String, cfgOverApproximation: String): Unit = {
    val samples = tacasSamples
    
    val env = ExecutionEnvironment.getExecutionEnvironment
    env.getConfig.disableSysoutLogging()
    
    for (s <- samples) {
      
      val begin = System.currentTimeMillis()
      
      val csResult = CoupledSimulationFlink.executeAlgorithm(env,
          cfgPath = s,
          cfgPreminimization = cfgPreminimization,
          cfgOverApproximation = cfgOverApproximation,
          cfgBenchmarkSizes = true,
          cfgReturnPartitionRelation = true)
          
      val time = System.currentTimeMillis() - begin
      val benchmark = csResult.benchmarkSizes.withDefaultValue("")
      val (csPart, csRel) = csResult.partitionRelation
      val csPartitionCount = csPart.values.toSet.size
      
      println(s + ", " + 
          benchmark("systemStates") + ", " +
          benchmark("systemTransitions") + ", " +
          benchmark("systemWeakTransitions") + ", " +
          benchmark("minimizedStates") + ", " +
          benchmark("minimizedTransitions") + ", " +
          benchmark("gameNodes") + ", " +
          benchmark("gameMoves") + ", " +
          csPartitionCount + ", " +
          csRel.size + ", " +
          time)
    }
  }
  def runTacasMark(): Unit = {
    val samples = tacasSamples

    val cfgOverApproximation = "bigstep"
    val cfgPreminimization = "delaybisim"

    val env = ExecutionEnvironment.getExecutionEnvironment
    env.getConfig.disableSysoutLogging()
    env.setParallelism(4)

    println("Warmup for time benchmark using the first four systems...")

    for (s <- samples.take(4)) {

      val begin = System.currentTimeMillis()

      CoupledSimulationFlink.executeAlgorithm(env,
        cfgPath = s,
        cfgPreminimization = cfgPreminimization,
        cfgOverApproximation = cfgOverApproximation)

      val time = System.currentTimeMillis() - begin
    }

    println("\nTime Benchmark\n")

    println("system, time/s")

    for (s <- samples) {
      
      val begin = System.currentTimeMillis()
      
      CoupledSimulationFlink.executeAlgorithm(env,
          cfgPath = s,
          cfgPreminimization = cfgPreminimization,
          cfgOverApproximation = cfgOverApproximation)
          
      val time = System.currentTimeMillis() - begin

      println(systemPathToTacasHandle(s) + ", " + time)
    }

    println("\nSystem sizes\n")

    println("S, ->, =|>, S_DBquotient, >->")

    for (s <- samples.dropRight(2)) {

      val begin = System.currentTimeMillis()

      val csResult = CoupledSimulationFlink.executeAlgorithm(env,
        cfgPath = s,
        cfgPreminimization = cfgPreminimization,
        cfgOverApproximation = "none",
        cfgBenchmarkSizes = true,
        cfgReturnPartitionRelation = true)

      val time = System.currentTimeMillis() - begin
      val benchmark = csResult.benchmarkSizes.withDefaultValue("")

      println(systemPathToTacasHandle(s) + ", " +
        benchmark("systemStates") + ", " +
        benchmark("systemTransitions") + ", " +
        benchmark("systemWeakTransitions") + ", " +
        benchmark("minimizedStates") + ", " +
        benchmark("gameMoves"))
    }
    //vasy_10_56 and vasy_25_25 are omitted as they would crash due to the unoptimized game not
    //fitting into the memory.]")
    println("vasy_10_56, o.o.m")
    println("vasy_25_25, o.o.m")

    println("\n>->_sigma, S_CSquotient, CSonQuotient")

    for (s <- samples) {

      val begin = System.currentTimeMillis()

      val csResult = CoupledSimulationFlink.executeAlgorithm(env,
        cfgPath = s,
        cfgPreminimization = cfgPreminimization,
        cfgOverApproximation = cfgOverApproximation,
        cfgBenchmarkSizes = true,
        cfgReturnPartitionRelation = true)

      val time = System.currentTimeMillis() - begin
      val benchmark = csResult.benchmarkSizes.withDefaultValue("")
      val (csPart, csRel) = csResult.partitionRelation
      val csPartitionCount = csPart.values.toSet.size

      println(systemPathToTacasHandle(s) + ", " +
        benchmark("gameMoves") + ", " +
        csPartitionCount + ", " +
        csRel.size)
    }

  }


}