From feb68ee9a8dddb69fad72537b0d188233e85c9f6 Mon Sep 17 00:00:00 2001 From: benkeks Date: Wed, 26 Jun 2024 14:00:26 +0200 Subject: [PATCH] Rename instable ~> unstable MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit (RvG calls it “unstable” failures) --- .../io/equiv/eqfiddle/ccs/CCSSamples.scala | 12 +++++----- .../hml/ObservationClassEnergyWeak.scala | 24 +++++++++---------- .../EnergyWeakSpectroscopyGame.scala | 8 +++---- 3 files changed, 22 insertions(+), 22 deletions(-) diff --git a/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/CCSSamples.scala b/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/CCSSamples.scala index 46564f1..0764674 100644 --- a/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/CCSSamples.scala +++ b/shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/CCSSamples.scala @@ -518,7 +518,7 @@ P58 = a.(tau.b + b + tau) |@compareSilent "A1, A2" |""".stripMargin - val stableInstableAbstraction = + val stableUnstableAbstraction = """|@comment "Pte/Ptl resemble Pe/Pl with all occurrences of idle renamed to tau" | |Ae = (idle.Ae + a) @@ -540,8 +540,8 @@ P58 = a.(tau.b + b + tau) |@compareSilent "Pe, Pl" |@compareSilent "Pte, Ptl" | - |@comment "Pe/Pl should be (instable&stable) readiness equivalent" - |@comment "Pte/Ptl are stable, but not instable (!) failure (and readiness) equivalent" + |@comment "Pe/Pl should be (unstable&stable) readiness equivalent" + |@comment "Pte/Ptl are stable, but not unstable (!) failure (and readiness) equivalent" | |Pe(x=200, y=10) |Pl(x=500, y=10) @@ -577,9 +577,9 @@ P58 = a.(tau.b + b + tau) Samples.Example("weak-edge-cases-david", "Weak Edge Cases by David", davidsEdgeCases), - Samples.Example("stable-instable-abstraction", - "Stable vs. instable abstraction", - stableInstableAbstraction), + Samples.Example("stable-unstable-abstraction", + "Stable vs. unstable abstraction", + stableUnstableAbstraction), Samples.Example("peterson-mutex", "Peterson Mutual exclusion", petersonMutex), diff --git a/shared/src/main/scala-2.12/io/equiv/eqfiddle/hml/ObservationClassEnergyWeak.scala b/shared/src/main/scala-2.12/io/equiv/eqfiddle/hml/ObservationClassEnergyWeak.scala index 999739a..8c2c2cc 100644 --- a/shared/src/main/scala-2.12/io/equiv/eqfiddle/hml/ObservationClassEnergyWeak.scala +++ b/shared/src/main/scala-2.12/io/equiv/eqfiddle/hml/ObservationClassEnergyWeak.scala @@ -5,8 +5,8 @@ case class ObservationClassEnergyWeak( observationHeight: Int = 0, /** the maximal amount of branching conjunctions when descending into a formula */ branchingConjunctionLevels: Int = 0, - /** the maximal amount of instable conjunctions when descending into a formula */ - instableConjunctionLevels: Int = 0, + /** the maximal amount of unstable conjunctions when descending into a formula */ + unstableConjunctionLevels: Int = 0, /** the maximal amount of stable conjunctions when descending into a formula */ stableConjunctionLevels: Int = 0, /** number of “strong” conjunctions among the conjunctionLevels */ @@ -29,7 +29,7 @@ case class ObservationClassEnergyWeak( } else if ( this.observationHeight >= that.observationHeight && this.branchingConjunctionLevels >= that.branchingConjunctionLevels && - this.instableConjunctionLevels >= that.instableConjunctionLevels && + this.unstableConjunctionLevels >= that.unstableConjunctionLevels && this.stableConjunctionLevels >= that.stableConjunctionLevels && this.immediateConjunctionLevels >= that.immediateConjunctionLevels && this.revivalHeight >= that.revivalHeight && @@ -40,7 +40,7 @@ case class ObservationClassEnergyWeak( } else if ( this.observationHeight <= that.observationHeight && this.branchingConjunctionLevels <= that.branchingConjunctionLevels && - this.instableConjunctionLevels <= that.instableConjunctionLevels && + this.unstableConjunctionLevels <= that.unstableConjunctionLevels && this.stableConjunctionLevels <= that.stableConjunctionLevels && this.immediateConjunctionLevels <= that.immediateConjunctionLevels && this.revivalHeight <= that.revivalHeight && @@ -60,7 +60,7 @@ case class ObservationClassEnergyWeak( ObservationClassEnergyWeak( Integer.max(this.observationHeight, that.observationHeight), Integer.max(this.branchingConjunctionLevels, that.branchingConjunctionLevels), - Integer.max(this.instableConjunctionLevels, that.instableConjunctionLevels), + Integer.max(this.unstableConjunctionLevels, that.unstableConjunctionLevels), Integer.max(this.stableConjunctionLevels, that.stableConjunctionLevels), Integer.max(this.immediateConjunctionLevels, that.immediateConjunctionLevels), Integer.max(this.revivalHeight, that.revivalHeight), @@ -76,7 +76,7 @@ case class ObservationClassEnergyWeak( ObservationClassEnergyWeak( Integer.min(this.observationHeight, that.observationHeight), Integer.min(this.branchingConjunctionLevels, that.branchingConjunctionLevels), - Integer.min(this.instableConjunctionLevels, that.instableConjunctionLevels), + Integer.min(this.unstableConjunctionLevels, that.unstableConjunctionLevels), Integer.min(this.stableConjunctionLevels, that.stableConjunctionLevels), Integer.min(this.immediateConjunctionLevels, that.immediateConjunctionLevels), Integer.min(this.revivalHeight, that.revivalHeight), @@ -90,7 +90,7 @@ case class ObservationClassEnergyWeak( override def toTuple = ( observationHeight, branchingConjunctionLevels, - instableConjunctionLevels, + unstableConjunctionLevels, stableConjunctionLevels, immediateConjunctionLevels, revivalHeight, @@ -103,14 +103,14 @@ case class ObservationClassEnergyWeak( object ObservationClassEnergyWeak { val INFTY = Integer.MAX_VALUE - // observationHeight, branchingConjLevels, instableConjs, stableConjs, immediateConjs, revivalHeight, positiveConjHeight, negativeConjHeight, negationLevels + // observationHeight, branchingConjLevels, unstableConjs, stableConjs, immediateConjs, revivalHeight, positiveConjHeight, negativeConjHeight, negationLevels // The Linear-time Branching-time Spectrum val BaseLTBTS = List( "enabledness" -> ObservationClassEnergyWeak( 1, 0, 0, 0, 0, 0, 0, 0, 0), "traces" -> ObservationClassEnergyWeak(INFTY, 0, 0, 0, 0, 0, 0, 0, 0), - "instable-failure" -> ObservationClassEnergyWeak(INFTY, 0, 1, 0, 0, 0, 0, 1, 1), + "unstable-failure" -> ObservationClassEnergyWeak(INFTY, 0, 1, 0, 0, 0, 0, 1, 1), "failure" -> ObservationClassEnergyWeak(INFTY, 0, 0, 1, 0, 0, 0, 1, 1), - "instable-readiness" -> ObservationClassEnergyWeak(INFTY, 0, 1, 0, 0, 1, 1, 1, 1), + "unstable-readiness" -> ObservationClassEnergyWeak(INFTY, 0, 1, 0, 0, 1, 1, 1, 1), "readiness" -> ObservationClassEnergyWeak(INFTY, 0, 0, 1, 0, 1, 1, 1, 1), //"failure-trace" -> ObservationClassEnergyWeak(INFTY, 0, 0, INFTY, 0, INFTY, 0, 1, 1), //"ready-trace" -> ObservationClassEnergyWeak(INFTY, 0, 0, INFTY, 0, INFTY, 1, 1, 1), @@ -166,7 +166,7 @@ object ObservationClassEnergyWeak { ObservationClassEnergyWeak( observationHeight = allClasses.map(_.observationHeight).max, branchingConjunctionLevels = allClasses.map(_.branchingConjunctionLevels).max + (if (isBranchingObs > 0) 1 else 0), - instableConjunctionLevels = allClasses.map(_.instableConjunctionLevels).max + (if (stabilityChecks.nonEmpty) 0 else 1), + unstableConjunctionLevels = allClasses.map(_.unstableConjunctionLevels).max + (if (stabilityChecks.nonEmpty) 0 else 1), stableConjunctionLevels = allClasses.map(_.stableConjunctionLevels).max + (if (stabilityChecks.nonEmpty) 1 else 0), immediateConjunctionLevels = allClasses.map(_.immediateConjunctionLevels).max + 1, revivalHeight = allClasses.map(_.revivalHeight).max, @@ -212,7 +212,7 @@ object ObservationClassEnergyWeak { ObservationClassEnergyWeak( observationHeight = andThenClass.observationHeight, branchingConjunctionLevels = andThenClass.branchingConjunctionLevels, - instableConjunctionLevels = andThenClass.instableConjunctionLevels, + unstableConjunctionLevels = andThenClass.unstableConjunctionLevels, stableConjunctionLevels = andThenClass.stableConjunctionLevels, immediateConjunctionLevels = andThenClass.immediateConjunctionLevels - (if (andThenClass.observationHeight <= 0 && andThenClass.stableConjunctionLevels <= 0) 0 else 1), // decreasing! diff --git a/shared/src/main/scala-2.12/io/equiv/eqfiddle/spectroscopy/EnergyWeakSpectroscopyGame.scala b/shared/src/main/scala-2.12/io/equiv/eqfiddle/spectroscopy/EnergyWeakSpectroscopyGame.scala index 2e36388..8b45763 100644 --- a/shared/src/main/scala-2.12/io/equiv/eqfiddle/spectroscopy/EnergyWeakSpectroscopyGame.scala +++ b/shared/src/main/scala-2.12/io/equiv/eqfiddle/spectroscopy/EnergyWeakSpectroscopyGame.scala @@ -8,7 +8,7 @@ import io.equiv.eqfiddle.ts.WeakTransitionSystem class EnergyWeakSpectroscopyGame[S, A, L](ts: WeakTransitionSystem[S, A, L], energyCap: Int = Int.MaxValue) extends SimpleGame with EnergyGame { - // obs, branchingConj, instableConj, stableConj, immediateConj, revivals, positiveHeight, negativeHeight, negations + // obs, branchingConj, unstableConj, stableConj, immediateConj, revivals, positiveHeight, negativeHeight, negations private val NoEnergyUpdate = new EnergyGame.EnergyUpdate(Array( 0, 0, 0, 0, 0, 0, 0, 0, 0), energyCap = energyCap) private val ObsEnergyUpdate = new EnergyGame.EnergyUpdate(Array(-1, 0, 0, 0, 0, 0, 0, 0, 0), energyCap = energyCap) private val InstableConjEnergyUpdate = new EnergyGame.EnergyUpdate(Array( 0, 0,-1, 0, 0, 0, 0, 0, 0), energyCap = energyCap) @@ -88,10 +88,10 @@ class EnergyWeakSpectroscopyGame[S, A, L](ts: WeakTransitionSystem[S, A, L], ene if (optimizeSymmetryDefWins && (qq0 contains p0)) { List() } else { - val instableConjMove = DefenderConjunction(p0, qq0) + val unstableConjMove = DefenderConjunction(p0, qq0) if (optimizeAttackerWins && qq0.isEmpty) { // prioritize instant wins because of stuck defender - List(instableConjMove) + List(unstableConjMove) } else { val stableConjMove = if (ts.isStable(p0)) { List(DefenderStableConjunction(p0, qq0.filter(ts.isStable(_)))) @@ -116,7 +116,7 @@ class EnergyWeakSpectroscopyGame[S, A, L](ts: WeakTransitionSystem[S, A, L], ene } yield { DefenderBranchingConjunction(p0, a, p1, qq0 -- qq0a, qq0a) } - dn ++ List(instableConjMove) ++ branchingConjs ++ stableConjMove + dn ++ List(unstableConjMove) ++ branchingConjs ++ stableConjMove } } case AttackerBranchingObservation(p0, qq0) =>