

InfluxDB
Power RealTime Data Analytics at Scale. Get realtime insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in realtime with unbounded cardinality.

Adding a vector clock is relatively straightforward (see e.g. https://github.com/tlaplus/Examples/commit/ee10c6ed1c65f1002c8ad402edceeffcf1a833e). For PlusCal, the vector clock can be computed from the PC variable: https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla

CommunityModules
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
Adding a vector clock is relatively straightforward (see e.g. https://github.com/tlaplus/Examples/commit/ee10c6ed1c65f1002c8ad402edceeffcf1a833e). For PlusCal, the vector clock can be computed from the PC variable: https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla
Related posts

Suggestions for model checking?

Formal definitions of "events" and "messages" in distributed systems?

Beginner Question on Model Checking

Why is the IDE telling me my actions will never be enabled? How should a mutable array of booleans be represented?

Where do I find examples of informal specs (RFCs) AND their formal versions (in TLA+ ideally) ?