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 📥

NaiveStrongBisimC.scala 1.39 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
package de.bbisping.coupledsim.algo

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

/**
 * Implementation of Naive Iterative Refinement from [BGR 2016]
 * 
 * */

class NaiveStrongBisimC[S, A, L] (
    override val ts: TransitionSystem[S, A, L])
  extends IterativeRefinementC[S, A, L] {
  
  val labelColors = {
    val parts = for {
      (_, s) <- ts.nodesByLabel
    } yield s
    Coloring.fromPartition(parts.toSet)
  }
  
  val actionColors =
    Coloring.fromPartition(ts.actions.map(Set(_)).toSet)
  
  override def initialApproximation: Coloring[S] = {
    // first step approximation for node-labeled transition systems
    labelColors
  }
  
  override def computeAfters(part: Coloring[S]): Map[S, Set[(Coloring.Color, Coloring.Color)]] = {
    val aft = for {
      (n, a, m) <- ts.step.tupleSet
      //TODO: see whether labelColors should also be included
    } yield (n, (actionColors(a), part(m)))
    aft.groupBy(_._1).mapValues(_.map(_._2))
    
    // [DPP2004, Section 7] proves (?) that the node labeling should only matter in the initializing phase.
    // --> so why do I seem to need it here?!
  }
  
  override def refine(part: Coloring[S], coloredAfters: Map[S, Set[(Coloring.Color, Coloring.Color)]])(implicit cmp: Ordering[S]): Coloring[S] = {
    (part.splitInsertColors(coloredAfters)).normalize
  }
}