Releases: tlaplus/CommunityModules
Releases · tlaplus/CommunityModules
Release list
202607181436
several theorems about graphs (#125)
* several theorems about graphs
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* rename operators in tests for graphs
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* rename proofs module so that it will be picked up by CI
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* fix two proof steps that appear to be shaky in the CI check
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* Add tests for Graphs SimplePath, AreConnectedIn and IsStronglyConnected
Check the operators exhaustively against their pure TLA+ definitions and
the ConnectionsIn oracle over all graphs on up to three nodes, plus edge
cases (self-loops, arguments outside the node set, composite/non-normalized
node values).
[Tests]
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
* Add Graphs module overrides for SimplePath, AreConnectedIn and IsStronglyConnected
Register three Java overrides in TLCOverrides. SimplePath enumerates
simple paths via DFS instead of materializing SeqOf(node, Cardinality(node));
AreConnectedIn and IsStronglyConnected use BFS (the latter forward and on the
transpose) rather than the quadratic all-pairs pure-TLA+ definitions.
The overrides cut GraphsTests (exhaustive checks over all graphs on up to
four nodes `\cup Graphs({1, 2, 3})`) from ~15 to ~5 minutes.
TLC's code is not reused: its only Value-based graph algorithm,
TransitiveClosure.Warshall, is non-reflexive, drops isolated nodes and is
O(V^3), so it fits none of these operators.
[TLC]
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
* Towards a TLAPS stdlib (#127)
* Theorems about Contains and majority supersets
Add and prove membership theorems for SequencesExt!Contains
(empty/Append/Cons/Concat/Tail/singleton plus heterogeneous-type
Append/Concat variants) and SupersetOfMajorityIsMajority for
FiniteSetsExt. All obligations checked with TLAPS.
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
* IsSorted operator and sortedness theorems
Add SequencesExt!IsSorted(s, op(_,_)), which holds iff s is sorted with
respect to an arbitrary binary relation op, with a formal doc comment
and examples. Add and prove the accompanying theorems SortedEmpty,
SortedSingleton, SortedAppend, SortedConcat, SortedInjective and
SortedSubSeq, whose order hypotheses on op (transitivity, irreflexivity)
are stated locally so they apply to any relation. All obligations
checked with TLAPS.
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
* theorems about sequences, finite sets, and quorum systems
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* fixing two apparently brittle proofs
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* align theorem statements in SequencesExtTheorems with those in the _proofs module
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
---------
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Co-authored-by: Stephan Merz <stephan.merz@loria.fr>
* several theorems about graphs
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* rename operators in tests for graphs
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* rename proofs module so that it will be picked up by CI
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* fix two proof steps that appear to be shaky in the CI check
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* minor changes
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* make SCCs maximal
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
* Add AbstractGraphs class to share implementation between directed and undirected graph modules
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
* final cleanup
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
---------
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Markus Alexander Kuppe <github.com@lemmster.de>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
202607140702
Towards a TLAPS stdlib (#127) * Theorems about Contains and majority supersets Add and prove membership theorems for SequencesExt!Contains (empty/Append/Cons/Concat/Tail/singleton plus heterogeneous-type Append/Concat variants) and SupersetOfMajorityIsMajority for FiniteSetsExt. All obligations checked with TLAPS. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * IsSorted operator and sortedness theorems Add SequencesExt!IsSorted(s, op(_,_)), which holds iff s is sorted with respect to an arbitrary binary relation op, with a formal doc comment and examples. Add and prove the accompanying theorems SortedEmpty, SortedSingleton, SortedAppend, SortedConcat, SortedInjective and SortedSubSeq, whose order hypotheses on op (transitivity, irreflexivity) are stated locally so they apply to any relation. All obligations checked with TLAPS. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * theorems about sequences, finite sets, and quorum systems Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * fixing two apparently brittle proofs Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * align theorem statements in SequencesExtTheorems with those in the _proofs module Signed-off-by: Stephan Merz <stephan.merz@loria.fr> --------- Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Signed-off-by: Stephan Merz <stephan.merz@loria.fr> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Co-authored-by: Stephan Merz <stephan.merz@loria.fr>
202607091326
Add Graphs module overrides for SimplePath, AreConnectedIn and IsStro…
202604221529
Theorems for sum of constant function Add SumFunctionOnSetConst and SumFunctionConst stating that summing a constant function over a finite set equals the constant times the cardinality of the set, together with corresponding proofs and an example in the doc comments. [Feature] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Signed-off-by: Stephan Merz <stephan.merz@loria.fr> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
202604061452
add ToBag operator (#123) * add ToBag operator Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * improve comment for ToBag operator Signed-off-by: Stephan Merz <stephan.merz@loria.fr> --------- Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
202603110432
Update GitHub Actions workflows to use the new output syntax for sett…
202602261933
make syntax compatible with TLAPM (#120) * make syntax compatible with TLAPM Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * reformulation of comment on syntax not supported by TLAPS Signed-off-by: Stephan Merz <stephan.merz@loria.fr> --------- Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
202601200755
two more theorems about folds (#119) Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
202601131539
Update SVGSerialize to use three-digit zero-padding for frame numbers…
202601110807
more theorems about folds (#118) * more theorems about folds Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * more theorems on folds Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * theorems for SumFunction Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * align statement of ReverseSubSeq Signed-off-by: Stephan Merz <stephan.merz@loria.fr> --------- Signed-off-by: Stephan Merz <stephan.merz@loria.fr>