Re: [tlaplus] Getting Started with TLA⁺ for Modeling an EV Charging Ecosystem

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

Hi Basant,

TLA+ certainly can accomplish all of your goals, although it should be noted that it really showcases its usefulness in domains where some combinatorial aspect generates a large number of possible system states. As a general rule, if you can attach unique human-readable names to every distinct state of your system, TLA+ might not be that useful. This will happen if you have a small number of distinct states, perhaps fewer than 10-20. However, others might disagree and believe that formal specification will be useful regardless.

If you would like to see a collection of existing TLA+ specifications, there is the tlaplus/examples repo. Resources to learn TLA+ can be found at Leslie Lamport's Learning TLA+ website or Hillel Wayne's learntla.com.

Andrew Helwer

On Tue, Jul 29, 2025 at 6:58 AM Basant Singh <mr.singh.basant@xxxxxxxxx> wrote:

Hello everyone,

I am brand new to TLA⁺ and recently discovered it while exploring ways to build a mathematical model of an electric‑vehicle (EV) charging ecosystem. My goals are to:

1. Define the full state space of the system — all possible configurations of chargers, sessions, reservations, meter readings, etc.

2. Specify the constraints that distinguish legal from illegal states (for example, “a connector cannot be in use by two sessions simultaneously,” or “a reservation must start and end within a valid time window”).

3. Automatically check which states are reachable under those constraints and identify any illegal configurations.

I’d appreciate any guidance on:

• How to structure a TLA⁺ module for this kind of system

• Key language constructs (variables, actions, invariants) I should focus on

• Best practices for modeling resource‑sharing systems and time constraints

• Starter tutorials or example specs that cover similar patterns (e.g., reservations, state machines, interleaving actions)

• Tips on using the TLC model checker to enumerate and verify states

• Pointers to existing work: Has anyone applied TLA⁺ (or a similar formal method) to EV charging systems or other reservation‑based, time‑driven domains? If so, could you share links to specs, papers, or case studies?

Thank you in advance for any pointers or references that could help me get up and running!

Basant Singh

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/600fac3f-eb7d-40c2-8934-44f59a184fd8n%40googlegroups.com.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVr%2BynqgX5TsGU_urvyTeNHfXiZ1_QYCS33BufRRjA%3Daw%40mail.gmail.com.