IterativeRefinementC.scala 938 Bytes
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
package de.bbisping.coupledsim.algo

import de.bbisping.coupledsim.ts.TransitionSystem
import de.bbisping.coupledsim.util.Coloring
import de.bbisping.coupledsim.util.FixedPoint

/**
 * Iterative Refinement Skeleton roughly following 
 * "Computing maximal weak and other bisimulations" [BGR 2016]
 */
trait IterativeRefinementC[S, A, L] {
  
  val ts: TransitionSystem[S, A, L]
  
  def initialApproximation: Coloring[S]
  
  def computeAfters(part: Coloring[S]): Map[S, Set[(Coloring.Color, Coloring.Color)]]
  
  def refine(part: Coloring[S], coloredAfters: Map[S, Set[(Coloring.Color, Coloring.Color)]])(implicit cmp: Ordering[S]): Coloring[S]
  
  def compute()(implicit cmp: Ordering[S]) = {

    FixedPoint[Coloring[S]] (
      (p => {
        //println("pa: " + p.toPartition())
        val cs = computeAfters(p)
        //println("cs: " + cs)
        refine(p, cs)
      }),
      _ == _
    ) (initialApproximation)
    
  }
  
}