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 📥

FixedPointCoupledSimilarity.scala 1.04 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
package de.bbisping.coupledsim.algo.cs

import de.bbisping.coupledsim.util.Relation
import de.bbisping.coupledsim.ts.WeakTransitionSystem
import de.bbisping.coupledsim.util.FixedPoint

/**
 * Straight forward implementation of coupled similarity derived from CS's gfp characterization.
 */

class FixedPointCoupledSimilarity[S, A, L] (
    val ts: WeakTransitionSystem[S, A, L]) {
  
  def compute() = {
    val initialCandidates = for {
      s1 <- ts.nodes
      s2 <- ts.nodes
      if ts.weakEnabled(s1) subsetOf ts.weakEnabled(s2)
    } yield (s1, s2)
    
    def csFun(sim: Relation[S]) = {
      sim.filter {
        (p, q) =>
          // enforce simulation
          (ts.post(p) forall {
            case (a, pp2) => pp2 forall { p2 =>
              val p2sim = sim.values(p2)
              ts.weakPost(q, a) exists p2sim
            }
          }) &&
          // enforce coupling
          (ts.silentReachable(q) exists { q1 => sim(q1, p) })
      }
    }
    
    FixedPoint[Relation[S]](csFun, _ == _) apply (new Relation[S](initialCandidates))
  }
}