Activity
Removed hyperlink to tlaplus-standard repo
Removed hyperlink to tlaplus-standard repo
Re-generate manifest from script
Re-generate manifest from script
Pull request merge
CI: smoke-test state space script
CI: smoke-test state space script
Pull request merge
Docs: added CONTRIBUTING.md and DEVELOPING.md
Docs: added CONTRIBUTING.md and DEVELOPING.md
Pull request merge
fixed proof for initial condition
fixed proof for initial condition
Merge branch 'master' into fixByzPaxos
Merge branch 'master' into fixByzPaxos
Merge branch 'fixByzPaxos' of github.com:tlaplus/Examples into fixByz…
Merge branch 'fixByzPaxos' of github.com:tlaplus/Examples into fixByz…
reverted definition of Success for model checking and adapted the proof
reverted definition of Success for model checking and adapted the proof
CI: terminate outdated CI runs
CI: terminate outdated CI runs
Pull request merge
Merge branch 'fewer-skipped-proofs' of github.com:tlaplus/Examples in…
Merge branch 'fewer-skipped-proofs' of github.com:tlaplus/Examples in…
Merge branch 'fixSimpleRegular' of github.com:tlaplus/Examples into f…
Merge branch 'fixSimpleRegular' of github.com:tlaplus/Examples into f…
variant of proof with explicit witness
variant of proof with explicit witness
fixed (and simplified) proof in byzpaxos/Consensus.tla
fixed (and simplified) proof in byzpaxos/Consensus.tla
Added --enable_assertions to pcal translate script
Added --enable_assertions to pcal translate script
Pull request merge
Merge branch 'fixSimpleRegular' of github.com:tlaplus/Examples into f…
Merge branch 'fixSimpleRegular' of github.com:tlaplus/Examples into f…
fixed proof of TeachingConcurrency/SimpleRegular.tla
fixed proof of TeachingConcurrency/SimpleRegular.tla
Check proofs with TLAPM pre-release.
Check proofs with TLAPM pre-release.
Pull request merge
fixed proof of LoopInvariance/BinarySearch
fixed proof of LoopInvariance/BinarySearch