Files
Baradb/formal-verification/models/backup.cfg
T
dimgigov 422df08ab9 feat: clean build + crossmodal.tla + TLA+ symmetry (v1.0.0-prep)
Build warnings cleanup (0 warnings):
- Suppress threadpool deprecation warning (baradadb.nim)
- Remove unused 'os' import (logging.nim)
- Fix ImplicitDefaultValue for newNode params (ast.nim)
- Add explicit cstring cast for posix.open (wal.nim)
- Fix HoleEnumConv for MsgKind parsing (server.nim)

TLA+ Formal Verification:
- Add symmetry reduction (Permutations) to all 9 existing specs
- Add SYMMETRY directive to all .cfg files
- New crossmodal.tla: cross-modal consistency spec
  * MetadataVectorConsistency, HybridResultValid
  * CommittedAtomicity, AbortedAtomicity, TxnStateValid
- New models/crossmodal.cfg

Tests:
- Add Cross-Modal TLA+ Faithfulness tests (4 tests)

Docs:
- Update PLAN.md and BUG_AUDIT.md with completed tasks
2026-05-13 09:24:04 +03:00

22 lines
292 B
INI

CONSTANTS
Files = {f1, f2}
Contents = {c1, c2}
MaxBackups = 3
KeepCount = 2
MaxSteps = 6
Nil = Nil
INIT Init
NEXT Next
CHECK_DEADLOCK FALSE
INVARIANTS
TypeOk
BackupSnapshotsValid
VerifyIntegrity
RetentionInvariant
HistoryConsistency
BackupIdValid
SYMMETRY Symmetry