Closed stevana closed 6 years ago
The code here is based Hans' answer about how Erlang QuickCheck does it and on: "The basic idea is to define the assertion {P} S {Q} to mean that if execution is begun anywhere in S with P true, then P will remain true until S terminates, and Q will be true if and when S terminates." -- Lamport, https://link.springer.com/article/10.1007/BF00289062 .
Work in progress; PR created for feedback.