Markus Alexander Kuppe
Markus Alexander Kuppe
May I ask why you didn't choose to contribute your examples to the "official" [Example project](https://github.com/tlaplus/Examples)?
We have always wanted to have more beginner friendly examples in the repo! I would suggest to contribute your examples into a single sub-directory under specifications/ with some descriptive name...
Failed attempt to use Linchecker: ```java package org.kuppe; import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingCTest; import org.jetbrains.kotlinx.lincheck.verifier.VerifierState; import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier; import org.junit.Test; @ModelCheckingCTest(requireStateEquivalenceImplCheck = false, threads = 2, verifier = LinearizabilityVerifier.class) public...
## This has been integrated into the tutorial with https://github.com/lemmy/BlockingQueue/commit/f3075bf4dcda25387b05d7f2d8787b61fb95a48b and https://github.com/lemmy/BlockingQueue/commit/b0bbddc1b28e9c8150fc2ccf7ce2f46da53d631d. Fairness constraint with which `NoStarvation` holds for `FairSpec` of (deadlock-free) BlockingQueue, i.e. `THEOREM FairSpec => Starvation`. ```diff diff...
@johnyf Do you think that starvation freedom (`Starvation`) for `FairSpec` can be proved with the new tlapm?
The refinement `BlockingQueue`
Theorems have been moved and renamed, breaking BQF proof. ```diff diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla index 4c6fc6e..c6a088b 100644 --- a/BlockingQueueFair.tla +++ b/BlockingQueueFair.tla @@ -1,5 +1,5 @@ ------------------------- MODULE BlockingQueueFair ------------------------- -EXTENDS...
Thanks for taking the time! I've created a [plunkr](http://plnkr.co/edit/MQHmOW2caNQ9oKKIvCBr?p=info) with the content served at https://wall.tlapl.us. As you will see, the different RSS feeds listed in index.html are not sorted globally....