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 📥

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

import de.bbisping.coupledsim.ts.WeakTransitionSystem
import de.bbisping.coupledsim.util.Coloring
import de.bbisping.coupledsim.ts.WeakTransitionSystem
import de.bbisping.coupledsim.util.LabeledRelation

/** takes an equivalence class coloring and builds a quotient automaton system.
 *  
 *  it will take some node from every class as representative (no merging of nodelabels or whatsoever!).
 *  the transitions of classes are merged. (the algorithm makes no assumptions like that nodes within
 *  a class have bisimilar transitions.)
 *  
 *  */
class BuildQuotientSystem[S, A, L] (
    ts: WeakTransitionSystem[S, A, L],
    coloring: Coloring[S]
  ) {
  
  def build() = {
    val partitions = coloring.partitions
    val reps = partitions.mapValues(_.head)
    
    val transitions = for {
      (color, partition) <- partitions.toList
      (a, post) <- ts.post(partition).toList
      tar <- post
    } yield (reps(color), a, reps(coloring(tar)))
    
    val nodeLabeling = for {
      rep <- reps.values
    } yield (rep, ts.nodeLabeling(rep))
    
    new WeakTransitionSystem(
        new LabeledRelation(transitions.toSet),
        nodeLabeling.toMap,
        ts.silentActions)
  }
  
}