TLA+ Operators section is not explicit

hwayne / learntla

A TLA+ guide

http://www.learntla.com

Creative Commons Attribution 4.0 International

278 stars 57 forks source link

TLA+ Operators section is not explicit #77

Closed gantsevdenis closed 5 years ago

gantsevdenis commented 5 years ago

This section suggests to define an operator

Five == 5
Five + 5 \* 10

However, it doesn't specify (can't find?) where to enter that expression? I have tried in "Evaluate Constant Expression", and throws a parsing error. I also tried to put it into "spec.tla" file, between begin and end algorithm, which throws an Unrecoverable Error. I ve also tried to put it after end algorithm, but nothing in there seems to be taken into account

hwayne commented 5 years ago

I should probably rewrite this whole section to make it clear how to actually test stuff