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 📥

BigStepEquivalence.scala 1.24 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.sigref

import de.bbisping.coupledsim.ts.TransitionSystem
import de.bbisping.coupledsim.util.Relation
import de.bbisping.coupledsim.util.Coloring
import de.bbisping.coupledsim.ts.WeakTransitionSystem

/**
 * weak bisimilarity only regarding the maximal steps (where the target states cannot perform further tau-transitions.)
 * */

class BigStepEquivalence[S, A, L] (
    override val ts: WeakTransitionSystem[S, A, L])
  extends SignatureRefinement[S, A, L](ts) {
    
  val tau = ts.silentActions.headOption.toSet
  
  val tauMaximalNode = {
    for {
      p <- ts.nodes
      if ts.silentReachable(p) subsetOf Set(p)
    } yield p
  }
  
  override def signature(s: S): Set[(Coloring.Color, Coloring.Color)] = {
    
    val visibleSteps = for {
      s1 <- ts.silentReachable(s)
      (a, s2s) <- ts.post(s1).toSet
      if (!ts.silentActions(a))
      s2 <- s2s
      s3 <- ts.silentReachable(s2)
      if ( (tauMaximalNode contains s3))
    } yield (actionColors(a), partition(s3))
    
    val internalStep = for {
      t <- tau
      s1 <- ts.silentReachable(s)
      if ((partition(s) != partition(s1)) && (tauMaximalNode contains s1))
    } yield (actionColors(t), partition(s1))
    
    visibleSteps ++ internalStep
  }
  
}