hwayne / learntla

A TLA+ guide
http://www.learntla.com
Creative Commons Attribution 4.0 International
278 stars 57 forks source link

Discuss State Contraints rather than DFS in "Infinite Loops" #56

Closed lemmy closed 6 years ago

lemmy commented 6 years ago

The section on infinite loops discusses the concept of DFS but State Constraints are much better suited to to restrict the state space. E.g. in the example at hand, a state constraint such as "x < 42" would be a good illustration. That's a) easier to come up with compared to 7 and b) is less blunt than simply pruning the state graph.