3 ms·
Even small python program has enormous state beyond the reach of automatic reduction to TLA+ model. BTW TLA+ is not too hard for basic usages. I argue it's muc
by bvrmn 3y ago
Even small python program has enormous state beyond the reach of automatic reduction to TLA+ model.
BTW TLA+ is not too hard for basic usages. I argue it's much simpler than PlusCal because doesn't have additional semantic layer.