Skip to content

Commit

Permalink
add distributed algorithm variant
Browse files Browse the repository at this point in the history
  • Loading branch information
@daemontus
daemontus committed Mar 24, 2017
1 parent fd94944 commit e3c04a9
Show file tree
Hide file tree
Showing 4 changed files with 361 additions and 173 deletions.
6 changes: 3 additions & 3 deletions build.gradle
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//initialize Kotlin build plugin
buildscript {
ext.kotlin_version = '1.1.0'
ext.kotlin_version = '1.1.1'

repositories {
jcenter()
Expand All @@ -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
Expand Down
206 changes: 36 additions & 170 deletions src/main/java/com/github/sybila/Components.kt
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -71,10 +63,43 @@ fun <T: Any> Channel<T>.isResultEmpty(op: Operator<T>) = 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<Params> {
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)
Expand Down Expand Up @@ -183,163 +208,4 @@ class Algorithm(

fun <T: Any> chooseSimple(op: Operator<T>): Pair<Int, T> = 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<String>) {

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<String, List<StateMap<Set<Rectangle>>>> = 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
}
}
Loading

0 comments on commit e3c04a9

Please sign in to comment.