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 📥

AGraphConstruction.scala 2.82 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
package de.bbisping.coupledsim.algo.transform

import scala.annotation.migration
import de.bbisping.coupledsim.ts.TransitionSystem
import de.bbisping.coupledsim.util.LabeledRelation
import de.bbisping.coupledsim.ts.DivergenceInformation
import de.bbisping.coupledsim.ts.WeakTransitionSystem

/** [CH1993, p. 15]
 *  (understanding the definition to have side effects (globally updating -->_T etc.)) */
class AGraphConstruction[S, A, L] (
    ts: WeakTransitionSystem[S, A, L] with DivergenceInformation[S],
    newState: (WeakTransitionSystem[S, A, L], Set[A], Boolean) => (S, L) 
    ) {
  
  // environment E for new states
  protected val newStates: collection.mutable.Map[(Set[S], Boolean), S] = collection.mutable.Map()
  
  /**
   * assumes that tau closure has already been built  
   */
  def compute(initial: S) = {
    build(new WeakTransitionSystem(LabeledRelation(), Map(), ts.silentActions), Set(initial), true)
  }
  
  def build(pats: WeakTransitionSystem[S, A, L] , activeStates: Set[S], convergent: Boolean): (WeakTransitionSystem[S, A, L], S) = {
    
    // reading S^tau as S^eta
    val tauStates = for {
      s <- activeStates
      sR <- ts.silentReachable(s)
    } yield sR
    
    newStates.get(tauStates, convergent) match {
      // if E(<S^tau, b>) exists then return <<T, Act, -->_T>, E(<S^tau, b>)>
      case Some(tsc) => 
        (pats, tsc)
      // else
      case None =>
        // c
        val c = convergent && tauStates.forall(!ts.diverges(_))
        // acc
        val accepting = if (c) { 
          for {
            p <- tauStates
            enabled = ts.enabled(p)
            if !enabled.exists(ts.silentActions)
            a <- enabled
          } yield a
        } else {
          Set[A]()
        }
        // t := newstate(acc, c)
        val (t, label) = newState(pats, accepting, c)
        
        // E := E[<S^tau,c> |-> t]
        newStates((tauStates, c)) = t
        
        // T := T union {t}
        var nodeLabeling = pats.nodeLabeling.updated(t, label)
        
        var step = pats.step 
        
        // reading s as p in ... | ? p : S^tau . s -->^a }
        val enabledVisibleActions = for {
          p <- tauStates
          a <- ts.enabled(p)
          if !ts.silentActions(a)
        } yield a
        
        for (a <- enabledVisibleActions) {
          // S_a
          val aStates = ts.post(tauStates, a)
          val (l, t1) = build(new WeakTransitionSystem(step, nodeLabeling, ts.silentActions), aStates, c)
          
          //TODO: change this to mutable data structures to faithfully capture the algorithm from [CH1993, p. 15] without complexity blow up..
          step = new LabeledRelation(step.tupleSet ++ l.step.tupleSet + ((t, a , t1))) 
          nodeLabeling ++= l.nodeLabeling
        }
        
        (new WeakTransitionSystem(step, nodeLabeling, ts.silentActions), t)
    }
  }
}