This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

TauLoopCompression.scala 1.72 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
package de.bbisping.coupledsim.algo.transform

import de.bbisping.coupledsim.ts.TransitionSystem
import de.bbisping.coupledsim.util.LabeledRelation
import de.bbisping.coupledsim.ts.WeakTransitionSystem
import scala.collection.mutable.HashMap
import scala.collection.mutable.HashSet
import de.bbisping.coupledsim.util.Coloring

/** tau-loop-compression
 *  
 *  nodes on a tau loop are considered equal by many weak similarities.
 *  we use Tarjans [Tar72] algorithm for strongly connected components to find
 *  tau-looped components.
 *  (along the lines of the algorithm from https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm)
 *  
 *  */
class TauLoopCompression[S, A, L] (
    ts: WeakTransitionSystem[S, A, L]
  ) {
  
  def compute() = {
    val coloring = computeColoring()
    new BuildQuotientSystem(ts, coloring).build()
  }
  
  def computeColoring() = {
    
    var currentIndex = 0
    var stack = List[S]()
    val index = new HashMap[S, Int]()
    val rep = new HashMap[S, Int]()
    val onStack = new HashSet[S]()
    
    def colorComponents(s: S) {
      index(s) = currentIndex
      rep(s) = currentIndex
      stack = s::stack
      onStack += s
      currentIndex += 1
      
      for (t <- ts.silentSteps.values(s)) {
        if (!index.contains(t)) {
          colorComponents(t)
          rep(s) = Math.min(rep(s), rep(t))
        } else if (onStack(t)) {
          rep(s) = Math.min(rep(s), index(t))
        }
      }
      
      if (rep(s) == index(s)) {
        stack = stack.dropWhile { t =>
          onStack -= t
          t != s
        }
      }
    }
    
    for {
      s <- ts.nodes
      if !index.contains(s)
    } {
      colorComponents(s)
    }
    
    Coloring(rep.toMap)
  }
  
}