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 📥

RemoveInstableStates.scala 1009 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
package de.bbisping.coupledsim.algo

import de.bbisping.coupledsim.ts.TransitionSystem
import de.bbisping.coupledsim.util.FixedPoint
import de.bbisping.coupledsim.ts.WeakTransitionSystem
import de.bbisping.coupledsim.util.LabeledRelation

/** removes transitions leading to instable non-divergent states.
 *  (assumes that a transitive closure has been computed before, but no reflexive closure,
 *  so that exactly the reflexive states are divergent.)*/
class RemoveInstableStates[S, A, L] (
    ts: WeakTransitionSystem[S, A, L]) {
  
  def compute() = {
    val instableNDStates = for {
      p <- ts.nodes
      val enabledSilent = ts.enabled(p) intersect ts.silentActions
      if enabledSilent.nonEmpty                    // instable state
      if !(ts.post(p, enabledSilent) contains p)   // non-divergent state
    } yield p
    
    val newTrans = for {
      (p1, a, p2) <- ts.step.tupleSet
      if !(instableNDStates contains p2)
    } yield (p1, a, p2)
    new LabeledRelation(newTrans)
  }
  
}