Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ensure preconditions are satisified when shrinking Commands actions #739

Conversation

jonaskoelker
Copy link
Contributor

In some cases a failing command sequence would shrink to a single
command whose precondition was not satisfied, e.g. dequeueing from an
initially empty queue. Ensuring preconditions are satisfied means
shrinking outputs a valid sequence of commands.

In some cases a failing command sequence would shrink to a single
command whose precondition was not satisfied, e.g. dequeueing from an
initially empty queue.  Ensuring preconditions are satisfied means
shrinking outputs a valid sequence of commands.
@jonaskoelker
Copy link
Contributor Author

jonaskoelker commented Dec 22, 2020

This is one part of #632, split out into its own commit, and now with tests.

Let me know if you'd like me to simplify the test. I'm sure it's possible, though the benefits are unclear to me: since many members of Commands are private it's hard to get at them, including for testing purposes. So we'll always have to test an effect of what I'm trying to fix, rather than the thing directly.

@ashawley
Copy link
Contributor

I haven't used the commands API a lot. How would a test case satisfy the pre-conditions, but then the failure cause it to shrink to something invalid? Are sequential commands being shrunk from the left-hand side when they should be shrunk from the right? Seems like it shouldn't be doing that. It should be following the same shrinking rules for lists in ScalaCheck.

Copy link
Contributor

@yannkaiser-asana yannkaiser-asana left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How would a test case satisfy the pre-conditions, but then the failure cause it to shrink to something invalid? Are sequential commands being shrunk from the left-hand side when they should be shrunk from the right? Seems like it shouldn't be doing that. It should be following the same shrinking rules for lists in ScalaCheck.

The shrinking rule for lists as I understand it try the first half, then the last half, then mixes either half with shrunk versions of the other half. (The rule restarts when another failing case is verified.)

For instance with commandds, if we were testing a Map-like structure implementation which turns out to be no-op and always return None

Scalacheck might find this failing test case:

  1. SetItem("A", 1)
  2. SetItem("B", 2)
  3. RemoveItem("B")
  4. GetItemOrNone("A") -> None # fail
  5. SetItem("C", 3)

We know that only items (1) and (4) are required to reproduce a failure, therefore (1, 4) will be the minimum shrink.

If RemoveItem has the precondition that the key already exist (unlike GetItemOrNone), Scalacheck might discover that:

  • You can remove (5) or (3) without changing the outcome
  • Removing (4) would keep the failure from occurring
  • Removing (2) would cause (3) to fail its precondition.
  • Removing both (2) and (3) doesn't change the outcome.

Surprisingly, I didn't encounter issues where Scalacheck would fail to verify preconditions during shrinking in 1.14, though I cannot figure out what exactly enforced this. It will be good to have this explicitly checked and tested.

Base automatically changed from master to main March 26, 2021 18:56
@jonaskoelker
Copy link
Contributor Author

jonaskoelker commented Mar 27, 2021

My bounded queue example also demonstrates this, though not in exactly in the gisted form. Here's a diff with gist links (and slightly mismatching file names), and first the session it produces:

[info] compiling 1 Scala source to /tmp/clean-copy/scalacheck/examples/bounded-queue/target/scala-2.12/test-classes ...
[info] ! BoundedQueue Spec.Bounded Queue is a bounded queue: Exception raised on property evaluation.
[info] > ARG_0: Actions(State(10,List()),List(Dequeue),List())
[info] > ARG_0_ORIGINAL: Actions(State(10,List()),List(Capacity, Size, Enqueue(-71), Dequeue, Capacity, Capacity, Size, Enqueue(127), Enqueue(0), Enqueue(31), Capacity, Enqueue(101), Dequeue, Dequeue, Enqueue(0), Enqueue(-1), Size, Enqueue(76), Enqueue(115), Enqueue(-84), Enqueue(92), Dequeue, Capacity, Enqueue(85), Capacity, Enqueue(1), Size, Size, Size, Dequeue, Capacity, Enqueue(-128), Capacity, Dequeue, Dequeue, Dequeue, Enqueue(-68), Enqueue(0), Size, Enqueue(-81), Capacity, Enqueue(78), Dequeue),List())
[info] > Exception: java.lang.UnsupportedOperationException: tail of empty list
[info] Failed: Total 1, Failed 0, Errors 1, Passed 0
[error] Error during tests:
[error]         BoundedQueueSpec
[error] (Test / test) sbt.TestsFailedException: Tests unsuccessful

