|
|
|
|
|
by oggy
1455 days ago
|
|
I used Spin a few years back, so my memory is a bit hazy, but I remember Promela (Spin's modeling language) feeling extremely low-level in comparison. It felt a bit like more limited C with non-deterministic choice stuck in there. TLA is a first-order logic language, and the tooling (while not great by modern language standards) felt more pleasant than Spin. It could be that you get faster model checking with Spin though, I'm not aware of any comparisons. |
|