TLA+ = formal language for modeling software above the code level and hardware above the circuit level by Leslie Lamport (of vector clock and Paxos fame, among other things.)
So there's \in, \subseteq and probably many others that are written just like in Latex. Notably \cap and \cup were also copied from Latex, which describe the shape of the symbol instead of its meaning. But not \to, \mapsto, \Vee and \Wedge, they're written as ASCII art ->, |->, \/ and /\.
Then there's SUBSET, which means power set ... yeah. -_-
For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners
https://lamport.azurewebsites.net/tla/tla.html
Then there's SUBSET, which means power set ... yeah. -_-
I wonder if anyone has worked on porting it to Lean and making tactics for it
I made https://github.com/RCSnyder/tlaplus-process-studio
https://tlaplus-process-studio.com/
For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners