Skip to content

Commit

Permalink
Removed failing test case
Browse files Browse the repository at this point in the history
  • Loading branch information
leventeBajczi committed Nov 17, 2023
1 parent 366970b commit 45a154f
Showing 1 changed file with 0 additions and 57 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -208,61 +208,4 @@ class XcfaPortfolioTest {
}


@Test
fun testDoubleAsyncXcfaPortfolio() {
val cnt = ExecCnt()

val parseContext = ParseContext()
val (xcfa, _, _) = getXcfaFromC(
stream = FileInputStream(javaClass.getResource("/c/dekker.i")!!.path),
parseContext = parseContext,
collectStatistics = false,
checkOverflow = false,
warningLogger = NullLogger.getInstance()
)

val config1 = ConfigNode(
name = "config1",
config = XcfaCegarConfig(domain = Domain.PRED_CART),
check = { inProcess, config ->
cnt.cnt++
val ret = if (inProcess)
config.checkInProcess(xcfa, SmtLibSolverManager.HOME.toAbsolutePath().toString(), false, "dekker.i",
ConsoleLogger(Logger.Level.INFO), parseContext, false)()
else config.check(xcfa, ConsoleLogger(Logger.Level.INFO))
cnt.cnt--
ret
},
inProcess = true
)

val config2 = ConfigNode(
name = "config2",
config = XcfaCegarConfig(maxEnum = 1),
check = { inProcess, config ->
cnt.cnt++
val ret = if (inProcess)
config.checkInProcess(xcfa, SmtLibSolverManager.HOME.toAbsolutePath().toString(), false, "dekker.i",
ConsoleLogger(Logger.Level.INFO), parseContext, false)()
else config.check(xcfa, ConsoleLogger(Logger.Level.INFO))
cnt.cnt--
ret
},
inProcess = true
)

val parallelConfig = OrthogonalNode("config", STM(config1, setOf()), STM(config2, setOf()))

val stm = STM(initNode = parallelConfig, edges = setOf())
val result = try {
stm.execute().second
} catch (e: Throwable) {
e
}

Assertions.assertEquals(0, cnt.cnt) { "Still running ${cnt.cnt} instances." }
Assertions.assertTrue(result is SafetyResult<*, *> && result.isSafe()) { " $result is not a SafetyResult.safe " }
}


}

0 comments on commit 45a154f

Please sign in to comment.