Skip to content

Commit

Permalink
Rename instable ~> unstable
Browse files Browse the repository at this point in the history 
(RvG calls it “unstable” failures)
  • Loading branch information
@benkeks
benkeks committed Jun 26, 2024
1 parent feeb9fa commit feb68ee
Show file tree
Hide file tree
Showing 3 changed files with 22 additions and 22 deletions.
12 changes: 6 additions & 6 deletions shared/src/main/scala-2.12/io/equiv/eqfiddle/ccs/CCSSamples.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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),
Expand Down
24 changes: 12 additions & 12 deletions shared/src/main/scala-2.12/io/equiv/eqfiddle/hml/ObservationClassEnergyWeak.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand All @@ -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 &&
Expand All @@ -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 &&
Expand All @@ -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),
Expand All @@ -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),
Expand All @@ -90,7 +90,7 @@ case class ObservationClassEnergyWeak(
override def toTuple = (
observationHeight,
branchingConjunctionLevels,
instableConjunctionLevels,
unstableConjunctionLevels,
stableConjunctionLevels,
immediateConjunctionLevels,
revivalHeight,
Expand All @@ -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),
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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!
Expand Down
8 changes: 4 additions & 4 deletions shared/src/main/scala-2.12/io/equiv/eqfiddle/spectroscopy/EnergyWeakSpectroscopyGame.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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(_))))
Expand All @@ -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) =>
Expand Down

0 comments on commit feb68ee

Please sign in to comment.