As the name suggests, the shrunk command sequence tries to dequeue out of an empty queue, which violates the dequeue precondition.

Here's the diff (relative to the gist URLs) which created this session:

--- BoundedQueue.gist	2021-03-27 20:01:39.581238656 +0100
+++ BoundedQueue.scala	2021-03-27 20:02:35.451445495 +0100
@@ -1,9 +1,10 @@
+// https://gist.githubusercontent.com/jonaskoelker/ac60ded3a310b8f0fb548a1eda9f8859/raw/ee26e3fffb94b528e2036d7edfef5f8a8f1ea3d2/bounded-queue.scala
 import scala.reflect.ClassTag
 
 class BoundedQueue[Element: ClassTag](val capacity: Int) {
   require(capacity >= 0)
 
-  val buffer = Array.ofDim(capacity + 1)
+  val buffer = Array.ofDim(capacity) // an arbitrary bug
   var writes = 0
   var reads = 0
 
--- BoundedQueueSpec.gist	2021-03-27 20:02:20.078852906 +0100
+++ BoundedQueueSpec.scala	2021-03-27 20:11:42.631507734 +0100
@@ -1,3 +1,4 @@
+// https://gist.githubusercontent.com/jonaskoelker/b4a1d00a3da97c6d56e7b3d8fee02716/raw/ded9d6f2141434fa7776492d70cb849e07bc203a/bounded-queue-spec.scala
 import org.scalacheck.{Arbitrary, Gen, Prop, Properties, Shrink}
 import org.scalacheck.commands.Commands
 import org.scalacheck.Prop.{forAll, propBoolean}
@@ -5,7 +6,9 @@
 import scala.util.{Try, Success}
 
 class BoundedQueueSpec extends Properties("BoundedQueue Spec") {
-  property("Bounded Queue is a bounded queue") = BoundedQueueSpec.property()
+  val seed = Some("Rq3IZx4dBV09eqHr1U0esQT6XehFZ3yrX6xPXXstLgJ=")
+  propertyWithSeed("Bounded Queue is a bounded queue", seed) =
+    BoundedQueueSpec.property()
 }
 
 object BoundedQueueSpec extends Commands {
@@ -67,7 +70,7 @@
       Gen.const(Size),
       Gen.const(Dequeue),
       Arbitrary.arbitrary[Element].flatMap(Enqueue(_))
-    )
+    ).retryUntil(_.preCondition(state))
 
   def newSut(state: State): Sut =
     new BoundedQueue(state.capacity)
@@ -75,20 +78,6 @@
   def initialPreCondition(state: State): Boolean =
     state.capacity >= 0 && state.elements.isEmpty
 
-  override def shrinkState: Shrink[State] = Shrink {
-    case State(capacity, elements) => for {
-      (cap, elems) <- implicitly[Shrink[(Int, Seq[Element])]].shrink((capacity, elements))
-    } yield State(cap, elems take cap)
-  }
-
-  override def shrinkCommand: Shrink[Command] = Shrink {
-    case Enqueue(n) => Stream(Capacity, Size, Dequeue) ++
-      implicitly[Shrink[Element]].shrink(n).map(Enqueue(_))
-    case Dequeue => Stream(Capacity, Size)
-    case Size => Stream(Capacity)
-    case Capacity => Stream.empty
-  }
-
   def canCreateNewSut(
     newState: State,
     initSuts: Traversable[State],

@yannkaiser-asana
Copy link
Contributor

Is there something I can help with here to get this into a mergeable state?

@Larsjur
Copy link

Larsjur commented Oct 7, 2021

I have tested the PR on two examples where shrinking previously lead to invalid command sequences and this seems to solve the problem 👍

@ashawley
Copy link
Contributor

ashawley commented Oct 11, 2021

Sorry for the delay. If this is fixing the issue for others, as in #839, we should get this merged.

Thanks for the contribution.

If it used to work, I wonder if we should track down what the change since 1.14.3 was that introduced the defect?

@yannkaiser-asana
Copy link
Contributor

Thank you for reviewing! I'm not familiar with the PR process in this project, who is expected to hit merge on this PR?

Copy link
Member

@rossabaker rossabaker left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I second @ashawley's question about tracking down what broke since 1.14. But if that investigation reveals an even deeper problem, we can roll this back without affecting bincompat. All evidence is that this is good now.

@rossabaker rossabaker merged commit dde403d into typelevel:main Mar 7, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants