Fix links to the Registry example

.github/workflows/ci.yaml

@@ -29,7 +29,7 @@ jobs:
           log-lines = 1000
 
     - name: Github cache ~/.cabal/packages, ~/.cabal/store and dist-newstyle
-      uses: actions/cache@v2.1.5
+      uses: actions/cache@v4
       with:
         path: |
           ~/.cabal/packages
@@ -73,7 +73,7 @@ jobs:
           accept-flake-config = true
 
     - name: Github cache ~/.cabal/packages, ~/.cabal/store and dist-newstyle
-      uses: actions/cache@v2.1.5
+      uses: actions/cache@v4
       with:
         path: |
           ~/.cabal/packages
@@ -87,7 +87,7 @@ jobs:
         nix develop --accept-flake-config --command .github/workflows/ci-haddock.sh
 
     - name: Upload build & test artifacts
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: haddocks
         path: ./docs
@@ -102,7 +102,7 @@ jobs:
         repository: input-output-hk/quickcheck-dynamic
 
     - name: Download generated documentation
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: haddocks
         path: docs

README.md

@@ -14,7 +14,7 @@ This repository hosts:
 ## Documentation
 
 * The original stateful testing approach is described in John Hughes' research paper: [https://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quviq-testing.pdf ](https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf)
-* The [Registry example](https://github.com/input-output-hk/quickcheck-dynamic/tree/main/quickcheck-io-sim-compat) is a common case study that's been explored in two papers:
+* The [Registry example](https://github.com/input-output-hk/quickcheck-dynamic/blob/main/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs) is a common case study that's been explored in two papers:
   * [How well are your requirements tested?](https://publications.lib.chalmers.se/records/fulltext/232552/local_232552.pdf)
   * and [Understanding Formal Specifications through Good Examples](https://mengwangoxf.github.io/Papers/Erlang18.pdf)
 * The dynamic logic addition allows you to specify that after a generated test sequence, the system is able to reach a specific required state. In other words, you can specify that some "good" state is reachable from any possible state.

quickcheck-dynamic/README.md

@@ -17,7 +17,7 @@ Plutus or Cardano.
   comments. Checkout [StateModel](https://hackage.haskell.org/package/quickcheck-dynamic/docs/src/Test.QuickCheck.StateModel.html)
   and [DynamicLogic](https://hackage.haskell.org/package/quickcheck-dynamic/docs/Test-QuickCheck-DynamicLogic.html) modules for
   some usage instructions.
-* For a concrete standalone example, have a look at `Registry` and `RegistryModel` modules from the companion [quickcheck-io-sim-compat](https://github.com/input-output-hk/quickcheck-dynamic/tree/main/quickcheck-io-sim-compat) package (not currently available on hackage), a multithreaded Thread registry inspired by the Erlang version of QuickCheck described in [this article](https://mengwangoxf.github.io/Papers/Erlang18.pdf)
+* For a concrete standalone example, have a look at the [`Registry`](https://github.com/input-output-hk/quickcheck-dynamic/blob/main/quickcheck-dynamic/test/Spec/DynamicLogic/Registry.hs) and [`RegistryModel`](https://github.com/input-output-hk/quickcheck-dynamic/blob/main/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs) module from the test suite, which respectively implement and model a multithreaded Thread registry inspired by the Erlang version of QuickCheck described in [this article](https://mengwangoxf.github.io/Papers/Erlang18.pdf)
 * For more documentation on how to quickcheck-dynamic is used to test
   Plutus DApps, check this
   [tutorial](https://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-models.html).