Slightly optimize game solving

.github/workflows/scala-test-webstage.yml

@@ -13,16 +13,16 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
     - name: Create code archive
       run: zip -r code.zip doc js-api js-client project shared web .sbtopts build.sbt README.md
-    - name: Set up JDK 11
-      uses: actions/setup-java@v3
+    - name: Set up JDK 17
+      uses: actions/setup-java@v4
       with:
-        java-version: '11'
+        java-version: '17'
         distribution: 'temurin'
-    - name: Coursier cache
-      uses: coursier/cache-action@v6
+        cache: 'sbt'
+    - uses: sbt/setup-sbt@v1
     - name: Run tests
       run: sbt "shared/test"
     - name: Compile webtool
@@ -32,7 +32,7 @@ jobs:
     - name: Add code archive to web deployment
       run: mv code.zip web/target/web/stage/
     - name: Deploy CI
-      uses: burnett01/rsync-deployments@5.2
+      uses: burnett01/rsync-deployments@7.0.1
       with:
         switches: -avzr --delete
         path: web/target/web/stage/
@@ -43,22 +43,22 @@ jobs:
     - name: Remove code archive from artifact
       run: rm web/target/web/stage/code.zip
     - name: Archive production webclient artifact
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ltbt-spectroscopy-webclient
         path: |
           web/target/web/stage
     - name: Archive production JS api artifact
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: ltbt-spectroscopy-js-api
         path: |
           js-api/target/eqfiddle-api.js
-    - name: Cleanup before cache
-      shell: bash
-      run: |
-        rm -rf "$HOME/.ivy2/local" || true
-        find $HOME/Library/Caches/Coursier/v1        -name "ivydata-*.properties" -delete || true
-        find $HOME/.ivy2/cache                       -name "ivydata-*.properties" -delete || true
-        find $HOME/.cache/coursier/v1                -name "ivydata-*.properties" -delete || true
-        find $HOME/.sbt                              -name "*.lock"               -delete || true
+    # - name: Cleanup before cache
+    #   shell: bash
+    #   run: |
+    #     rm -rf "$HOME/.ivy2/local" || true
+    #     find $HOME/Library/Caches/Coursier/v1        -name "ivydata-*.properties" -delete || true
+    #     find $HOME/.ivy2/cache                       -name "ivydata-*.properties" -delete || true
+    #     find $HOME/.cache/coursier/v1                -name "ivydata-*.properties" -delete || true
+    #     find $HOME/.sbt                              -name "*.lock"               -delete || true

js-client/src/main/scala-2.12/io/equiv/eqfiddle/tool/control/Structure.scala

@@ -24,6 +24,7 @@ import io.equiv.eqfiddle.hml.Spectrum
 import io.equiv.eqfiddle.spectroscopy.SpectroscopyInterface
 import io.equiv.eqfiddle.algo.WeakTransitionSaturation
 import io.equiv.eqfiddle.algo.sigref.Bisimilarity
+import io.equiv.eqfiddle.algo.sigref.BranchingBisimilarity
 import io.equiv.eqfiddle.algo.transform.BuildQuotientSystem
 import io.equiv.eqfiddle.hml.ObservationClass
 
@@ -269,15 +270,29 @@ object Structure {
       ts
     }
 
-    val bisimMinimized = labels.collect { case (id, label) if label.act.contains('bisim_minimized) => id }
-    val minimizedTs = if (bisimMinimized.nonEmpty) {
-      val bisimColoring = new Bisimilarity(saturatedTs, Some(rel.getReachablePart(bisimMinimized) -- mainNodes)).computePartition()
+    val bisimMinimizedIds =
+      labels.collect { case (id, label) if label.act.contains('bisim_minimized) => id }
+    val minimizedTs = if (bisimMinimizedIds.nonEmpty) {
+      val bisimColoring = new Bisimilarity(saturatedTs, Some(rel.getReachablePart(bisimMinimizedIds) -- mainNodes)).computePartition()
       new BuildQuotientSystem(saturatedTs, bisimColoring, mainNodes).build()
     } else {
       saturatedTs
     }
 
-    minimizedTs
+    val branchingBisimMinimizedIds =
+      labels.collect { case (id, label) if label.act.contains('srbb_minimized) => id }
+    val minimizedTs2 = if (branchingBisimMinimizedIds.nonEmpty) {
+      val bisimColoring = new BranchingBisimilarity(
+        minimizedTs,
+        Some(rel.getReachablePart(branchingBisimMinimizedIds) -- mainNodes),
+        stabilityRespecting = true
+      ).computePartition()
+      new BuildQuotientSystem(minimizedTs, bisimColoring, mainNodes).build()
+    } else {
+      minimizedTs
+    }
+
+    minimizedTs2
   }
 
   case class StructureCallOperation(slug: String, resetReplay: Boolean = true) extends StructureAction {

shared/src/main/scala-2.12/io/equiv/eqfiddle/algo/sigref/BranchingBisimilarity.scala

@@ -0,0 +1,43 @@
+package io.equiv.eqfiddle.algo.sigref
+
+import io.equiv.eqfiddle.ts.TransitionSystem
+import io.equiv.eqfiddle.util.Relation
+import io.equiv.eqfiddle.util.Coloring
+import io.equiv.eqfiddle.algo.AlgorithmLogging
+import io.equiv.eqfiddle.ts.WeakTransitionSystem
+
+/**
+ * Signature refinement branching bisimilarity algorithm
+ * 
+ * (following [WHHSB2006])
+ * 
+ * */
+
+class BranchingBisimilarity[S, A, L] (
+    override val ts: WeakTransitionSystem[S, A, L],
+    onStates: Option[Set[S]] = None,
+    stabilityRespecting: Boolean = false
+  ) extends SignatureRefinement[S, A, L](ts, onStates) {
+
+  val stabilizationColor = actionColors.freshColor()
+
+  override def signature(s: S): Set[(Coloring.Color, Coloring.Color)] = {
+    val stepSigs: Set[(Coloring.Color, Coloring.Color)] = for {
+      s1 <- ts.silentReachable(s)
+      if partition(s) == partition(s1)
+      (a, s2s) <- ts.post(s1).toSet
+      s2 <- s2s
+      if (!ts.silentActions(a) || partition(s) != partition(s2))
+    } yield (actionColors(a), partition(s2))
+
+    if (!stabilityRespecting) {
+      stepSigs
+    } else {
+      stepSigs ++ (for {
+        s1 <- ts.silentReachable(s)
+        if partition(s) == partition(s1) && ts.isStable(s1)
+      } yield (stabilizationColor, partition(s1))
+      )
+    }
+  }
+}

shared/src/main/scala-2.12/io/equiv/eqfiddle/algo/transform/BuildQuotientSystem.scala

@@ -26,7 +26,9 @@ class BuildQuotientSystem[S, A, L] (
       (color, partition) <- partitions.toList
       (a, post) <- ts.post(partition).toList
       tar <- post
-    } yield (reps(color), a, reps(coloring(tar)))
+      srcRep = reps(color)
+      tarRep = reps(coloring(tar))
+    } yield (srcRep, a, tarRep)
 
     val nodeLabeling = for {
       rep <- reps.values

shared/src/main/scala-2.12/io/equiv/eqfiddle/game/GameLazyDecision.scala

@@ -31,15 +31,13 @@ trait GameLazyDecision[P] extends AbstractGameDiscovery {
   val printToDoLength: Boolean = false
 
   private def priceUpdate(node: GameNode, newPrices: Iterable[P]) = {
-    // assumes old and new price sets not to contain any dominated prices
     val oldPrices = attackerVictoryPrices(node)
-    val interestingNewPrices = newPrices.filterNot(p => oldPrices.exists(op => priceIsBetterOrEq(op, p)))
-    if (interestingNewPrices.nonEmpty) {
-      val interestingOldPrices = oldPrices.filterNot(p => interestingNewPrices.exists(priceIsBetter(_, p)))
-      attackerVictoryPrices(node) = interestingOldPrices ++ interestingNewPrices.filterNot(p => interestingNewPrices.exists(op => priceIsBetter(op, p)))
-      true
-    } else {
+    val newPricesMin = newPrices.filterNot(p => newPrices.exists(op => priceIsBetter(op, p))).toList
+    if (newPricesMin.forall(p => oldPrices.contains(p))) {
       false
+    } else {
+      attackerVictoryPrices(node) = newPricesMin
+      true
     }
   }
 

shared/src/main/scala-2.12/io/equiv/eqfiddle/spectroscopy/EnergyWeakSpectroscopy.scala

@@ -254,7 +254,7 @@ class EnergyWeakSpectroscopy[S, A, L] (
       val bisimilarNodes = for {
         gn <- hmlGame.discovered
         if (gn match { case hmlGame.AttackerObservation(_, qq) => qq.size == 1; case _ => false }) &&
-          !hmlGame.attackerVictoryPrices.isDefinedAt(gn)
+          (!hmlGame.attackerVictoryPrices.isDefinedAt(gn) || hmlGame.attackerVictoryPrices(gn).isEmpty)
       } yield (gn, Set[HennessyMilnerLogic.Formula[A]]())
 
       val distinguishingNodeFormulasExtended = distinguishingNodeFormulas ++ bisimilarNodes
@@ -299,7 +299,7 @@ class EnergyWeakSpectroscopy[S, A, L] (
       val bisimilarNodes = for {
         gn <- hmlGame.discovered
         if (gn match { case hmlGame.AttackerObservation(_, qq) => qq.size == 1; case _ => false }) &&
-          !hmlGame.attackerVictoryPrices.isDefinedAt(gn)
+          (!hmlGame.attackerVictoryPrices.isDefinedAt(gn) || hmlGame.attackerVictoryPrices(gn).isEmpty)
       } {
         hmlGame.attackerVictoryPrices(gn) = List()
       }

shared/src/main/scala-2.12/io/equiv/eqfiddle/spectroscopy/FastSpectroscopy.scala

@@ -155,12 +155,11 @@ class FastSpectroscopy[S, A, L] (
       val bisimilarNodes = for {
         gn <- hmlGame.discovered
         if (gn match { case hmlGame.AttackerObservation(_, qq) => qq.size == 1; case _ => false }) &&
-          !hmlGame.attackerVictoryPrices.isDefinedAt(gn)
+          (!hmlGame.attackerVictoryPrices.isDefinedAt(gn) || hmlGame.attackerVictoryPrices(gn).isEmpty)
       } yield (gn, Set[HennessyMilnerLogic.Formula[A]]())
 
       val distinguishingNodeFormulasExtended = distinguishingNodeFormulas ++ bisimilarNodes
 
-
       val gameString = debugLog(
         graphvizGameWithFormulas(hmlGame, hmlGame.attackerVictoryPrices.toMap, distinguishingNodeFormulasExtended),
         asLink = "https://edotor.net/?engine=dot#"
@@ -201,7 +200,7 @@ class FastSpectroscopy[S, A, L] (
       val bisimilarNodes = for {
         gn <- hmlGame.discovered
         if (gn match { case hmlGame.AttackerObservation(_, qq) => qq.size == 1; case _ => false }) &&
-          !hmlGame.attackerVictoryPrices.isDefinedAt(gn)
+          (!hmlGame.attackerVictoryPrices.isDefinedAt(gn) || hmlGame.attackerVictoryPrices(gn).isEmpty)
       } {
         hmlGame.attackerVictoryPrices(gn) = List()
       }