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 📥

WeakTransitionSystem.scala 3.06 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 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
package de.bbisping.coupledsim.ts

import de.bbisping.coupledsim.util.LabeledRelation
import de.bbisping.coupledsim.util.Relation
import scala.collection.mutable.LinkedList
import scala.collection.mutable.Seq
import scala.collection.mutable.Queue

class WeakTransitionSystem[S, A, L](
    step: LabeledRelation[S, A],
    nodeLabeling: Map[S, L],
    override val silentActions: Set[A])
  extends TransitionSystem[S, A, L](step, nodeLabeling)
    with SilentActions[A] {
  
  def this(ts: TransitionSystem[S, A, L], silentActions: Set[A]) {
    this(ts.step, ts.nodeLabeling, silentActions)
  }
  
  val silentSteps = {
    step filter {
      case (p1, a, p2) => silentActions(a)
    } toRelation
  }
  
  import scala.collection.mutable.HashMap
  import scala.collection.mutable.HashSet
  private val silentReachableCache = new HashMap[S, Set[S]]
  
  def silentReachableCached(s: S): Set[S] = {
    silentReachableCache.getOrElseUpdate(s, {
      computeSilentReachableCached(s)
    })
  }
  
  private def computeSilentReachableCached(s: S): Set[S] = {
    val visited: HashSet[S] = HashSet()
    val todo = Queue[S](s)
    
    while (todo.nonEmpty) {
      val a = todo.dequeue()
      if (!visited(a)) {
        visited += a
        silentReachableCache.get(a) match {
          case None => 
            todo ++= silentSteps.values(a)
          case Some(reach) =>
            visited ++= reach
        }
      }
    }
    
    visited.toSet
  }
  
  //val silentReachable = (silentSteps.transitiveClosureFast.reflexiveClosureOn(nodes)) rep
  
  def silentReachable(s: S): Set[S] = silentReachableCached(s)
  
  val silentReachableInverse = Map[S, Set[S]]()//new Relation(silentReachable).inverse.rep
  
  def tauMaximalNode(s: S) = {
    step.rep(s) exists { case (a, ss) =>
      silentActions(a) && ss.nonEmpty
    }
  }
  
  def weakEnabled(s: S) = {
    for {
      s1 <- silentReachable(s)
      a <- enabled(s1)
      if !silentActions(a)
    } yield a
  }
  
  def weakEnabled2(s: S) = {
    for {
      s1 <- silentReachable(s)
      a <- enabled(s1)
    } yield a
  }
  
  def weakReachingActions(s: S) = {
    for {
      s1 <- silentReachableInverse(s)
      a <- reachingActions(s1)
      if !silentActions(a)
    } yield a
  }
  
  def weakPost(s: S, a: A): Set[S] = {
    val ss1 = silentReachable(s)
    if (silentActions(a)) {
      ss1
    } else {
      for {
        s2 <- post(ss1, a)
        s3 <- silentReachable(s2)
      } yield s3
    }
  }
  
  def weakPost(s: S): Map[A, Set[S]] = {
    for {
      a <- weakEnabled2(s)
    } yield (a, weakPost(s, a))
  } toMap
  
  def weakPre(s: S, a: A): Set[S] = {
    val ss1 = silentReachableInverse(s)
    if (silentActions(a)) {
      ss1
    } else {
      for {
        s2 <- pre(ss1, a)
        s3 <- silentReachableInverse(s2)
      } yield s3
    }
  }
  
  def weakPre(s: S): Map[A, Set[S]] = {
    {
      for {
        a <- weakReachingActions(s)
      } yield (a, weakPre(s, a))
    }.toMap
  }
  
  def weakPre(ss: Set[S]): Map[A, Set[S]] = {
    for { s <- ss; sp <- weakPre(s) toList } yield sp
  }.groupBy(_._1).mapValues(_.flatMap(_._2))
  
}