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 📥

GameCoupledSimilarityPlain.scala 2.24 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
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

/**
 * Implementation of coupled similarity derived from CS's characterization as a simple game.
 * [Plain version tries to stay close to the presentation in the thesis]
 */

class GameCoupledSimilarityPlain[S, A, L] (
    val ts: WeakTransitionSystem[S, A, L])
  extends AlgorithmLogging[S, A, L] {
  
  case class CSAttackerNode(p: S, q: S) extends SimpleGame.AttackerNode
  case class CSDefenderStepNode(a: A, p: S, q: S) extends SimpleGame.DefenderNode
  case class CSDefenderCouplingNode(p: S, q: S) extends SimpleGame.DefenderNode
  
  class CoupledSimulationBaseGame
    extends SimpleGame with GameDiscovery with WinningRegionComputation {
    
    override def initialNodes: Iterable[SimpleGame.GameNode] = for {
      s1 <- ts.nodes
      s2 <- ts.nodes
    } yield CSAttackerNode(s1, s2)
    
    def successors(gn: GameNode): Iterable[GameNode] = gn match {
      case CSAttackerNode(p0, q0) =>
        val dn = for {
          (a,pp1) <- ts.post(p0)
          p1 <- pp1
        } yield CSDefenderStepNode(a, p1, q0)
        dn ++ List(CSDefenderCouplingNode(p0, q0))
      case CSDefenderStepNode(a, p1, q0) =>
        for {
          q1 <- ts.weakPost(q0, a)
        } yield CSAttackerNode(p1, q1)
      case CSDefenderCouplingNode(p0, q0) =>
        for {
          q1 <- ts.silentReachable(q0)
        } yield CSAttackerNode(q1, p0)
    }
  }
  
  def compute() = {
    
    val csGame = new CoupledSimulationBaseGame() 

    println("cs plain 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)
  }
}