use tarjan algorithm for explicit evaluation

build.gradle

@@ -19,7 +19,7 @@ apply plugin: 'application'
 
 group = "com.github.sybila"
 mainClassName = "com.github.sybila.ExplicitKt"
-version = '0.5.0-alpha1'
+version = '0.5.0-tarjan'
 
 
 // In this section you declare where to find the dependencies of your project

src/main/java/com/github/sybila/Explicit.kt

@@ -1,16 +1,13 @@
 package com.github.sybila
 
-import com.github.sybila.checker.channel.SingletonChannel
-import com.github.sybila.checker.operator.TrueOperator
-import com.github.sybila.checker.partition.asSingletonPartition
 import com.github.sybila.ode.generator.NodeEncoder
 import com.github.sybila.ode.generator.bool.BoolOdeModel
+import com.github.sybila.ode.generator.rect.RectangleOdeModel
 import com.github.sybila.ode.model.OdeModel
 import com.github.sybila.ode.model.Parser
 import com.github.sybila.ode.model.computeApproximation
 import java.io.File
 import java.util.*
-import kotlin.system.measureTimeMillis
 
 fun OdeModel.forEachParameter(action: (OdeModel) -> Unit) {
 
@@ -65,6 +62,7 @@ fun OdeModel.forEachParameter(action: (OdeModel) -> Unit) {
         if (model.parameters.isEmpty()) action(model)
         else {
             for (value in valuations.last()) {
+                if (value == 0.0) continue
                 substitute(
                         model.substituteLastParameter(value),
                         valuations.dropLast(1), action
@@ -93,28 +91,30 @@ fun OdeModel.substituteLastParameter(value: Double): OdeModel = this.copy(
 fun main(args: Array<String>) {
     val modelFile = File(args[0])
 
-    val odeModel = Parser().parse(modelFile).computeApproximation(fast = true, cutToRange = false)
+    val odeModel = Parser().parse(modelFile).computeApproximation(fast = false, cutToRange = false)
 
-    Algorithm(8, false).run {
-        var count = 0
-        val time = measureTimeMillis {
-            odeModel.forEachParameter { model ->
-                val transitionSystem = SingletonChannel(BoolOdeModel(model).asSingletonPartition())
-                transitionSystem.run {
-                    // counter is synchronized
-                    val counter = Count(this)
+    val f = RectangleOdeModel(odeModel)
 
-                    // compute results
-                    val allStates = TrueOperator(this)
-                    startAction(allStates, counter)
+    val states = Array<List<Int>>(f.stateCount) { emptyList() }
 
-                    //blockWhilePending()
+    val tarjan = Tarjan()
 
-                    count = Math.max(counter.size, count)
-                }
+    var max = 0
+
+    odeModel.forEachParameter { model ->
+        BoolOdeModel(model).run {
+            // create state space
+            for (s in 0 until stateCount) {
+                states[s] = s.successors(true).asSequence().map { it.target }.toList()
+            }
+
+            val result = tarjan.getSCComponents(states)
+            if (result in (max + 1)..9) {
+                max = result
             }
         }
-        println("Count: $count in $time")
-        executor.shutdown()
     }
+
+    println("Done")
+    //println("Found max $max components")
 }

src/main/java/com/github/sybila/Tarjan.java

@@ -0,0 +1,75 @@
+package com.github.sybila;
+
+/**
+ *     Java Program to Implement Tarjan Algorithm
+ **/
+
+import java.util.*;
+
+/** class Tarjan **/
+class Tarjan
+{
+    /** number of vertices **/
+    private int V;
+    /** preorder number counter **/
+    private int preCount;
+    /** low number of v **/
+    private int[] low;
+    /** to check if v is visited **/
+    private boolean[] visited;
+    /** to store given graph **/
+    private List<Integer>[] graph;
+    /** to store all scc **/
+    private int sccComp;
+    private Stack<Integer> stack = new Stack<>();
+
+    /** function to get all strongly connected components **/
+    public int getSCComponents(List<Integer>[] graph)
+    {
+        V = graph.length;
+        this.graph = graph;
+        low = new int[V];
+        visited = new boolean[V];
+        stack.clear();
+        //stack = new Stack<>();
+        sccComp = 0;
+
+        for (int v = 0; v < V; v++)
+            if (!visited[v])
+                dfs(v);
+
+        return sccComp;
+    }
+
+    /** function dfs **/
+    private void dfs(int v)
+    {
+        low[v] = preCount++;
+        visited[v] = true;
+        stack.push(v);
+        int min = low[v];
+        for (int w : graph[v])
+        {
+            if (!visited[w])
+                dfs(w);
+            if (low[w] < min)
+                min = low[w];
+        }
+        if (min < low[v])
+        {
+            low[v] = min;
+            return;
+        }
+        //List<Integer> component = new ArrayList<>();
+        int w;
+        do
+        {
+            w = stack.pop();
+            //component.add(w);
+            low[w] = V;
+        } while (w != v);
+        sccComp += 1;
+        //sccComp.add(component);
+    }
+
+}