After issue tarantool/tarantool#11374 is implemented we'll be in the state, where we have working TLA+ specification of tarantool, but any change in replication, transaction or wal related logic may make it irrelevant, it will stop displaying the real state transitions of Tarantool.
Until the issue tarantool/tarantool#11377 is implemented we should add a compulsory NO_TLA label to commit msg, so that developers wouldn't miss that.
After issue tarantool/tarantool#11374 is implemented we'll be in the state, where we have working TLA+ specification of tarantool, but any change in replication, transaction or wal related logic may make it irrelevant, it will stop displaying the real state transitions of Tarantool.
Until the issue tarantool/tarantool#11377 is implemented we should add a compulsory
NO_TLAlabel to commit msg, so that developers wouldn't miss that.