From 241ed5f43a6bb2752b6063851c775634b2e1acb1 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 13 Feb 2024 10:30:30 +0100 Subject: [PATCH] Added RandomXsts and XstsSerializer --- .../hu/bme/mit/theta/xsts/cli/RandomXsts.kt | 370 ++++++++++++++++++ .../bme/mit/theta/xsts/cli/XstsSerializer.kt | 87 ++++ 2 files changed, 457 insertions(+) create mode 100644 subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/RandomXsts.kt create mode 100644 subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsSerializer.kt diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/RandomXsts.kt b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/RandomXsts.kt new file mode 100644 index 0000000000..514e94dd87 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/RandomXsts.kt @@ -0,0 +1,370 @@ +package hu.bme.mit.theta.xsts + +import XstsSerializer +import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.inttype.IntExprs +import hu.bme.mit.theta.core.type.inttype.IntType +import hu.bme.mit.theta.core.utils.ExprUtils +import kotlin.random.Random + +fun main() { + val writtenVars = object : StmtVisitor>, Set>> { + override fun visit(stmt: SkipStmt?, param: Set>): Set> { + return param + } + + override fun visit(stmt: AssumeStmt?, param: Set>): Set> { + return param + } + + override fun visit(stmt: AssignStmt, param: Set>): Set> { + return setOf(stmt.varDecl) + param + } + + override fun visit(stmt: HavocStmt, param: Set>): Set> { + return setOf(stmt.varDecl) + param + } + + override fun visit(stmt: SequenceStmt, param: Set>): Set> { + var res = param + for (s in stmt.stmts) { + res = s.accept(this, setOf()) + } + return res + } + + override fun visit(stmt: NonDetStmt, param: Set>): Set> { + var res = param + for (s in stmt.stmts) { + res = s.accept(this, setOf()) + } + return res + } + + override fun visit(stmt: OrtStmt?, param: Set>?): Set> { + TODO("Not yet implemented") + } + + override fun visit(stmt: LoopStmt, param: Set>): Set> { + return stmt.stmt.accept(this, param) + } + + override fun visit(stmt: IfStmt, param: Set>): Set> { + return stmt.then.accept(this, stmt.elze.accept(this, param)) + } + + } + + val numCtrl = 2 + val numOther = 3 + val numClock = 2 + val all = numCtrl + numOther + numClock + val xsts = RandomXsts(100, 3).generateRandomXsts(12, numCtrl, numClock, numOther) { + val decls = it.tran.accept(writtenVars, setOf()) + decls.size == all // all vars are written + } + var orig = XstsSerializer.serializeXsts(xsts) + orig = orig.replace(Regex("var clock([0-9]+) : integer")) {"var clock${it.groupValues[1]} : clock"} + orig = orig.replace(Regex("havoc clock([0-9]+)"), "__delay") + println(orig) + println("prop { ${XstsSerializer.serializeExpr(xsts.prop)} }") +} + +fun generateXsts(seed: Int): XSTS { + val writtenVars = object : StmtVisitor>, Set>> { + override fun visit(stmt: SkipStmt?, param: Set>): Set> { + return param + } + + override fun visit(stmt: AssumeStmt?, param: Set>): Set> { + return param + } + + override fun visit(stmt: AssignStmt, param: Set>): Set> { + return setOf(stmt.varDecl) + param + } + + override fun visit(stmt: HavocStmt, param: Set>): Set> { + return setOf(stmt.varDecl) + param + } + + override fun visit(stmt: SequenceStmt, param: Set>): Set> { + var res = param + for (s in stmt.stmts) { + res = s.accept(this, setOf()) + } + return res + } + + override fun visit(stmt: NonDetStmt, param: Set>): Set> { + var res = param + for (s in stmt.stmts) { + res = s.accept(this, setOf()) + } + return res + } + + override fun visit(stmt: OrtStmt?, param: Set>?): Set> { + TODO("Not yet implemented") + } + + override fun visit(stmt: LoopStmt, param: Set>): Set> { + return stmt.stmt.accept(this, param) + } + + override fun visit(stmt: IfStmt, param: Set>): Set> { + return stmt.then.accept(this, stmt.elze.accept(this, param)) + } + + } + + val numCtrl = 2 + val numOther = 3 + val numClock = 2 + val all = numCtrl + numOther + numClock + val xsts = RandomXsts(seed, 3).generateRandomXsts(10, 1, 1, 3) { +// val decls = it.tran.accept(writtenVars, setOf()) +// decls.size == all // all vars are written + true + } + return xsts +} + +class RandomXsts(seed: Int, val exprMaxDepth: Int) { + + lateinit var ctrlVars: List> + lateinit var otherVars: List> + lateinit var boolVars: List> + lateinit var clockVars: List> + lateinit var intVars: List> + + val random = Random(seed) + + fun generateRandomXsts( + depth: Int, + numCtrl: Int, + numClock: Int, + numOther: Int, + constraint: (XSTS) -> Boolean + ): XSTS { + var xsts: XSTS + do { + val trans = generateRandomStmt(depth, numCtrl, numClock, numOther) + val env = Stmts.NonDetStmt(listOf(Stmts.Skip())) + val init = Stmts.NonDetStmt(listOf(Stmts.Skip())) + val initExpr = BoolExprs.And( + ctrlVars.map { IntExprs.Eq(it.ref, IntExprs.Int(0)) } + + boolVars.map { BoolExprs.Not(it.ref) } + + intVars.map { IntExprs.Eq(it.ref, IntExprs.Int(0)) } + ) + var expr: Expr + do expr = randomBoolExpr(0) + while (ExprUtils.getVars(expr).isEmpty()) + xsts = XSTS( + mapOf(), + ctrlVars.toSet(), + init, NonDetStmt.of(listOf(trans)), env, initExpr, expr + ) + } while (!(constraint(xsts))) + return xsts + } + + fun generateRandomStmt(depth: Int, numCtrl: Int, numClock: Int, numOther: Int): Stmt { + var i = 2 + ctrlVars = Array(numCtrl) { Decls.Var("ctlr${i++}", IntType.getInstance()) }.toList() + do { + otherVars = listOf( + Decls.Var("var0", IntType.getInstance()) as VarDecl, + Decls.Var("var1", BoolType.getInstance()) as VarDecl, + ) + Array(numOther - 2) { randomVar("var${i++}") }.toList() + } while (otherVars.all { it.type is IntType } || otherVars.all { it.type is BoolType }) + boolVars = otherVars.filter { it.type is BoolType }.map { it as VarDecl } + intVars = otherVars.filter { it.type is IntType }.map { it as VarDecl } + clockVars = Array(numClock) { Decls.Var("clock${i++}", IntType.getInstance()) }.toList() + + return randomIntermediate(0, depth) + } + + fun randomVar(name: String): VarDecl { + return listOf( + {Decls.Var(name, IntType.getInstance()) as VarDecl}, + {Decls.Var(name, BoolType.getInstance()) as VarDecl} + ).random(random)() + } + + fun randomIntermediate(currDepth: Int, maxDepth: Int): Stmt { + if (currDepth == maxDepth) return randomLeaf() + return listOf( + { randomLeaf() }, + { randomSeq(currDepth + 1, maxDepth) }, + { randomNonDet(currDepth + 1, maxDepth) }, + { randomIf(currDepth + 1, maxDepth) }, +// { randomLoop(currDepth + 1, maxDepth) }, + ).random(random)() + } + + fun randomLeaf(): Stmt { + return listOf( +// { Stmts.Skip() }, + { randomAssign() }, + { randomAssign() }, + { randomAssume() }, +// { randomHavoc() }, + ).random(random)() + } + + fun randomSeq(currDepth: Int, maxDepth: Int): Stmt { + return Stmts.SequenceStmt(listOf( + randomIntermediate(currDepth+1, maxDepth), + randomIntermediate(currDepth+1, maxDepth) + )) + } + + fun randomNonDet(currDepth: Int, maxDepth: Int): Stmt { + return Stmts.NonDetStmt(listOf( + randomIntermediate(currDepth+1, maxDepth), + randomIntermediate(currDepth+1, maxDepth) + )) + + } + + fun randomIf(currDepth: Int, maxDepth: Int): Stmt { + var expr: Expr + do expr = randomBoolExpr(0) + while (ExprUtils.getVars(expr).isEmpty()) + return IfStmt.of(expr, + randomIntermediate(currDepth+1, maxDepth), + randomIntermediate(currDepth+1, maxDepth) + ) + } + + fun randomBoolExpr(currDepth: Int): Expr { + return (if(currDepth == exprMaxDepth) + listOf( + { BoolExprs.True() }, + { boolVars[random.nextInt((boolVars.size))].ref }, + ).random(random) + else + listOf( + { BoolExprs.True() }, + { boolVars[random.nextInt((boolVars.size))].ref }, + { BoolExprs.Not(randomBoolExpr(currDepth + 1)) }, + { BoolExprs.And( + randomBoolExpr(currDepth + 1), + randomBoolExpr(currDepth + 1) + ) }, + { BoolExprs.Or( + randomBoolExpr(currDepth + 1), + randomBoolExpr(currDepth + 1)) + }, + { BoolExprs.Imply(randomBoolExpr(currDepth + 1), randomBoolExpr(currDepth + 1)) }, + { BoolExprs.Iff(randomBoolExpr(currDepth + 1), randomBoolExpr(currDepth + 1)) }, + { BoolExprs.Xor(randomBoolExpr(currDepth + 1), randomBoolExpr(currDepth + 1)) }, + { IntExprs.Eq(randomIntExpr(currDepth + 1), randomIntExpr(currDepth + 1)) }, + { IntExprs.Geq(randomIntExpr(currDepth + 1), randomIntExpr(currDepth + 1)) }, + { IntExprs.Leq(randomIntExpr(currDepth + 1), randomIntExpr(currDepth + 1)) }, + { IntExprs.Lt(randomIntExpr(currDepth + 1), randomIntExpr(currDepth + 1)) }, + { IntExprs.Gt(randomIntExpr(currDepth + 1), randomIntExpr(currDepth + 1)) }, + { IntExprs.Neq(randomIntExpr(currDepth + 1), randomIntExpr(currDepth + 1)) }, + ).random(random))() + } + + + fun randomIntExpr(currDepth: Int): Expr { + return (if(currDepth == exprMaxDepth) + listOf( + {IntExprs.Int(random.nextInt(5))}, + {intVars[random.nextInt((intVars.size))].ref}, + ).random(random) + else + listOf( + {IntExprs.Int(random.nextInt(5))}, + {intVars[random.nextInt((intVars.size))].ref}, + {IntExprs.Neg(randomIntExpr(currDepth+1))}, + {IntExprs.Add(randomIntExpr(currDepth+1), randomIntExpr(currDepth+1))}, + { + IntExprs.Mul(randomIntExpr(currDepth+1), + randomIntExpr(currDepth+1)) + }, + {IntExprs.Sub(randomIntExpr(currDepth+1), randomIntExpr(currDepth+1))}, + ).random(random))() + } + + fun randomLoop(currDepth: Int, maxDepth: Int): Stmt { + return LoopStmt.of(randomIntermediate(currDepth+1, maxDepth), ctrlVars.random(random), + IntExprs.Int(0), + randomIntExpr(0) { ctrlVars.containsAll(ExprUtils.getVars(it)) } + ) + } + + fun randomAssign(): Stmt { + return (listOf({ + val v = otherVars.random(random) + when (v.type) { + is IntType -> Stmts.Assign(v as VarDecl, randomIntExpr { ExprUtils.getVars(it).size > 0 && it != v.ref}) + is BoolType -> Stmts.Assign(v as VarDecl, randomBoolExpr { ExprUtils.getVars(it).size > 0 && it != v.ref}) + else -> throw Exception() + } + }, + { Stmts.Assign(ctrlVars.random(random), randomIntExpr(0)) }, + )+(if (clockVars.isEmpty()) listOf() else listOf({ randomClockReset() }))).random(random)() + } + + fun randomIntExpr(currDepth: Int = 0, constraint: (Expr) -> Boolean): Expr { + var res: Expr + do {res = randomIntExpr(currDepth)} while (!(constraint(res))) + return res + } + + fun randomBoolExpr(currDepth: Int=0, constraint: (Expr) -> Boolean): Expr { + var res: Expr + do {res = randomBoolExpr(currDepth)} while (!(constraint(res))) + return res + } + + fun randomAssume() = (listOf(this::randomDataAssume) + (if (clockVars.isEmpty()) listOf() else listOf(this::randomClockConstraint))).random(random)() + + fun randomDataAssume(): Stmt { + var expr: Expr + do expr = randomBoolExpr(0) + while (ExprUtils.getVars(expr).isEmpty()) + + return Stmts.Assume(expr) + } + + fun randomClockReset(): Stmt { + val c = clockVars.random(random) + val resetTo = IntExprs.Int(random.nextInt(4)) + return Stmts.Assign(c, resetTo) + } + + fun randomClockConstraint(): Stmt { + val c = if(clockVars.size == 1) clockVars[0].ref else listOf( + { clockVars.random(random).ref }, + { + val c1 = clockVars.random(random) + val c2 = (clockVars - listOf(c1)).random() + IntExprs.Sub(c1.ref, c2.ref) + } + ).random()() + + val compareTo = IntExprs.Int(random.nextInt(10)) + return Stmts.Assume(listOf( + {IntExprs.Leq(c, compareTo)}, + {IntExprs.Lt(c, compareTo)}, + {IntExprs.Geq(c, compareTo)}, + {IntExprs.Gt(c, compareTo)}, + {IntExprs.Eq(c, compareTo)}, + ).random(random)()) + } + + fun randomHavoc(): Stmt { + return Stmts.Havoc((otherVars+clockVars).random(random)) + } +} \ No newline at end of file diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsSerializer.kt b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsSerializer.kt new file mode 100644 index 0000000000..7029d5a654 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsSerializer.kt @@ -0,0 +1,87 @@ +import hu.bme.mit.theta.core.dsl.impl.ExprWriter +import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.inttype.IntType +import hu.bme.mit.theta.xsts.XSTS + +object XstsSerializer: StmtVisitor { + + val typeNames = mapOf( + BoolType.getInstance() to "boolean", + IntType.getInstance() to "integer" + ).withDefault { it.toString() } + + fun serializeXsts(xsts: XSTS): String { + val builder = StringBuilder() + for (ctrlVar in xsts.ctrlVars) { + builder.appendLine("ctrl var ${ctrlVar.name} : integer") + } + for (v in xsts.vars - xsts.ctrlVars) { + builder.appendLine("var ${v.name} : ${typeNames[v.type]}") + } + builder.appendLine() + + builder.appendLine("init {\n assume (${serializeExpr(xsts.initFormula)});\n${xsts.init.accept(this, null)}\n}") + builder.appendLine("trans {\n${xsts.tran.accept(this, null)}\n}") + builder.appendLine("env {\n${xsts.env.accept(this, null)}\n}") + + return builder.toString() + } + + fun serializeExpr(expr: Expr<*>): String{ + return ExprWriter.instance().write(expr) + } + + override fun visit(stmt: SkipStmt?, param: Void?): String { + return "" + } + + override fun visit(stmt: AssumeStmt, param: Void?): String { + return "assume (${serializeExpr(stmt.cond)});" + } + + override fun visit(stmt: AssignStmt, param: Void?): String { + return "${stmt.varDecl.name} := (${serializeExpr(stmt.expr)});" + } + + override fun visit(stmt: HavocStmt, param: Void?): String { + return "havoc ${stmt.varDecl.name};" + } + + override fun visit(stmt: SequenceStmt, param: Void?): String { + return stmt.stmts.joinToString("\n") { "${it.accept(this, null)}" } + } + + override fun visit(stmt: NonDetStmt, param: Void?): String { + return "choice ${stmt.stmts.joinToString(" or ") { "{\n${it.accept(this, null)}\n}"}}" + } + + override fun visit(stmt: OrtStmt?, param: Void?): String { + TODO("Not yet implemented") + } + + override fun visit(stmt: LoopStmt, param: Void?): String { + /* + for i from 1 to y+1 do { + x:=x-1; + } + */ + return """ + for ${stmt.loopVariable.name} from (${serializeExpr(stmt.from)}) to (${serializeExpr(stmt.to)}) do { + ${stmt.stmt.accept(this, null)} + }""".trimIndent() + } + + override fun visit(stmt: IfStmt, param: Void?): String { + return """ + if (${serializeExpr(stmt.cond)}) { + ${stmt.then.accept(this, null)} + } else { + ${stmt.elze.accept(this, null)} + } + """.trimIndent() + } + +}