diff --git a/build.gradle b/build.gradle index 2e67c5e..a02bb51 100644 --- a/build.gradle +++ b/build.gradle @@ -1,6 +1,6 @@ //initialize Kotlin build plugin buildscript { - ext.kotlin_version = '1.1.0' + ext.kotlin_version = '1.1.1' repositories { jcenter() @@ -18,8 +18,8 @@ apply plugin: 'kotlin' apply plugin: 'application' group = "com.github.sybila" -mainClassName = "com.github.sybila.ComponentsKt" -version = '0.3.1' +mainClassName = "com.github.sybila.MainKt" +version = '0.4.0' // In this section you declare where to find the dependencies of your project diff --git a/src/main/java/com/github/sybila/Components.kt b/src/main/java/com/github/sybila/Components.kt index cc92173..6cce918 100644 --- a/src/main/java/com/github/sybila/Components.kt +++ b/src/main/java/com/github/sybila/Components.kt @@ -1,24 +1,16 @@ package com.github.sybila import com.github.sybila.checker.Channel -import com.github.sybila.checker.CheckerStats import com.github.sybila.checker.Operator import com.github.sybila.checker.StateMap import com.github.sybila.checker.channel.SingletonChannel import com.github.sybila.checker.map.RangeStateMap -import com.github.sybila.checker.map.SingletonStateMap import com.github.sybila.checker.operator.* import com.github.sybila.checker.partition.asSingletonPartition -import com.github.sybila.checker.solver.SolverStats import com.github.sybila.huctl.DirectionFormula import com.github.sybila.ode.generator.rect.Rectangle import com.github.sybila.ode.generator.rect.RectangleOdeModel -import com.github.sybila.ode.model.Parser -import com.github.sybila.ode.model.computeApproximation -import org.kohsuke.args4j.CmdLineException -import org.kohsuke.args4j.CmdLineParser -import org.kohsuke.args4j.Option -import java.io.File +import com.github.sybila.ode.model.OdeModel import java.io.PrintStream import java.util.* import java.util.concurrent.Executors @@ -71,10 +63,43 @@ fun Channel.isResultEmpty(op: Operator) = op.compute().entries(). // ----------------------- MAIN ALGORITHM ------------------------------------- -class Algorithm( +class LocalAlgorithm( parallelism: Int, private val useHeuristics: Boolean -) { +) : Algorithm { + + override fun compute(model: OdeModel, config: Config, logStream: PrintStream?): Count { + val transitionSystem = SingletonChannel(RectangleOdeModel(model, + createSelfLoops = !config.disableSelfLoops + ).asSingletonPartition()) + + transitionSystem.run { + + // transition system is not synchronized, however, it is read-safe. + // hence if we pre-compute all transitions before actually starting the algorithm, + // we can safely perform operations in parallel. + (0 until stateCount).forEach { + it.predecessors(true) + it.predecessors(false) + it.successors(true) + it.successors(false) + } + + logStream?.println("Transition system computed. Starting component search...") + + // counter is synchronized + val counter = Count(this) + + // compute results + val allStates = TrueOperator(this) + startAction(allStates, counter) + + blockWhilePending() + executor.shutdown() + + return counter + } + } val executor = Executors.newFixedThreadPool(parallelism)!! //private val executor = Executors.newFixedThreadPool(2) @@ -183,163 +208,4 @@ class Algorithm( fun chooseSimple(op: Operator): Pair = op.compute().entries().next() -} -// ---------------------- PLUMBING TO PUT IT ALL TOGETHER ------------------------ - -internal fun String.readStream(): PrintStream? = when (this) { - "null" -> null - "stdout" -> System.out - "stderr" -> System.err - else -> PrintStream(File(this).apply { this.createNewFile() }.outputStream()) -} - -enum class ResultType { HUMAN, JSON } - -data class Config( - @field:Option( - name = "-h", aliases = arrayOf("--help"), help = true, - usage = "Print help message" - ) - var help: Boolean = false, - @field:Option( - name = "-m", aliases = arrayOf("--model"), required = true, - usage = "Path to the .bio file from which the model should be loaded." - ) - var model: File? = null, - @field:Option( - name = "-ro", aliases = arrayOf("--result-output"), - usage = "Name of stream to which the results should be printed. Filename, stdout, stderr or null." - ) - var resultOutput: String = "stdout", - @field:Option( - name = "-lo", aliases = arrayOf("--log-output"), - usage = "Name of stream to which logging info should be printed. Filename, stdout, stderr or null." - ) - var logOutput: String = "stdout", - @field:Option( - name = "--fast-approximation", - usage = "Use faster, but less precise version of linear approximation." - ) - var fastApproximation: Boolean = false, - @field:Option( - name = "--cut-to-range", - usage = "Thresholds above and below original variable range will be discarded." - ) - var cutToRange: Boolean = false, - @field:Option( - name = "--disable-self-loops", - usage = "Disable selfloop creation in transition system." - ) - var disableSelfLoops: Boolean = false, - @field:Option( - name = "-r", aliases = arrayOf("--result"), - usage = "Type of result format. Accepted values: human, json." - ) - var resultType: ResultType = ResultType.HUMAN, - @field:Option( - name = "--parallelism", - usage = "Recommended number of used threads." - ) - var parallelism: Int = Runtime.getRuntime().availableProcessors(), - @field:Option( - name = "--disable-heuristic", - usage = "Use to disable the set size state choosing heuristic" - ) - var disableHeuristic: Boolean = false -) - -fun main(args: Array) { - - val config = Config() - val parser = CmdLineParser(config) - - try { - parser.parseArgument(*args) - - if (config.help) { - parser.printUsage(System.err) - System.err.println() - return - } - - val logStream: PrintStream? = config.logOutput.readStream() - - logStream?.println("Loading model and computing approximation...") - - val modelFile = config.model ?: throw IllegalArgumentException("Missing model file.") - - val odeModel = Parser().parse(modelFile).computeApproximation( - fast = config.fastApproximation, cutToRange = config.cutToRange - ) - - logStream?.println("Configuration loaded. Computing transition system") - - val transitionSystem = SingletonChannel(RectangleOdeModel(odeModel, - createSelfLoops = !config.disableSelfLoops - ).asSingletonPartition()) - - // reset statistics - - SolverStats.reset(logStream) - CheckerStats.reset(logStream) - - // enter transition system context - Algorithm(config.parallelism, !config.disableHeuristic).run { - transitionSystem.run { - - // transition system is not synchronized, however, it is read-safe. - // hence if we pre-compute all transitions before actually starting the algorithm, - // we can safely perform operations in parallel. - (0 until stateCount).forEach { - it.predecessors(true) - it.predecessors(false) - it.successors(true) - it.successors(false) - } - - logStream?.println("Transition system computed. Starting component search...") - - // counter is synchronized - val counter = Count(this) - - // compute results - val allStates = TrueOperator(this) - startAction(allStates, counter) - - blockWhilePending() - executor.shutdown() - - logStream?.println("Component search done.") - logStream?.println("Max number of components: ${counter.max}.") - logStream?.println("Min number of components: ${counter.min}.") - - config.resultOutput.readStream()?.use { outStream -> - if (config.resultType == ResultType.HUMAN) { - for (i in 0 until counter.size) { // print countTSCC for each parameter set - outStream.println("${i + 1} terminal components: ${counter[i].map { it.asIntervals() }}") - } - } else { - val result: MutableMap>>> = HashMap() - for (i in 0 until counter.size) { - result["${i + 1}_terminal_components"] = listOf(SingletonStateMap(0, counter[i], ff)) - } - - outStream.println(printJsonRectResults(odeModel, result)) - } - } - } - } - - } catch (e : CmdLineException) { - // if there's a problem in the command line, - // you'll get this exception. this will report - // an error message. - System.err.println(e.message) - System.err.println("pithya [options...]") - // print the list of available options (with fresh defaults) - CmdLineParser(Config()).printUsage(System.err) - System.err.println() - - return - } } \ No newline at end of file diff --git a/src/main/java/com/github/sybila/DistComponents.kt b/src/main/java/com/github/sybila/DistComponents.kt new file mode 100644 index 0000000..5be4f92 --- /dev/null +++ b/src/main/java/com/github/sybila/DistComponents.kt @@ -0,0 +1,158 @@ +package com.github.sybila + +import com.github.sybila.checker.* +import com.github.sybila.checker.channel.connectWithSharedMemory +import com.github.sybila.checker.map.RangeStateMap +import com.github.sybila.checker.partition.asUniformPartitions +import com.github.sybila.ode.generator.rect.RectangleOdeModel +import com.github.sybila.ode.model.OdeModel +import java.io.PrintStream +import java.util.* +import java.util.concurrent.Executors +import java.util.concurrent.Future + +fun Params.weight() = this.fold(0.0) { acc, rect -> + acc + rect.asIntervals().map { Math.abs(it[1] - it[0]) }.fold(1.0) { acc, dim -> acc * dim } +} + +fun StateMap.asOp(): Operator = ExplicitOperator(this) + +inline fun List.flatRun(action: T.() -> R): List = this.map { it.run(action) } +inline fun List.zipRun(context: List, action: V.(T) -> R): List + = this.zip(context).map { it.second.run { action(it.first) } } + +class DistAlgorithm( + private val parallelism: Int +) : Algorithm { + + override fun compute(model: OdeModel, config: Config, logStream: PrintStream?): Count { + + val transitionSystem = RectangleOdeModel(model) + + transitionSystem.run { + + // transition system is not synchronized, however, it is read-safe. + // hence if we pre-compute all transitions before actually starting the algorithm, + // we can safely perform operations in parallel. + (0 until stateCount).forEach { + it.predecessors(true) + it.predecessors(false) + it.successors(true) + it.successors(false) + } + + val channels = (0 until parallelism).map { this }.asUniformPartitions().connectWithSharedMemory() + + val fullStateSpace = (0 until stateCount).asStateMap(tt) + + val initialSpace = channels.flatRun { fullStateSpace.restrictToPartition() } + + val counter = Count(this) + + paramRecursionTSCC(channels, initialSpace, counter) + executor.shutdown() + + return counter + } + + } + + val executor = Executors.newFixedThreadPool(parallelism)!! + + fun Model.paramRecursionTSCC(channels: List>, states: List>, counter: Count) { + var universe = states + + fun List>.isStrongEmpty() = this.zip(channels).map { (map, solver) -> + executor.submit { + solver.run { + map.entries().asSequence().all { it.second.isNotSat() } + } + } + }.all { it.get() } + + fun List>.compute(): List> = this.map { op -> + executor.submit> { + op.compute() + } + }.map { it.get() } + + fun List>.choose() = this.map { map -> + executor.submit> { + var max: Pair? = null + var maxWeight: Double = 0.0 + map.entries().forEach { (state, p) -> + val weight = p.weight() + if (weight > maxWeight) { + max = state to p + maxWeight = weight + } + } + max + } + }.fold?>, Pair?>(null) { current, future -> + val new = future.get() + current?.assuming { it.second.weight() > new?.second?.weight() ?: 0.0 } ?: new + }!! + + //println("Start recursion: ${universe.isStrongEmpty()}") + + while (!universe.isStrongEmpty()) { + + //println("Iteration") + + val (v, vParams) = universe.choose() + + val limits = channels.flatRun { + RangeStateMap(0 until stateCount, value = vParams, default = ff).restrictToPartition().asOp() + } + + val vOp = channels.flatRun { v.asStateMap(vParams).restrictToPartition().asOp() } + + val F = universe.zip(vOp).zipRun(channels) { (universe, vOp) -> + And(universe.asOp(), FWD(vOp)) + } + + val B = F.zip(vOp).zipRun(channels) { (F, vOp) -> + And(F, BWD(vOp)) + } + + val F_minus_B = F.zip(B).zipRun(channels) { (F, B) -> + And(F, Not(B)) + } + + F_minus_B.compute().assuming { !it.isStrongEmpty() }?.let { + paramRecursionTSCC(channels, it, counter) + } + + val BB = universe.zip(F).zipRun(channels) { (universe, F) -> + And(universe.asOp(), BWD(F)) + } + + val V_minus_BB = universe.zip(limits).zip(BB).zipRun(channels) { (pair, BB) -> + val (uni, limit) = pair + And(And(uni.asOp(), limit), Not(BB)) + } + + val V_minus_BB_result = V_minus_BB.compute() + + //println("V/BB: $V_minus_BB_result") + + val componentParams = V_minus_BB_result.asSequence().flatMap { it.entries().asSequence() } + .fold, Params>(HashSet()) { acc, (_, params) -> + acc or params + } + + if (componentParams.isSat()) { + counter.push(componentParams) + paramRecursionTSCC(channels, V_minus_BB_result, counter) + } + + universe = universe.zip(limits).zipRun(channels) { (universe, limit) -> + And(universe.asOp(), Not(limit)) + }.compute() + + } + + } + +} \ No newline at end of file diff --git a/src/main/java/com/github/sybila/Main.kt b/src/main/java/com/github/sybila/Main.kt new file mode 100644 index 0000000..9044512 --- /dev/null +++ b/src/main/java/com/github/sybila/Main.kt @@ -0,0 +1,164 @@ +package com.github.sybila + +import com.github.sybila.checker.CheckerStats +import com.github.sybila.checker.StateMap +import com.github.sybila.checker.map.SingletonStateMap +import com.github.sybila.checker.solver.SolverStats +import com.github.sybila.ode.generator.rect.Rectangle +import com.github.sybila.ode.model.OdeModel +import com.github.sybila.ode.model.Parser +import com.github.sybila.ode.model.computeApproximation +import org.kohsuke.args4j.CmdLineException +import org.kohsuke.args4j.CmdLineParser +import org.kohsuke.args4j.Option +import java.io.File +import java.io.PrintStream +import java.util.* + +typealias Params = MutableSet + +interface Algorithm { + fun compute(model: OdeModel, config: Config, logStream: PrintStream?): Count +} + +// ---------------------- PLUMBING TO PUT IT ALL TOGETHER ------------------------ + +internal fun String.readStream(): PrintStream? = when (this) { + "null" -> null + "stdout" -> System.out + "stderr" -> System.err + else -> PrintStream(File(this).apply { this.createNewFile() }.outputStream()) +} + +enum class ResultType { HUMAN, JSON } +enum class AlgorithmType { LOCAL, DIST } + +data class Config( + @field:Option( + name = "-h", aliases = arrayOf("--help"), help = true, + usage = "Print help message" + ) + var help: Boolean = false, + @field:Option( + name = "-m", aliases = arrayOf("--model"), required = true, + usage = "Path to the .bio file from which the model should be loaded." + ) + var model: File? = null, + @field:Option( + name = "-ro", aliases = arrayOf("--result-output"), + usage = "Name of stream to which the results should be printed. Filename, stdout, stderr or null." + ) + var resultOutput: String = "stdout", + @field:Option( + name = "-lo", aliases = arrayOf("--log-output"), + usage = "Name of stream to which logging info should be printed. Filename, stdout, stderr or null." + ) + var logOutput: String = "stdout", + @field:Option( + name = "--fast-approximation", + usage = "Use faster, but less precise version of linear approximation." + ) + var fastApproximation: Boolean = false, + @field:Option( + name = "--cut-to-range", + usage = "Thresholds above and below original variable range will be discarded." + ) + var cutToRange: Boolean = false, + @field:Option( + name = "--disable-self-loops", + usage = "Disable selfloop creation in transition system." + ) + var disableSelfLoops: Boolean = false, + @field:Option( + name = "-r", aliases = arrayOf("--result"), + usage = "Type of result format. Accepted values: human, json." + ) + var resultType: ResultType = ResultType.HUMAN, + @field:Option( + name = "--parallelism", + usage = "Recommended number of used threads." + ) + var parallelism: Int = Runtime.getRuntime().availableProcessors(), + @field:Option( + name = "--disable-heuristic", + usage = "Use to disable the set size state choosing heuristic" + ) + var disableHeuristic: Boolean = false, + @field:Option( + name = "--algorithm-type", + usage = "Specify the type of the algorithm." + ) + var algorithm: AlgorithmType = AlgorithmType.LOCAL +) + +fun main(args: Array) { + + val config = Config() + val parser = CmdLineParser(config) + + try { + parser.parseArgument(*args) + + if (config.help) { + parser.printUsage(System.err) + System.err.println() + return + } + + val logStream: PrintStream? = config.logOutput.readStream() + + logStream?.println("Loading model and computing approximation...") + + val modelFile = config.model ?: throw IllegalArgumentException("Missing model file.") + + val odeModel = Parser().parse(modelFile).computeApproximation( + fast = config.fastApproximation, cutToRange = config.cutToRange + ) + + logStream?.println("Configuration loaded. Computing transition system") + + // reset statistics + + SolverStats.reset(logStream) + CheckerStats.reset(logStream) + + + val algorithm = if (config.algorithm == AlgorithmType.LOCAL) + LocalAlgorithm(config.parallelism, !config.disableHeuristic) + else + DistAlgorithm(config.parallelism) + + val counter = algorithm.compute(odeModel, config, logStream) + + logStream?.println("Component search done.") + logStream?.println("Max number of components: ${counter.max}.") + logStream?.println("Min number of components: ${counter.min}.") + + config.resultOutput.readStream()?.use { outStream -> + if (config.resultType == ResultType.HUMAN) { + for (i in 0 until counter.size) { // print countTSCC for each parameter set + outStream.println("${i + 1} terminal components: ${counter[i].map { it.asIntervals() }}") + } + } else { + val result: MutableMap>>> = HashMap() + for (i in 0 until counter.size) { + result["${i + 1}_terminal_components"] = listOf(SingletonStateMap(0, counter[i], counter[i])) + } + + outStream.println(printJsonRectResults(odeModel, result)) + } + } + + } catch (e : CmdLineException) { + // if there's a problem in the command line, + // you'll get this exception. this will report + // an error message. + System.err.println(e.message) + System.err.println("terminal-components [options...]") + // print the list of available options (with fresh defaults) + CmdLineParser(Config()).printUsage(System.err) + System.err.println() + + return + } +} \ No newline at end of file