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 📥

GameCoupledSimilarity.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 85 86 87 88 89 90 91 92 93
package de.bbisping.coupledsim.algo.cs

import de.bbisping.coupledsim.util.Relation
import de.bbisping.coupledsim.ts.WeakTransitionSystem
import de.bbisping.coupledsim.util.FixedPoint
import scala.collection.mutable.Queue
import de.bbisping.coupledsim.algo.AlgorithmLogging
import de.bbisping.coupledsim.game.WinningRegionComputation
import de.bbisping.coupledsim.game.GameDiscovery
import de.bbisping.coupledsim.game.SimpleGame
import de.bbisping.coupledsim.algo.sigref.BigStepEquivalence

/**
 * Implementation of coupled similarity derived from CS's characterization as a simple game.
 */

class GameCoupledSimilarity[S, A, L] (
    override val ts: WeakTransitionSystem[S, A, L])
  extends GameCoupledSimilarityPlain[S, A, L](ts) {
  
  class CoupledSimulationGameWithApproximation(
      override val initialNodes: Iterable[SimpleGame.GameNode],
      csOverApproximation: Set[CSAttackerNode],
      csUnderApproximation: (S, S) => Boolean)
    extends CoupledSimulationBaseGame
      with GameDiscovery with WinningRegionComputation {
    
    override def successors(gn: GameNode): Iterable[GameNode] = gn match {
      case CSAttackerNode(p0, q0) =>
        if (csUnderApproximation(p0, q0)) {
          List()
        } else {
          super.successors(gn)
        }
      case _: SimpleGame.DefenderNode =>
        super.successors(gn) collect {
          case an: CSAttackerNode if csOverApproximation contains an => an
          case dn: SimpleGame.DefenderNode => dn
        }
    }
  }
  
  def initialsByEnabledSets() = {
    for {
      s1 <- ts.nodes
      s2 <- ts.nodes
      if ts.weakEnabled(s1) subsetOf ts.weakEnabled(s2)
    } yield CSAttackerNode(s1, s2)
  }
  
  def initialsByBigStepEquivalence() = {
    val bsEquiv = new BigStepEquivalence(ts)
    bsEquiv.computePartition()
    
    
    println("preparing join...")
    val sigs = for {
      s <- ts.nodes
    } yield (s, bsEquiv.signature(s))
    
    println("joiiiin...")
    for {
      (s1, s1Sig) <- sigs
      (s2, s2Sig) <- sigs
      if s1Sig.size <= s2Sig.size && (s1Sig subsetOf s2Sig) 
    } yield CSAttackerNode(s1, s2)
  }
  
  override def compute() = {
    
    // parameter for GameDiscovery
    val initialCandidates = initialsByBigStepEquivalence()
    
    println("initial size: " + initialCandidates.size)
    
    val csGame = new CoupledSimulationGameWithApproximation(
       initialCandidates,
       initialCandidates,
       (p0, q0) => ts.silentReachable(q0)(p0))

    println("cs game size: " + csGame.discovered.size)
    val attackerWin = csGame.computeWinningRegion()
    
    // the coupled simulation is exactly the attacker nodes not won by the attacker
    val simNodes = for {
      gn <- csGame.discovered
      if gn.isInstanceOf[CSAttackerNode] && !attackerWin(gn)
      CSAttackerNode(p, q) = gn
    } yield (p, q)
    
    new Relation[S](simNodes.toSet)
  }
}