Markus Alexander Kuppe
Markus Alexander Kuppe
The more examples the better but for the sake of consistency, I'd suggest to rename the repo and generally change the wording from "tlaplus" to "pluscal".
Ubuntu 20.04 - Linux avocado 5.4.0-42-generic #46-Ubuntu SMP Fri Jul 10 00:24:02 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux ```bash markus@avocado:~/src/Other/JCoz(master)$ make run-rmi-host java \ -cp $(readlink -f ./src/java/target/client-*-jar-with-dependencies.jar):/usr//lib/jvm/java-8-oracle//lib/tools.jar \ jcoz.service.JCozService...
### Polish * `Starvation` -> `NoStarvation`, `StarvationFree`, or `StarvationFreedom` * `Invariant` -> `NoDeadlock` or `DeadlockFree` (proof has theorem `DeadlockFreedom`) * Java `take` vs. TLA `get` action names * Align bound...
https://github.com/alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing https://github.com/lemmy/BlockingQueue/blob/0761ecfdb0e3aef3db1aa78df6f4aa0b60e5736d/.devcontainer/devcontainer.json#L10-L13 https://github.com/tlaplus/Examples/blob/f49468c12a3236ff1b39447f531378b85889e38e/.devcontainer/devcontainer.json#L14-L16
https://github.com/tlaplus/tlapm/issues/15 makes it necessary to update [TLAPS.tla](https://github.com/lemmy/BlockingQueue/blob/master/TLAPS.tla) in this repository to the newest version in TLAPM.
https://github.com/tlaplus-workshops/ewd998
```html | ``` My [index.html](http://wall.tlapl.us) has the following aping stance with ```order-by="timestamp"``` but the ordering only seems to affect the local ordering per aping plugin. How do I globally order...
```shell markus@banana:/opt/graalvm/graalvm-ce-java16-21.1.0$ head Some.csv trace#level#P#C#B#over#under 1#4#1#1#8#1#0 1#12#2#2#256#2#0 1#11#1#1#16#1#0 1#14#2#2#256#2#0 1#17#2#2#2#1#0 2#13#2#2#32#2#0 2#21#2#2#1#1#0 1#14#2#2#4#1#0 2#56#4#4#16#4#0 ``` ```R data % group_by(P,C,B) %>% summarise(mean_level = mean(level)) ``` ```shell markus@banana:/opt/graalvm/graalvm-ce-java16-21.1.0$ uname -a Linux banana...
The [second conjunct in the liveness property](https://github.com/tlaplus/Examples/blob/616c4c2e00dd7084c623d1dcc83b140279652fb4/specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.tla#L43-L44) of [MCInnerSerial](https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/AdvancedExamples/) fails to evaluate (detected by adding the TLA+ [examples as CI tests](https://github.com/tlaplus/Examples/commit/22e6b2daae5e0173ac856e8eab5c01abd90b39d4) for TLC): ```tla TLC2 Version 2.16 of Day Month...
Today's development teams follow the practice of [continuous integration (CI)](https://en.wikipedia.org/wiki/Continuous_integration). This trend is fueled by a plethora of (for-free) cloud services such as [TravisCI](https://travis-ci.org/), [Azure Pipelines](https://azure.microsoft.com/en-us/services/devops/pipelines/) or self-hosted automation servers...